Dear all, 

I’m stuck with a problem related with the use of functors for implementing a library.
The library concerns Labeled Transition Systems but i’ll present it in a simplified version using sets.

Suppose i have a (very simplified !) Set module, which i will call Myset to distinguish from that of the standard library :

———— myset.mli
module type T = sig
  type elt 
  type t 
  val empty: t
  val add: elt -> t -> t
  val elems: t -> elt list
  val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
end

module Make (E : Set.OrderedType) : T with type elt = E.t
——— 

———— myset.ml
module type T = sig … (* idem myset.mli *) end

module Make (E : Set.OrderedType) = struct
  module Elt = E
  type elt = E.t
  type t = { elems: elt list; }  
  let empty = { elems = [] }
  let add q s = { elems = q :: s.elems }  (* obviously wrong, but does not matter here ! *)
  let elems s = s.elems
  let fold f s z = List.fold_left (fun z e -> f e z) z s.elems
end
——— 

First, i add a functor for computing the product of two sets :

———— myset.mli (cont’d)
module Product (S1: T) (S2: T) :
sig
  include T with type elt = S1.elt * S2.elt
  val product: S1.t -> S2.t -> t
end
——— 

———— myset.ml (cont’d)
module Product
  (S1: T)
  (S2: T) =
struct
  module R =
    Make (struct type t = S1.elt * S2.elt let compare = compare end)
    include R
    let product s1 s2 =
      S1.fold
        (fun q1 z ->
           S2.fold
             (fun q2 z -> R.add (q1,q2) z)
             s2
             z)
        s1
        R.empty
end
——— 

Here’s a typical usage of the Myset module : 

—— ex1.ml 
module IntSet = Myset.Make (struct type t = int let compare = compare end)
module StringSet = Myset.Make (struct type t = string let compare = compare end)

let s1 = IntSet.add 1 (IntSet.add 2 IntSet.empty)
let s2 = StringSet.add "a" (StringSet.add "b" StringSet.empty)

module IntStringSet = Myset.Product (IntSet) (StringSet)

let s3 = IntStringSet.product s1 s2
——

So far, so good. 

Now suppose i want to « augment » the Myset module so that some kind of attribute is attached to each set element. I could of course just modify the definition of type [t] and the related functions in the files [myset.ml] and [myset.mli]. But suppose i want to reuse as much as possible the code already written. My idea is define a new module - let’s call it [myseta] (« a » for attributes) - in which the type [t] will include a type [Myset.t] and the definitions of this module will make use, as much as possible, of those defined in [Myset].

Here’s a first proposal (excluding the Product functor for the moment) : 

———— myseta.mli
module type Attr = sig type t end

module type T = sig
  type elt 
  type attr
  type t 
  module S: Myset.T
  val empty: t
  val add: elt * attr -> t -> t
  val elems: t -> elt list
  val attrs: t -> (elt * attr) list
  val set_of: t -> S.t
  val fold: (elt * attr -> 'a -> 'a) -> t -> 'a -> 'a
end

module Make (E : Set.OrderedType) (A: Attr) : T with type elt = E.t and type attr = A.t
——— 

———— myseta.ml
module type Attr = sig type t end

module type T = sig (* idem myseta.mli *) end

module Make (E : Set.OrderedType) (A : Attr) = struct
  module Elt = E
  type elt = E.t
  type attr = A.t
  module S = Myset.Make(E)
  type t = { elems: S.t; attrs: (elt * attr) list }
  let empty = { elems = S.empty; attrs = [] }
  let add (e,a) s = { elems = S.add e s.elems; attrs = (e,a) :: s.attrs }
  let elems s = S.elems s.elems
  let attrs s = s.attrs
  let set_of s = s.elems
  let fold f s z = List.fold_left (fun z e -> f e z) z s.attrs
end
——— 

In practice, of course the [Attr] signature will include other specifications.
In a sense, this is a « has a » inheritance : whenever i build a [Myseta] module, i actually build a [Myset] sub-module and this module is used to implement all the set-related operations. 
Again, so far, so good.
The problem shows when i try to define the [Product] functor for the [Myseta] module :
It’s signature is similar to that of the [Myset.Product] functor, with an added sharing constraint for attributes (in fact, we could imagine a more sophisticated scheme for merging attributes but cartesian product is here) :

———— myset.mli (cont’d)
module Product (S1: T) (S2: T) :
sig
  include T with type elt = S1.elt * S2.elt
             and type attr = S1.attr * S2.attr
  val product: S1.t -> S2.t -> t
end
——— 

Now, here’s my current implementation

———— myset.ml (cont’d)
module Product
  (S1: T)
  (S2: T) =
struct
  module R =
    Make
      (struct type t = S1.elt * S2.elt let compare = compare end)
      (struct type t = S1.attr * S2.attr let compare = compare end)
  include R
  module P = Myset.Product(S1.S)(S2.S)
  let product s1 s2 =
    { elems = P.product (S1.set_of s1) (S2.set_of s2);
            attrs =
        List.fold_left
          (fun acc (e1,a1) ->
             List.fold_left (fun acc (e2,a2) -> ((e1,e2),(a1,a2))::acc) acc (S2.attrs s2))
          []
          (S1.attrs s1) }
end
——— 

I use the [Myseta.Make] functor for building the resulting module [named R here]. For defining the [product] function, i first use the [Myset.Product] functor applied on the two related sub-modules [S1] and [S2] to build the product module (named P here) and re-use the [product] function of this module to compute the [elems] component of the result. The other component is computed directly. 
The problem is that when i try to compile this i get this message : 

File "myseta.ml", line 44, characters 14-53:
Error: This expression has type P.t = Myset.Product(S1.S)(S2.S).t
       but an expression was expected of type S.t = R.S.t

My intuition is that a sharing constraint is missing somewhere but i just cannot figure out where to add it. 
I tried to rewrite the signature of the [Myseta.Product] functor (in [myseta.mli]) as :

module Product (S1: T) (S2: T) :
sig
  include T with type elt = S1.elt * S2.elt
             and type attr = S1.attr * S2.attr
             and type S.t = Myset.Product(S1.S)(S2.S).t  (* added constraint *)
  val product: S1.t -> S2.t -> t
end

but it did not change anything..

So my question is : is my diagnostic correct and, if yes, which constraint(s) are missing and where; or, conversely, am i completely « misusing » the functor mechanisms for implementing this kind of « reuse by inclusion » ? 

Any help will be grealy appreciated : i’ve been reading and re-reading about functors for the last two days but have the impression that at this step, things get more and more opaque.. :-S

In anycase, the source code is here : http://filez.univ-bpclermont.fr/lamuemlqpm

Jocelyn