Re: [Caml-list] Polymorphic variants question

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

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