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 <http://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
>