RFC: Let `export` create namespace aliases

Summary

Extend Lean.aliasExtension to include data for namespace aliases. Modify the export syntax to be able to create namespace aliases, and to add other open-like declarations for hiding names or renaming names.

Motivation

The current export command has a number of limitations:

• It only supports creating single aliases from one name in the namespace hierarchy to another.
• It's not possible to name these aliases.
• Creating an alias to a declaration that's also a namespace doesn't also create aliases for all names in that alias.

Illustrating this third limitation, consider the problem of making an inductive type available from a parent namespace. This works fine to make the type itself available, but one would need to export all the constructors and other functions separately.

namespace NS
inductive T
  | mk
end NS

export NS (T)

#check T -- NS.T
#check T.mk -- error: unknown constant

Another motivation is #6189, which makes dot notation take aliases into account. Given a PR like perhaps #6267, which makes it possible to create generic libraries of functions meant to be used with dot notation, we face a limitation for export. In particular, we anticipate users wanting to design libraries of functions in a generic namespace and then export that namespace into the namespace of the type that wants to use these for dot notation. With the current export, users would need to export individual functions. To make this convenient, there needs to be a way to export the entire namespace, and permanently, in the sense that future additions to the source namespace will appear in the target namespace, even if the additions are made after the export command.

Guide-level explanation

Here is a proposed docstring for the new export command:

Adds aliases into the current namespaces for names from other namespaces.

There are two kinds of aliases:

• Name aliases make a name aDecl refer to another name dDecl.
• Namespace aliases make all names in a namespace ans refer to names in another namespace ns.

The export command be used in a few different ways:

• export NS₁ … NSₙ makes the current namespace be an alias for the namespaces NS₁, …, NSₙ.
  If the current namespace is A and NSᵢ.x exists, then this causes A.x to be an alias for NSᵢ.x.

• export NS hiding def₁ … defₙ makes the current namespace be an alias for the namespace NS
  like in export NS, but none of the NS.defᵢ names are aliased.

• export NS (def₁ … defₙ) creates aliases for the names NS.def₁, …, NS.defₙ in the current namespace.
  If the current namespace is A, then A.defᵢ refers to whatever NS.defᵢ resolves to.

• export NS renaming def₁ → def₁', …, defₙ → defₙ' is like export NS (def₁ … defₙ) but it enables
  naming the aliases; A.defᵢ' refers to whatever NS.defᵢ resolves to.

Aliases make names visible in the current namespace without a prefix (like open).
The only rule for protected declarations is that when resolving an atomic identifier,
only non-protected declarations are considered.

Unlike the open command, the export command does not activate scoped namespaces.

Reference-level explanation

The export command creates aliases, which are like "symbolic links" in the name hierarchy. For example, an export A (x) from within the namespace B produces an alias B.x ~> y, where y is what the name A.x resolves to, and an export A from within the namespace B produces a family of aliases B.* ~> A.*. Alias resolution is recursive, allowing resolution to follow a chain of namespace exports.

