From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <oleg@okmij.org>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 3A7837F30A
	for <caml-list@sympa.inria.fr>; Fri,  8 Mar 2013 12:10:13 +0100 (CET)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  oleg@okmij.org) identity=pra; client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org";
  x-conformance=sidf_compatible
Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of
  oleg@okmij.org designates 66.39.3.115 as permitted sender)
  identity=mailfrom; client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@www1.g3.pair.com) identity=helo;
  client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org";
  x-sender="postmaster@www1.g3.pair.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AtoEAGPGOVFCJwNza2dsb2JhbABDsngBk0IODQcWPIN6iRUMmhqhBI8pgyoDlkoBgR6SXA
X-IPAS-Result: AtoEAGPGOVFCJwNza2dsb2JhbABDsngBk0IODQcWPIN6iRUMmhqhBI8pgyoDlkoBgR6SXA
X-IronPort-AV: E=Sophos;i="4.84,807,1355094000"; 
   d="scan'208";a="6091111"
Received: from www1.g3.pair.com ([66.39.3.115])
  by mail2-smtp-roc.national.inria.fr with SMTP; 08 Mar 2013 12:10:12 +0100
Received: (qmail 36330 invoked by uid 9370); 8 Mar 2013 11:10:10 -0000
Date: 8 Mar 2013 11:10:10 -0000
Message-ID: <20130308111010.36329.qmail@www1.g3.pair.com>
From: oleg@okmij.org
To: caml-list@inria.fr
X-Validation-by: oleg@okmij.org
Subject: [Caml-list] A brief guide to a bit of the OCaml type checker


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.