From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.7 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, SPF_NEUTRAL autolearn=disabled version=3.1.3 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 945A7BBBB for ; Sun, 3 Sep 2006 17:00:45 +0200 (CEST) Received: from wx-out-0506.google.com (wx-out-0506.google.com [66.249.82.234]) by nez-perce.inria.fr (8.13.6/8.13.6) with ESMTP id k83F0imS012125 for ; Sun, 3 Sep 2006 17:00:45 +0200 Received: by wx-out-0506.google.com with SMTP id s6so1744348wxc for ; Sun, 03 Sep 2006 08:00:44 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:from:subject:date:to:x-mailer; b=gxoS24wh+Lh8Xk9UXOlmIQzvdvuwfEYOQqZX5Cde6t6xone50dmucqchR0u0/IVflcusFLQ9wHJkXCxJYvlU/MySeGJMcCBN2gbUJiOLZaRGwYzSSatPx0sfBXA+clXrtZmTOVDGht2ASNZhCdRfGT33eTXbgKmf05p9Btmj9Jg= Received: by 10.70.103.12 with SMTP id a12mr5969398wxc; Sun, 03 Sep 2006 08:00:44 -0700 (PDT) Received: from ?192.168.0.3? ( [70.19.59.48]) by mx.gmail.com with ESMTP id i33sm6439111wxd.2006.09.03.08.00.43; Sun, 03 Sep 2006 08:00:43 -0700 (PDT) In-Reply-To: <20060903.180856.123164161.garrigue@math.nagoya-u.ac.jp> References: <7E1CAC5D-67CC-4A5C-8DE6-BB2A60A6615B@gmail.com> <20060902.201646.110439764.garrigue@math.nagoya-u.ac.jp> <20060903.180856.123164161.garrigue@math.nagoya-u.ac.jp> Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <90F4D998-FB49-4EA5-81EA-DB0746B10071@gmail.com> Cc: caml-list@yquem.inria.fr Content-Transfer-Encoding: 7bit From: Andres Varon Subject: Re: [Caml-list] Polymorphic variants question Date: Sun, 3 Sep 2006 11:00:40 -0400 To: Jacques Garrigue X-Mailer: Apple Mail (2.752.2) X-j-chkmail-Score: MSGID : 44FAEE1C.000 on nez-perce : j-chkmail score : X : 0/20 1 X-Miltered: at nez-perce with ID 44FAEE1C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; variants:01 functor:01 unions:01 ocaml:01 compiler:01 functor:01 unions:01 intersection:01 compiler:01 ocaml:01 refining:98 polymorphic:01 signatures:01 caml-list:01 constraint:01 > > Just that I don't see how you could possibly enforce the above > condition either, without something in the signatures to tell the > system that argument sets of B.t and C.t must be disjoint. > Or you are telling me that, as you already included "type t = [B.t | > C.t]" in the return type of the functor, there is already an implicit > constraint on B.t and C.t. This is right indeed, but the point is that > you need some logic to handle this constraint; and you want also to be > able to create unions without necessarily writing it in the outside > signature. > I haven't modified the ocaml compiler to be able to make that functor, but I have made the small change (or I made a small change and left a bunch of holes!), so that unions must always be disjoint, you can still use the intersection of type by refining one, but unions should always be disjoint (ok, it is turned on with a flag in the compiler). This is a desirable feature in the context of my program, though I can see that making unions from compatible types is also desirable in other contexts. I want to add exactly the assumption you mention, if type t = [B.t | C.t] is included in the type of the functor, that implicit constraint is there, otherwise, what will be the proper behavior of the function for a tag that appears in both C.t and B.t? one overrides the other? It seems to me that in the context of that functor, the union must be of disjoint types, not only for that problematic case of yours, but even for the compatible cases, otherwise, I cannot guarantee that the functor that composes two modules that have even been proved correct, will still be correct; if they are disjoint, I clean my hands with many problematic corners. You know far better than me how hard would it be to get this going, but I asked because I would like to try to prototype this idea in Ocaml, unless there is some flaw that would be induced in the type system. It seems to be useful (certainly for me at least :-)). Thanks! Andres > Jacques Garrigue