Should we remove/deprecate λ?

Stream: lean4

[François G. Dorais]

Does it make sense to keep λ as a hard-coded alternative to fun? I'm not sure about the answer to this question. There's good reasons for both sides. The main ones seem to be this:

• On the keep side, I mostly think of historical reasons. Primarily Alonzo Church, who originated the λ-calculus. Also, Lean historically supported λ since Lean 2 (possibly even Lean 1?).

• On the ditch side, λ is used for a lot of other things outside the λ-calculus. Also, fun is just fun to write and not worse than typing λ. Additionally, λ is a perfectly normal Greek letter so why shouldn't it be allowable as an identifier?

Aside: Why aren't Cyrillic letters allowed in identifiers?

[Eric Wieser]

Also, fun is just fun to write and not worse than typing λ

For whatever reason we didn't believe this in Lean 3, where fun x, x was also valid syntax

[François G. Dorais]

@Eric Wieser I love the misquotation!

[Kevin Buzzard]

I would love to reclaim lambda as the canonical element of the field k like in the maths texts for vector spaces

[Eric Wieser]

But we'd never use it because in mathlib almost all such elements actually belong to a ring R!

[François G. Dorais]

This is really distant memory but I think maybe fun was an addition to Lean 3 and Lean 2 only accepted λ? I'm probably making that up since Lean 2 is so far away...

PS: I do still have unported Lean 2 code on my hard drive... lol! It's beyond fixing now...

[Mario Carneiro]

I think that λ is not so friendly to mathematical uses. It's type theory jargon. Also λ x => e looks worse to me than λ x, e as a logician, while fun x => e looks more stylistically consistent. (The same thing applies with \mapsto in place of =>, IMO)

[Evante Garza]

I think it's also used for arbitrary limit ordinals.

[Henrik Böving]

I do like the idea of getting rid off duplicate syntax in general, for example with inductive we have to my knowledge 3 variants: inductive Foo := inductive Foo where and inductive Foo

[Max Nowak 🐉]

I’m guessing there is a reason why we can’t just have x => 1+x, so no lambda or fun at all?

[Kevin Buzzard]

In maths this is the notation we use (with mapsto)

[Mario Carneiro]

we have discussed it before, maybe someone can find the thread

[Mario Carneiro]

it seems likely that such a notation wouldn't be able to take multiple binders

[Max Nowak 🐉]

If we can write multiple Pi binders as (a b : Nat) -> …, it would be consistent if you could write multiple lambda binders as (a b) => ….

[Mario Carneiro]

I mean multiple actual binders

[Mario Carneiro]

like (a : Nat) (b : Int) |-> ...

[Eric Wieser]

But we could allow (a : Nat) => (b : Int) => ...

[Eric Wieser]

Sure, mathematicians probably wouldn't write that on paper, bur nor would they write (a : Nat) -> (b : Int) -> ...

[Max Nowak 🐉]

Most of the time you skip the types on lambda binders anyway.

[Jireh Loreaux]

I actually prefer fun for (human) clarity of parsing anyway.

[Mac Malone]

Mario Carneiro said:

it seems likely that such a notation wouldn't be able to take multiple binders

However, we could still have the shorthand x => y for single explicit binder lambdas (like JS has), which would be nice for a lot of common use cases.

[Mac Malone]

After all, the syntax is just term " => " term (since patterns in Lean 4 generalize to term)
EDIT: Using funBinder also doesn't break things (however, it does change what an {x} binder means)

[Mac Malone]

Here is a quick example:

