Say I have the following contrived example code:
a(1)
function a(x) {
var n = b(x)
var m = c(x)
return n + m
}
function b(x) {
var n = d(x / 2)
var m = e(x)
return n - m
}
function c(x) {
var n = d(x)
var m = e(x)
return n * m
}
function d(x) {
return x + 2
}
function e(x) {
return x + 3
}
Then, I am analyzing the method d(x)
. From just analyzing it by itself, we can infer that x must be some sort of number. We do this by what seems like simulating x + 2
, and realizing that for that to be satisfied x must be a number. Not quite sure how to implement the type inference here, not sure if it uses symbolic evaluation too.
But then we get to the function call a(1)
. In this case to do typechecking / type inference on d(x)
, we have to somehow traverse down the tree of functions, simulating how x
is transformed along the way. It finds out that it is divided by 2 somewhere in there, so it goes from integer to float. So we check based on our original assumption that d(x)
is a number, and agree that it will be valid.
That is just me roughly trying to figure out how to do type checking / type inference.
I'm wondering two things:
- If you need to do some sort of symbolic evaluation to do type checking / inference. If so, any suggestions on resources or places/ways to better understand that.
- Say we have a gigantic app with millions of lines of code. Say between
a(x)
andd(x)
there were 500 function calls, doing all sorts of things tox
. Wondering if we have to simulate that entire process to figure out ifx
will be a valid type, or if we can somehow limit the scope and do some sort of shortcut. If we had to traverse the 100's of functions for every variable, that would be a ton of evaluation and would be slow. So wondering how to limit the scope of the search somehow, to do type checking / inference.
Basically I am figuring out how to do type checking / inference. The resources are mostly on the lambda calculus from what I've found, which I am not too familiar with and works differently I would imagine than an imperative program.
For example, they seem to be mentioning that here:
(1) 3.2 Type Graph
After each method has been converted into its intermediate representation, zscript gradually builds a type graph by each method called by the program. The CPA is non-iterative. Only the methods that could potentially be called are processed, and (except for templates) they are only processed one time only. In our implementation of the algorithm, we use a work list. First, the constructor of the class containing the main method, and the main method itself is added to the work list. Then, while the work list is not empty, the methods of the work list are processed. During the processing of a method, more methods may be added to the work list. The algorithm terminates when no more methods remain to be analyzed.