Using the above, export A (x) from within B creates an ExportDecl.explicit `B.x `y record in the alias environment extension, and export A from within B creates an ExportDecl.namespace `B `A [] record. The export A hiding a, b, c variant creates an ExportDecl.namespace `B `A [`a, `b`, `c`] record.

Abstract description: "m is an alias for n" is a relation on names.

1. If n₁ is an alias for n₂ and n₂ is an alias for n₃ then n₁ is an alias for n₃.
2. Given an ExportDecl.explicit aDecl dDecl record, then aDecl is an alias for dDecl. Futhermore, if dDecl is a namepace then the rule for ExportDecl.namespace aDecl dDecl [] also applies.
3. Given an ExportDecl.namespace ans ns except record, then for all names m not in except, if m = Name.str m' id, ns ++ m' is a namespace, and ans ++ m is not a private name, then ans ++ m is an alias for ns ++ m.

For a name m, we say "alias m resolves to n" if m maps to n and n is a declaration or a reserved name. The result of resolveAlias m is a list containing every n such that alias m resolves to n.

The difference between the behavior of ExportDecl.explict ans ns and ExportDecl.namespace ans ns [] is that the first one additionally makes ans an alias for ns if ns is a declaration. The second does not — it only causes names appearing inside ns to be aliased inside ans.

The condition that ExportDecl.namespace only resolves names whose prefix is a namespace ensures that we can implement this with a (terminating!) efficient algorithm, since this ensures the problem is equivalent to a graph search on a finite graph. Otherwise for example a namespace alias of A into the root namespace would diverge looking for x, A.x, A.A.x, and so on.

Regarding protected declarations, the rule for aliases during name resolution is that if alias m resolves to n, if m is an atomic name, and if n is protected, then the alias is not used.

Drawbacks

• Namespace aliases are more complicated than simple identifier aliases.
• We will need to extend the AliasState with more indexes to be able to efficiently resolve names, especially in consideration of the fact that name resolution is a core algorithm.
• Name resolution is a core algorithm, and there is risk of disrupting its current behavior.
• This does require fixing downstream projects. For example, Subset in core is an alias for HasSubset.Subset, and this RFC makes it possible to write Subset.trans to refer to HasSubset.Subset.trans. Mathlib was writing Subset.trans to refer to Set.Subset.trans, and so there is an ambiguity that needs resolution.

Rationale

• The current name aliases are weaker than users think they should be. In particular, the fact that name aliases to declarations that are namespaces don't export the namespace too. Covering this use case is almost enough for this entire RFC. However, this leaves the gap of exporting namespaces by themselves, even if they aren't declarations themselves, which is a small overhead to implement as well.
• Ideally aliases are uniquely resolved. There is an issue covering this already (#5258) and implementing this RFC presents no challenge to fixing that issue. The reference-level explanation has a rule that the "is an alias for" relation is transitive, which may seem odd given the ideal of unique resolution. However, we think that it is easier to reason about failures of unique resolution (which could be introduced through the union of exports from multiple imported modules) if the relation is made to be transitive. The alternative would have been that only ExportDecl.namespace ans ns expect includes the transitivity, but the corresponding description is more complicated to write down.
• It's been confusing that export cannot do what open can, with respect to exporting full namespaces or renaming exported names. Giving export the syntax of open (minus the parts about scoped names) eases this.
• We do not address scoped in this RFC. This would be additional complexity, and we do not have any use cases to support the complexity yet.

Given that some parts of name resolution (for example for dot notation) make use of unfolding, another design for namespace aliases could go through abbrev. For example, given

abbrev Foo := Nat

we could add a rule that Foo.zero first tries Foo.zero, which doesn't resolve, then (Foo).zero, which fails because Nat is a Type and there is no dot notation for Type, and then it could try unfolding Foo, seeing it is a constant, and then using the constant as a namespace to resolve zero. We think this rule is harder to explain, and also relying on unfolding like this means name resolution is only possible as a consequence of elaboration, but we want to be able to resolve names themselves. Furthermore, we can emulate this effect with namespace aliases instead:

namespace Foo
export Nat
end Foo

and additionally we can make Foo be an alias for multiple namespaces, giving it the union of all the namespaces' names, which is not possible with this abbrev proposal.

Unresolved questions and future possibilities

As mentioned in Rationale, this RFC does not address scoped. The export command could be used to accumulate namespaces just for the purpose of activating all their scoped attributes. In this RFC we do not specify that doing open on a namespace that's an alias for another namespace should activate that namespace.

Community feedback

A number of considerations in this RFC come from examples brought up in private discussions. The Zulip thread for the RFC was supportive, including a #mathlib4 thread where the Subset.trans issue was brought up.

Reference implementation: #6393.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with Lean.aliasExtension, AliasState, resolveAlias, and the ExportDecl rules described in the RFC, then compare them with reference implementation #6393. Done means export supports namespace aliases, hiding, and renaming with recursive alias resolution while preserving the stated protected and scoped-namespace behavior.