Re: Caml type inference of references and mutable records

[Pierre Weis <Pierre.Weis@inria.fr>]

> Dear Camlers,
> 
> I am looking for papers where the Caml's current polymorphic typing and
> inference algorithm of mutable data types are studied in detailed.  I am
> mainly interested in the typing of references and mutable records.
> 
> I have found two papers by Xavier Leroy on the INRIA repository that
> describe different approaches to the typing of references; there are:
> "Polymorphic type inference and assignment", 1991, and "Polymorphism by name
> for references and continuations", 1993.  But it is not clear to me if any
> of these approaches is used currently in Caml.
> 
> Thanks,
> 
> Ivan Sanabria-Piretti

None of the articles you mentioned (nor Xavier's thesis that gave also
interesting and powerful typing disciplines for mutable values) are
currently used to implement type checking of polymorphic data
structures in Caml. This is due either to too complex type algebras,
too difficult type checking disciplines, unclear restrictions to
typable programs, or drastic modifications to the source language
(either modifications to modules' interfaces or to the evaluation
regime of the language).

The current restriction to obtain safe typing of references is much
more simple and pratical; it is described in the FAQ of the language
(http://pauillac.inria.fr/caml/FAQ/FAQ_EXPERT-eng.html#polymorphisme);
it has also been discussed in the Caml mailing list, long time ago
(see for instance http://caml.inria.fr/archives/199403/msg00011.html);
it is based on the ``value polymorphism'' introduced by Andrew
K. Wright in his article ``Simple Imperative Polymorphism. Lisp and
Symbolic Computation 8(4): 343-355 (1995)''.

Hope this helps,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/