[Caml-list] Re: References and polymorphism

[Dawid Toton <d0@wp.pl>]

> They certainly did: http://mlton.org/ValueRestriction has links to the various papers on the subject (the present scheme was not the first solution for SML, as it notes).
>
I don't get one thing about this. It seems that all examples which 
justify the value restriction are unsound just because a ref cell is 
given too general type.
Why not to just forbid too general 'a ref types? See the example from 
the page cited above (with explicit quantifier added):

let f : forall 'a. 'a -> 'a =
   let r : 'a option ref = ref None in
   fun x -> (* do evil things with the ref cell *)
     let y = !r in
     let () = r := Some x in
     match y with
       | None -> x
       | Some y -> y

The problem is that the 'a variable is bound by a general quantifier and 
at the same time it is used to give a type to the ref cell. But if this 
were forbidden, I see no need for the value restriction at all. For example:

let g : forall 'a. 'a -> 'a =
   fun (x : exists 'b. 'b) ->
     let r : 'b option ref = ref None in
     (* nothing bad can happen *)
     ...

Dawid