The unsound type checker of Caml Light.

[Martin Elsman <mael@id.dth.dk>]

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