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