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

[rossberg@mpi-sws.org]

Dawid Toton wrote:
> 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 *)
>      ...

Nothing useful can happen either. You could never read a value back from r
and use/return it as an 'a or for anything else. So why would you want to
store it there in the first place?

Also, I don't quite understand how your type annotations are supposed to
match up. If x : exists 'b. 'b, then f can't be forall 'a. 'a -> 'a.

/Andreas