Re: Documentation for the type-checker for Caml Light

[Didier.Remy@inria.fr (Didier Remy)]

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