From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q0BDw3rA012774
	for <caml-list@sympa-roc.inria.fr>; Wed, 11 Jan 2012 14:58:03 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AjgCACqUDU/UTWUIjWdsb2JhbABDhQ+nWCIBAQEBCQkLCRIGIYFyAQEFIwQLAQUIAQE2Ag8JAhgCAgUWCwICCQMCAQIBRQYBDAYCAQGHeKR2aoM3AY4mB4EviViBFppOjH8
X-IronPort-AV: E=Sophos;i="4.71,493,1320620400"; 
   d="scan'208";a="126430919"
Received: from mx4.wp.pl ([212.77.101.8])
  by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 11 Jan 2012 14:57:58 +0100
Received: (wp-smtpd smtp.wp.pl 18110 invoked from network); 11 Jan 2012 14:57:57 +0100
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wp.pl; s=1024a;
          t=1326290277; bh=Xqh3r6SDdu6oNPeXWtAHlyguSxZNnvloD26reywes8I=;
          h=From:To:Subject;
          b=xXgA+YLMWeWm9lkJjHsG2I2iHR7vmW/Fvo8ap/kb29xbJOOR7YIs8Wc3XfEfXMnvw
           ZLGqp6QaWn5tzHUFefmUYWLQcYT5GVwv5sMXQG1gmU7Og9LTMps9MvUj2IEBmqGoIM
           5/LgEx7BUxptM51j5fBrHm8XsKe0f6dpinzVu1sc=
Received: from 18-161.2-0.pl (HELO [192.168.1.100]) (d0@[91.189.18.161])
          (envelope-sender <d0@wp.pl>)
          by smtp.wp.pl (WP-SMTPD) with AES256-SHA encrypted SMTP
          for <rossberg@mpi-sws.org>; 11 Jan 2012 14:57:57 +0100
Message-ID: <4F0D9564.8040407@wp.pl>
Date: Wed, 11 Jan 2012 14:57:56 +0100
From: Dawid Toton <d0@wp.pl>
User-Agent: Mozilla/5.0 (X11; Linux i686; rv:9.0) Gecko/20111220 Thunderbird/9.0
MIME-Version: 1.0
To: rossberg@mpi-sws.org, caml-list <caml-list@yquem.inria.fr>
References: <1326209342.96423.YahooMailNeo@web111502.mail.gq1.yahoo.com>    <1326214824.62249.YahooMailNeo@web111507.mail.gq1.yahoo.com>    <E51C5B015DBD1348A1D85763337FB6D9C26218B6@Remus.metastack.local>    <4F0D6913.4090207@wp.pl> <307f99bdbbb797985a66a4798b2dd1f1.squirrel@mail.mpi-sws.org>
In-Reply-To: <307f99bdbbb797985a66a4798b2dd1f1.squirrel@mail.mpi-sws.org>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
X-WP-AV: skaner antywirusowy poczty Wirtualnej Polski S. A.
X-WP-SPAM: NO 0000000 [gQP0]                               
Subject: Re: [Caml-list] Re: References and polymorphism

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