Re: [Caml-list] Polymorphic variants question

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Andres Varon <avaron@gmail.com>

> > 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