* [Caml-list] "with module" surprises
@ 2011-05-09 14:27 Yaron Minsky
2011-05-09 15:12 ` Markus Mottl
0 siblings, 1 reply; 6+ messages in thread
From: Yaron Minsky @ 2011-05-09 14:27 UTC (permalink / raw)
To: caml-list
I've gotten bitten recently by the semantics of "with module", and after
getting an explanation about how this seems to work in OCaml, I'm now
deeply confused. Here's the example I was shown:
module M = struct
let x = 13
end
module type S = sig
module M' : sig end
end
with module M' = M
The inferred types for this will be:
module M : sig val x : int end
module type S = sig module M' : sig val x : int end end
Whereas I would have expected this:
module M : sig val x : int end
module type S = sig module M' : sig end end
In other words, the "with module" constraint has added new structure to
the signature S, rather than just adding constraints. This strikes me
as deeply strange, and indeed, has caused a bunch of head-scratching
here when using "with module". Is this a bug? Or is this really the
desired semantics. My understanding is that in SML, "with module"
simply adds in a bunch of type-level sharing constraints. From that
point of view, this behavior is pretty surprising.
Not only that, it's what the OCaml manual says. From section 6.10.4
The constraint [module module-path = extended-module-path] adds type
equations to all type components of the sub-structure denoted by
[module-path], making them equivalent to the corresponding type
components of the structure denoted by [extended-module-path].
y
--
Yaron Minsky
^ permalink raw reply [flat|nested] 6+ messages in thread* Re: [Caml-list] "with module" surprises 2011-05-09 14:27 [Caml-list] "with module" surprises Yaron Minsky @ 2011-05-09 15:12 ` Markus Mottl 2011-05-09 16:26 ` Yaron Minsky 0 siblings, 1 reply; 6+ messages in thread From: Markus Mottl @ 2011-05-09 15:12 UTC (permalink / raw) To: Yaron Minsky; +Cc: caml-list The current semantics seems to make sense to me. E.g. module type M' = sig type t end specifies that M' needs a type t. It doesn't say that a module matching this signature needs to keep t abstract. You can hence specialize this signature using "with" to e.g. require that it be an "int". Module constraints work similarly. If a signature is empty, this doesn't mean that a module matching it must not contain anything, rather the opposite: any module can match it. You can again specialize the signature using "with" to require further entries. The module passed to "with" only needs to match the first signature, which is trivially true in this case. Its own (possibly inferred) signature will then specialize the previous signature, potentially adding more entries. A maybe more intuitive way to think about this is following: in OCaml you can only make things more strict, never less strict. An empty signature is less strict (can be matched by more modules) than a non-empty one. Hence extending it is the right "direction". Markus On Mon, May 9, 2011 at 10:27, Yaron Minsky <yminsky@janestreet.com> wrote: > I've gotten bitten recently by the semantics of "with module", and after > getting an explanation about how this seems to work in OCaml, I'm now > deeply confused. Here's the example I was shown: > > module M = struct > let x = 13 > end > > module type S = sig > module M' : sig end > end > with module M' = M > > The inferred types for this will be: > > module M : sig val x : int end > module type S = sig module M' : sig val x : int end end > > Whereas I would have expected this: > > module M : sig val x : int end > module type S = sig module M' : sig end end > > In other words, the "with module" constraint has added new structure to > the signature S, rather than just adding constraints. This strikes me > as deeply strange, and indeed, has caused a bunch of head-scratching > here when using "with module". Is this a bug? Or is this really the > desired semantics. My understanding is that in SML, "with module" > simply adds in a bunch of type-level sharing constraints. From that > point of view, this behavior is pretty surprising. > > Not only that, it's what the OCaml manual says. From section 6.10.4 > > The constraint [module module-path = extended-module-path] adds type > equations to all type components of the sub-structure denoted by > [module-path], making them equivalent to the corresponding type > components of the structure denoted by [extended-module-path]. > > y > > -- > Yaron Minsky > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] "with module" surprises 2011-05-09 15:12 ` Markus Mottl @ 2011-05-09 16:26 ` Yaron Minsky 2011-05-09 17:21 ` Markus Mottl 0 siblings, 1 reply; 6+ messages in thread From: Yaron Minsky @ 2011-05-09 16:26 UTC (permalink / raw) To: Markus Mottl; +Cc: caml-list [-- Attachment #1: Type: text/plain, Size: 3826 bytes --] I agree that specializing modules is a reasonable thing to do in general. But that's not what I think the "with" syntax is usually for. It's usually for adding sharing constraints, and this kind of modification of a module is not the same thing as adding a constraint. Note that the following code fails, as I think it should: module type S' = sig end with type t = int Do you by any chance have a use-case that you think benefits from these semantics? y On Mon, May 9, 2011 at 11:12 AM, Markus Mottl <markus.mottl@gmail.com>wrote: > The current semantics seems to make sense to me. E.g. > > module type M' = sig type t end > > specifies that M' needs a type t. It doesn't say that a module > matching this signature needs to keep t abstract. You can hence > specialize this signature using "with" to e.g. require that it be an > "int". > > Module constraints work similarly. If a signature is empty, this > doesn't mean that a module matching it must not contain anything, > rather the opposite: any module can match it. You can again > specialize the signature using "with" to require further entries. The > module passed to "with" only needs to match the first signature, which > is trivially true in this case. Its own (possibly inferred) signature > will then specialize the previous signature, potentially adding more > entries. > > A maybe more intuitive way to think about this is following: in OCaml > you can only make things more strict, never less strict. An empty > signature is less strict (can be matched by more modules) than a > non-empty one. Hence extending it is the right "direction". > > Markus > > On Mon, May 9, 2011 at 10:27, Yaron Minsky <yminsky@janestreet.com> wrote: > > I've gotten bitten recently by the semantics of "with module", and after > > getting an explanation about how this seems to work in OCaml, I'm now > > deeply confused. Here's the example I was shown: > > > > module M = struct > > let x = 13 > > end > > > > module type S = sig > > module M' : sig end > > end > > with module M' = M > > > > The inferred types for this will be: > > > > module M : sig val x : int end > > module type S = sig module M' : sig val x : int end end > > > > Whereas I would have expected this: > > > > module M : sig val x : int end > > module type S = sig module M' : sig end end > > > > In other words, the "with module" constraint has added new structure to > > the signature S, rather than just adding constraints. This strikes me > > as deeply strange, and indeed, has caused a bunch of head-scratching > > here when using "with module". Is this a bug? Or is this really the > > desired semantics. My understanding is that in SML, "with module" > > simply adds in a bunch of type-level sharing constraints. From that > > point of view, this behavior is pretty surprising. > > > > Not only that, it's what the OCaml manual says. From section 6.10.4 > > > > The constraint [module module-path = extended-module-path] adds type > > equations to all type components of the sub-structure denoted by > > [module-path], making them equivalent to the corresponding type > > components of the structure denoted by [extended-module-path]. > > > > y > > > > -- > > Yaron Minsky > > > > -- > > Caml-list mailing list. Subscription management and archives: > > https://sympa-roc.inria.fr/wws/info/caml-list > > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > > Bug reports: http://caml.inria.fr/bin/caml-bugs > > > > > > > > -- > Markus Mottl http://www.ocaml.info markus.mottl@gmail.com > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > [-- Attachment #2: Type: text/html, Size: 5406 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] "with module" surprises 2011-05-09 16:26 ` Yaron Minsky @ 2011-05-09 17:21 ` Markus Mottl 2011-05-09 17:33 ` Andreas Rossberg 0 siblings, 1 reply; 6+ messages in thread From: Markus Mottl @ 2011-05-09 17:21 UTC (permalink / raw) To: yminsky; +Cc: caml-list I think the example you gave correctly fails, because you are trying to specialize a non-existent type rather than augment an existing module signature. The name of the type / signature appearing on the left-hand side of the "with" constraints must exist. A use case for the intended semantics might be reexporting of functor arguments: module Make (Arg : ARG) : S with module Spec = Arg = struct module Spec = Arg ... end It could be bad from a design perspective to lose substructures in "Spec" which were unknown to "S". Markus On Mon, May 9, 2011 at 12:26, Yaron Minsky <yminsky@gmail.com> wrote: > I agree that specializing modules is a reasonable thing to do in general. > But that's not what I think the "with" syntax is usually for. It's usually > for adding sharing constraints, and this kind of modification of a module is > not the same thing as adding a constraint. Note that the following code > fails, as I think it should: > > module type S' = sig end > with type t = int > > Do you by any chance have a use-case that you think benefits from these > semantics? > > y > > On Mon, May 9, 2011 at 11:12 AM, Markus Mottl <markus.mottl@gmail.com> > wrote: >> >> The current semantics seems to make sense to me. E.g. >> >> module type M' = sig type t end >> >> specifies that M' needs a type t. It doesn't say that a module >> matching this signature needs to keep t abstract. You can hence >> specialize this signature using "with" to e.g. require that it be an >> "int". >> >> Module constraints work similarly. If a signature is empty, this >> doesn't mean that a module matching it must not contain anything, >> rather the opposite: any module can match it. You can again >> specialize the signature using "with" to require further entries. The >> module passed to "with" only needs to match the first signature, which >> is trivially true in this case. Its own (possibly inferred) signature >> will then specialize the previous signature, potentially adding more >> entries. >> >> A maybe more intuitive way to think about this is following: in OCaml >> you can only make things more strict, never less strict. An empty >> signature is less strict (can be matched by more modules) than a >> non-empty one. Hence extending it is the right "direction". >> >> Markus >> >> On Mon, May 9, 2011 at 10:27, Yaron Minsky <yminsky@janestreet.com> wrote: >> > I've gotten bitten recently by the semantics of "with module", and after >> > getting an explanation about how this seems to work in OCaml, I'm now >> > deeply confused. Here's the example I was shown: >> > >> > module M = struct >> > let x = 13 >> > end >> > >> > module type S = sig >> > module M' : sig end >> > end >> > with module M' = M >> > >> > The inferred types for this will be: >> > >> > module M : sig val x : int end >> > module type S = sig module M' : sig val x : int end end >> > >> > Whereas I would have expected this: >> > >> > module M : sig val x : int end >> > module type S = sig module M' : sig end end >> > >> > In other words, the "with module" constraint has added new structure to >> > the signature S, rather than just adding constraints. This strikes me >> > as deeply strange, and indeed, has caused a bunch of head-scratching >> > here when using "with module". Is this a bug? Or is this really the >> > desired semantics. My understanding is that in SML, "with module" >> > simply adds in a bunch of type-level sharing constraints. From that >> > point of view, this behavior is pretty surprising. >> > >> > Not only that, it's what the OCaml manual says. From section 6.10.4 >> > >> > The constraint [module module-path = extended-module-path] adds type >> > equations to all type components of the sub-structure denoted by >> > [module-path], making them equivalent to the corresponding type >> > components of the structure denoted by [extended-module-path]. >> > >> > y >> > >> > -- >> > Yaron Minsky >> > >> > -- >> > Caml-list mailing list. Subscription management and archives: >> > https://sympa-roc.inria.fr/wws/info/caml-list >> > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> > Bug reports: http://caml.inria.fr/bin/caml-bugs >> > >> > >> >> >> >> -- >> Markus Mottl http://www.ocaml.info markus.mottl@gmail.com >> >> >> -- >> Caml-list mailing list. Subscription management and archives: >> https://sympa-roc.inria.fr/wws/info/caml-list >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> Bug reports: http://caml.inria.fr/bin/caml-bugs >> > > -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] "with module" surprises 2011-05-09 17:21 ` Markus Mottl @ 2011-05-09 17:33 ` Andreas Rossberg 2011-05-09 18:56 ` Markus Mottl 0 siblings, 1 reply; 6+ messages in thread From: Andreas Rossberg @ 2011-05-09 17:33 UTC (permalink / raw) To: Markus Mottl; +Cc: yminsky, caml-list On May 9, 2011, at 19.21 h, Markus Mottl wrote: > A use case for the intended semantics might be reexporting of > functor arguments: > > module Make (Arg : ARG) : S with module Spec = Arg = struct > module Spec = Arg > ... > end > > It could be bad from a design perspective to lose substructures in > "Spec" which were unknown to "S". If I understand your example correctly, then I don't think it does what you think it does. That is, if you apply Make to some M that is wider than ARG, you still won't have the additional components in F(M).Spec, because M gets narrowed to ARG by the functor application anyway. /Andreas ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] "with module" surprises 2011-05-09 17:33 ` Andreas Rossberg @ 2011-05-09 18:56 ` Markus Mottl 0 siblings, 0 replies; 6+ messages in thread From: Markus Mottl @ 2011-05-09 18:56 UTC (permalink / raw) To: Andreas Rossberg; +Cc: yminsky, caml-list If "S" referred to "ARG" as signature for "Spec", too, then you are right, and that's probably by far the usual case. You could still export anything in "ARG" that's not in the signature for "Spec" imposed by "S". But I agree this example is not nearly as useful as it might seem. Not sure I have ever depended on this feature in actual code. If so, this must be exceedingly rare, but semantically it still seems like the right behavior to me. Markus On Mon, May 9, 2011 at 13:33, Andreas Rossberg <rossberg@mpi-sws.org> wrote: > On May 9, 2011, at 19.21 h, Markus Mottl wrote: >> >> A use case for the intended semantics might be reexporting of functor >> arguments: >> >> module Make (Arg : ARG) : S with module Spec = Arg = struct >> module Spec = Arg >> ... >> end >> >> It could be bad from a design perspective to lose substructures in >> "Spec" which were unknown to "S". > > If I understand your example correctly, then I don't think it does what you > think it does. That is, if you apply Make to some M that is wider than ARG, > you still won't have the additional components in F(M).Spec, because M gets > narrowed to ARG by the functor application anyway. > > /Andreas > > -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2011-05-09 18:56 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2011-05-09 14:27 [Caml-list] "with module" surprises Yaron Minsky 2011-05-09 15:12 ` Markus Mottl 2011-05-09 16:26 ` Yaron Minsky 2011-05-09 17:21 ` Markus Mottl 2011-05-09 17:33 ` Andreas Rossberg 2011-05-09 18:56 ` Markus Mottl
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox