|Anonymous | Login | Signup for a new account||2013-12-11 09:58 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006063||OCaml||OCaml typing||public||2013-07-04 03:49||2013-07-08 15:18|
|Priority||normal||Severity||feature||Reproducibility||have not tried|
|Target Version||Fixed in Version|
|Summary||0006063: Simplify the typing of module aliases|
|Description||Currently, constructs such as|
module M = A.B.C
let module M = A.B.C in ...
have a high type-checking cost: a new module is created and added to the environment, which requires typing A.B.C and strenghtening; moreover, in the case of let module, one has to ensure that types from M do no escape (i.e. expand them to A.B.C.t).
It would be much simpler to use the same code as for open, just adding aliases to the environment.
As a result there would be no need to check anything, and this construct could be allowed in class definitions for instance. This would change the printing of types in normal mode, but if you use the -short-paths option, you would still get the benefit of abbreviations when printing types.
In theory this is OK to do that even if the type contains applications (but only to paths).
I believe this is 100% backwards compatible, but this may need some check for the case where some .cmi disappears. The behavior of type checking in presence of dangling paths is not completely specified.
|Tags||No tags attached.|
OK, I was maybe a bit too ambitious.
This seems fine for "let module", since it only adds a binding to the environment, but modules in structures also generate fields in the corresponding signature. So if we want to handle them as aliases, we probably need aliases in signatures too.
I.e. would like to write
module M = A.B.C
in the signature too, just like one can write equations in type definitions.
But this is a bit of another story (cf. papers by Keiko Nakata and me...)
edited on: 2013-07-04 16:42
This feature seems fine, but I wonder if it wouldn't be better to provide a proper module alias statement (I have seen "open A.B.C as M" suggested before).
Unlike "module M = A.B.C" it would not add a generate a field in the signature, and unlike "let module M = A.B.C in" it would not have a runtime cost.
I think this is probably what most people want when they write something like "module M = A.B.C" anyway.
This could work with class definitions, so that the example from the caml-list would be:
class z = let open String as A in object end;;
In the case of "let module", you should actually be able to type more programs with this new interpretation of let-module, so this is an improvement, with the same advantages as a special "open" syntax (while being more general), and without the need for new syntax.
I also believe it is better if people can go on with the idioms they are used to.
For normal modules, this is another story.
I believe that a proper treatment of module aliases would actually make applicative functors easier to understand, but this requires some extension to the type system (at least internally).
Maybe this should be considered seriously.
edited on: 2013-07-05 17:05
Just to clarify, are you saying that this proposal will allow the following to type-check:
let f (sm : 'a Map.Make(String).t) =
let module S = String in
let module SMap = Map.Make(S) in
and will avoid the current runtime cost of local module aliases:
If so, then I agree that a local "open .. as .." statement is unnecessary. As you say, things are more complicated for normal modules.
Yes, this is what I mean.
Module aliases introduced by let-module would become completely transparent, and as a result you would get more equalities.
(Actually, the implementation I have in mind just reuses the same machinery as open to add duplicated information to the environment.)
At first I thought that it would apply immediately to paths containing functor applications too.
This would make sense since you can already write code such as:
module M = Set.Make(Set.Make(String))
However, this would require changes, since for the backend paths of values are not supposed to contain functor applications. Letting modules have two paths in the environment (one for typing, and one for compilation) should do the trick.
|Is there a natural formalization of the proposed change, or would the resulting system mimics the implementation (one special rule for the case where the let-bound module is a path)?|
|2013-07-04 03:49||garrigue||New Issue|
|2013-07-04 03:49||garrigue||Status||new => assigned|
|2013-07-04 03:49||garrigue||Assigned To||=> garrigue|
|2013-07-04 09:38||garrigue||Note Added: 0009682|
|2013-07-04 12:45||lpw25||Note Added: 0009689|
|2013-07-04 16:42||lpw25||Note Edited: 0009689||View Revisions|
|2013-07-05 07:38||garrigue||Note Added: 0009697|
|2013-07-05 17:03||lpw25||Note Added: 0009702|
|2013-07-05 17:05||lpw25||Note Edited: 0009702||View Revisions|
|2013-07-06 02:37||garrigue||Note Added: 0009710|
|2013-07-08 15:18||frisch||Note Added: 0009721|
|Copyright © 2000 - 2011 MantisBT Group|