macro:arg b:term:max " => " x:term : term => `(fun $b => $x)

#eval [0, 1, 2].map x => 2*x + 1 -- [1, 3, 5]
#eval [0, 1, 2].map (x : Nat) => 2*x + 1 -- [1, 3, 5]
#eval [(0, 1), (2, 3)].map (a, b) => a + b -- [1, 5]

structure Box (α) where a : α
#eval [Box.mk 0, .mk 1].map {a} => 2*a + 1 -- [1, 3]
#eval [Box.mk 0, .mk 1].map (.mk x) => 2*x + 1 -- [1, 3]

[François G. Dorais]

I'm wary of having ... => ... as a shortcut for fun ... => ..., with or without limitations. This is for similar reasons I tend to prefer fun over λ: somebody somewhere probably has another legitimate use for => and using it as part of the core language may make that use impossible even as local or scoped notation. Then again, the same can be said about ×, ⬝, ⊕, so it's not exactly clear where to draw a line.

[Mac Malone]

François G. Dorais said:

somebody somewhere probably has another legitimate use for => and using it as part of the core language may make that use impossible even as local or scoped notation. Then again, the same can be said about ×, ⬝, ⊕, so it's not exactly clear where to draw a line.

Yeah, I think Lean 4 already consumes enough notation that I think alternative schemes are not worth considering. Furthermore, if an end-user really wants it, they can also override Lean 4 builtin notation with higher priority syntax.

[Mac Malone]

Also, in mathlib, which uses ↦ for => instead, such a shorthand can be freely added without conflicting with other possible uses of =>.

[Shreyas Srinivas]

François G. Dorais said:

I'm wary of having ... => ... as a shortcut for fun ... => ..., with or without limitations. This is for similar reasons I tend to prefer fun over λ: somebody somewhere probably has another legitimate use for => and using it as part of the core language may make that use impossible even as local or scoped notation. Then again, the same can be said about ×, ⬝, ⊕, so it's not exactly clear where to draw a line.

It is used as notation for key-value pairs in hashmaps in some programming languages.

[Shreyas Srinivas]

Inside lean, it is used in match arms

[Shreyas Srinivas]

What would the right priority be for this notation?

[Mac Malone]

Shreyas Srinivas said:

What would the right priority for this notation?

Which notation? If you mean the shorthand, arg (just like fun).

[Mac Malone]

Oh, wait, arg is precedence, not priority. I would just give it the default priority, it does not actually conflict with any other builtin Lean 4 notation.

[Mac Malone]

(Match arms are not in term.)

[Shreyas Srinivas]

This one : ... => ...

[Mac Malone]

Oh, upon further testing, I guess it does conflict with match arms because the LHS of an arm can be a term which can, with this shorthand, include =>.

[Mac Malone]

In that case, the notation needs to be something other than => (e.g. ↦ or some ascii art like |-> which Mario was using).

[Mac Malone]

So, better example:

macro:arg b:term:max " ↦ " x:term : term => `(fun $b => $x)

#eval [0, 1, 2].map x ↦ 2*x + 1 -- [1, 3, 5]
#eval [0, 1, 2].map (x : Nat) ↦ 2*x + 1 -- [1, 3, 5]
#eval [(0, 1), (2, 3)].map (a, b) ↦ a + b -- [1, 5]

structure Box (α) where a : α
#eval [Box.mk 0, .mk 1].map {a} ↦ 2*a + 1 -- [1, 3]
#eval [Box.mk 0, .mk 1].map (.mk x) ↦ 2*x + 1 -- [1, 3]

def foo : Option Nat → Nat
| .some x => x -- still works
| .none => 0

[Shreyas Srinivas]

Mac said:

In that case, the notation needs to be something other than => (e.g. ↦ or some ascii art like |-> which Mario was using).

In the examples, my mind keeps seeing map x together followed by the arrow and then the expression. it feels very unintuitive.

[Mac Malone]

Fair, I see that for the basic map x sometimes too. One could put the expression in parentheses to disambiguate if they so desire:

#eval [0, 1, 2].map (x ↦ 2*x + 1) -- [1, 3, 5]

[Mac Malone]

I definitely do not see that for the more complex matches, though. For example, (a, b) ↦ a + b is very naturally a function for me (as it parallels JS function syntax).

[Shreyas Srinivas]

Mac said:

I definitely do not see that for the more complex matches, though. For example, (a, b) ↦ a + b is very naturally a function for me (as it parallels JS function syntax).

is (a, b) a tuple or two args?

[Mac Malone]

Due to currying both are essentially equivalent! :laughing:

[Mac Malone]

(The answer to your question is a tuple for the Lean example and two arguments in JS.)

[Shreyas Srinivas]

Mac said:

Due to currying both are essentially equivalent! :laughing:

