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

[Dawid Toton <d0@wp.pl>]

On 2012-01-11 12:43, rossberg@mpi-sws.org wrote:
> 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?
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.
> 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.
Dawid