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

[module type of] does not produce type equalities for representation types #5241

Open
vicuna opened this issue Mar 24, 2011 · 11 comments
Open

[module type of] does not produce type equalities for representation types #5241

vicuna opened this issue Mar 24, 2011 · 11 comments

Comments

@vicuna
Copy link

@vicuna vicuna commented Mar 24, 2011

Original bug ID: 5241
Reporter: lealanko
Status: acknowledged (set by @damiendoligez on 2011-05-16T14:48:05Z)
Resolution: open
Priority: normal
Severity: feature
Version: 3.13.0+dev
Category: typing
Monitored by: yziquel dario till "Julien Signoles"

Bug description

The manual says:

"The construction module type of module-expr expands to the module type (signature or functor type) inferred for the module expression module-expr."

Hence, I would expect [module N = M] to be equivalent to [module N : module type of M = M]. However, this is not true:

        Objective Caml version 3.13.0+dev3 (2011-03-07)

# module M = struct type a = Foo end;;
module M : sig type a = Foo end
# module N = M;;
module N : sig type a = M.a = Foo end
# module N : module type of M = M;;
module N : sig type a = Foo end

Because of the lacking type equality, [N.a] is now distinct from [M.a]. This causes a bit of headache. There is a workaround:

        Objective Caml version 3.12.1+dev5 (2010-10-12)

# module M = struct type a = Foo end;;
module M : sig type a = Foo end
# module N : module type of M with type a = M.a = M;;
module N : sig type a = M.a = Foo end

This does not yet work in 3.13 since r10669 apparently hasn't yet been merged to trunk. But still, I don't think this should be needed. [module type of] should give the most specific signature of a module, and for types with representations, that should include a type equation.

@vicuna
Copy link
Author

@vicuna vicuna commented Mar 28, 2011

Comment author: @garrigue

IIRC, this is actually the intended behavior.
The rationale is that you may want to use "module type of" to provide
a different implementation of an existing module.
In that case, you may not want the types to be identical.
As you point out, r10669 solves most of the problem, since it allows
to recover the equations with little code duplication.
It should go in trunk when 3.12.1 is released, but maybe I should merge
it myself before that...

@vicuna
Copy link
Author

@vicuna vicuna commented Mar 28, 2011

Comment author: lealanko

What additional safety does hiding the type equality provide? If the interface defined a polymorphic variant instead of a variant, then the type in an including interface would be equal to the original, and I don't think anyone would consider this a problem.

I am using [include M] to wholly re-export M from a larger module, and I'd like to indicate this in the interface with [include module type of M]. If I have to add equality constraints for all the exported type representations, maintenance becomes more of a hassle as the including module has to track the evolution of the types in M.

@vicuna
Copy link
Author

@vicuna vicuna commented Mar 28, 2011

Comment author: @garrigue

OK, I should have noted that there are two distinct problems.
One is about abstract types. We clearly want to be able to obtain a signature where the abstract types are allowed to be distinct, or this would not allow alternative implementations.
Another one is datatypes. Indeed, if the datatype definition is identical, it might seem ok to add an equation.
But there are still difficulties: what to do if the definition includes references to abstract types for the same module? If we add an equation, we actually require those abstract types to be identical... And while detecting this kind of situation might be possible, I'm afraid the semantics would be too complicated.

A last solution would be to have two "module type of", one with the current semantics, and another adding the equations from the beginning. But I have no idea for the syntax...

@vicuna
Copy link
Author

@vicuna vicuna commented Mar 28, 2011

Comment author: lealanko

The reimplementation use case indeed requires that abstract types are kept abstract.

Still, to me, [module type of M] very much gives the impression that it is the signature of the module M, not just some abstract signature that M happens to implement.

I suspect that very often if we want to reimplement a module Foo, we actually want to implement the signature defined in foo.mli. So here is a feature suggestion that would be even more generally useful:

Let every interface file foo.mli define a module type Foo in the global module type scope. If we also have foo.ml, then we just have Foo : Foo. This should be no problem since modules and module types have different namespaces. Then, if we want to reimplement that interface as MyFoo : Foo, we just write a myFoo.mli whose body is "include Foo".

So [Foo] would be the signature defined in foo.mli, with the types just as abstract or transparent as they are defined in that file, and [module type of Foo] would be the signature of the particular module Foo, with all the type equalities that this implies.

This would be useful also because at times it would be convenient to have a lone foo.mli define a global name for a signature Foo, even if there is no foo.ml.

@vicuna
Copy link
Author

@vicuna vicuna commented Sep 19, 2012

Comment author: @damiendoligez

So this is really a feature request (and a big one): that .mli files bind module type names like .ml files bind module names.

@vicuna
Copy link
Author

@vicuna vicuna commented Oct 15, 2012

Comment author: lealanko

Certainly not! That was simply an offhand suggestion regarding how to best accommodate the "reimplement existing module" use case. The actual problem I am reporting is that because [module type of] currently tries to accommodate this use case, it does not expand to the module type inferred for the module expression, while the documentation claims it does.

@github-actions
Copy link

@github-actions github-actions bot commented May 15, 2020

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
@Drup
Copy link
Contributor

@Drup Drup commented May 21, 2020

@lpw25 Do you still intent to change this ?

@lpw25
Copy link
Contributor

@lpw25 lpw25 commented May 21, 2020

I do. I have written the patch to make module type of Foo produce the type currently produced by module type of struct include Foo in the past, and used that to test the change on Jane Street's code base. My conclusion from that experiment was that the change would be much less painful once other parts of the module system were also strengthened. In particular, aliases of functor parameters and with module.

So, the change is essentially blocked on having transparent module ascription.

@Drup
Copy link
Contributor

@Drup Drup commented May 21, 2020

So, the change is essentially blocked on having transparent module ascription.

Fair enough. :)

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

@github-actions github-actions bot commented Jul 21, 2021

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

4 participants