From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 7F9BDBB9A for ; Mon, 7 Nov 2005 14:39:30 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jA7DdUWY001840 for ; Mon, 7 Nov 2005 14:39:30 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id OAA05952 for ; Mon, 7 Nov 2005 14:39:29 +0100 (MET) Received: from imag.imag.fr (imag.imag.fr [129.88.30.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jA7DdTdQ001830 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Mon, 7 Nov 2005 14:39:29 +0100 Received: from [147.171.255.214] (mac-clerc.imag.fr [147.171.255.214]) by imag.imag.fr (8.13.0/8.13.0) with ESMTP id jA7DdRMU022953 for ; Mon, 7 Nov 2005 14:39:27 +0100 (CET) Mime-Version: 1.0 (Apple Message framework v746.2) In-Reply-To: <20051107.121102.78704390.garrigue@math.nagoya-u.ac.jp> References: <20051101.092744.112578253.garrigue@math.nagoya-u.ac.jp> <4CB7BAE5-122C-4241-B744-F9D1F5F3D96D@free.fr> <20051107.121102.78704390.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Message-Id: Content-Transfer-Encoding: quoted-printable From: Xavier Clerc Subject: Re: [Caml-list] Question about polymorphic variants Date: Mon, 7 Nov 2005 14:39:58 +0100 To: caml-list@inria.fr X-Mailer: Apple Mail (2.746.2) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-1.6 (imag.imag.fr [129.88.30.1]); Mon, 07 Nov 2005 14:39:27 +0100 (CET) X-IMAG-MailScanner: Found to be clean X-IMAG-MailScanner-Information: Please contact the ISP for more information X-j-chkmail-Score: MSGID : 436F5911.000 on concorde : j-chkmail score : X : 0/20 1 X-Miltered: at concorde with ID 436F5912.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 436F5911.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 variants:01 compiler:01 patched:01 arrays:01 unboxed:01 compiler:01 equivalently:01 polymorphic:01 unsafe:01 jacques:01 jacques:01 caml:02 objective:02 variables:02 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Le 7 nov. 05 =E0 04:11, Jacques Garrigue a =E9crit : > From: Xavier Clerc > >> Thanks for your answer, I start to grasp how existence of "top" can >> be related to related to my question. >> However, I must confess that I am still puzzled by the fact that your >> example heavily rely on the actual representations of elements and >> not only on their types. >> A question is still pending in my mind (in fact, always the same >> question, reformulated to sound like I am making some progress) : if >> the compiler(s) where patched to treat all arrays either as boxed or >> as unboxed, would it be safe to get rid of the leading underscore in >> the inferred type ? > > Possibly. That is, only if there is nothing else in the representation > of values that makes impossible to assume the existence of top. > This counter-example is simple enough, but to check that top is sound > one would have to check the whole compiler and libraries. > The point is that, if you do not require the existence of top from the > beginning, you may end up doing lots of things that make it impossible > to add it later. > >> Equivalently, is the use of "top" (using Obj.repr and relatives) >> unsafe only because of concrete representation or for theoretical >> reason ? > > Theory is only a way to prove that practice is correct. > There is no theoretical reason not to have top (one can design a > sound theory with top), but if practice does not allow to add top, > then theory does not allow us to generalize contravariant type > variables. > > Put differently, it had been known that the existence of top would > matter, implementation might have been different. Or the conclusion > might have been that assuming top would be too much of a burden in > practice, and it might have been intentionally dropped anyway. Not > allowing a compiler to change representation according to types can be > seen as rather drastic, even if Objective Caml doesn't do it a lot. > > Jacques Garrigue > Thanks again for your thorough and precious explanations. Best regards, Xavier Clerc=