RFC: dotParam widget for controlling dot notation

[kmill]

Summary

Add a dotParam identity function (like optParam, etc.) that is used to mark which parameter is used for dot notation. If there is a dotParam-annotated parameter, then dot notation uses this parameter, rather than using the current type-matching rule.

Reference implementation: #6267

Motivation

In #6189, we now have the ability to export functions into a namespace for the purpose of dot notation. However, this still has a limitation: one of the main applications to exporting functions is to be able to use generic functions for dot notation.

For example, Mathlib has API for SetLike and FunLike. Currently, it's only possible to use such API using normal function application notation, but it would be convenient to be able to use it via dot notation. Having dotParam would allow such API to be exported into relevant namespaces. This eliminates code duplication.

A similar application would be graph theory in Mathlib. Having dotParam would make it possible to use a generic typeclass-based formulation of the adjacency relation, to preserve being able to write G.Adj v w rather than Adj G v w. This genericity is useful because there are many kinds of graph types for different applications, and we want to be able to re-use API between all these graph types.

Given RFC #6394 export, then dotParam becomes even more useful, because that RFC allows for exporting full namespaces into other namespaces, rather than single definitions.

Guide-level explanation

When resolving generalized field notation (a.k.a. "dot notation") x.f, first we compute the type of x. Suppose it is of the form S a b c for some constant S. In that case, we resolve that the function for dot notation is S.f. Let the parameters for the type of S.f have types p_1, ..., p_n.

1. If any of these p_i are of the form dotParam _, then that parameter is used for x. Otherwise,
2. If any of these p_i is of the form S .., then than parameter is used for x. Otherwise,
3. If there is a CoeFun instance for S.f applied to n arguments, then we apply the instance and try resolution again. Otherwise,
4. We try unfolding the type of x and try resolution again.

Drawbacks

• This adds additional complications to the language, and users will have to pepper declarations with dotParam.
• There is the complication that dotParam applies before applying CoeFun instances. The consequence is that there is a chance that the type-based rule for dot notation resolution could apply before applying the CoeFun instance, even if the CoeFun instance would enable the dotParam-based resolution.

Rationale

• There was a suggestion to use an attribute instead of dotParam. Attributes mean that dot notation resolution can't be resolved using only the type of the declaration. For example, attributes would prevent being able to control dot notation in conjunction with CoeFun.
• We could also consider using the first explicit argument if the type-based method failed. This would avoid the drawback of needing to pepper libraries with dotParam, but we think dotParam is more flexible. Using dotParam also avoids needing to compute which parameter is relevant (which takes some number of isDefEqs).
• We could use a name-based system, like only using self for generalized field notation, but we think that this would be a negative because this would be pressure against using well-chosen parameter names.
• We already have experience with optParam, autoParam, optParam, and semiOptParam. Because of this, we likely won't have any issues with dotParam-annotated params in metaprograms or tactic.s

Unresolved questions and future possibilities

We might consider changing the rule for dot notation to look only at explicit arguments. Currently it looks at all arguments to make structure field notation work similarly to generalized field notation, but structure field notation always applies to the self parameter. Usually self is the first explicit parameter, with the exception of classes. If we consider class fields to be special cases, then we may consider first explicit arguments to be a sort of default for generalized field notation. We could say "if the name was exported, then use the first explicit argument" instead.

Community feedback

#1629 suggested using self-named parameters, but there was an argument that this would put negative pressure on libraries to name parameters the generic self rather than something usefully named. Johan Commelin suggested using an attribute-based system. This author suggested dotParam.

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.