From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id QAA03390 for caml-red; Wed, 16 Aug 2000 16:57:59 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA02639 for <caml-list@pauillac.inria.fr>; Wed, 16 Aug 2000 16:53:49 +0200 (MET DST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e7GErm905283;
	Wed, 16 Aug 2000 16:53:48 +0200 (MET DST)
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id QAA02857; Wed, 16 Aug 2000 16:53:47 +0200 (MET DST)
From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <200008161453.QAA02857@pauillac.inria.fr>
Subject: Re: Caml type inference of references and mutable records
In-Reply-To: <000701c005f0$2d50e4e0$837c01a3@athos.comlab.ox.ac.uk> from Ivan Sanabria-Piretti at "Aug 14, 100 02:04:27 pm"
To: Ivan.Sanabria@comlab.ox.ac.uk (Ivan Sanabria-Piretti)
Date: Wed, 16 Aug 2000 16:53:47 +0200 (MET DST)
Cc: caml-list@inria.fr
X-Mailer: ELM [version 2.4ME+ PL28 (25)]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: weis@pauillac.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/