[Caml-list] A brief guide to a bit of the OCaml type checker

[Caml-list] A brief guide to a bit of the OCaml type checker

[oleg]

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.

Re: [Caml-list] A brief guide to a bit of the OCaml type checker

[Anthony Tavener]

[-- Attachment #1: Type: text/plain, Size: 1317 bytes --]

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
>

[-- Attachment #2: Type: text/html, Size: 2095 bytes --]