in the underlying LC yes. but we do have distinct tuple types with fst and snd operations.

[Mac Malone]

@Shreyas Srinivas True, hence the "essentially" and the laughter. :wink:

[Max Nowak 🐉]

Hence why I was suggesting simply using spaces to separate multiple args.

[Mac Malone]

@Shreyas Srinivas I'm not sure what you mean by that?

[Shreyas Srinivas]

Mac said:

Shreyas Srinivas I'm not sure what you mean by that?

I was too tired to get your joke (end of day). After you clarified, I got it and laughed( bonus: I was also eating curry at that time)

[Shreyas Srinivas]

Max Nowak 🐺 said:

Hence why I was suggesting simply using spaces to separate multiple args.

I don't understand

[Shreyas Srinivas]

Specifically, I don't see how space between args changes readability, when the issue is that intuitively map seems to be getting applied to x in the first example.

[Max Nowak 🐉]

I just meant that (a, b) => … would take a tuple, while (a b) => … would take two parameters.

[Max Nowak 🐉]

But I’m honestly not sure if that’s a good idea.

[James Gallicchio]

the (\. + 1) syntax works well for me for short/quick lambdas, don't really feel the need for e.g. (x => x+1)

[Shreyas Srinivas]

Max Nowak 🐺 said:

I just meant that (a, b) => … would take a tuple, while (a b) => … would take two parameters.

It would be very confusing as far as lean syntax goes since we usually don't have brackets for function parameters unless we are indicating two parameters of the same type. So this would be a third type of syntax people need to watch out for, for something as simple as defining a lambda, because in other places, this kind of bracket notation, especially without a type annotation, could be a function application. I don't know if having multiple gotchas for basic syntax is such a good idea.

I honestly don't understand the point of any of this. What problem does this shorthand solve? Writing fun just requires typing 3 characters, enormously simplifies reading (and vacuously, implementation effort, since it is already implemented), and doesn't use up notation that might come in handy elsewhere as François points out. If at all necessary a shorthand could be introduced locally, couldn't it?

[François G. Dorais]

@Shreyas Srinivas Maybe there shoudn't be such a shortcut? (See my earlier post.) Then again, it's a nice problem to work out: extending => this way without breaking stuff. But maybe that's a bit off topic? I think so... but I would still enjoy seeing the outcome... elsewhere?

[Shreyas Srinivas]

François G. Dorais said:

Shreyas Srinivas Maybe there shoudn't be such a shortcut? (See my earlier post.)

I agree with this. As always, I am just worried about making syntax changes at such a basic level with so many ambiguities, and not being able to anticipate all the chaos this could cause downstream.

Then again, it's a nice problem to work out: extending => this way without breaking stuff. But maybe that's a bit off topic? I think so... but I would still enjoy seeing the outcome.

This will be interesting as a conversation on experimenting with new syntax. In that spirit it would be nice to see where it goes. But I can also imagine that any solution to this will be very brittle.

[Mario Carneiro]

Shreyas Srinivas said:

It would be very confusing as far as lean syntax goes since we usually don't have brackets for function parameters unless we are indicating two parameters of the same type. So this would be a third type of syntax people need to watch out for, for something as simple as defining a lambda, because in other places, this kind of bracket notation, especially without a type annotation, could be a function application. I don't know if having multiple gotchas for basic syntax is such a good idea.

This is not really true:

def f1 (x y) := x = () ∧ y = 1
def f2 (x y : _) := x = () ∧ y = 1
#check fun (x y) => x = () ∧ y = 1
#check fun (x y : _) => x = () ∧ y = 1
#check ∀ (x y), x = () ∧ y = 1
#check ∀ (x y : _), x = () ∧ y = 1

all of which are demonstrating two variables of different types declared in the same binder

[Shreyas Srinivas]

Mario Carneiro said:

Shreyas Srinivas said:

It would be very confusing as far as lean syntax goes since we usually don't have brackets for function parameters unless we are indicating two parameters of the same type. So this would be a third type of syntax people need to watch out for, for something as simple as defining a lambda, because in other places, this kind of bracket notation, especially without a type annotation, could be a function application. I don't know if having multiple gotchas for basic syntax is such a good idea.

