[Caml-list] Q: functors and "has a" inheritance

[Caml-list] Q: functors and "has a" inheritance

[Jocelyn Sérot]

[-- Attachment #1: Type: text/plain, Size: 6770 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 19484 bytes --]

Re: [Caml-list] Q: functors and "has a" inheritance

[Nicolas Ojeda Bar]

[-- Attachment #1: Type: text/plain, Size: 8020 bytes --]

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
>

[-- Attachment #2: Type: text/html, Size: 19771 bytes --]

Re: [Caml-list] Q: functors and "has a" inheritance

[Jocelyn Sérot]

[-- Attachment #1: Type: text/plain, Size: 8599 bytes --]

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
> 


[-- Attachment #2: Type: text/html, Size: 21965 bytes --]

Re: [Caml-list] Q: functors and "has a" inheritance

[Gerd Stolpmann]

[-- Attachment #1: Type: text/plain, Size: 13532 bytes --]

Am Mittwoch, den 06.07.2016, 10:44 +0200 schrieb Jocelyn Sérot:
> 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 ?

Exactly. The feature is called "applicative functors", if you want to
Google it. The results of two functor applications are considered
compatible when the arguments of the functors are module paths that are
identical or aliases of each other. So, e.g. for

module Arg1 = struct type t = int let zero=0 end
module Arg2 = struct type t = int let zero=0 end
module Arg3 = struct type t = Arg1.t let zero=0 end
module M1 = Make(Arg1)
module M2 = Make(Arg1)
module M3 = Make(Arg2)
module M4 = Make(Arg3)
module M5 = Make(struct type t = int let zero=0 end)

only M1 and M2 are compatible. The compiler doesn't even look at the
types of the argument module, it's only the module name/path that
counts.

Your design might work when you change Product:

module Product (S1: T) (S2: T)
  (P : T with type elt = S1.elt * S2.elt
          and type attr = S1.attr * S2.attr)
sig
  val product: S1.t -> S2.t -> P.t
end

i.e. the "real" product module is the argument P, and this functor only
defines the product function. This way you can instantiate it for any P.

Gerd

> 
> 
> 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
> > 
> > 
> 

-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

Re: [Caml-list] Q: functors and "has a" inheritance

[Petter Urkedal]

On 2016-07-06, Jocelyn Sérot wrote:
> 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 ?

Gerd nicely explained how, so I'm just add a note about why:

1. If the module contained a function rather than a plain constant, it
   would be undecidable in general whether the two structures were
   equal.

2. Even if we could (or adopted syntactic equality as an approximation),
   it would break abstraction:  Structures imported from or depending on
   external libraries could be coincidentally equal at some point and
   different after an upgrade.

So, we would be left with a rather ad-hoc rule about how to compare
structures.  The nominal approach taken by OCaml is consistent even if a
bit conservative.  Note that module paths may include functor
applications.

Re: [Caml-list] Q: functors and "has a" inheritance

[Jocelyn Sérot]

Thanks for the explanations, Gerd and Petter.

At least i now have a name for the wall i’m bumping into ;)

Gerd, i can’t figure out how your proposed workaround can solve the problem : if P is an argument of the Product functor, it has to be built before applying it, hasn't it ? So either we are back to the initial problem or we have to require that the end user manually builds it ? Am i missing sth ?

Incidentelly, i tried another workaround : instead of augmenting the [Myset] module for getting the [MysetA] module, i tried the other way : first define a SetA module with attributes attached to elements and then define a « normal » Set module by « hiding » some operations and redefining some others. Seems i’m stumbling on the same problem.. :( Could it be the case that functors just cannot support the reuse mechanism i’m seeking for ??

Jocelyn


Le 6 juil. 2016 à 12:15, Petter Urkedal <paurkedal@gmail.com> a écrit :

> On 2016-07-06, Jocelyn Sérot wrote:
>> 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 ?
> 
> Gerd nicely explained how, so I'm just add a note about why:
> 
> 1. If the module contained a function rather than a plain constant, it
>   would be undecidable in general whether the two structures were
>   equal.
> 
> 2. Even if we could (or adopted syntactic equality as an approximation),
>   it would break abstraction:  Structures imported from or depending on
>   external libraries could be coincidentally equal at some point and
>   different after an upgrade.
> 
> So, we would be left with a rather ad-hoc rule about how to compare
> structures.  The nominal approach taken by OCaml is consistent even if a
> bit conservative.  Note that module paths may include functor
> applications.

Re: [Caml-list] Q: functors and "has a" inheritance

[Mikhail Mandrykin]

Hello,

On среда, 6 июля 2016 г. 11:54:28 MSK Gerd Stolpmann wrote:
> Am Mittwoch, den 06.07.2016, 10:44 +0200 schrieb Jocelyn Sérot:
> > Hi Nicolas,

> Your design might work when you change Product:
> 
> module Product (S1: T) (S2: T)
>   (P : T with type elt = S1.elt * S2.elt
>           and type attr = S1.attr * S2.attr)
> sig
>   val product: S1.t -> S2.t -> P.t
> end
> 
> i.e. the "real" product module is the argument P, and this functor only
> defines the product function. This way you can instantiate it for any P.

It's also possible to explicitly name the anonymous module "struct type t = 
S1.elt * S2.elt let compare = compare end" e.g. by exposing it in the output 
signature of Product:
  module E : Set.OrderedType with type t = S1.elt * S2.elt
  include T with type elt = E.t and type t = Make(E).t
instead of 
  include T with type elt = S1.elt * S2.elt
in myset.mli (module Product)

Then if Product implementation is changed appropriately i.e.
  module E = (struct
    type t = S1.elt * S2.elt
    let compare = compare
  end)
module R = Make (E)

instead of
  module R =
    Make
      (struct
        type t = S1.elt * S2.elt
        let compare = compare
      end)
  include R
in myset.ml (module Product),

the anonymous module can be named and shared explicitly:
  module P = Myset.Product(S1.S)(S2.S)
  module R =
    Make
      (P.E)
      (struct type t = S1.attr * S2.attr let compare = compare end)
  include R
instead of
  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)
in myset.ml (module Product)

The only remaining problem then is missing equality between elt and S.elt in 
the signature Myseta.T:
module S: Myset.T --> module S: Myset.T with type elt = elt
This makes it work with elems = P.product ...
Then the additional constraint
              ...
              and type S.t = Myset.Product(S1.S)(S2.S).t
in myset.mli
can be turned into
  module P : sig module E : Set.OrderedType end
               ... and type S.t = Myset.Make(P.E).t

Regards, Mikhail
> 
> Gerd
> 
> > 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


-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru

Re: [Caml-list] Q: functors and "has a" inheritance

[Jocelyn Sérot]

[-- Attachment #1: Type: text/plain, Size: 170 bytes --]

Hi Mikhail,

This solves the problem ! 

For those interested, i attach the final code.
Note that I didn’t even need your last patch. 

Thanks A LOT

Jocelyn


[-- Attachment #2: myset2.tar.gz --]
[-- Type: application/x-gzip, Size: 2245 bytes --]

[-- Attachment #3: Type: text/plain, Size: 13923 bytes --]


Le 6 juil. 2016 à 14:59, Mikhail Mandrykin <mandrykin@ispras.ru> a écrit :

> Hello,
> 
> On среда, 6 июля 2016 г. 11:54:28 MSK Gerd Stolpmann wrote:
>> Am Mittwoch, den 06.07.2016, 10:44 +0200 schrieb Jocelyn Sérot:
>>> Hi Nicolas,
> 
>> Your design might work when you change Product:
>> 
>> module Product (S1: T) (S2: T)
>>  (P : T with type elt = S1.elt * S2.elt
>>          and type attr = S1.attr * S2.attr)
>> sig
>>  val product: S1.t -> S2.t -> P.t
>> end
>> 
>> i.e. the "real" product module is the argument P, and this functor only
>> defines the product function. This way you can instantiate it for any P.
> 
> It's also possible to explicitly name the anonymous module "struct type t = 
> S1.elt * S2.elt let compare = compare end" e.g. by exposing it in the output 
> signature of Product:
>  module E : Set.OrderedType with type t = S1.elt * S2.elt
>  include T with type elt = E.t and type t = Make(E).t
> instead of 
>  include T with type elt = S1.elt * S2.elt
> in myset.mli (module Product)
> 
> Then if Product implementation is changed appropriately i.e.
>  module E = (struct
>    type t = S1.elt * S2.elt
>    let compare = compare
>  end)
> module R = Make (E)
> 
> instead of
>  module R =
>    Make
>      (struct
>        type t = S1.elt * S2.elt
>        let compare = compare
>      end)
>  include R
> in myset.ml (module Product),
> 
> the anonymous module can be named and shared explicitly:
>  module P = Myset.Product(S1.S)(S2.S)
>  module R =
>    Make
>      (P.E)
>      (struct type t = S1.attr * S2.attr let compare = compare end)
>  include R
> instead of
>  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)
> in myset.ml (module Product)
> 
> The only remaining problem then is missing equality between elt and S.elt in 
> the signature Myseta.T:
> module S: Myset.T --> module S: Myset.T with type elt = elt
> This makes it work with elems = P.product ...
> Then the additional constraint
>              ...
>              and type S.t = Myset.Product(S1.S)(S2.S).t
> in myset.mli
> can be turned into
>  module P : sig module E : Set.OrderedType end
>               ... and type S.t = Myset.Make(P.E).t
> 
> Regards, Mikhail
>> 
>> Gerd
>> 
>>> 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
> 
> 
> -- 
> Mikhail Mandrykin
> Linux Verification Center, ISPRAS
> web: http://linuxtesting.org
> e-mail: mandrykin@ispras.ru