Transparent ascription

[clementblaudeau]

See rendered version of the RFC

I propose to add transparent ascription in the signature language, and do a redesign of the aliasing mechanism. I've included some context, a description of the change, some technical details, and some of the topics that may spark some discussions.

[gasche]

A remark on backward compatibility:

• Dune generates its module-alias-introducing code itself during builds. This means that it can be adapted to a different syntax if we want -- and only use it on compiler versions that support it. This means that the vast majority of module-alias users today pose no backward-compatibility concern.
• But there remains several large-ish projects that use module aliases manually, by writing a mapping file. The standard library is the prime example, but other large projects that have not yet migrated to Dune (for example: Coccinelle) still use manual mapping files. My intuition is that there are enough such projects that we must design a transition story carefully -- as is done in the RFC.

[lpw25]

This all looks great to me. One thing that isn’t made clear in the description is the linking behaviour of explicit static aliases when -no-alias-deps isn’t passed to the compiler. I would argue that the behaviour should be unchanged in that case: explicit static aliases should never force something to be linked.

Then I’d probably go the other way with your “End state for the ambiguous syntax” design decision: we can move people off of -no-alias-deps and onto explicit static aliases over time, but I see no harm in supporting the flag with your proposed transition behaviour indefinitely.

[clementblaudeau]

Thank you for the feedback! I've integrated most comments from Xavier and Gabriel.

I agree that static aliases could also not force linking (when not accessed), and I can update the RFC in that direction if there is consensus. If we go this way, would it make sense to remove the -no-alias-deps flag altogether ? (making un-accessed aliases never linked). Are there situations where users want to force linking ?

Regarding the end state for the ambiguous syntax, I feel that the inference of static/dynamic alias could still be a bit surprising for users, but I have no strong opinion on this.

[diremy]

Regarding the end state for the ambiguous syntax, I feel that the inference of static/dynamic alias could still be a bit surprising for users, but I have no strong opinion on this.

I think the two are different notions for different usage and that the author should say what he wants and the system would check. So I think, in the end, the choice should alway be explicit from the user, either at each definition or using an explicit default.

Of course, I would be happy to be convinced that the implicit use is convenient in some specific scenario is you have such examples.

[gasche]

@lpw25 and @xavierleroy: I'd like to encourage @clementblaudeau to work on an implementation of this RFC (as part of his OCaml Foundation-funded stint on the module system implementation). Does that sound reasonable to you, or do you have further feedback / questions / aspects that should be resolved before moving to a prototype implementation?

[lpw25]

I don’t have any further feedback, and the changes I proposed above are small things that can easily be adjusted after the PR is written.

[xavierleroy]

I had a nice chat with @clementblaudeau and I understand the proposal better. It looks really well thought-out, so let's move to the prototype implementation !

[OlivierNicole]

Thank you for the very clear RFC which I was able to follow despite my relative ignorance of the subtleties of the module system.

You mentioned transparent ascription a while ago in a discussion^1 where lazy module strengthening was also mentioned. It is my understanding that lazy module strengthening is used at Jane Street primarily to improve performance, and may also be a candidate for upstreaming.

I’m wondering, can the same performance gain be obtained with transparent ascription, by making the right implementation choices?

Also, you said:

If transparent ascription is added to the language, the only case I see where lazy strengthening will still be useful is if the user wants a copy of a module that is not also an alias, as in:

module X : T = ...
module X' =  struct include X end 
(* with lazy strengthening : *) module X' : T with X

Does this seem useful enough that we still would want a way to express T with X?

[samsa1]

Just a small comment to add more motivations for this proposal : I would be beneficial for modular implicits because it would help reduce the number of false ambiguities.

I also just happened the other day to write a bunch of modules with almost the same signature (the only difference was only in the type declaration). However currently it seems that you either abstract the type defined inside the module or need to write a whole line : module SInt : Show with type t = int = struct ... end Being able to write directly module M :> Show = struct ... end without loosing type definition seems better in that situation.

[clementblaudeau]

After working on the first step of this proposal, and documenting more aliasing bugs (mostly 13997, but also 13979 and 13897) I've done some slight updates to the RFC. The key change is that, once transparent signatures will be up and running, I propose to restrict static aliasing to persistent modules only (modules that can be accessed from the toplevel):

module X0 = struct end
module X0'  == X0 (* ok, top-level modules are persistent *)
module X0'' == Stdlib.List (* ok, external modules are persistent *)

module M = struct
  module X1 = struct end
  module X1' == X1 (* ok, X is reachable from the toplevel as M.X *)

  module F (Y:sig end) = struct
    module X2 = struct end 
    module X2'  == X2 (* not ok *)
    module X2'' == Y  (* not ok *)
  end
  
  module G () = struct
    module X3 = struct end
    module X3' == X3  (* not ok *)
  end
  
  module type T = sig
    module X4 : sig end 
    module X4' == X4 (* not ok *)
  end
end

Crucially, persistent modules are not affected by substitutions (at functor application, during signature constraints, etc.) and therefore, aliases to them never need to be scrapped (see 13997 for more details). Overall, I would argue that static aliases to non-persistent modules are inherently brittle, and become unjustified in the presence of transparent signatures. Using a transparent signature instead of a static alias only costs an extra field at compile time, which feels acceptable. But maybe I am missing use-cases ? @lpw25 @garrigue