Function dot notation error

Stream: lean4

[Kyle Miller]

Is dot notation on functions supposed to respect which arguments are explicit vs implicit?

In this example, it appears dot notation is inserting the function as the implicit argument:

def Function.foo {f : α → β} (g : β → γ) := g ∘ f
variable (f : α → β) (g : β → γ)
#reduce f.foo
-- fun g x => g (f x)

This is what I was experimenting with until I realized it might be that dot notation is trying to fill in γ in Function.swap:

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
/-
:6:7 application type mismatch
  @Function.swap ?m.151 ?m.152 mul
argument
  mul
has type
  Nat → Nat → Nat : Type
but is expected to have type
  ?m.151 → ?m.152 → Sort ?u.142 : Sort (max (max (?u.142 + 1) ?u.143) ?u.144)
-/
#check (mul.swap 1 2 : Nat)
/-
:17:17 invalid universe level, ?u.264 is not greater than 0

:17:8 application type mismatch
  @Function.swap ?m.239 ?m.240 mul
argument
  mul
has type
  Nat → Nat → Nat : Type
but is expected to have type
  ?m.239 → Nat → Sort ?u.230 : Sort (max (?u.230 + 1) ?u.232)
-/
#check (Function.swap mul : Nat → Nat → Nat) 1 2 -- works
#check (mul.swap : Nat → Nat → Nat) 1 2
/-
:31:8 application type mismatch
  @Function.swap ?m.1489 ?m.1490 mul
argument
  mul
has type
  Nat → Nat → Nat : Type
but is expected to have type
  ?m.1489 → ?m.1490 → Sort ?u.1480 : Sort (max (max (?u.1480 + 1) ?u.1481) ?u.1482)

:31:7 type mismatch
  Function.swap
has type
  ((a : ?m.1489) → (b : ?m.1490) → ?m.1511 a b) →
    (b : ?m.1490) → (a : ?m.1489) → ?m.1511 a b : Sort (imax (imax ?u.1482 ?u.1481 ?u.1480) ?u.1481 ?u.1482 ?u.1480)
but is expected to have type
  Nat → Nat → Nat : Type
-/

[Kyle Miller]

Oh, I didn't realize that Lean 4 has changed how dot notation works from Lean 3 like this. In Lean 3 dot notation looks for the first explicit argument with the right type, but now it allows implicit arguments too. (It looks like Lean 4 started the Lean 3 way but changed in this commit from 2020).

A short example illustrating the difference:

structure S where
  n : Nat

def S.foo {s : S} : Nat := s.n * 2

def s : S := ⟨37⟩

#eval s.foo
/- works, but in Lean 3 would give
invalid field notation, function 'S.foo' does not have explicit argument with type (S ...)
-/

[Kyle Miller]

Here's an example (in addition to Function.swap) that I might have expected to work with dot notation, but the function arguments conflict with the type family arguments:

def Function.pi_comp {β γ : α → Sort _}
  (g : (x : α) → β x → γ x) (f : (x : α) → β x) (x : α) : γ x :=
g x (f x)

theorem forall_imp {p q : α → Prop}
  (h : ∀ a, p a → q a) (h' : ∀ a, p a) : ∀ a, q a :=
h.pi_comp h'
/-
type mismatch
  Function.pi_comp ?m.171
has type
  ((x : ?m.124) → ?m.144 x) → (x : ?m.124) → ?m.145 x : Sort (imax (imax ?u.117 ?u.116) ?u.117 ?u.115)
but is expected to have type
  ∀ (a : α), q a : Prop
-/

[Kevin Buzzard]

I guess I certainly remember thinking more than once "grr, I wish lean 3 would let dot notation work here even though the argument I want to insert is implicit"

[Kyle Miller]

Very brief RFC:

As a first step when inserting arguments for an LVal in addLValArg, the elaborator should look for an argument named self, check that it is the only argument with that name (otherwise raise an error), and then use that argument for the expression for the field notation no matter the baseName.

This (1) allows one to use field notation to work for Function even if there are type family arguments like in the above examples and (2) allows one to use field notation for extension methods that make use of typeclass instances (or coercions) associated to a type.

[Sebastian Ullrich]

Do you have an example for your second use case? The function must still be in the type's namespace for the elaborator to find it.

[Kyle Miller]

@Sebastian Ullrich Yes, I have a number of example applications (this goes back to some posts I had about graphs and getting G.adj u v to work for G having a type that implement a HasAdj class).

Here's an example from a recent mathlib discussion that would be useful, since many different types re-implement a .nonempty predicate in the same way, and we like dot notation in mathlib for nonempty:

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

[Sebastian Ullrich]

I see, it makes sense in combination with export

[Victor Maia]

how do I import a file in the same dir? I'm trying import Base, but it says nat_exp.lean:1:0: error: unknown package 'Base', even though there is a file named Base.lean on the same directory, which type-checks just fine

[Kevin Buzzard]

@Victor Maia if this question is unrelated to the above discussion can you ask it in a new thread?

[Victor Maia]

oops, sorry - I'm new to Zulip

[Kevin Buzzard]

No problem!

[Kyle Miller]

Would it be worth fleshing out the mini-RFC at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Function.20dot.20notation.20error/near/296860982 further? Or is it clear what the problem is and what sorts of applications would be enabled by letting a user specify the argument that field notation applies to?

There are a couple alternative designs to the simplistic one of using an argument named self:

• Use a type annotation for the argument that should receive the object of the field notation.
• Use an attribute to specify the name of the argument that should receive the object of the field notation. (This also makes the feature more opt-in.)

[Leonardo de Moura]

@Kyle Miller Yes, a GitHub issue would be perfect.