Step by Step Type Inference
I am attempting to explain the type inference algorithm I used in the Cat interpreter (TypeInferer.cs). I know it is somewhat cryptic, but hopefully it makes enough sense to those particularly interested type inference to be useful. Remember in Cat ‘A is a stack variable and ‘a is a type variable.
Given a program, represented as a sequence of functions with known types: (’A -> ‘B) (’C -> ‘D) (’E -> ‘F) etc. (always possible because every program can be expressed as a series of primitive functions with well-defined types).
- To compose two functions (’A -> ‘B) and (’C -> ‘D) the result is a new function of type: (’A -> ‘D) (call this the result type)
- You now need to express the variables of ‘D in terms of variables in ‘A. To do so you need to find unifying variables. You also need to replace variable with concrete types when they are known.
- We start with a basic constraint equation: ‘B = ‘C
- This generates a set of constraint equations:
- If ‘B = ‘R ‘x and ‘C = ‘S ‘y then ‘R = ‘S and ‘x and ‘y.
- If both sides are functions: (’R -> ‘S) and (’T -> ‘U) then we generate new constraints from the equations: ‘R = ‘T and ‘S = ‘U.Â
- If both sides of an equality are variables, generate a unifier associated with both sides.
- If one side of an equality is a variable, but the other isn’t then we will replace all instance of the variable with the type.
- Recursively replace all variables in the result type with the unifiers
- Compose the result type with the type of the next function, until no more functions are left
Below is a real example of the Cat interpreter for inferring the type of [swap 12 add_int swap] using the #t command.
// swap, 12
Before unification:
('S0 't1 't2 -> 'S3 int)
'S0 't2 't1 = 'S3Constraints:
'S3 = 'S0 't2 't1Unifiers:
'S3 = 'S0 't2 't1
Type: ('S0 't1 't2 -> 'S0 't2 't1 int)// swap 12, add_int
Before unification:
('S4 't5 't6 -> 'S7 int)
'S4 't6 't5 int = 'S7 int int
Constraints:
'S7 = 'S4 't6
't5 = int
Unifiers:
't5 = int
'S7 = 'S4 't6
Type: ('S4 int 't6 -> 'S4 't6 int)
// swap 12 add_int, swap
Before unification:
('S8 int 't9 -> 'S10 't12 't11)
'S8 't9 int = 'S10 't11 't12
Constraints:
't12 = int
't11 = 't9
'S10 = 'S8
Unifiers:
't11 = 't13
't9 = 't13
'S10 = 'S14
'S8 = 'S14
't12 = int
Type: ('S14 int 't13 -> 'S14 int 't13)