From: Mikhail Mandrykin <mandrykin@ispras.ru>
To: caml-list@inria.fr, Gerd Stolpmann <info@gerd-stolpmann.de>
Cc: "Jocelyn Sérot" <Jocelyn.Serot@univ-bpclermont.fr>
Subject: Re: [Caml-list] Q: functors and "has a" inheritance
Date: Wed, 06 Jul 2016 15:59:34 +0300 [thread overview]
Message-ID: <44481375.r3GYhIioXc@molnar> (raw)
In-Reply-To: <1467798868.25014.8.camel@e130.lan.sumadev.de>
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
next prev parent reply other threads:[~2016-07-06 12:59 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-07-05 15:25 Jocelyn Sérot
2016-07-06 7:49 ` Nicolas Ojeda Bar
2016-07-06 8:44 ` Jocelyn Sérot
2016-07-06 9:54 ` Gerd Stolpmann
2016-07-06 12:59 ` Mikhail Mandrykin [this message]
2016-07-06 13:35 ` Jocelyn Sérot
2016-07-06 10:15 ` Petter Urkedal
2016-07-06 12:29 ` Jocelyn Sérot
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=44481375.r3GYhIioXc@molnar \
--to=mandrykin@ispras.ru \
--cc=Jocelyn.Serot@univ-bpclermont.fr \
--cc=caml-list@inria.fr \
--cc=info@gerd-stolpmann.de \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).