This is not really true:

def f1 (x y) := x = () ∧ y = 1
def f2 (x y : _) := x = () ∧ y = 1
#check fun (x y) => x = () ∧ y = 1
#check fun (x y : _) => x = () ∧ y = 1
#check ∀ (x y), x = () ∧ y = 1
#check ∀ (x y : _), x = () ∧ y = 1

all of which are demonstrating two variables of different types declared in the same binder

In each of these cases in #check, it is clear that you are declaring a function or a universally quantified prop. Because of fun and forall.

[Shreyas Srinivas]

Oh, I see, you mean the first sentence of my message.

[Shreyas Srinivas]

What I mean is, that from an end user's perspective, I have not seen these forms very frequently (hence "usually")

[Mario Carneiro]

It wouldn't be inconsistent with the rest of the grammar though. The type of each binder is elaborated separately. Here's another example:

#check ∀ (x y : List _), x = [()] ∧ y = [1]

[Mario Carneiro]

FWIW, metamath uses something close to the unadorned syntax: $(x \in A\mapsto e)$ is what we would write as fun x : A ↦ e

[Shreyas Srinivas]

Mario Carneiro said:

It wouldn't be inconsistent with the rest of the grammar though. The type of each binder is elaborated separately. Here's another example:

#check ∀ (x y : List _), x = [()] ∧ y = [1]

With explicit brackets required?

[Mario Carneiro]

#check ∀ x y : List _, x = [()] ∧ y = [1] works too

[Shreyas Srinivas]

To avoid issues like this : :point_down:
Shreyas Srinivas said:

In the examples, my mind keeps seeing map x together followed by the arrow and then the expression. it feels very unintuitive.

[Mario Carneiro]

I'm not defending the unadorned syntax here, I think it would be somewhat ambiguous for reasons already mentioned

[Mario Carneiro]

unless you have something like metamath's required parentheses around the mapsto

[Mario Carneiro]

which IMO wouldn't fit very well with lean's general design aesthetic

[James Gallicchio]

(though the simple lambda syntax does require parentheses around it heh)

[Mac Malone]

Shreyas Srinivas said:

Mac said:

Shreyas Srinivas I'm not sure what you mean by that?

I was too tired to get your joke (end of day). After you clarified, I got it and laughed( bonus: I was also eating curry at that time)

Ha. I was apparently also distracted as meant to ask that question about Max's response, not yours (I mistakenly thought his was yours). However, you ended up asking the same question anyway. :rofl:

[Martin Dvořák]

Are we making a strategic decision about what syntax will be in the official release of Lean 4?

[Kevin Buzzard]

I should think that Leo has no interest in changing anything, so probably not.

[Eric Wieser]

This topic seems to have diverged to alternative syntaxes, from the original topic of removing/deprecating λ

[Eric Wieser]

Should we deprecate it / lint against it in Mathlib? Or at least recommend one spelling over the other in the style guide?

[Jireh Loreaux]

I did recommend one over the other in the style guide :wink: but I would be happy if we deprecate or lint against it.

[Eric Wieser]

(cc @Yaël Dillies, who asked whether we had actually recorded the decision anyway; it sounds like the answer is now "yes, https://leanprover-community.github.io/contribute/style.html#the-anonymous-function-arrow")

[Yaël Dillies]

I still don't really get why there's any preference at all. λ is nice and concise. fun looks like a declaration name.

[Johan Commelin]

Can we use $\lambda$ to mean a scalar in a field? (E.g., an eigenvalue, etc...)

[Yaël Dillies]

example (λ : ℕ) : λ = λ := rfl -- expected '_' or identifier

[Anatole Dedecker]

In the same vein, did we take a clear decision about <| vs $?

[Ruben Van de Velde]

I thought we moved away from lambda to free it up for identifiers, but perhaps that'd need some core changes

[Pedro Sánchez Terraf]

Mario Carneiro said:

I think that λ is not so friendly to mathematical uses. It's type theory jargon. Also λ x => e looks worse to me than λ x, e as a logician, while fun x => e looks more stylistically consistent. (The same thing applies with \mapsto in place of =>, IMO)

I think this is on spot; I think many people would rather have λ available as an identifier.
By the way, I like ↦over => for this particular use.

[Martin Dvořák]

The switch from λ x, e to fun x => e is my least favorite syntactic change from Lean 3 to Lean 4.
And, to add another unpopular opinion, I prefer => over ↦ because the latter looks almost like → visually.

[Martin Dvořák]

I should note that, before I found Lean, I used to write λ x. e as a notation for functions on paper, hence the Lean 3 version was much closer to what I was used to (than the the Lean 4 version is).

[Scott Morrison]

:bicycle: :painting:

[Martin Dvořák]

Did you mean :bike: :house: ?

[Scott Morrison]

Sure. I couldn't find a shed emoji, but remembered the original story was about choosing what colour to paint the said shed ...

[Jireh Loreaux]

@Anatole Dedecker yes, but the stance is only unofficial in the style guide: we make mention of <| but do not mention $. You should prefer the former over the latter for parallelism with |>.

[Eric Wieser]

I think it would be fine to just declare $ as against mathlib style (possibly even via a linter); having two spellings for exactly the same thing just means more things to teach beginners, and that it's harder to read lean code when switching from one file to another

[James Gallicchio]

and of course the symmetry with |> and <| makes it immediately better in my eyes :)

[Patrick Massot]

It's really too bad <| is so long.

[James Gallicchio]

\<| is one character wide if you prefer :p

[James Gallicchio]

oh, that doesn't work. what's the shortcut for the unicode version??

[Patrick Massot]

I don't think there is a unicode version. However many fonts will make a ligature there.

[James Gallicchio]

got it :)

[Yaël Dillies]

|> is really unnatural imo and I never use <| so the symmetry argument doesn't hold.

[Yaël Dillies]

I also do not get which way around you're supposed to read the symbols so I'd end up mixing them up.

[Yaël Dillies]

And it's more ASCII art, of course.

[Anatole Dedecker]

It's in reverse: <| is the equivalent of $. |> is great because it works fine with dot notation: you can do foo x |>.bar y |>.baz instead of ((foo x).bar y).baz, with potential line breaks just before |>.

[Yaël Dillies]

Ahah, point made :smile:

[Anatole Dedecker]

I agree that none of this is "intuitive", but it's at least not worse than $

[Jireh Loreaux]

I'm not sure if this is the intended meaning, but I view it like a shell pipe | with an arrow saying which side is being piped into which other side, but that's just my own personal mnemonic that I didn't realize I had until just now.

[Anatole Dedecker]

Wait is that not the intended meaning?

[Jireh Loreaux]

I don't know, i just realized that's how I thought of it and I wasn't sure if that was the common or intended meaning.

[Kevin Buzzard]

I'm like Yael, I never know which way to point, I often just guess :-)

[Kyle Miller]

@Jireh Loreaux I think that's the intended mnemonic. In F# I've seen sequences of the |> operator be called pipelines. (I guess F# also has fun things like f <|| p for f p.1 p.2.)

(My own personal mnemonic I didn't realize I had is that <| is sort of like a little cliff face, so in f <| x you have x at a higher elevation, and everything to the right of <| is grouped together into the same plateau.)

[Eric Rodriguez]

for me I quite like the idea of it acting like a funnel and "funneling" everything together

[Thomas Murrills]

For me f <| g x looks like it feeds the argument g x into f. Or that we’re zooming into f’s argument spot, kind of like a magnification callout bubble.

As someone who never had to get used to $, it looks somewhat busy and letterlike to me—I can tell at a glance how symbols are grouped in f <| g x (the spacing helps too: g x becomes a visual unit apart from f) but not f $ g x (“wait, is one of those not a letter?”). Then again, I am using a font which makes <| a clean triangle. I think I’d still prefer <| for looking clearer to me than $ if I weren’t, but maybe not as much.

[Sebastien Gouezel]

To remember which is which, I use that (the first symbol of) <|and ( are curved in the same direction so they correspond to each other, while |> and ) are curved in the same direction so they correspond to each other.

[James Gallicchio]

it's definitely encouraging that there are so many reasonable ways to remember them. maybe we PR these to the docstrings!