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

[Markus Mottl <markus.mottl@gmail.com>]

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