Re: [Caml-list] Re: References and polymorphism

[Gabriel Scherer <gabriel.scherer@gmail.com>]

How would you make the distinction between

  let f : 'a . unit -> 'a list ref =
    fun () -> ref ([] : 'a list)

and

  let f : 'a . unit -> 'a list ref =
    let r = ref ([] : 'a list) in
    fun () -> r

?

On Wed, Jan 11, 2012 at 11:48 AM, Dawid Toton <d0@wp.pl> wrote:
>> 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
>