When studying the OCaml type checker I have come across an elegant but
seemingly little known type generalization algorithm based on type
levels. Interestingly, the same levels also help type check local
modules, existentials, and polymorphic records. I am thankful to
Didier Re'my, the discoverer of the algorithm, for describing the
bigger picture, sharing intuitions and history, and pointing out more
applications of the type levels (e.g., MLF).

The following web page

        http://okmij.org/ftp/ML/generalization.html

attempts to popularize the algorithm, explain it on toy type checkers
and describe its implementation in the OCaml type checker. Hopefully
one might get a better idea what the OCaml type checker is really
doing.



--
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs