0005241: [module type of] does not produce type equalities for representation types

Notes
(0005852) garrigue (manager) 2011-03-28 03:41	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...

(0005853) lealanko (reporter) 2011-03-28 12:58	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.

(0005854) garrigue (manager) 2011-03-28 15:46	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...

(0005855) lealanko (reporter) 2011-03-28 16:37	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.

(0008116) doligez (manager) 2012-09-19 15:08	So this is really a feature request (and a big one): that .mli files bind module type names like .ml files bind module names.

(0008259) lealanko (reporter) 2012-10-15 21:19	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.

Issue History
Date Modified	Username	Field	Change
2011-03-24 23:17	lealanko	New Issue
2011-03-28 03:41	garrigue	Note Added: 0005852
2011-03-28 12:58	lealanko	Note Added: 0005853
2011-03-28 15:46	garrigue	Note Added: 0005854
2011-03-28 16:37	lealanko	Note Added: 0005855
2011-05-16 16:48	doligez	Status	new => acknowledged
2012-07-10 15:18	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-19 15:08	doligez	Note Added: 0008116
2012-09-19 15:08	doligez	Severity	minor => feature
2012-09-19 15:08	doligez	Target Version	4.00.1+dev =>
2012-10-15 21:19	lealanko	Note Added: 0008259

Relationships