I am back at work on the type inference engine on Cat. I threw out the old one because the code was just simply atrocious. The observation that stacks and types are different kinds also had an implication on how to design the objects.
I’ve written a paper on the type-system of Cat but it it is very dense and formal. This post is an attempt to explain the type inference algorithm using a step by step example of infering a type for the expression: “[] eval eval” (which in Joy would be “[] i i”). My first step is to ask the question, how do you compute the type of the function:
define ee { eval eval }
The first step is establishing what the type of “eval” is. Using the type notation I developed for Cat, we can write it as:
eval : ('A ('A -> 'B) -> 'B)
That is to say “eval” expects a function on top of the input stack which maps from a stack kind ('A) to another stack kind ('B). Below the function should be the set of types that constitute ('A). If we want to figure out the type of “ee” we start by writing:
eval : (A (A -> B) -> B) eval : (A (A -> B) -> B)
In this occurence, the A and B in the first occurence of “eval” are not the same as those in the second. In order to avoid naming conflicts we need to give new names to the second occurence:
eval : (A (A -> B) -> B) eval : (C (C -> D) -> D)
When writing ‘eval eval’ we are implicitly composing two functions. This means we need to apply the following type rule for composition:
Given x : (’A -> ‘B) and y : (’C -> ‘D) then x y = (’A -> ‘D) and ‘B = ‘C
So applying the rule to “eval eval” gives us the following type for “ee”:
ee : ('A ('A -> 'B) -> 'D)
and the axiom:
'B = 'C ('C -> 'D)
Substituting for 'B we get:
ee : ('A ('A -> 'C ('C -> 'D)) -> 'D)
This makes sense, the first “eval” requires a function on the top of the stack, the second “eval” also requires a function on the top of the stack, so this implies that the result of calling the first eval must produce a stack with a function on top.
Now let’s consider the following case, which is rather tricky: what is the type of “[] ee”? It should be the same as eval, since the first eval does nothing. Applying the type rules should yield the answer, and will assure that the type we inferred is correct.
The first step is to figure out the function of []. In Cat notation it has the type:
[] : ( -> ( -> ))
In other words it pushes a function on the stack which does not consume any parameters and does not produce any result. If were to fill in the implicit stack variables we would get:
[] : ('A -> 'A ('B -> 'B))
The rule for adding missing stack variables is that for each function if either the production or consumption does not have a stack variable at the bottom (the furthest left) a new stack variable is created and added to both the bottom of the production and the consumption.
Now we can compose this with ee (while renaming conflicting variables):
[] : ('A -> 'A ('B -> 'B)) ee : ('C ('C -> 'E ('E -> 'F)) -> 'F)
Now applying the compose rule we get:
[] ee : ('A -> 'F)
And the axiom:
'A ('B -> 'B) = 'C ('C -> 'E ('E -> 'F))
This directly implies:
'A = 'C
'B -> 'B = 'C -> 'E ('E -> 'F)
'B = 'C
'B = 'E ('E -> 'F)
By deduction :
'C = 'E ('E -> 'F)
And finally :
'A = 'E ('E -> 'F)
Now we can substitute for 'A :
[] ee : ('E ('E -> 'F) -> 'F)
Renaming 'E to 'A and 'F to 'B gives us the more recognizable:
[] ee : ('A ('A -> 'B) -> 'B)
And voila, the same type as “eval”, just as we hoped.
