# How could one write typing rules with variables defined at call-site?

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 y).

The problem is: when I'm typechecking the g function, I have no information on my context about the x or 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.)

• I recommend looking at the work connecting SSA to ANF or to CPS (see Kelsey [1995] referenced in the previous paper). As for your approach so far, I would recommend arranging things so that scoping is rationalized. In most (theoretical, at least) uses of SSA, variables are not scoped and work is done for one (top-level) function at a time. In a functional rendition, you need to differentiate between functions that merely represent parts of the control flow graph and external functions which are typically treated as black boxes. – Derek Elkins Oct 31 '17 at 6:41
• I do understand the relation between them (I haven't read this paper in particular; thanks for the ref, @DerekElkins), actually this is the reason why I'm making a "SSA-style lambda calculus". The doubt remains, though; how could I make a formal type system for such a calculus, without resorting to making all inner variables (nested within a "global" function) belong the same scope? (Which I'll call "plan B".) – paulotorrens Oct 31 '17 at 6:49
• The Sequent Core recently introduced for GHC Haskell gives a principled approach to understanding and working with "local functions" that really represent control flow (sub)graphs. That paper has a brief discussion of SSA as well. At any rate, the scoping issue you have will go away once you distinguish between local control flow and external functions. Functions representing local control flow will always have the relevant variables in scope. Other functions need to be explicitly inlined. – Derek Elkins Oct 31 '17 at 7:11