From mboxrd@z Thu Jan  1 00:00:00 1970
Received: by pauillac.inria.fr; Wed, 2 Mar 94 17:34:58 +0100
Received: from margaux.inria.fr by pauillac.inria.fr; Wed, 2 Mar 94 15:37:46 +0100
Received: from quincy.inria.fr by margaux.inria.fr, Wed, 2 Mar 94 15:37:43 +0100
Received: by quincy.inria.fr; Wed, 2 Mar 94 15:37:23 +0100
Message-Id: <9403021437.AA12106@quincy.inria.fr>
Subject: Re: Documentation for the type-checker for Caml Light
To: xavier@Theory.Stanford.EDU (Xavier Leroy)
Date: Wed, 2 Mar 1994 15:37:22 +0100 (MET)
Cc: mael@id.dth.dk, caml-list@margaux.inria.fr
In-Reply-To: <9403011945.AA24974@Thelonius.Stanford.EDU> from "Xavier Leroy" at Mar 1, 94 11:45:03 am
From: Didier.Remy@inria.fr (Didier Remy)
Reply-To: Didier.Remy@inria.fr
Organization: INRIA, BP 105, F-78153 Le Chesnay Cedex
Phone: (33) 1 3963 5317 -- Sec: (33) 1 3963 5684 -- Fax: (33) 1 3963 5330
X-Mailer: ELM [version 2.4 PL13]
Content-Type: text
Sender: weis@pauillac.inria.fr

> The Caml Light typechecker also uses "levels" on type variables to
> implement generalization efficiently. This folklore trick is described
> in Weis and Leroy's book "Le langage Caml" (in French, unfortunately),
> and also (but much more abstractly) in some publications by Didier
> Remy. I believe Didier is on the list, so maybe he can provide more
> references.

What Xavier Leroy refers to is described in the paper [1]  together with the
addition of an equational  theory on ML  types (abstract at the  end of this
message). 

The idea is to mark all nods & variables of types with integers that keep
track of the first occurrence of those nods & variables in the typing context.
The unification algorithm has to update the marks when merging two types.
Generalization of a type can then be done in time proportional to the number
of nods & variables that have been introduced since the most recent LET
instead of checking through the whole type environment (that might be very
large).

The unification algorithm of Caml Light reuses similar marks, but they are
not updated at the same place. 

    Didier.

----------------

[1]   Didier R\'emy.  "Extending ML Type System with a Sorted Equational
      Theory".  INRIA Research Report 1766, year 1992.

      Can be retrieved by anonymous ftp as eq-theory-on-types.{dvi,ps}.Z at

          ftp.inria.fr:INRIA/Projects/cristal/Didier.Remy/