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
Behavior of 'module type of' w.r.t. module aliases #6307
Comments
Comment author: @gasche My gut feeling (with a healthy disrespect for what the theory or Instead, I would expect having to write something such as:
Where the S signature re-abstracts over all type and module components I guess my message is that we should let "module type of" be used to I would be in favor of switching (module type) to the strengthened |
Comment author: @alainfrisch
Another fix (which applies also if the submodule contains abstract types and we want to keep a strengthened version): module L1 = struct Actually, rewriting: module X = A to module X = struct include A end seems to be a way to recover the pre-alias semantics in a systematic way (it could be automated by a ppx filter). |
Comment author: @alainfrisch In which use cases would one prefer the current behavior of 'module type of' w.r.t. module aliases? |
Comment author: @garrigue
In the case you want to keep the information that the submodules keep their identity. This said, this may be too restrictive even when you want to use this for an extended implementation, as this means that you cannot reimplement submodules. So I tend to agree with you that 'module type of' should remove module aliases, independently of whether strengthening was a good idea or not. |
Comment author: @garrigue OK, I added a patch that does what you want: it removes aliases in submodules too. However, I need to think a bit more about the soundness aspect. I we additionally have to check for the well-typedness of the signature, this is much more work :( |
Comment author: @alainfrisch Which case do you see of a signature depending on an alias (and which breaks when the alias is expanded)? |
Comment author: @garrigue Here is an example: module F (X : sig end) = struct type t = A end module type S = module type of M The functor G only accepts modules containing the same type t, but in the signature S this is not the case, since F was applied on different modules. So S is invalid, and would be refused if input explicitly. module M' : S = M I'm not yet sure whether this creates problems or not... |
Comment author: @lpw25 Personally, I think that For example, an obvious use for include (module type of Foo) as the interface for a module which had: include Foo in its implementation. In this case it is clear that you want the strengthened version and the module aliases included.
If you want to reimplement submodules then you just need to use: module M : (module type of Foo.M) include (module type of Foo) with module M := M This is probably a good thing as it makes your re-implementation obvious. (An even better way would be to write: include (module type of Foo) with module M : (module type of Foo.M) but for some reason we do not allow |
Comment author: @lpw25
Actually, maybe this doesn't work. I think that I am using "with module" backwards. |
Comment author: @garrigue Indeed, the problem with strengthening by default is that 'with' is only allowed to make a signature more specific, not less. Also, concerning module aliases, it seems that an expected property of 'module type of' is that it should generate a signature with as little dependencies as possible. If we keep aliases, we introduce a dependency. So having a 'module type of' remove module aliases seems a good idea to me.
An additional question is whether to remove aliases inside functors too (the current patch only does it for submodules). |
Comment author: @lpw25
Is this just because currently module aliases are not produced by functors? For example, I think on trunk the following is not allowed: module F (X : S) : sig module M = X end = struct Which means that many current uses of Or is there some other major cause of backwards incompatibility? |
Comment author: @garrigue Well, actually you can add an alias to a signature. module type S1 = sig module M : sig type t end end;; You can also see the strangeness (which is not new) by trying: module type S1' = S1 with module M = M;; Concerning functors, this is completely unrelated. |
Comment author: @lpw25
I think that it actually is safe to allow module aliases of If we consider an example: (* Some arbitrary module types where S can be coerced to T (* A functor expecting U whose result includes a (generative) (* A module of type S *) (* A functor expecting T whose result includes an alias and (* F applied to M *) As you say, it is obviously safe to have sig This means that whilst There are two places where When used directly in a path, this is clearly safe because the When used as the argument to a functor things are more subtle, Note that, in this discussion, when I have written It is possible that I have missed something, but I think this |
Comment author: @lpw25
Does this mean that making In general, I have always thought that the feature: S with module X = Y didn't really make sense. You couldn't write S with module X : T since you are then adding a statement which could actually have been in However, with the arrival of module aliases, this can now make sense: you could indeed have written Indeed, the main criticism in Yaron's bug report was that the behaviour of |
Comment author: @garrigue It took me a long time, but I found an example showing that producing a malformed signature is dangerous in practice. The example is below. (* Counter example *) module M = struct module type S = module type of M module M' : S = M;; module Int2 = struct type t = int let compare x y = compare y x end module type S' = sig module rec M2 : S' = M2;; (* should succeed! (but this is bad) *) let M2.W eq = W Eq;; let s = List.fold_right SInt.add [1;2;3] SInt.empty;; |
Comment author: @lpw25
If you're going to check that a signature is well-formed after an operation then you might as well allow destructive substitution to weaken signatures and then check that the result is well-formed. Then |
Comment author: @garrigue I added a new correct patch. |
Comment author: @garrigue A few answers to Leo:
The approach in my patch is to ensure that the signature is well-formed, by adopting a conservative policy, but I do not check it after hand. This would be more complicated, as the code doing that is mixed with the translation from untyped syntax...
I just showed that you can introduce an alias in a signature if you want to.
We are clearly talking about different problems. let y = 3 With the current semantics, this would print 3. Note that we could also develop a conservative semantics, which would keep both the alias and the restricted signature. I tried, but this is a lot of work, as the two approaches have to be handled in parallel. |
Comment author: @lpw25
Couldn't you apply this conservative policy to destructive substitutions, so that: module M : (module type of Foo.M) include (module type of Foo) with module M := M would allow people to remove the module aliases themselves if they needed to. In general, I think it would be better for
Is opening the only place where a larger signature can cause unexpected errors? If so, then perhaps we could provide a warning in such cases, on by default for the first few versions after the change. |
Comment author: @alainfrisch
Another case with "include" where a larger signature can cause an error: module M = struct type t end;; module N = struct include M type t end module N = struct include (M : sig end) type t end |
Comment author: @lpw25
Or even: module X = struct let x = 3 end;;module X : sig val x : int end let x = 1;;val x : int = 1 module Y = struct include X let y = x end;;module Y : sig val x : int val y : int end Y.y;;
module Y = struct include (X : sig end) let y = x end;;module Y : sig val y : int end Y.y;;
Although, I think these could also be detected and warned about. |
Comment author: @garrigue Fixed in trunk at revision 14451, applying remove_alias_correct.diff. |
Original bug ID: 6307
Reporter: @alainfrisch
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:25:46Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.02.0+dev
Category: typing
Tags: patch
Related to: #6325
Monitored by: @gasche @diml @jmeber "Julien Signoles" @yallop @hcarty
Bug description
The introduction of module aliases can break code which uses 'module type of'. Example:
Previously, the type of F's argument was "sig module X : sig end end", and now it is "sig module X = A1 end", making L2 incompatible with it.
A discussion about what to do started on caml-devel. Here is Jacques' reply to my email:
An easy fix when the submodule contains no abstract types is to add an annotation on module X:
module L1 = struct
module X : module type of A1 = A1
end
I'm not sure of what you mean by your second sentence.
'module type of' does keep type aliases.
The only specific behavior is that it does not strengthen the types, i.e. it does not add aliases to abstract types.
This is not what happens here for the module aliases: the alias comes from the definition in L1, not from module type of.
So this would not just mean not adding aliases, but actively removing them from the signature, recursively.
This said I agree that the choice not to strengthen abstract types had your use case in mind.
Since the problem we see here is again specific to this use case, it could be reasonable to solve it in the same direction.
However, there is also a new problem here: if we do not leave the alias by default, we need a way to reintroduce it.
Currently "(module type of L1) with module X = A1" does not reintroduce an alias.
I suppose it should introduce one, so this is rather a bug.
I'm not sure what is the best solution.
In particular, experience has shown that not strengthening 'module type of' was actually a bad idea.
In at least 95% of cases you want the strengthened version, and doing the strengthening by hand is a pain.
The use case you describe here seems pretty rare, to the point I was even wondering wether we should not revert to the strengthening semantics. But, as rare as it is, you demonstrated that it happens in practice, so maybe we need two versions of 'module type of'.
I suppose it also relates to the expected semantics of 'module type of'.
Is it just something which looks up a module type in the environment,
or is it something more meta-level, which behaves like syntactically copying the module type.
#6305 is an example of that: there the intuition is that 'module type of A' should not introduce a dependency on A, since we do not access any internal part of A, but this would require some specific treatment.
#6305
File attachments
The text was updated successfully, but these errors were encountered: