Dot notation problem for functions and a suggested improvement

[kmill]

Dot notation for functions does not behave in an expected way when there are type families. For example, if we define a dependent Function.swap function, we might expect (or at least want) that f.swap would be the function f with swapped arguments. However, due to the way the elaborator selects which argument to use when resolving field notation, it is impossible to use field notation here since it will use f for the implicit type family argument. For example:

def Function.swap {α β} {γ : α → β → Sort _} (f : (a : α) → (b : β) → γ a b)
  (b : β) (a : α) : γ a b := f a b

def mul : Nat → Nat → Nat := (· * ·)
#check Function.swap mul -- works
#check mul.swap -- error since this elaborates to `Function.swap (γ := mul)`

This would not be an issue if Lean 4 only selected an explicit argument when resolving field notation like in Lean 3. However, the Lean 4 method that ignores whether an argument is explicit is an improvement upon Lean 3 since it unifies the behavior of true projections and extended fields.

To be able to use field notation for definitions such as Function.swap there needs to be some way to tell the elaborator which argument to use when resolving field notation.

Here is a simple-to-implement suggestion: if a declaration has an argument named self then that will be used for the argument when resolving dot notation. It should be an error when resolving field notation if a declaration has more than one self argument. Otherwise, if there is no self argument, the current argument selection procedure is used.

It would open up some further possibilities if when field notation is being elaborated using a self argument that we do not do the usual check that the type of that argument is a match for the generalized structure. This would be useful for mathlib in that we can create additional definitions and lemmas as "extension methods" using the export mechanism:

class HasMem (α : outParam $ Type _) (β : Type _) where
  mem : α → β → Prop

infix:50 " ∈ " => HasMem.mem

def HasMem.nonempty [HasMem α β] (self : β) : Prop :=
∃ x, x ∈ self

def Set (α : Type _) := α → Prop

instance : HasMem α (Set α) where
  mem x s := s x

namespace Set
export HasMem (nonempty)
end Set

variable (s : Set α)
#check s.nonempty -- currently an error

As of a couple weeks ago, Lean 3 has nearly the same field resolution rules as Lean 4, except for the fact that it still only uses explicit arguments. Once it is clear what (if anything) will change about Lean 4's field resolution rules, I will finish the backport to Lean 3 to help with mathport.

[tydeu]

I had a similar RFC that proposed to use self for arguments meant to be with dot notation a while back in this Zulip thread. Unfortunately, it is currently maintainers only, but I think could be moved out of there? The debate there on the naming convention may be helpful in the discussion here.