Documentation for the type-checker for Caml Light

Documentation for the type-checker for Caml Light

[Martin Elsman]

Hello Caml-list listener's

Does anybody know if there exist any documentation of the type-
checker of Caml Light. 'The ZINC Experiment: An Economical
Implementation of The ML-Language' by Xavier Leroy, 1990 does
not include type-checking :-(.

I'm trying to attach equality type variables to Caml Light
together with imperative type variables and overloaded
builtin operators. The code of Caml Light is not 'just' the
Hindley/Milner/Robinson kind of thing, though there are
similarities. What are dangerous type variables and why does
the type checker include two unification algorithms?

Best regards

Martin Elsman

-----------------------------------------------------------------------
Martin Elsman                       The Technical University of Denmark
E-Mail: mael@id.dth.dk                   Department of Computer Science
-----------------------------------------------------------------------

Re: Documentation for the type-checker for Caml Light

[Xavier Leroy]

> The code of Caml Light is not 'just' the
> Hindley/Milner/Robinson kind of thing, though there are
> similarities.

There are a number of tricks in the efficient implementation of type
inference that you won't find in Hindley, Milner, nor Robinson, indeed.
Some are described in Cardelli's paper "Basic polymorphic type-checking",
Science of computer programming, 8(2). 

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 are dangerous type variables

A type analysis to prevent polymorphic mutable structures (e.g.
polymorphic references), similar in purpose to imperative type
variables but much superior in my opinion. See my POPL 91 paper and
my PhD thesis (available on
ftp.inria.fr:INRIA/Projects/cristal/Xavier.Leroy).

> and why does
> the type checker include two unification algorithms?

I don't understand what you're alluding to. Where is the second algorithm?

- Xavier Leroy

Re: Documentation for the type-checker for Caml Light

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