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

["Jocelyn Sérot" <Jocelyn.Serot@univ-bpclermont.fr>]

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