I'm trying to write typing rules for a simple language, which is basically a lambda calculus with SSA-like $\phi$-nodes, which basically exchange formal parameters for actual parameters.
For simplicity, let's assume the simply typed lambda calculus, with let and where as syntactic sugar (as usual, functions may only take one parameter; where declares mutually recursive functions).
For example, the following Haskell-like code:
f 10 where f x = let y = x + 10 in (g x) + (g y) g z = z
It would be simple to write a simply typed typing rules for this. I can incrementally build the context as usual whenever a variable is defined. But I'm using $\phi$-nodes, and the actual code for my language would look like this:
f_1 where f = let x = φ(10) in let y = x + 10 in (g_1) + (g_2) g = let z = φ(x, y) in z
Here, we exchange the function parameters for the actual values that may be used when calling them. The
z parameter of the
g function is bound to
φ(x, y), because
g was called twice (once with
x as the argument, once with
The problem is: when I'm typechecking the
g function, I have no information on my context about the
y variables, they came from another context (at the call-site)! How could I make typing rules for a simply typed version of such language?
I.e., how can I formalize the judgement rules such that I can correctly typecheck
g here? (Without having to resort to merge everything into a single big scope, which arguably is the usual.)