From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q0BBhO07005169
	for <caml-list@sympa-roc.inria.fr>; Wed, 11 Jan 2012 12:43:24 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AvIBAO50DU+LEwExe2dsb2JhbABCrGgiAQEWJgUggXIBAQEEJwsBDQEBNwEPBQYOCi5XBiSsXIQhAY4VB4wdlRCSPQ
X-IronPort-AV: E=Sophos;i="4.71,492,1320620400"; 
   d="scan'208";a="138752621"
Received: from hera.mpi-sb.mpg.de ([139.19.1.49])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 11 Jan 2012 12:43:19 +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=zJi7ZNA6hzMOtz6dgkFi5Gv4MrgupxJXI/
	PjObZanzE=; b=Iiw46LUmplnSDVS4xSnejxrj+P3y7FW9apmvrOFv4SE9LN5puY
	R3/Z1XZpAxWnyppWJgHZ3qSUprb1XVVAGEQKOzfBOBmc20XH2JnyhQqJ+VrdLLdC
	8IBRRuvUkhAk/sb4mIViercCKvPqKF99HgnDNwxYiELbJqq8qfd7i4mDY=
Received: from newzak.mpi-klsb.mpg.de ([139.19.1.29]:42820)
	by hera.mpi-sb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with esmtp (Exim 4.69) id 1RkwaH-0006Iz-GQ; Wed, 11 Jan 2012 12:43:18 +0100
Received: from local
	by newzak.mpi-klsb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with local (Exim 4.72) id 1RkwaH-0006Un-0A; Wed, 11 Jan 2012 12:43:13 +0100
Received: from 74.125.57.233
        (SquirrelMail authenticated user rossberg)
        by mail.mpi-sws.org with HTTP;
        Wed, 11 Jan 2012 12:43:13 +0100
Message-ID: <307f99bdbbb797985a66a4798b2dd1f1.squirrel@mail.mpi-sws.org>
In-Reply-To: <4F0D6913.4090207@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>
Date: Wed, 11 Jan 2012 12:43:13 +0100
From: rossberg@mpi-sws.org
To: "Dawid Toton" <d0@wp.pl>
Cc: "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:
> 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