[Caml-list] "with module" surprises

[Caml-list] "with module" surprises

[Yaron Minsky]

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

Re: [Caml-list] "with module" surprises

[Markus Mottl]

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

Re: [Caml-list] "with module" surprises

[Yaron Minsky]

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

Re: [Caml-list] "with module" surprises

[Markus Mottl]

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

Re: [Caml-list] "with module" surprises

[Andreas Rossberg]

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

Re: [Caml-list] "with module" surprises

[Markus Mottl]

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