Hi JocelynOne issue is that you have two modules, P and R.S, of the form Set.Make(X), Set.Make (X') for modules X and X' which are structurally equal. Unfortunately this is not enough for the OCaml module system to deduce that P.t and R.S.t are compatible. In general if F is a functor with output signature S and t is abstract type in S, then F(X).t and F(X').t will be compatible exactly when X and X' are literally the same module. I don't think you will be able to fix this by adding type sharing constrains.CheersNicolasOn Tue, Jul 5, 2016 at 5:25 PM, Jocelyn Sιrot <Jocelyn.Serot@univ-bpclermont.fr> wrote:Dear all,Im stuck with a problem related with the use of functors for implementing a library.The library concerns Labeled Transition Systems but ill 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.mlimodule type T = sigtype elttype tval empty: tval add: elt -> t -> tval elems: t -> elt listval fold: (elt -> 'a -> 'a) -> t -> 'a -> 'aendmodule Make (E : Set.OrderedType) : T with type elt = E.t myset.mlmodule type T = sig (* idem myset.mli *) endmodule Make (E : Set.OrderedType) = structmodule Elt = Etype elt = E.ttype 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.elemslet fold f s z = List.fold_left (fun z e -> f e z) z s.elemsendFirst, i add a functor for computing the product of two sets : myset.mli (contd)module Product (S1: T) (S2: T) :siginclude T with type elt = S1.elt * S2.eltval product: S1.t -> S2.t -> tend myset.ml (contd)module Product(S1: T)(S2: T) =structmodule R =Make (struct type t = S1.elt * S2.elt let compare = compare end)include Rlet product s1 s2 =S1.fold(fun q1 z ->S2.fold(fun q2 z -> R.add (q1,q2) z)s2z)s1R.emptyendHeres a typical usage of the Myset module : ex1.mlmodule 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 s2So 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 - lets 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].Heres a first proposal (excluding the Product functor for the moment) : myseta.mlimodule type Attr = sig type t endmodule type T = sigtype elttype attrtype tmodule S: Myset.Tval empty: tval add: elt * attr -> t -> tval elems: t -> elt listval attrs: t -> (elt * attr) listval set_of: t -> S.tval fold: (elt * attr -> 'a -> 'a) -> t -> 'a -> 'aendmodule Make (E : Set.OrderedType) (A: Attr) : T with type elt = E.t and type attr = A.t myseta.mlmodule type Attr = sig type t endmodule type T = sig (* idem myseta.mli *) endmodule Make (E : Set.OrderedType) (A : Attr) = structmodule Elt = Etype elt = E.ttype attr = A.tmodule 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.elemslet attrs s = s.attrslet set_of s = s.elemslet fold f s z = List.fold_left (fun z e -> f e z) z s.attrsendIn 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 :Its 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 (contd)module Product (S1: T) (S2: T) :siginclude T with type elt = S1.elt * S2.eltand type attr = S1.attr * S2.attrval product: S1.t -> S2.t -> tendNow, heres my current implementation myset.ml (contd)module Product(S1: T)(S2: T) =structmodule 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 Rmodule 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) }endI 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).tbut an expression was expected of type S.t = R.S.tMy 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) :siginclude T with type elt = S1.elt * S2.eltand type attr = S1.attr * S2.attrand type S.t = Myset.Product(S1.S)(S2.S).t (* added constraint *)val product: S1.t -> S2.t -> tendbut 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 : ive 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.. :-SIn anycase, the source code is here : http://filez.univ-bpclermont.fr/lamuemlqpmJocelyn