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 q0BAmuYt002569
	for <caml-list@sympa-roc.inria.fr>; Wed, 11 Jan 2012 11:48:58 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AjgCANZoDU/UTWUIjWdsb2JhbABChQ+nWSIBAQEBCQkLCRIGIYFyAQEEASMEEQgBATYCBAsLGgIFFgsCAgkDAgECAUUGDQgBAReHXwIGpG5qgzcBjhYHgS+JWIEWmk6Mfw
X-IronPort-AV: E=Sophos;i="4.71,492,1320620400"; 
   d="scan'208";a="126399697"
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 11:48:57 +0100
Received: (wp-smtpd smtp.wp.pl 17951 invoked from network); 11 Jan 2012 11:48:51 +0100
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wp.pl; s=1024a;
          t=1326278932; bh=i2Joc/gjWaqzzExw61h0Jp6eDNq9/wECC0n2PV2nhOU=;
          h=From:To:Subject;
          b=fGcLJ7yaIhTA5gpUc6QAJwL38cEpBMknlNC6bT9NVoc1w0wiROiN5ioJMuGw50JKu
           WY3N5qq55/6HLLIr1+aLeUjogLl/Fu6D+kExwSEATj6lfeFYE/1MGdFvmvu0wAMOty
           yceALuOvmOecPdlId04BHHCEanLpmyF7YWCRG0vM=
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 <caml-list@yquem.inria.fr>; 11 Jan 2012 11:48:51 +0100
Message-ID: <4F0D6913.4090207@wp.pl>
Date: Wed, 11 Jan 2012 11:48:51 +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: 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>
In-Reply-To: <E51C5B015DBD1348A1D85763337FB6D9C26218B6@Remus.metastack.local>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
X-WP-AV: skaner antywirusowy poczty Wirtualnej Polski S. A.
X-WP-SPAM: NO 0000000 [YXM0]                               
Subject: [Caml-list] Re: References and polymorphism

> They certainly did: http://mlton.org/ValueRestriction has links to the various papers on the subject (the present scheme was not the first solution for SML, as it notes).
>
I don't get one thing about this. It seems that all examples which 
justify the value restriction are unsound just because a ref cell is 
given too general type.
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 *)
     ...

Dawid