From mboxrd@z Thu Jan  1 00:00:00 1970
Received: by pauillac.inria.fr; Mon, 21 Mar 94 17:10:22 +0100
Received: from margaux.inria.fr by pauillac.inria.fr; Sat, 19 Mar 94 17:58:55 +0100
Received: from concorde.inria.fr by margaux.inria.fr, Sat, 19 Mar 94 17:58:52 +0100
Received: from idfs3.id.dth.dk (idfs3.id.dth.dk [130.225.76.53]) by concorde.inria.fr (8.6.7/8.6.6) with ESMTP id RAA09622 for <caml-list@margaux.inria.fr>; Sat, 19 Mar 1994 17:58:50 +0100
Received: from localhost (localhost [127.0.0.1]) by idfs3.id.dth.dk (8.6.4/8.6.4) with SMTP id RAA08113; Sat, 19 Mar 1994 17:57:35 +0100
From: Martin Elsman <mael@id.dth.dk>
Message-Id: <199403191657.RAA08113@idfs3.id.dth.dk>
X-Authentication-Warning: idfs3.id.dth.dk: Host localhost didn't use HELO protocol
To: caml-list@margaux.inria.fr
Cc: mael@idfs3.id.dth.dk
Subject: The unsound type checker of Caml Light.
Date: Sat, 19 Mar 94 17:57:34 +0100
X-Mts: smtp
Sender: weis@pauillac.inria.fr

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