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 q0C9tHHn028745 for ; Thu, 12 Jan 2012 10:55:17 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsQBAICtDk/UTWUHjWdsb2JhbAA8B4UOp3giAQEBAQkJCwkSBiGBcgEBBSMECwEFCAEBOA8JAhgCAgUhAgIPAkYGAQwGAgEBh3ilRGqDNwGNfAeBL4c4giCBFppPjH8 X-IronPort-AV: E=Sophos;i="4.71,497,1320620400"; d="scan'208";a="126557918" Received: from mx3.wp.pl ([212.77.101.7]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 12 Jan 2012 10:55:11 +0100 Received: (wp-smtpd smtp.wp.pl 18531 invoked from network); 12 Jan 2012 10:55:04 +0100 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wp.pl; s=1024a; t=1326362104; bh=OVo2Ge4Wc/rT/ZT6cVkbN1JiMmM6JCS/gSdr/SboGhM=; h=From:To:Subject; b=p3VGoZk53It+m/nArYH4xz43rjUHVqiBYBY7D4Wc+kHheUU8XpJeisllyqwS9USv6 Xx5UXnjN5cBqZvXA22Z1pDZS/EaoQoT5Tj/lqmT8BEk38g8B/oytixYYSPJJwueuIj 0gX7EqsnL1eWf1h9n6FqHGT6cbTntBtLAzfzvPsQ= Received: from 18-161.2-0.pl (HELO [192.168.1.100]) (d0@[91.189.18.161]) (envelope-sender ) by smtp.wp.pl (WP-SMTPD) with AES256-SHA encrypted SMTP for ; 12 Jan 2012 10:55:04 +0100 Message-ID: <4F0EADF6.10309@wp.pl> Date: Thu, 12 Jan 2012 10:55:02 +0100 From: Dawid Toton 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 References: <1326209342.96423.YahooMailNeo@web111502.mail.gq1.yahoo.com> <1326214824.62249.YahooMailNeo@web111507.mail.gq1.yahoo.com> <4F0D6913.4090207@wp.pl> <4F0D87E8.90602@wp.pl> <13b032314ec2f8f50916bcfa6eb7f72b.squirrel@mail.mpi-sws.org> <4F0D9501.60107@wp.pl> <869af1b432cfe71214ce68625a92a1c0.squirrel@mail.mpi-sws.org> In-Reply-To: <869af1b432cfe71214ce68625a92a1c0.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 [gaPE] Subject: Re: [Caml-list] Re: References and polymorphism On 2012-01-11 16:42, rossberg@mpi-sws.org wrote: > Dawid Toton wrote: >> On 2012-01-11 14:15, rossberg@mpi-sws.org wrote: >>>> let f3 : forall ˆ€'a . unit -> 'a list ref = >>>> fun (type 'aa) -> >>>> let r = ref ([] : 'aa list) in >>>> fun () -> >>>> r >>>> >>>> (* f3: Fine, but it would require some work at compile time or smart >>>> transformations to keep types erased at run-time. Also, keeping the >>>> first actual argument (staying for 'aa) implicit would need extra rules >>>> to resolve ambiguities (decide when this argument is applied). *) >>> No, this would be unsound, because "fun (type t) -> ..." does not the >>> suspend computation -- there'd be only one ref. It's not System F. >> c) computation is not suspended in the sense that the allocation is done >> at compile time, but the implementation tries to keep only one ref cell >> for this purpose. This is impossible. The function can't be compiled >> this way. > It is actually: > > d) computation is not suspended, allocation is done when the declaration is > evaluated, for some. >> The c) option is incorrect, as I understand it, regardless what type >> system flavour is chosen. > Not sure why you think so, but in any case, that's essentially what's > happening. Type abstraction or application is not operationally observable > in OCaml, or any similar language. Which is exactly the reason why the > whole soundness issue with polymorphism + references arises, and you have to > disallow certain combinations. This specific example, the f3 function, won't happen in OCaml-like language at all, because of the forall quantifier in type annotation for the function. While I get the point that this generalization is forbidden by the value restriction, what I'm trying to say is that the value restriction is not needed here and I can't think of any convincing example in favour of if. Here is how we get the right result without the value restriction rule: first the compiler has to choose the strategy (a), (b) or (c/d). For (a) and (b) it can say that it isn't smart enough and refuse to compile the code. On the other hand, the (c/d) case is rejected, because of the impossible allocation of r: types int list ref and string list ref are incompatible, hence one allocation for all the cases is insufficient. This is so simple, because we are not interested in generalized ref cells, I mean, values of forall 'a.('a list ref) types are useless and I think that less sophisticated typechecker shouldn't even consider this type. It is perhaps more clear if said this way: the strategy (c/d) is equivalent to starting with the f0/f2 function body in order to build something equivalent to f3. But f2 cannot be cast to f3, because (r : ∀'c. 'c list) allocated in f2 cannot be cast to 'aa list ref. An error message would say that types 'c and 'aa cannot be unified, or - if the quantifier for the function type is yet to be chosen - typechecker would give up with forall and continue with a type variable (a type exists). In case of ordinary OCaml, things are even simpler. One can't express f3. My current understanding is that only f4 and the following are possible: ∃'b. let f : X 'a. (unit -> 'a list ref) = let r = ref ([] : 'b list) in fun (type 'aa) -> fun () -> r Only existential quantifier will fit X so the whole thing is well typed. Again, no value restriction intervenes. Dawid