Le 6 juil. 2016 à 14:59, Mikhail Mandrykin 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 >>> >>> 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 >>>> >>>> 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