Zulip Chat Archive

Stream: new members

Topic: Haskell-like section notation


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 13 2020 at 20:48):

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

view this post on Zulip 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?).

view this post on Zulip 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 (-;

view this post on Zulip 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

view this post on Zulip Kyle Miller (Jul 14 2020 at 08:39):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 14 2020 at 08:41):

it has to do with keeping low lookahead parsing

view this post on Zulip Mario Carneiro (Jul 14 2020 at 08:41):

but I don't recall all the details

view this post on Zulip 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.

view this post on Zulip Kyle Miller (Jul 14 2020 at 08:53):

(deleted)


Last updated: May 11 2021 at 12:15 UTC