From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.5 required=5.0 tests=DNS_FROM_RFC_ABUSE 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by yquem.inria.fr (Postfix) with ESMTP id E432DBB83
	for <caml-list@yquem.inria.fr>; Sat,  2 Sep 2006 13:17:14 +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 k82BHC6Y030412
	for <caml-list@yquem.inria.fr>; Sat, 2 Sep 2006 13:17:14 +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 k82BGp3S006690;
	Sat, 2 Sep 2006 20:16:52 +0900 (JST)
Date: Sat, 02 Sep 2006 20:16:46 +0900 (JST)
Message-Id: <20060902.201646.110439764.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 <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <7E1CAC5D-67CC-4A5C-8DE6-BB2A60A6615B@gmail.com>
References: <012901c6cdec$64edf490$6a7ba8c0@treble>
	<1157138993.22787.34.camel@rosella.wigram>
	<7E1CAC5D-67CC-4A5C-8DE6-BB2A60A6615B@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 44F96838.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; variants:01 sig:01 val:01 struct:01 constructors:01 struct:01 trivial:01 ocaml:01 polymorphic:01 abstract:01 compile:01 compile:01 caml-list:01 constraint:01 int:01 

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