Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"with module" semantics seem broken #5514

Closed
vicuna opened this issue Feb 24, 2012 · 22 comments
Closed

"with module" semantics seem broken #5514

vicuna opened this issue Feb 24, 2012 · 22 comments

Comments

@vicuna
Copy link

vicuna commented Feb 24, 2012

Original bug ID: 5514
Reporter: yminsky
Status: acknowledged (set by @lefessan on 2012-03-26T13:17:55Z)
Resolution: open
Priority: high
Severity: feature
Version: 3.12.1
Target version: later
Category: typing
Has duplicate: #6140 #7337
Related to: #5460 #6365
Monitored by: @gasche nlinger mehdi cfalls @jberdine "Julien Signoles" @hcarty @garrigue

Bug description

I 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
@vicuna
Copy link
Author

vicuna commented Feb 24, 2012

Comment author: @gasche

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?

@vicuna
Copy link
Author

vicuna commented Feb 24, 2012

Comment author: yminsky

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)

@vicuna
Copy link
Author

vicuna commented Feb 25, 2012

Comment author: yminsky

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)

@vicuna
Copy link
Author

vicuna commented Feb 27, 2012

Comment author: yminsky

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.

@vicuna
Copy link
Author

vicuna commented Mar 7, 2012

Comment author: @garrigue

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. #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.

@vicuna
Copy link
Author

vicuna commented Mar 7, 2012

Comment author: @gasche

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.

@vicuna
Copy link
Author

vicuna commented Mar 12, 2012

Comment author: @xavierleroy

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.

@vicuna
Copy link
Author

vicuna commented Mar 27, 2012

Comment author: @protz

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 :).

@vicuna
Copy link
Author

vicuna commented Apr 9, 2014

Comment author: @garrigue

Maybe we could now try to fix this one (after 4.02 ?), and check with opam that it's ok.

Am I correct that the right behavior would be obtained by replacing
Sig_module(id, newmd, rs) :: rem
by
Sig_module(id, Mtype.strengthen_decl env md path, rs)

I.e., that it suffices to check that the rhs is a subtype of the expected signature, and then strengthen the expected signature using the provide path ?

@vicuna
Copy link
Author

vicuna commented Apr 9, 2014

Comment author: @lpw25

Note that an alternative to this solution (weakening with module) is to change how functors work with aliases (strengthening functors). If aliases were strengthened by functors then Yaron's code would work fine.

I think that the most sensible meaning for S with module M = N is to add module M = N into S which, thanks to module aliases, is now possible.

In another thread Jacques mentioned that this is not entirely backwards compatible because opening a module returned by a functor would add additional things into the environment, however I think this could be easily detected and warned about.

I also think with module M : S and with module type S = T should be supported as well.

@vicuna
Copy link
Author

vicuna commented Apr 9, 2014

Comment author: @garrigue

By the way, I used the version with Mtype.strengthen_decl in place of using the rhs, and could compile without problem both Coq and Core/Async (didn't check Frama-C).
The point is that it is doing what the manual claims is the meaning.

Leo: yes, I know that another semantics is possible, and I have written several papers with Keiko Nakata on that subject. But, this is a wholly different approach, which changes how one understands functors.
Such a change could only occur if we were to include the whole thing, including the new typing of recursive modules, but this means rewriting a large part of the module code. Compare this with changing one line to go back to the official semantics.
By the way, what do you mean by "with module M : S" ? Replacing the signature of M by S ?

@vicuna
Copy link
Author

vicuna commented Apr 13, 2014

Comment author: @lpw25

By the way, what do you mean by "with module M : S" ? Replacing the signature of M by S ?

Yes

@vicuna
Copy link
Author

vicuna commented Aug 6, 2016

Comment author: @paurkedal

Could we also have a with-constraint which works like currently documented? How about S with type N = M to add type equations for coinciding types, leaving the rest of N unaffected?

In any case, I think it would be good if the documentation is updated; I was about to open an documentation issue when I discovered this one.

@vicuna
Copy link
Author

vicuna commented Aug 30, 2016

Comment author: furuse

I have doubly reported this at #7337

Section 6.10.4 of the document should be more detailed.

@vicuna
Copy link
Author

vicuna commented Mar 14, 2017

Comment author: @garrigue

Requalifying as feature, as this would change the implemented semantics, and probably break some programs.

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 15, 2020
@garrigue
Copy link
Contributor

We need to do something. Either fix or document.

@Drup
Copy link
Contributor

Drup commented May 21, 2020

At this point, it's pretty clear we want to keep the semantics of with module (where extra fields are inserted). The alternative semantics such as with module M : S might come naturally with transparent ascriptions.

@lpw25
Copy link
Contributor

lpw25 commented May 21, 2020

it's pretty clear we want to keep the semantics of with module

I would say that we want to strengthen the semantics, so that it adds a module alias.

Your actual point still stands though: transparent ascriptions give a better way to get the weaker signatures if you want them, so we don't need to weaken the semantics of with module.

@github-actions github-actions bot removed the Stale label Jun 24, 2020
@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label Jul 21, 2021
@trefis trefis removed the Stale label Jul 21, 2021
@yminsky
Copy link

yminsky commented Jul 25, 2021

Seems like this should stay open until the behavior is changed, or the documentation is fixed, as @garrigue said.

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

6 participants