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

[rossberg@mpi-sws.org]

Dawid Toton wrote:
>>> 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?
>
> I can read from r and use it as 'b option. This is useful in general: a
> mutable store can be used locally to speed up computations. I can
> imagine working on 'b array to benefit from fast lookup.

But what do you do with that store? You can retrieve values from it, but
neither can use them locally (because they-re fully abstract) nor return
them (because they are not typed 'a). So it's useless to store them.

>> 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.
> Use de Morgan's laws for quantifiers:
>
> (∃x. x) → y
>
> ¬((∃x. x) ∧ ¬y)
>
> ¬(∃x. (x ∧ ¬y))
>
> ∀x.(¬(x ∧ ¬y))
>
> ∀x.(x → y)
>
> I see, this is probably abuse of constructive logic in this case, but I
> believe the idea stays the same.

Yeah, I don't see how this is applicable here.

/Andreas