Mantis Bug Tracker
Main | My View | View Issues | Change Log | Roadmap
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005514OCamlOCaml typingpublic2012-02-24 01:562012-09-21 13:20
Reporteryminsky 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version3.12.1 
Target Version4.01.0+devFixed in Version 
Summary0005514: "with module" semantics seem broken
DescriptionI just had a frustrating experience debugging some compiler errors
that came up from the use of "with module", and to me, the current
semantics of "with module" seem broken. I brought this up last year,
and it didn't get much traction, so I thought I would try again.

The short version is:

    Unlike the sharing constraints from "with type", "with module" can
    actually add new structure to the signature it's operating on.
    This is profoundly surprising, and can lead to hard to track down
    errors. It would be less surprising and easier to work with if
    "with module", like "with type", only added sharing constraints.

Now for the long vesion.

Let's build up to the problem. First, we'll define a module signature
S that contains a sub-module M.

    module type S = sig
       module M : sig type t type s end
    end

If I want to create a version of S that exposes more information about
the types , I can do so by adding a sharing constraint, as follows:

    module type S' = S with type M.t = int and type M.s = string

And if you do that in the top-level, you will see the following
definition for S':

    module type S' = sig
       module M : sig type t = int
                      type s = string
                  end
    end

which is exactly what you would expect. Now this is where "let
module" comes in. "let module" lets you expose all of the type
equalities in M at once, by exposing the equalities of all the types
in one module with the types in another module N. So, we can do this:

    module N = struct type t = int
                      type s = string
               end

    module type S'' = S with module M = N

And again, you get what you expect. The signature of S'' is:

    module type S'' = sig
       module M : sig type t = int
                      type s = string
                  end
    end

