RFC: Enhancing the extended field notation (dot notation)

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.

Start by reading the proposal and its examples, then review the related RFCs #1629 and #3031 and the linked Zulip discussions. Determine the intended behavior for attributes, namespaces, and self, including the typeclass caveat; the work is done when the agreed dot-notation design is implemented and the example behaves as specified.