Simplify the typing of module aliases

[vicuna]

Original bug ID: 6063
Reporter: @garrigue
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:27:39Z)
Resolution: fixed
Priority: normal
Severity: feature
Version: 4.02.0+dev
Fixed in version: 4.02.0+dev
Category: typing
Related to: #4166
Monitored by: pcouderc @gasche @ygrek @hcarty @yakobowski

Bug description

Currently, constructs such as

module M = A.B.C

or

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.

[vicuna]

Comment author: @garrigue

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

[vicuna]

Comment author: @lpw25

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

[vicuna]

Comment author: @garrigue

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.

[vicuna]

Comment author: @lpw25

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
SMap.is_empty sm

and will avoid the current runtime cost of local module aliases:

http://janestreet.github.io/ocaml-perf-notes.html#local-module-definitions-are-not-free

If so, then I agree that a local "open .. as .." statement is unnecessary. As you say, things are more complicated for normal modules.

[vicuna]

Comment author: @garrigue

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.

[vicuna]

Comment author: @alainfrisch

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

[vicuna]

Comment author: @garrigue

Merged the module-alias branch to trunk at revision 14394.
You need to use the -trans-mod option to enjoy relaxed dependencies for cmis and compiled units.

[vicuna]

Comment author: @garrigue

The name of the option is now -no-alias-deps, rather than -trans-mod, which was rather cryptic.
Basically it allows you use to alias units (file modules) without registering a dependency of them.
It is even OK if the file is not there, but you get a warning 49 in that case.

Note that one part of the description is not done yet: allowing a restricted for of let module in classes.
Have to think what would be the best restriction. It might be something related to Mtypes.contains_type: allow anything that does not generate new types.