The bad case is where your module M has some extra structure in it.
So, if you write:

    module N = struct type t = int
                      type s = string
                      let x = 3
               end

    module type S''' = S with module M = N

Now, however, you'll discover that S''' is actually this interface:

    module type S''' = sig
       module M : sig type t = int
                      type s = string
                      val x : int
                  end
    end

Meaning, rather than just adding some sharing constraints, we've
actually destructively modified the signature S!

It's worth noting that the OCaml manual gives no hint of the current
behavior. Here's what it says in section 6.10.4:

   and S with module M = N denotes the signature

           sig type t module M: (sig type u=N.u end) end
TagsNo tags attached.
Attached Files

- Relationships
related to 0005460assignedgarrigue Request: Replace/rename/remove module types 

-  Notes
(0006967)
gasche (developer)
2012-02-24 22:48

 I agree that the current behavior is not coherent with the manual description, which explicitly says that `with module` is a precisely shorthand for equating all the type components of the module, and do not mention adding value components.

I'd argue, however, that the implemented behavior is natural and desirable. With the "with type" construct, it is possible to enrich a type, from an abstract type to an explicitly defined type; the constraint being that the signature resulting from "with type" is weaker (less general) than the original one. It seems natural that "with module" allow to transform a module type into any richer module type, so that the result signature is weaker than the original one.

I can see use cases for this feature: for example if you have a signature requesting that some module component K be an OrderedType, and you apply `with module K = String`, I would expect modules in the resulting signature to have the whole String module available (rather than only `with type K.t = string`).

In fact, I'm not sure in which case you would want the behavior you're depicting; I feel it could be argued that the documentation should be corrected to match the behavior, rather than the other way around. What are your use cases for this feature, for which the current behavior is wrong and frustrating?
(0006968)
yminsky (reporter)
2012-02-24 23:53
edited on: 2012-02-25 19:17

 A few points:

a) I've put below a code snippet that outlines the real-world use-case that most recently caused me to stub my toe.
b) The behavior indicated in the docs would have worked well in this use-case
c) The behavior indicated in the docs lines up nicely with SML, where Stephen Weeks assures me he's used it a lot and found it very helpful.
d) I know of no use case that requires the current semantics (though I'm happy to be informed otherwise! Your example seems plausible on the face of it, but I haven't seen it in practice so I'm unsure. Have you found this to be useful in real code?)

Here's the use-case I hit:


(* A simple interface, that we're going to use as an argument to a functor *)
module type LITTLE = sig
  type t
end

(* Note that Big matches Little, but it has some more elements (hence, the name "Big") *)
module Big = struct
  type t = int
  let x = 0
end

(* We want to build modules of this type *)
module type CONTAINS_LITTLE = sig
  module Little : LITTLE
  (* in reality, we would have some other stuff here that used Little *)
end

(* Here's a functor for making a CONTAINS_LITTLE, using a LITTLE as the argument *)
module Make (Arg : LITTLE) : CONTAINS_LITTLE with module Little = Arg = struct
  module Little = Arg
end

(* But now, this fails, because the "with module" expands Little to Big, and Make doesn't
   (and can't) keep all the features of Big that are not in LITTLE. *)
module Z : (CONTAINS_LITTLE with module Little = Big)
  = Make(Big)

(* This version, however, does work. *)
module Z : (CONTAINS_LITTLE with type Little.t = Big.t)
  = Make(Big)
(0006970)
yminsky (reporter)
2012-02-25 19:30

 After some further reflection, I realized that my actual use-case is better served by "with module M := N". Here's a rewrite of the code above, with a few extra fields to make it a tad more realistic.

(* A simple interface, that we're going to use as an argument to a functor *)
module type LITTLE = sig
  type t
  val z : t
end

(* Note that Big matches Little, but it has some more elements (hence, the name "Big") *)
module Big = struct
  type t = int
  let z = 0
  type u = string
end

(* We want to build modules of this type *)
module type CONTAINS_LITTLE = sig
  module Little : LITTLE
    (* in reality, we would have some other stuff here that used Little *)
  val z : Little.t * Little.t
end


(* Here's a functor for making a CONTAINS_LITTLE, using a LITTLE as the argument *)
module Make (Arg : LITTLE) : CONTAINS_LITTLE with module Little := Arg = struct
  module Little = Arg
  let z = (Little.z, Little.z)
end

(* But now, this fails, because the "with module" expands Little to Big, and Make doesn't
   (and can't) keep all the features of Big that are not in LITTLE. *)
module Z : (CONTAINS_LITTLE with module Little := Big)
  = Make(Big)
(0006972)
yminsky (reporter)
2012-02-27 17:24

 Playing around with the above some more, I've found that it's sometimes the right thing, but that I also sometimes just want the type equalities. So I'm still interested in the change as originally proposed.
(0007016)
garrigue (manager)
2012-03-07 08:25

 I think we should do something about this one.
Yaron is right that the manual only talks about type components,
so that the current implementation doesn't meet that specification.

Moreover, the argument that "with type" instantiates type components does not apply here: it would apply to an hypothetical "with module type" (cf. PR#5460), but not to "with module".
In ocaml, all module signatures are opaque, and making the signature of K transparent seems incoherent to me.
(This might be a useful behavior, but not a natural one for ocaml).

So I propose modifying the implementation to fit the specification, as Yaron asked.
Note that the behaviour of "with module M :=" would be unchanged.
(0007018)
gasche (developer)
2012-03-07 10:03

 Indeed, I missed the difference between "with module" and "with module type". In signatures, modules are only used to access their type components; so "with module" is most useful to express sharing of type components, as the manual describes.

I don't know if your "I propose" was meant to receive an acknowledgment -- you're the one going to implement this anyway -- but I now think that's the right way to go. It would be even nicer indeed if "with module type" could be included as well.
(0007051)
xleroy (administrator)
2012-03-12 18:46

 I'm nervous about such a big change in the interpretation of "with module": how much existing code is this going to break? Clearly, some experiments are in order (using e.g. GODI or odb or Debian's packages as a test suite) before we commit on the change.
(0007193)
protz (manager)
2012-03-27 11:15

 Disclaimer: hack follows.

You can restrict the inclusion of M by using the empty-recursive module trick.

First,

module rec X: S = X

This allows us to speak about M through X.M (writing S.M gives an error, since there's no module named S, just a signature).

Then,

module N': (module type of X.M) = N

This is N restricted to the elements that are found in M.

Finally,

module type S'' = S with module M = N'

seems to do what you want.

Everyone here is probably aware of this trick, but I just wanted to mention that the behavior you wish for is already possible, using some hackery, indeed :).

- Issue History
Date Modified Username Field Change
2012-02-24 01:56 yminsky New Issue
2012-02-24 22:48 gasche Note Added: 0006967
2012-02-24 23:53 yminsky Note Added: 0006968
2012-02-24 23:54 yminsky Note Edited: 0006968 View Revisions
2012-02-25 19:17 yminsky Note Edited: 0006968 View Revisions
2012-02-25 19:30 yminsky Note Added: 0006970
2012-02-27 17:24 yminsky Note Added: 0006972
2012-03-07 08:25 garrigue Note Added: 0007016
2012-03-07 08:26 garrigue Relationship added related to 0005460
2012-03-07 10:03 gasche Note Added: 0007018
2012-03-12 18:46 xleroy Note Added: 0007051
2012-03-26 15:17 lefessan Status new => acknowledged
2012-03-27 11:15 protz Note Added: 0007193
2012-07-10 11:39 doligez Target Version => 4.01.0+dev
2012-07-31 13:36 doligez Target Version 4.01.0+dev => 4.00.1+dev
2012-09-21 12:45 doligez Target Version 4.00.1+dev => 4.01.0+dev

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker