Efficient and Insightful Generalization
okmij.org
A short guide on OCaml type checker, describing the surprisingly elegant algorithm for generalization, which generalizes to first-class polymorphism, MLF and local types. Polymorphism and regions have much in common.

There is more to Hindley-Milner type inference than the Algorithm W. In 1988, Didier Rémy was looking to speed up the type inference in Caml and discovered an elegant method of type generalization. Not only it is fast, avoiding scanning the type environment. It smoothly extends to catching of locally-declared types about to escape, to type-checking of universals and existentials, and even to MLF.

Alas, both the algorithm and its implementation in the OCaml type checker are little known and little documented. This page is to explain and popularize Rémy’s algorithm, and to decipher a part of the OCaml type checker. The page also aims to preserve the history of Rémy’s algorithm.

Read How OCaml type checker works