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 q0BDuUmv012551 for ; Wed, 11 Jan 2012 14:56:30 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjgCACqUDU/UTWUIjWdsb2JhbAA8B4UPp1giAQEBAQkJCwkSBiGBcgEBBSMECwEFCAEBOA8JAhgCAgUhAgIPAkYGAQwGAgEBh3ikdmqDNwGOJgeBL4c4giCBFppOjH8 X-IronPort-AV: E=Sophos;i="4.71,493,1320620400"; d="scan'208";a="126430674" 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 14:56:24 +0100 Received: (wp-smtpd smtp.wp.pl 8265 invoked from network); 11 Jan 2012 14:56:18 +0100 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wp.pl; s=1024a; t=1326290178; bh=/5AWZHEVNBDHyhT4b/cO1sMxfc8sN8ILjQHRcgJ/P24=; h=From:To:Subject; b=O8IUIAF9wzDo3vjTVgQ1Laxg4e1fjX1+M7u3P1f0AmQVTBRdcSwU8gG/Qn5gp12wW rFeL5jtSgb+MTGKwjzoTqthaWHupS8hdwkYzCr8X4XWydSHVn2HUZka5K7uIXBeflJ k6LpNPp3O7W8PDc1o0uZk0Aotis02Z2LSA71KFkg= 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 ; 11 Jan 2012 14:56:18 +0100 Message-ID: <4F0D9501.60107@wp.pl> Date: Wed, 11 Jan 2012 14:56:17 +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: caml-list , rossberg@mpi-sws.org 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> In-Reply-To: <13b032314ec2f8f50916bcfa6eb7f72b.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 [sVO0] Subject: [Caml-list] Re: References and polymorphism 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. The c) option is incorrect, as I understand it, regardless what type system flavour is chosen. Dawid