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 q0BFYUEo016681
	for <caml-list@sympa-roc.inria.fr>; Wed, 11 Jan 2012 16:34:34 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AkoBAIurDU+LEwExe2dsb2JhbABCrQ0BAQsLJgUggXIBAQEDAScLAQ0BATcBDwUEAg4KLlcGJIdppRmEIQGOJQeMHZUQkj0
X-IronPort-AV: E=Sophos;i="4.71,493,1320620400"; 
   d="scan'208";a="126450628"
Received: from infao0809.mpi-sb.mpg.de (HELO hera.mpi-sb.mpg.de) ([139.19.1.49])
  by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 11 Jan 2012 16:34:34 +0100
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=mpi-sb.mpg.de; s=mail200803; h=Message-ID:In-Reply-To:
	References:Date:Subject:From:To:Cc:MIME-Version:Content-Type:
	Content-Transfer-Encoding; bh=2l7HZEuY0UV8kU6txiZ22f3w6B0/sS6uZQ
	x+74eghpw=; b=O8pw72hqgLvkvJFGzjhB9i5BQ1t8rizfHeNopnO9iGySU2r4gb
	H6T+SDVCVqAXEoSHuAY44gJEdFwEDMYLWufuqp/nt2jy/7PGJzb+sQOYx/8FC17e
	YzY5hnQX/UHuKyKsZ5G4cNrxgHFh/pqo3SxxI1fQUALo35wOBPocn2P3E=
Received: from newzak.mpi-klsb.mpg.de ([139.19.1.29]:42606)
	by hera.mpi-sb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with esmtp (Exim 4.69) id 1Rl0C2-00086q-Ul; Wed, 11 Jan 2012 16:34:32 +0100
Received: from local
	by newzak.mpi-klsb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with local (Exim 4.72) id 1Rl0C2-0008L3-FC; Wed, 11 Jan 2012 16:34:26 +0100
Received: from 74.125.57.233
        (SquirrelMail authenticated user rossberg)
        by mail.mpi-sws.org with HTTP;
        Wed, 11 Jan 2012 16:34:26 +0100
Message-ID: <0bfbfcb5fc4da2f9f021abc9da89aec5.squirrel@mail.mpi-sws.org>
In-Reply-To: <4F0D8FD6.1060605@wp.pl>
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>
    <4F0D8FD6.1060605@wp.pl>
Date: Wed, 11 Jan 2012 16:34:26 +0100
From: rossberg@mpi-sws.org
To: "Dawid Toton" <d0@wp.pl>
Cc: rossberg@mpi-sws.org, "caml-list" <caml-list@yquem.inria.fr>
User-Agent: SquirrelMail/1.4.21
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-15
Content-Transfer-Encoding: 8bit
X-Priority: 3 (Normal)
Importance: Normal
Subject: Re: [Caml-list] Re: References and polymorphism

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