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=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 3A81DBBBB for ; Mon, 4 Sep 2006 01:19:13 +0200 (CEST) Received: from rabbit.math.nagoya-u.ac.jp (rabbit.math.nagoya-u.ac.jp [133.6.130.5]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k83NJB6I029824 for ; Mon, 4 Sep 2006 01:19:12 +0200 Received: from localhost (moose-172 [172.16.254.3]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id k83NIkuu021934; Mon, 4 Sep 2006 08:18:46 +0900 (JST) Date: Mon, 04 Sep 2006 08:18:39 +0900 (JST) Message-Id: <20060904.081839.38906751.garrigue@math.nagoya-u.ac.jp> To: avaron@gmail.com Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Polymorphic variants question From: Jacques Garrigue In-Reply-To: <90F4D998-FB49-4EA5-81EA-DB0746B10071@gmail.com> References: <20060903.180856.123164161.garrigue@math.nagoya-u.ac.jp> <90F4D998-FB49-4EA5-81EA-DB0746B10071@gmail.com> 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 44FB62EF.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 variants:01 sig:01 sig:01 refining:98 polymorphic:01 polymorphic:01 From: Andres Varon > > 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. Interesting point. I'm still convinced that, as polymorphic variants provide mixed union by opposition to the disjoint union of normal variants, it would be a pity to restrict them by default. But since our idea is to add compatibility constraints to functor parameters, to explicitly allow combining two abstract variant types, it is actually easy to extend compatibilities with exclusive ones. That is, to allow mixed sum you would write (omiting the private's) module A(B : sig type t = [> ] end)(C : sig type t = [> ] ~ [B.t]) = ... The above ~ [B.t] means that C.t should be compatible with C.t (common tags should have identical types), allowing to create the union [B.t | C.t]. To accomodate your needs for disjoint sum, we just need a small variation on that module A(B : sig type t = [> ] end)(C : sig type t = [> ] ~ [~B.t]) = ... Here ~ [~B.t] would mean that C.t shouldn't contain any tag from B.t, enforcing that they are disjoint. Of course this still allows creating the union [B.t | C.t]. Jacques Garrigue