f x y+1

Stream: general

[Jukka Suomela]

Hi all, is there some good way to avoid this footgun (other than being careful):

f x y+1

The intention was of course to write f x (y+1), while this gets parsed as (f x y)+1, and if everything is Nat, this compiles fine and does something very different from what was the intention. Can I somehow get e.g. a lint for stuff like this?

[Ruben Van de Velde]

I don't think we have that at this point, though I'm not sure about "of course"

[Jukka Suomela]

I guess I'd write spaces around + like f x y + 1 if I ment (f x y) + 1? Or do Lean users actually write f x y+1 intentionally?

[Jukka Suomela]

(Sorry I'm very new, and confused about lots of things, including how one is expected to format Lean 4 code.)

[Ruben Van de Velde]

Lots of users, so probably someone's written that to mean what it means now

[Ruben Van de Velde]

I'd probably write the spaces as well, personally

[Kevin Buzzard]

I wrestled with this for a while when I came to Lean. The rule is that functions are greedy, they will eat the next thing they see if they want an input. More precisely the binding power of a function is something like 1024, whereas the binding power of things like addition is something like 50, so the function wins easily. This isn't really something we're going to be able to lint for, this is just some basic principle of functional programming which as a mathematician I'd never seen before but soon got used to.

[Kevin Buzzard]

Note that y+1 is bad style, we always put spaces y + 1, and of course you can't hope that writing y+1 magically means "put brackets around this thing", that's not how computers work I guess.

[Jukka Suomela]

I wonder if there could be a lint at least saying it's bad style? :)

[Jukka Suomela]

A human being that changes f x y+1 to f x y + 1 as a result of a lint warning might also much more easily spot the bug…

[Joachim Breitner]

Kevin Buzzard said:

Note that y+1 is bad style, we always put spaces y + 1, and of course you can't hope that writing y+1 magically means "put brackets around this thing", that's not how computers work I guess.

Well, I've been dreaming about a language that works that way for a while, and others have built languages that do. But most don't, lean doesn't, and probably for the better :-)

[Edward van de Meent]

TIL Terence Tao isn't the only one with a blog on this zulip

[Trebor Huang]

This is the same syntax in Haskell so maybe folks there have some suggestions.

[Martin Dvořák]

I sometimes write f x y.succ so that I don't have to write the parentheses.
Writing f x y+1 to express f x y + 1 is abomination.

[Martin Dvořák]

BTW this is the reason why reading AlphaProof's output is so painful for me.

[Martin Dvořák]

That said, it would be really difficult to lint against it.
To make matters worse, I can imagine writing f x (y+1) without spaces (basically any time y is not a natural number) and not wanting any complains that + should have spaces around it.

[Martin Dvořák]

Edward van de Meent said:

TIL Terence Tao isn't the only one with a blog on this zulip

Did you think we were all NPCs except for him?

[Joachim Breitner]

Do you mean NBC (Non-blogging characters)?

[Edward van de Meent]

Martin Dvořák
not at all. Am i an NPC because i don't have a blog?

[Jukka Suomela]

@Martin Dvořák E.g. Python has some code style recommendations (PEP 8) basically saying that e.g. a + b*c + d is OK and a + b * c + d is of course also OK but stuff like a+b * c+d is bad. That is, if you omit spaces, you can't do it in places in which spacing "goes against precedence". Your example would be similar. But I tried to find a Python linter that implements exactly this recommendation correctly, and failed. :)

[Martin Dvořák]

Jukka Suomela said:

Martin Dvořák E.g. Python has some code style recommendations (PEP 8) basically saying that e.g. a + b*c + d is OK and a + b * c + d is of course also OK but stuff like a+b * c+d is bad.

This is exactly aligned with my philosophy.

However, writing such a linter for Lean would be even more difficult than for Python.

[Jon Eugster]

There is a linter by @Damiano Testa with a "pedantic linter" / "pp-roundtrip-linter" which seems to be somewhat what's asked here: lint anything which is pretty-printed differently than it was written.

I think it's activated by

set_option linter.ppRoundtrip true

[Martin Dvořák]

Does it trigger on things that get pretty-printed incorrectly?

[Jon Eugster]

I think it compares the pretty-printed code with what's written originally and marks any difference. Kinda a first iteration of a tool like python's PEP-8.

But yes, there are false-positives where the pretty-printing is not correct yet. One reason it is off by default

[Damiano Testa]

I'm late to this, but what Jon said is almost exactly what the linter does: it compares the string that has been typed, with the output of pretty-printing it, allowing some slack for where to place paragraph breaks. Besides that, it will flag any difference. The output should not be taken too seriously, but does flag some common mistakes (as well as flagging things that it should not flag).