Open nomeata opened 11 months ago
It would be good to compare this to some other solutions, for example Lean could provide an attribute it applies to auxiliary definitions, and downstream tools could take this into account. Or, Lean could annotate the names in such a way that downstream tools can see these are auxiliary (like perhaps prepending with an underscore, which is a pre-existing way to make it be an "internal" name).
Regarding visibility modifiers, one of the rules of thumb in mathlib is that you never want any definitions to be private
, since there's a good chance you'll want to prove something about the definition eventually. Definitions made with let
are not "private" per se, since their entire definition is embedded in the host definition inside the let
expression. Definitions made with let rec
are hoisted to being top-level definitions so that they can be compiled with the equation compiler. There's also the question of what Lean is supposed to do if you have a private
definition with a public
definition in a where
clause.
There are other bits of syntax that generate auxiliary top-level definitions as well, for example match
expressions. Downstream tools use heuristics to decide whether a top-level definition is auxiliary. For example, Name.isInternal and Docgen's isBlacklisted.
That makes sense, so a should-appear-in-documentation vs. should-not-appear-in-documentation marker, orthogonal to the existing visibility flags, could be useful? Especially if let rec
definitions have the should-not-appear-in-documentation
attribute by default, but allow it to be changed back explicitly. If we want different defaults for normal vs. lifted definitions, this needs to be an attribute known to Core, right?
Proposal
While local
let
declarations are properly private, localwhere
andlet rec
declarations float to top-level definitions (namespaced within the enclosing definiton’s name).To downstream tooling (doc generation, linters), these look like normal public definitions, e.g show up in the module API description. I find this surprising, and would assume them to be an implementation detail of the enclosing function, and not or only hard to get your hands on from the outside.
One possible fix is to treat them always like
private
definitions (as experimented with in #2717). But there seem to be use case where you do want outside access to local definitions (otherwise why would docstrings be supported, and presumably in proofs it might be useful).A more refined fix is to allow the visibility modifiers
public
,private
andprotected
to be used inwhere
andlet rec
, giving the developer control over whether these definitions should or should not be externally visible. Possibly withprivate
being the default.Another direction would be to simply somehow mark these definitions as “lifted from local definitions”, and let the tooling decide what to with it (e.g. the docstring linter could not complain about them; the API documentation could omit them unless there is a docstring).
Community Feedback
Previously briefly discussed on Zulip.
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.