From: oleg@okmij.org
To: caml-list@inria.fr
Subject: [Caml-list] A brief guide to a bit of the OCaml type checker
Date: 8 Mar 2013 11:10:10 -0000 [thread overview]
Message-ID: <20130308111010.36329.qmail@www1.g3.pair.com> (raw)
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.
next reply other threads:[~2013-03-08 11:10 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-03-08 11:10 oleg [this message]
2013-03-10 6:55 ` Anthony Tavener
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20130308111010.36329.qmail@www1.g3.pair.com \
--to=oleg@okmij.org \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).