RFC: Enhancing the extended field notation (dot notation)

[FR-vdash-bot]

Proposal

There have been several RFCs about the enhancement of dot notation. (#1629, #3031) This RFC suggests using attributes to specify the namespace of the function used by dot notation, and using self (suggested in #1629) to specify arguments. (Note: If the function is a field of a type class, the self name will not work because the typeclass parameter takes up that name. This method might need to be improved.) For example:

class A (α : Type _) where
  a : α → Nat

structure B where
  b : Nat

instance : A B := ⟨B.b⟩

attribute [dot_namespace A] B

def A.get {α : Type _} [A α] (self : α) : Nat := a self

variable (b : B)

#check b.get -- Wanted `A.get b`, still pretty print as `b.get`

This helps a lot with the use of typeclass APIs in Mathlib. For example, it makes it easier to use APIs in the FunLike and SetLike hierarchies, and easier to migrate from specialized APIs to general APIs based on type classes.

The approach proposed in this RFC is closer to current mechanisms than previous RFCs, thus it is easier to implement and maintain and less likely to produce unintended results.

Community Feedback

Previous RFCs and related discussions: #1629 #3031 Zulip Zulip Zulip Zulip

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.

[kmill]

#6267 implements a version of this RFC, paired with the already merged #6189, but the effect is not exactly the same. It has a mechanism where you use export paired with a dotParam-annotated argument. A limitation of is that you don't get to use everything from another namespace, only the names that you export.

Potentially we could also add a mechanism like what's proposed in this issue — a way to export entire namespaces for dot notation purposes — but I'd appreciate feedback with motivating examples.