## Stream: new members

#### Kyle Miller (Jul 13 2020 at 20:47):

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 (Jul 13 2020 at 20:48):

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

#### Kyle Miller (Jul 13 2020 at 21:00):

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 (Jul 14 2020 at 04:52):

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 (Jul 14 2020 at 08:26):

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 (Jul 14 2020 at 08:39):

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

#### Mario Carneiro (Jul 14 2020 at 08:41):

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 (Jul 14 2020 at 08:41):

it has to do with keeping low lookahead parsing

#### Mario Carneiro (Jul 14 2020 at 08:41):

but I don't recall all the details

#### Kyle Miller (Jul 14 2020 at 08:52):

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 (Jul 14 2020 at 08:53):

(deleted)

Last updated: May 11 2021 at 12:15 UTC