Type Systems
Create only one type variable for each distinct program variable; all occurrences of a given variable must have the same type!
Create a “compound type variable” ? ? ? for each subexpression that appears as the head M of an application (M N).
For each constant c, assign it the type ?(c). Every subexpression now has a symbolic type.
For each application (M N) where M has symbolic type ? ? ?, equate ? with the symbolic type of N and equate ? with the symbolic type of (M N).
For each abstraction (?x M) where x has symbolic type ? and M has symbolic type ?, equate ? ? ? with the symbolic type of (?x M).
Solve the resulting set of equations on symbolic types (which are just symbolic expressions that can be represented as trees) using the unification algorithm (invented by John Alan Robinson, a professor of philosophy at Rice in the 1960’s). The generated solution is a substitution mapping type variables to symbolic types.