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