Type Systems
What is unification? Tree pattern matching where match variables only appear as leaves.
- A naïve recursive algorithm can be written in a few lines of Scheme or ML.
- The common practical algorithm relies on a union-find representation of finite sets to record equivalent symbolic types. Every set contains at least one symbolic type that is just a variable. This algorithm runs in essentially linear time.
- A linear algorithm exists but it is not as efficient for problems of practical size as the union-find based algorithm.
Question: is the reconstructed type unique? Many ?-calculus programs have multiple typings. Consider the program (?x x). It can be assigned the type ???, for any type ? ? T , e.g., (int ? int), (int ? int) ? (int ? int), …
The type reconstruction algorithm deftly addresses this problem by returning the
most general symbolic typing; all of the possible ground typings (containing no type
variables) are substitution instances of this typing. For this reason, the typing
produced by the type reconstruction algorithm is called the principal typing (or type)