Haskell-like section notation

Stream: new members

[Kyle Miller]

In Haskell, there is a sometimes-convenient notation for partial application of arguments to binary operators, called a section. For example, (+1) means λ x, x + 1 and (2*) means λ x, 2 * x. Experimentally, Lean has (+1) and (*2) but not the (1+) and (2*) variants. Lean's expression syntax is complicated enough that I'm not surprised it doesn't have sections in general, but is there some place in the documentation that at least describes what is possible here?

[Johan Commelin]

(+) 2 = \lam x, 2 + x and I think (+2) is the other one.

[Kyle Miller]

I forgot to test (+). That's good to know. It's sort of odd that Lean has left sections but no right sections, and I wonder if there is a reason or if it's a bug in the parser (untested due to lack of use?).

[Johan Commelin]

Well, maybe it's just because (+) 2 also works, and isn't soo much longer. Of course it's slightly confusing that the meaning depends a lot on whether the ) is between the + and 2 or after it.
But moving parentheses is known to have devastating effects in all of maths (-;

[Mario Carneiro]

There is a parsing complication involved in making right sections work, so since as Johan said you can do without it, we didn't bother

[Kyle Miller]

Is it the (-1) complication, or something else?

[Mario Carneiro]

Basically, it's easy to tell you are looking at a left section because it starts with an infix operator, but a right section is more complicated because it involves an aborted infix parse

[Mario Carneiro]

it has to do with keeping low lookahead parsing

[Mario Carneiro]

but I don't recall all the details

[Kyle Miller]

I see, that sounds about right. I think Haskell manages having sections by parsing entire expressions as sequences of alternating expressions and operators, only forming the expression tree later (there are other ways, but this allows Haskell to have locally defined operators and precedences). Lean's notation is a lot more flexible than Haskell's mere infix operators, and this trick doesn't seem to apply.

[Kyle Miller]

(deleted)