Resources and Errata for
The essence of ML type inference
(Chapter 10 of
By lack of space, a lot of material was left out of our chapter.
Here is a draft extended version of it
Compared to the published version, it adds (among other things):
Section 1.10 on universal quantification in constraints,
including: first-order unification under a mixed prefix; how
to handle type annotations; polymorphic recursion; boxed universal
types and existential types.
Section 1.11 on rows,
including: row unification; how to type-check operations on records
A prototype implementation
A prototype implementation of a type inference engine based on constraint
solving is available under the GPL license.
You can download it and
Page 445, Figure 10-11, rule S-Ex-3. There is a dangling prime
in the rule's right-hand side, which should belong to the
preceding "S" symbol.