Re: The unsound type checker of Caml Light.

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

It is well known that the Caml Light typechecker is unsound for
mutable objects. It is clearly mentioned in the man page:

     BUGS

          ...

          Polymorphic references, and more generally mutable concrete
          types, are not safe: it is possible to create polymorphic refer-
          ences through a functional encoding.

That's clear: functional_ref is a functional encoding that create
polymorphic references.

As far as I know there is no working versions of Caml featuring the
kind of type systems described in Xavier's thesis. They are sound and
powerful, but may be too complex for common usage.

Nevertheless we definitively have to fix these bugs of the
typechecker. We probably have to switch to the simple scheme proposed
by the FX communauty in 1987 and shown to be pratical by Wright in
1993: restrict type generalisation to pure expressions (or
non-expansive expressions), or to values in Wright's terminology. This
is clearly correct, though it has somme drawbacks, since it forbids
some styles of programming, which intensively relies on polymorphism
obtained by partial applications of polymorphic functionals.

Hope this helps,

Pierre Weis
----------------------------------------------------------------------------
Cristal Project
INRIA, BP 105, F-78153 Le Chesnay Cedex (France)
E-mail: Pierre.Weis@inria.fr
Telephone: +33 1 39 63 55 98
----------------------------------------------------------------------------