Re: [Caml-list] Polymorphic variants question

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

From: Andres Varon <avaron@gmail.com>
[...]
> In the same line of ideas, I wish I could do something like the
> following :
> 
> module type S = sig
> 	type t
> 	val f : t -> int
> end
> 
> module A (B : S with type t = [> ]) (C : S with type t = [> ]) : S  
> with type t = [B.t | C.t] = struct
> 	type t = [ B.t | C.t ]	
> 
> 	let f x =
> 		match x with
> 		| #A.t as x -> A.f x	
> 		| #B.t as x -> B.f x
> end
> 
> Of course the example won't even compile, but I think it reflects the  
> spirit of what I would like to do. I know this is just not possible  
> due to a practical reason (#A.t is expanded to the constructors that  
> it includes, and therefore, A.t has to be fully known at compile  
> time, correct?). Is there a theoretical reason to have this  
> constraint though?

Just that the concrete type is much simpler.
The abstract type does not work directly, as you need a way to ensure
that B.t and C.t are compatible. Otherwise, one could write

module D = A(struct type t = [ `A of int] ... end)
            (struct type t = [ `A of string] ... end)

which is clearly incorrect.

The good news is that, with Romain Bardou, we have now solved this not
so trivial problem (at least at the theoretical level), so there is
some hope. 
Note however that there are also some more practical problems, and
whether this gets into ocaml or not does not depend only on the
theory...

Jacques Garrigue