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
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
