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 q0BB7pRF003859 for ; Wed, 11 Jan 2012 12:07:51 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgECABhsDU9KfVK0kGdsb2JhbABCnDeQKQgiAQEBAQkJDQcUBCGBcgEBAQQSAhMZARsSCwEDDAYFCwMKDSEiAREBBQEKEgYTEgkHh2CaJgqLaoJvhGY/iHECBQuDcoggBJUMjgU9g3s X-IronPort-AV: E=Sophos;i="4.71,492,1320620400"; d="scan'208";a="126403112" Received: from mail-we0-f180.google.com ([74.125.82.180]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 11 Jan 2012 12:07:46 +0100 Received: by werp11 with SMTP id p11so714274wer.39 for ; Wed, 11 Jan 2012 03:07:45 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=p8XEpyPnwNQzW6pFmX6FiExJ63bHQJXZipxl00ZMQHo=; b=aFbIbNqCpIY48wUQypujkkp8c9u/09ancj/Nkx+4GUfcEm8HtGJ7lS0vTQ6B3eU5Pq avghNxqesH5eynxlhfwCxKuN3Gx8Uzj9DJkbYsMzAVYxzOR2stFARo/LMAmI8CiH9Qnk olfhc3+86+rv8GBczlBs/NrHABG5gFp/Ny2eA= Received: by 10.216.131.150 with SMTP id m22mr3206491wei.8.1326280065187; Wed, 11 Jan 2012 03:07:45 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.198.147 with HTTP; Wed, 11 Jan 2012 03:07:24 -0800 (PST) In-Reply-To: <4F0D6913.4090207@wp.pl> References: <1326209342.96423.YahooMailNeo@web111502.mail.gq1.yahoo.com> <1326214824.62249.YahooMailNeo@web111507.mail.gq1.yahoo.com> <4F0D6913.4090207@wp.pl> From: Gabriel Scherer Date: Wed, 11 Jan 2012 12:07:24 +0100 Message-ID: To: Dawid Toton Cc: caml-list Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q0BB7pRF003859 Subject: Re: [Caml-list] Re: References and polymorphism How would you make the distinction between let f : 'a . unit -> 'a list ref = fun () -> ref ([] : 'a list) and let f : 'a . unit -> 'a list ref = let r = ref ([] : 'a list) in fun () -> r ? On Wed, Jan 11, 2012 at 11:48 AM, Dawid Toton wrote: >> 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 > > > -- > Caml-list mailing list.  Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >