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
Comments
Comment author: @gasche I agree that the current behavior is not coherent with the manual description, which explicitly says that 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 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? |
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. 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) |
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) |
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. |
Comment author: @garrigue I think we should do something about this one. 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". So I propose modifying the implementation to fit the specification, as Yaron asked. |
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. |
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. |
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 :). |
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 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 ? |
Comment author: @lpw25 Note that an alternative to this solution (weakening I think that the most sensible meaning for 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 |
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). 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. |
Comment author: @lpw25
Yes |
Comment author: @paurkedal Could we also have a with-constraint which works like currently documented? How about 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. |
Comment author: furuse I have doubly reported this at #7337 Section 6.10.4 of the document should be more detailed. |
Comment author: @garrigue Requalifying as feature, as this would change the implemented semantics, and probably break some programs. |
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. |
We need to do something. Either fix or document. |
At this point, it's pretty clear we want to keep the semantics of |
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 |
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. |
Seems like this should stay open until the behavior is changed, or the documentation is fixed, as @garrigue said. |
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. |
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:
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.
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:
And if you do that in the top-level, you will see the following
definition for S':
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:
And again, you get what you expect. The signature of S'' is:
The bad case is where your module M has some extra structure in it.
So, if you write:
Now, however, you'll discover that S''' is actually this interface:
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
The text was updated successfully, but these errors were encountered: