## Stream: general

### Topic: notation for partially applied terms

#### Floris van Doorn (Aug 25 2020 at 05:36):

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 (Aug 25 2020 at 05:37):

: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 (Aug 25 2020 at 05:37):

: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 (Aug 25 2020 at 05:37):

: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 (Aug 25 2020 at 05:40):

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

#### Mario Carneiro (Aug 25 2020 at 06:54):

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 (Aug 25 2020 at 08:25):

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 (Aug 25 2020 at 08:43):

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

#### Mario Carneiro (Aug 25 2020 at 08:45):

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 (Aug 25 2020 at 09:24):

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 (Aug 25 2020 at 09:25):

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 (Aug 25 2020 at 09:31):

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 (Aug 25 2020 at 09:31):

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 (Aug 25 2020 at 17:33):

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 (Aug 25 2020 at 18:12):

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 (Feb 22 2021 at 16:15):

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 (Feb 22 2021 at 16:19):

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

Last updated: Dec 20 2023 at 11:08 UTC