Dot notation quirk

Stream: lean4

[Robin Carlier]

structure foo where
  bar : Nat

def baz {f : foo} : foo where
  bar := f.bar.succ

def my_foo : foo := ⟨0⟩

#eval baz (f := my_foo).bar -- 1

I understand the logic of why that works, but allowing this is a little bit confusing imho.

[Edward van de Meent]

Wait what

[Edward van de Meent]

Yea, I feel like that shouldn't be valid syntax

[Yaël Dillies]

I think this is actually really practical because this syntax could mean nothing else and the alternative is lengthy: #eval baz (f := my_foo) |>.baz

[Edward van de Meent]

Adding a mere 3 characters

[Yaël Dillies]

Well, I use it quite a lot

[Robin Carlier]

I see that it can’t mean anything else, but years of programming gets you into the habit of interpreting (...).foo as applying foo to whatever is in the parentheses, not to the parentheses + what’s behind them.

[Edward van de Meent]

Yes, it feels like it should have a higher precedence than function application

[Edward van de Meent]

(and similar notations with unbracketed spaces)

[Kyle Miller]

Please tell me that you're not using this for anything serious @Yaël Dillies

[Yaël Dillies]

Hmm, well, I'm sure I've used it in Toric at some point. I guess that's serious?

[Bhavik Mehta]

Surely the alternative is #eval (baz (f := my_foo)).bar

[Edward van de Meent]

yes, although a downside is you have to go back to place the opening bracket, which is also effort

[Aaron Liu]

Not if you have the foresight to place it first

[Edward van de Meent]

Foresight? What's that :upside_down:

[Yaël Dillies]

Aaron Liu said:

Not if you have the foresight to place it first

Well usually how it happens is that you write a long list of chained dot notation and suddenly you notice there isn't enough type information for the lemma to apply (or possibly the lemma doesn't apply, but Lean won't tell you why until you fill in some metavariables in the proof term), so you go back to your list of chained dot notation and fill in each metavariable one by one using this funky proof (arg := value).next_proof syntax until it works/gives a better error message

[Kyle Miller]

This is clearly unintended syntax -- please don't let this one escape your lab Yaël!

I'm very amused that the rules line up to make such an unlikely thing parse in a useful way.

[Ruben Van de Velde]

I guess we can't call it Dr Dillies's monster yet :innocent:

[Jz Pan]

What about this

structure foo where
  test : Nat
deriving Repr

def foo.bar (f : foo) : foo where
  test := f.test * 2

def baz (f : foo) : foo where
  test := f.test + 1

def my_foo : foo := ⟨0⟩

#eval baz (f := my_foo).bar
#eval baz (my_foo).bar

[Mario Carneiro]

Yeah I've been aware of this issue for a while and always write it as (foo (a := x)).1 even though lean is fine without it. It's similar to the issue with foo ...1 (aka (foo ..).1) which was fixed some time ago. It would be great if the fixes here weren't so fragile (I won't be surprised if in a few weeks we find out foo fun x => by simp.1 parses as foo (fun x => by simp).1 or something)

[Mario Carneiro]

...it does, actually (well, foo fun x => (by simp).1 but close enough) :melt:

[Edward van de Meent]

well that one i kinda get, by simp is "atomic" relative to dot notation since it changes categories...

[Mario Carneiro]

I think the reliable way to fix this is to allow it to parse, and then reject if the argument left of the dot is anything other than an identifier or a grouped expression

[Mario Carneiro]

Edward van de Meent said:

well that one i kinda get, by simp is "atomic" relative to dot notation since it changes categories...

sure one can explain the behavior, but it's not intended behavior, people visually expect spaces to break the meaning and would read it as by (simp.1) which is nonsense

[Mario Carneiro]

if I use something else there like rw then it can get even more confusing

[Edward van de Meent]

yea, fair