Aliasing a functor application in a module interface?

Learning
,
1

I keep trying to write things like this in module interfaces

module Var : Map.OrderedType
module VarSet = Map.Make(Var)
(*                      ^
  Syntax error: 'end' expected *)

This is rejected, it appears that module Foo = Bar is only allowed when Bar does not contain module applications (see the manual: Type-level module aliases). Instead I have to write the following, which is accepted and seems to do what I want (but I’m sure sometimes it doesn’t for a subtle reason):

module Var : Map.OrderedType
module VarSet : module type of Map.Make(Var)

Question: why can’t we just write the module alias?
(I guess I should know, but I forgot long ago.)

(cc @garrigue, @lpw25, @Drup)

P.S.: Is this something that “transparent module ascriptions” are supposed to help for? (I thought they were required to mention a functor argument inside an alias, not to alias functor applications.)

2 Likes
2

I’m sure you must have a good reason, but out of curiosity, could you not do module VarSet : Map.S with type key = Var.t?

3

See this PR and associated discussion

4

Good question! Problems with Map.S with type key = Var.t include the following:

  • It’s more work than = Map.Make(Var) (which I have to use in the implementation anyway), I have to find the S and the key
  • Some functors don’t give an explicit name to their output signature (module F (M : sig .. end) : sig .. end = struct ..end), and then there is no S to refer to.
  • Some modules signatures export many types, and submodules, and it’s a lot of work to come up with the right with type ... = ... constraints.
  • This approach creates maintenance work: if tomorrow Map.S gets a new abstract type, I need to go back and add a new with type = ... constraint. Coupling was introduced by depending on the details of the signature.
3 Likes
5

Thanks @lpw25 for the excellent pointer. What I understand from your post in the thread is that the main blocker is the fact that module aliases are currently used in -no-alias-deps mode, they are only present at type-checking time and not present as runtime in the module data. Morally, this breaks for functor applications which need to be computed somewhere.

(If we hadn’t coupled module-aliases with “weak dependencies” as a poor human’s namespacing system, we wouldn’t have any problem with functor applications at all, if I understand correctly.)

If we want to have the option to have “erased (absent) aliases” and “present aliases”, without a syntax for the user to explicitly make the distinction, we need to figure out how to decide which alias goes in which category, in a way that has nice properties – in particular, is stable by substitution/reduction when a functor application can be simplified away to a specific module.

1 Like