[Caml-list] Need help with higher order functors

[SEROT Jocelyn <Jocelyn.SEROT@univ-bpclermont.fr>]

Hi,

I'm trying to implement an extension of the Set module including the  
notion of cartesian product.

The interface of the module is :

(** File pset.mli *)

module type ELT_PROD = sig
   include Set.OrderedType
   type t1
   type t2
   val product: t1 -> t2 -> t
end

module type SET_PROD = sig
   include Set.S
   type t1
   type t2
   val product: t1 -> t2 -> t
end

module MakeProduct
     (E1: Set.OrderedType)
     (E2: Set.OrderedType)
     (C: functor (E1: Set.OrderedType) -> functor (E2:  
Set.OrderedType) -> ELT_PROD with type t1 = E1.t and type t2 = E2.t)
     : SET_PROD
       with type t1 = Set.Make(E1).t
       and type t2 = Set.Make(E2).t
       and type  t = Set.Make(C(E1)(E2)).t
       and type elt = C(E1)(E2).t

The [MakeProduct] functor takes the signature of element types and a  
functor describing how to combine these elements for building the set  
product.
An "obvious" definition of such a functor could be

module MakePair (E1: Set.OrderedType) (E2: Set.OrderedType) = struct
   type t = E1.t * E2.t
   let compare = Pervasives.compare
   type t1 = E1.t
   type t2 = E2.t
   let product x y = x,y
end

so that the definition of the "natural" cartesian product of two sets  
with with elements having sig Int and Bool resp., should be

module IntBoolSet = MakeProduct (Int) (Bool) (MakePair)

but taking an extra functor argument for [MakeProduct] allows  
specialized definitions of the product. For example, here's an  
alternative definition of the MakePair functor which
could be passed to MakeProduct :

module MakePair' (E1: Set.OrderedType) (E2: Set.OrderedType) = struct
   type t = Pair of E1.t * E2.t
   let compare = Pervasives.compare
   type t1 = E1.t
   type t2 = E2.t
   let product x y = Pair (x,y)
end

The problem i have is in the implementation of the Mset module :

(** File mset.ml *)

module type SET_PROD = sig
   include Set.S
   type t1
   type t2
   val product: t1 -> t2 -> t
end

module type ELT_PROD = sig
   include Set.OrderedType
   type t1
   type t2
   val product: t1 -> t2 -> t
end

module MakeProduct
     (E1: Set.OrderedType)
     (E2: Set.OrderedType)
     (C: functor (E1: Set.OrderedType) -> functor (E2:  
Set.OrderedType) -> ELT_PROD with type t1 = E1.t and type t2 = E2.t) =
struct
   module S1 = Set.Make (E1)
   module S2 = Set.Make (E2)
   module P = C (E1) (E2)
   module R = Set.Make(P)
   include R
   type t1 = S1.t
   type t2 = S2.t
   let product s1 s2 =
     let f x y t = R.add (P.product x y) t in
     let g x t = S2.fold (f x) s2 t in
     S1.fold g s1 R.empty
end

Unfortunately, this does not compile. I get a long error message,  
ending with :

(* excerpt of the compiler log : *)

            module R :
              sig
                type elt = P.t
                type t = Set.Make(P).t
                val empty : t
                ...
              end
            type elt = P.t
            type t = Set.Make(P).t
            val empty : t
            ....
            type t1 = S1.t
            type t2 = S2.t
            val product : S1.t -> S2.t -> R.t
          end
        is not included in
          sig
            type elt = C(E1)(E2).t
            type t = Set.Make(C(E1)(E2)).t
            val empty : t
            ...
            type t1 = Set.Make(E1).t
            type t2 = Set.Make(E2).t
            val product : t1 -> t2 -> t
          end
        Type declarations do not match:
          type t = Set.Make(P).t
        is not included in
          type t = Set.Make(C(E1)(E2)).t

I suspect that some sharing constraint is missing here, but cannot spot where.
I was expecting that  declaration
   module P = C (E1) (E2)
in the functor definition should automatically enforce the equality of types
P.t and C(E1)(E2).t, and, hence, of types Set.Make(P).t and  
Set.Make(C(E1)(E2)).t.
Obviously not.

Any help would be greatly appreciated ;)

Thanks in advance,

Jocelyn