The unsound type checker of Caml Light.

Martin Elsman (mael@id.dth.dk)
Sat, 19 Mar 94 17:57:34 +0100

From: Martin Elsman <mael@id.dth.dk>
Message-Id: <199403191657.RAA08113@idfs3.id.dth.dk>
To: caml-list@margaux.inria.fr
Subject: The unsound type checker of Caml Light.
Date: Sat, 19 Mar 94 17:57:34 +0100

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