notation for partially applied terms

Stream: general

[Floris van Doorn]

There are different ways to write un-applied or partially applied functions that have infix notation:

• (λ x, x + c) is the same as (+ c)
• (λ x y, x + y) is the same as (+)
• (λ y, c + y) is the same as ((+) c)

Same holds for other infix notations: = ≠ * / ≤ < > ≥

So for example for l : list ℕ you can write the expression (l.filter (≠ 1)).foldr (+) 0.

In #3935 I suggested to consistently use the shorter, but more confusing notation.

So here a poll (vote by reacting) (warning: the emote reactions might not be ordered correctly):

[Floris van Doorn]

:one: we should consistently use (λ x, x + c);
:two: we should consistently use (+ c);
:three: the author should decide which one to use.

[Floris van Doorn]

:one: we should consistently use (λ x y, x + y);
:two: we should consistently use (+);
:three: the author should decide which one to use.

[Floris van Doorn]

:one: we should consistently use (λ y, c + y);
:two: we should consistently use ((+) c);
:three: the author should decide which one to use.

[Scott Morrison]

The third poll is the only one I have a strong opinion on.

[Mario Carneiro]

Remark: "(λ x, x + c) is the same as (+ c)" is literally true, in the sense that one is parser notation for the other. For (+) and (+) c, these are partial applications, meaning they are eta-contracted versions of the lambdas, and so some tactics will be able to tell the difference, so they are not exactly substitutable in all contexts.

[Patrick Massot]

I think that having (+ c) and ((+) c meaning two different things is extremely confusing. It's not so bad with a commutative operation, but I guess you also want to use this trick with potential non-commutative multiplication. I really don't want to spend a couple of second of thinking about which one is which each time I see this.

[Mario Carneiro]

I would reserve its use to functional programming stuff. It falls in the same mental category as (+) <$> f <*> g for me

[Mario Carneiro]

But I don't think we should have a particular required style about this either. Let the author decide how to present this for whatever purpose it is put to

[Chris Wong]

Haskell (which I assume this syntax came from) also allows (c +) to mean \lam y, c + y. I don't think ((+) c) is ever preferred there, except in the few cases where it's mandatory.

[Mario Carneiro]

Of course we would prefer to write that, but due to a limitation of lean's parser you can't write left sections

[Chris Wong]

Yep, understood. I guess the point I was trying to make was that ((+) c) might confuse functional programmers as well :stuck_out_tongue:

[Gabriel Ebner]

As the clover begins to bloom, we could look forward and copy its section syntax:

notation `⬝+ ` x := (λ y, y + x)
notation x ` +⬝` := ((+) x)

#check (⬝+1)
#check (1+⬝)

[Floris van Doorn]

I added Gabriel's suggestion as a new option to the poll.
But it seems like the preliminary result is to not change our current approach (too much).

[Patrick Massot]

This suggestion require new notation for each new function, right? That being said, having it for addition and multiplication would already cover a lot of cases.

[Eric Wieser]

Based on the result of this poll, should we be changing the statement of src#comp_mul_left and src#is_left_regular to not use the (*) notation?

[Yakov Pechersky]

The only time the comp_mul come up in my experience (and why I wrote them) was for rewriting of composed foldrs or list.prods