lambda

Stream: mathlib4

[Johan Commelin]

Lean 4 switched to fun instead of lambda as syntax for function expressions. But we still can't use lambda for scalars in a field:

import Mathlib

variable (K : Type) [Field K] (λ : K)
-- unexpected token ')'; expected '_' or identifier

What is needed to make this work?

cc @Kyle Miller

[Ruben Van de Velde]

Switch is a big word when they also still support lambda for that

[Johan Commelin]

Fair enough. I would nevertheless really like to get $\lambda : K$ working.

[Kyle Miller]

Yeah, docs#Lean.Parser.Term.fun still allows lambda. I think there is an old RFCs about expanding the allowed letters in identifiers, and perhaps removing lambda for fun could be part of that?

("Switched" is only eight letters. The biggest near synonyms I could think of would be "approbated" or "acquiesced" :-))

[Julian Berman]

The docs for maxPrec(which lambda in function syntax seems to use) say essentially "we discourage using higher values but that's not disallowed". Does ignoring that recommendation give a way to hack around the syntax? (I.e. can notation:(maxPrec + 1) do a thing which makes lambda either a normal identifier again or else always look for some Field class in the environment)?

[Florent Schaffhauser]

Is there maybe another Unicode character that looks like $\lambda$? Perhaps accessible by typing something like \lambda1? (is what they sometimes do in other programming languages, but probably for very specific and localised purposes)
Edit I really feel that the thumbs-down on an innocuous remark phrased as a question is bordering on abuse. Are you trying to prevent discussion? I am getting more and more afraid of participating in this channel. And I am not even saying something false.

[Kyle Miller]

No @Julian Berman, in docs#Lean.isLetterLike lambda is explicitly carved out.

[Julian Berman]

Flo (Florent Schaffhauser) said:

Is there maybe another Unicode character that looks like $\lambda$? Perhaps accessible by typing something like \lambda1?

(https://graphemica.com/search?q=lambda is what's in unicode -- but that doesn't mean it's a valid identifier character)

[Kyle Miller]

I think you might be able to do some one-off syntax, but people will soon want to write things like λ₁ or λ', which need λ to be available as an identifier start character.

[Kyle Miller]

Plus, that only solves the problem for terms. You'd want these to be usable wherever an ident is expected, like in Johan's use case.

[Johan Commelin]

I think it would be very nice if we could toggle a switch that makes $\lambda$ behave in CS mode or in maths mode :grinning:

[Johan Commelin]

Category theory uses λ_ in some parts of mathlib. But otherwise, λ almost doesn't appear in mathlib.
I'm sure there will be plenty of libraries that would be sad to not have CS mode lambda. But mathlib would be very happy with maths mode lambda.

[Kyle Miller]

Lean 4 already doesn't have Pi notation (in mathlib we have that as our own extension). It seems reasonable to me to continue with greek letter removal.

However: the reason that these greek letters aren't allowed in identifiers is so that λx => x parses. If it were an allowed identifier start character, then this would start with the identifier λx and lead to a parse error.

[Kyle Miller]

I personally don't see that as important, but I saw this rationale in the code somewhere so it needs consideration.

[Patrick Massot]

If you bring this up with Leo, please make it clear that it would be nice but this is not crucial at all.

[Kyle Miller]

I found the issue, and I think Leo's comment is where I picked up on the rationale for the restrictions: https://github.com/leanprover/lean4/issues/700

[A.]

Flo (Florent Schaffhauser) said:

Is there maybe another Unicode character that looks like $\lambda$? Perhaps accessible by typing something like \lambda1?

If you were asking whether there is some other unicode character that looks like lambda and that we can use as an identifier, then the answer is no (or it was last time I checked). Perhaps that's how you should interpret the thumbs down? The closest is the capital Λ.

[Kyle Miller]

There's

• Coptic laula: Ⲗ
• Coptic small laula: ⲗ
• mathematical sans-serif bold small lamda: 𝝺
• mathematical bold small lamda: 𝛌
• Buginese nga: ᨂ

(via https://shapecatcher.com/)

[A.]

Does Lean permit those now?

[Kyle Miller]

Oh, I missed "that we can use as an identifier". Probably not, I didn't check, but it's more likely that core Lean could provide support for these as identifiers than lambda itself.

[A.]

No.

[Ruben Van de Velde]

Even if we could use those, I think that would be worse than not using lambda at all