The unsound type checker of Caml Light.

The unsound type checker of Caml Light.

[Martin Elsman]

Dear caml-list listeners,

After having studied Xavier's thesis it is obvious that the type-
checker of Caml Light is NOT sound. (There are problems with
references hidden in 'functional objects' (closures).

The following example shows how the type system can be brought
to failure:

The function:  

	let functional_ref = fun x ->
	    let r = ref x
	    in (fun () -> !r), (fun y -> r := y);;

is well typed in Caml Light and has the type

	functional_ref : 'a -> (unit -> 'a) * ('a -> unit) = <fun>

Let us define

	let (read, write) = functional_ref(fun x -> x);;

and the following types are infered

	write : ('a -> 'a) -> unit = <fun>
	read : unit -> 'a -> 'a = <fun>

We can now make a function that adds 1 to the reference:

	write(fun n -> n+1);;

Now the type checker fails:

	#if read()(true) then 1 else 3;;
	- : int = 3
	#read()(true);;
	- : bool = false
	#read()(23);;
	- : int = 24
	#read()(false);;
	- : bool = false

If a datatype is created we can add 1 to one of its constructors!!!:

	#type t = A | B of int * int;;
	Type t defined.

	#read()(A);;
	- : t = A
	#read()(B(5,6));;
	- : t = A

I know that its possible to solve this problem (the answer is given
in chapter 3 and 4 in Xavier's thesis).

Has anybody implemented such a sound type checker for Caml Light.

Best regards,

Martin Elsman

Re: The unsound type checker of Caml Light.

[Pierre Weis]

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