From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 935C0D460 for ; Mon, 7 Nov 2005 04:10:20 +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 jA73AJj1017529 for ; Mon, 7 Nov 2005 04:10:20 +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 EAA19419 for ; Mon, 7 Nov 2005 04:10:19 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jA73AHD1017523 for ; Mon, 7 Nov 2005 04:10:18 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id jA73ABf5022760; Mon, 7 Nov 2005 12:10:12 +0900 (JST) Date: Mon, 07 Nov 2005 12:11:02 +0900 (JST) Message-Id: <20051107.121102.78704390.garrigue@math.nagoya-u.ac.jp> To: xcforum@free.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] Question about polymorphic variants From: Jacques Garrigue In-Reply-To: <4CB7BAE5-122C-4241-B744-F9D1F5F3D96D@free.fr> References: <20051101.092744.112578253.garrigue@math.nagoya-u.ac.jp> <4CB7BAE5-122C-4241-B744-F9D1F5F3D96D@free.fr> X-Mailer: Mew version 4.2 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 436EC59B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 436EC599.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 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