Type Systems
Question: what is the relationship between the (untyped) ?-calculus and the (simply) typed ?-calculus?
Many expressions (and complete programs) in the (untyped) ?-calculus cannot be typed in the (simply) typed ?-calculus!
- Example: (?x (x x))
x requires a type ? = ? ? ?, but no such type exists
If the constant operations terminate for all inputs, then every typable program terminates for all inputs!
Question: is there a tractable algorithm for determining the type of an expression in the (untyped) ?-calculus and rejecting the expression if no such type exists? Yes! The standard algorithm (called the type reconstruction algorithm) is based on a very simple idea:
- generate a distinct type variable for every subexpression of the given expression M,
- record the equality constraints between these variables dictated by the typing rule that matches the program context in which the subexpression associated with each variable appears, and
- solve these constraints.