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 q0BFh0J1017098 for ; Wed, 11 Jan 2012 16:43:00 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkoBALesDU+LEwExe2dsb2JhbAA7B60NAQELCyYFIIFyAQEBAwEnCwENAQE3AQQLBQQCDgouVwYTEYdppReEIQGOJgeIZ4M2lRCSPQ X-IronPort-AV: E=Sophos;i="4.71,493,1320620400"; d="scan'208";a="126452023" 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:42:55 +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=Yv65N3QyBxfoW54F7ptjSidE+KjoFH+/Qc 1TBTslRXc=; b=h6gyQyQ8Y6v6YnGMNsjYZF5w3xTQAFtXzuR7gnLhh2hG4zX1XM ENlSSG251coKEtTYsRDj4k/o0nY7O4nDKh6kXcclO4J4R+avZZlAPcrVzJIdHBU2 QVXSQDWq8ewfk0/OPHnZITn82aCyT3DH3ut+BlKauN6iyDCK5+ZF7JE1Q= Received: from newzak.mpi-klsb.mpg.de ([139.19.1.29]:35733) by hera.mpi-sb.mpg.de (envelope-from ) with esmtp (Exim 4.69) id 1Rl0KC-0001pg-Ie; Wed, 11 Jan 2012 16:42:54 +0100 Received: from local by newzak.mpi-klsb.mpg.de (envelope-from ) with local (Exim 4.72) id 1Rl0KC-0008PN-3A; Wed, 11 Jan 2012 16:42:52 +0100 Received: from 74.125.57.233 (SquirrelMail authenticated user rossberg) by mail.mpi-sws.org with HTTP; Wed, 11 Jan 2012 16:42:52 +0100 Message-ID: <869af1b432cfe71214ce68625a92a1c0.squirrel@mail.mpi-sws.org> In-Reply-To: <4F0D9501.60107@wp.pl> 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> Date: Wed, 11 Jan 2012 16:42:52 +0100 From: rossberg@mpi-sws.org To: "Dawid Toton" Cc: "caml-list" , rossberg@mpi-sws.org 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: > 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. > > I would insist that it won't crash at run-time. > Consider the possibilities: > a) type abstraction suspends the computation - no run-time crash; there > are implementation problems as in my comment above > b) computation is not suspended in the sense that the job is done at > compile time - for each possible type 'aa a separate ref cell is > allocated. This is of course problematic in practice, but still sound. > 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. > > I would say that the difference between a) and b) is minor, just a > choice between more static or more dynamic implementation of the same > semantics. It is actually: d) computation is not suspended, allocation is done when the declaration is evaluated, for some. That is more or less equivalent to (c) when the declaration is in global scope. > 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. /Andreas