Hi Nicolas,

Thanks fro your answer.
If i understand correctly, you mean that if i write, say :

module type S = sig type t val zero: t end
module type T = sig type t val zero: t end
module Make (X : S) = (struct type t = X.t * X.t let zero = X.zero, X.zero end : T)
module M1 = Make (struct type t = int let zero = 0 end)
module M2 = Make (struct type t = int let zero = 0 end)

then the compiler will never be able to deduce that M1.t and M2.t are indeed compatible. Am i right ?

I guess it is because re-use the [Myseta.Product] functor only views the abstract types exposed by the [Myset.Make] and [Myset.Product] output signatures.

Seems therefore i am really stuck :(

Jocelyn

Le 6 juil. 2016 ΰ 09:49, Nicolas Ojeda Bar <nicolas.ojeda.bar@lexifi.com> a ιcrit :

> Hi Jocelyn
> 
> One 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.
> 
> Cheers
> Nicolas
> 
> 
> On Tue, Jul 5, 2016 at 5:25 PM, Jocelyn Sιrot <Jocelyn.Serot@univ-bpclermont.fr> wrote:
> 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
>