This seems like a good topic to add to Lambda the Ultimate. I'm a perpetual
lurker without an account, and I think "front page" topics are limited to
regular contributors?

I'm no type-theorist, but this is still an interesting peek under the hood.


On Fri, Mar 8, 2013 at 4:10 AM, <oleg@okmij.org> wrote:

>
> 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
>