Are "↦" and "=>" interchangeable?

Stream: lean4

[Ching-Tsun Chou]

In sec.9.4.1 of "Mathematics in Lean" there are the examples shown below. I noticed I can replace any "↦" by "=>" and the example will continue to work. Are the two symbols "↦" and "=>" interchangeable?

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext I j
  fin_cases i <;> fin_cases j <;> rfl

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) * (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext I j
  fin_cases i <;> fin_cases j <;> rfl

example {n : ℕ} (v : Fin n → ℝ) :
    Matrix.vandermonde v = Matrix.of (fun i j : Fin n ↦ v i ^ (j : ℕ)) :=
  rfl

[Kyle Miller]

Yes, they're interchangable for fun.

[Edward van de Meent]

they aren't when matching patterns, however.

[Kyle Miller]

If you set set_option pp.unicode.fun true, then Lean will pretty print the arrow too.

[Kyle Miller]

Edward van de Meent said:

they aren't when matching patterns, however.

In particular, it will be a parse error for match's =>

[Kyle Miller]

But you don't mean they're not interchangeable in fun ⟨x, y⟩ ↦ x + y, right @Edward van de Meent?

[Edward van de Meent]

indeed, i was referring to the following kinds of pattern matching:

def double (n:Nat) : Nat := match n with
  | 0 => 0
  | n + 1 => (double n) + 2

def double' : Nat -> Nat
  | 0 => 0
  | n + 1 => double' n + 2

theorem or_self {p : Prop} : Or p p -> p := by
  intro h
  cases h with
  | inl hp => exact hp
  | inr hp => exact hp

[Patrick Massot]

They are not really interchangeable in the sense that => is wrong and ↦ is right. But Lean understands both.

[Edward van de Meent]

it is wrong?

[Edward van de Meent]

from the mathlib style guide:

Anonymous functions

Lean has several nice syntax options for declaring anonymous functions. For very simple functions, one can use the centered dot as the function argument, as in (· ^ 2) to represent the squaring function. However, sometimes it is necessary to refer to the arguments by name (e.g., if they appear in multiple places in the function body). The Lean default for this is fun x => x * x, but the ↦ arrow (inserted with \mapsto) is also valid. In mathlib the pretty printer displays ↦, and we slightly prefer this in the source as well. The lambda notation λ x ↦ x * x, while syntactically valid, is disallowed in mathlib in favor of the fun keyword.

[Patrick Massot]

Yes, this is clearly ASCII art for the implication symbol. It could be the symbol for natural transformations, but it has nothing to do here. This is an unfortunate historical mistake coming from earlier programming languages.

[Edward van de Meent]

it only says "slightly preferred"

[Mario Carneiro]

Patrick is being intentionally provocative there

[Edward van de Meent]

ah
that was not clear to me

[Kevin Buzzard]

It just looks daft to mathematicians, in the same way that <= looks daft for \le. It reminds me of the 1980s. It's probably analogous to you looking at old FORTRAN CODE

[François G. Dorais]

To point out the obvious caveat: ↦ only works in Mathlib. Core and Batteries only use =>.

[Kyle Miller]

That's not the case @François G. Dorais, it's part of the core syntax. You can use fun x ↦ x without mathlib.

[Michael Rothgang]

Is there interest in mass-replacing (some/most) of mathlib's "=>" by "\mapsto"? There are about 40 000 occurrences right now; making automatic replacements is relatively easy and can go a long way. (Enforcing "\mapsto" via a syntax linter would be easy.)

[François G. Dorais]

Kyle Miller said:

That's not the case François G. Dorais, it's part of the core syntax. You can use fun x ↦ x without mathlib.

Interesting. Why is it prohibited in Batteries?

[Kyle Miller]

Core style is also to use =>, but, still, it works. I would guess that Batteries style is to copy core style as much as possible?

[Ruben Van de Velde]

I think such a large scale replacement has a significant cost for very little benefit

[Damiano Testa]

Also, match only allows =>, right? So any mass-replacement would have to take that into account.

[Edward van de Meent]

a decent heuristic might be checking if the | character appears somewhere before it on the same line

[Edward van de Meent]

if it does, it is decently likely not a fun

[Eric Wieser]

Ruben Van de Velde said:

I think such a large scale replacement has a significant cost for very little benefit

Arguably a weaker version of the same could be said for having two ways to spell the same thing, and mathlib using a mixture of them

[Edward van de Meent]

a regex like fun([^↦])*?(=>) should be able to find the right arrows to replace, i think

[Eric Wieser]

Nope, that misfires on

#check fun | 1 => 2 | _ => 0

[Edward van de Meent]

wait, that's valid notation?

[Edward van de Meent]

huh

[Edward van de Meent]

learn something every day, i guess.

[Edward van de Meent]

i guess adding a \| in the set not to match would fix it?

[Edward van de Meent]

i.e. fun([^↦\|])*?(=>)?

[Eric Wieser]

Nope, then you're in trouble with fun (x : match true with | true => Nat | false => Nat) => x

[Edward van de Meent]

ok. that's not something you can prepare for with proper regular expressions, however. Still, it should account for the majority of uses, no?

[Eric Wieser]

Personally I'd argue that switching to ↦ globally in mathlib is a bad idea, because then we have to explain why fun | .op x => x and fun x ↦ x use different arrows.

[Edward van de Meent]

i agree with that, my point was more that should we want to switch, there is a decent heuristic for finding "wrong arrows" that only in some unfortunate cases doesn't work.

[Kyle Miller]

This feels a lot like trying to settle on whether to use -- hyphen comments or /- bracketed comments -/. There's not much of a difference (and with ↦ vs => there's no difference other than saving a character for the 100 character limit), and it changes 40k lines for what benefit?

[Kyle Miller]

I tend to like (my understanding of) Wikipedia-style rules — don't do a blanket change of "colour" to "color" (or vice versa), but if you happen to be passing by making substantial edits, then you can change the style locally.

[Edward van de Meent]

(assuming there exists a preference)

[Eric Wieser]

Was it a deliberate choice to not permit ↦ notation in match arms?

[Kyle Miller]

My recollection of the history was that ↦ was added by popular request either late 2022 or early 2023, and there was probably some worry about it being a slippery slope. If you add it to match arms, then that would mean tactics too, right? given that there's a match tactic?

[Eric Wieser]

match feels sort of ok, but I guess induction would be weird

[Eric Wieser]

The status quo seems like the worst of both worlds, where mathlib gets to be inconsistently inconsistent with core!

[Kyle Miller]

At least core supports ↦, even if it's not the style.

[Edward van de Meent]

Eric Wieser said:

The status quo seems like the worst of both worlds, where mathlib gets to be inconsistently inconsistent with core!

i'm sorry, complaining that an inconsistent thing is inconsistent with something else seems pointless. that's like saying False as axiom is bad because it contradicts False -> False.

[Kyle Miller]

(A really annoying incompatibility is Type*. I hope core adopts this syntax at some point!)

[Eric Wieser]

Edward van de Meent said:

i'm sorry, complaining that an inconsistent thing is inconsistent with something else seems pointless.

The claim was that even if we did the 40k lines of replacement discussed early, mathlib would still have to explain to mathematicians why there are (only sometimes) "weird" => arrows in functions.

[Edward van de Meent]

the claim claimed to be about status quo, not the hypothetical case where we get rid of fun a =>

[Eric Wieser]

Ah, I meant the status quo of core's support for the arrows

[Patrick Massot]

I very strongly think we should get rid of as many => as possible in Mathlib. But we need Mario’s refactoring tool to do this. Regex won’t do it.

[Damiano Testa]

If this change is wanted, then writing the linter to flag such uses is really the main missing piece. Automatically applying the substitutions can be done via Mario's refactor or otherwise, as long as the linter says where to apply the changes.

[Michael Rothgang]

Patrick Massot said:

I very strongly think we should get rid of as many => as possible in Mathlib. But we need Mario’s refactoring tool to do this. Regex won’t do it.

So if I propose on PR (or several) getting rid of (say) 10 000 of them, you'd approve it? Sounds like a deal.

[Patrick Massot]

Yes, if you ping me here.

[Michael Rothgang]

@Patrick Massot #19576 fixes about 20 000 occurrences

[Kim Morrison]

I won't actually hold anyone up doing this, but for the record I (still) think ↦ is a bad idea, and the small increase in familiarity to mathematicians doesn't outweigh the confusion of having two ways to say the same thing.

[Bulhwi Cha]

Perhaps we should encourage newcomers to install and use monospace fonts with programming ligatures.

[Eric Wieser]

I think programming ligatures are a bad idea when you have all of unicode to reach for, unless Lean picks a custom font with a custom set of ligatures and strongly recommends everyone uses it

[Eric Wieser]

They work well in languages where the source promises to be mostly ascii

[Bulhwi Cha]

Personally, I don't mind seeing both Unicode characters and programming ligatures; it's not hard to distinguish between them. I use Victor Mono, by the way.

20241129_11h59m56s_programming-ligatures.png

[Edward van de Meent]

Michael Rothgang said:

Patrick Massot #19576 fixes about 20 000 occurrences

aww, testing fails :rolling_on_the_floor_laughing:

[Mario Carneiro]

Eric Wieser said:

Personally I'd argue that switching to ↦ globally in mathlib is a bad idea, because then we have to explain why fun | .op x => x and fun x ↦ x use different arrows.

Or even fun | .op x => x vs fun (.op x) ↦ x! I think the answer is that lean is just inconsistent here.

[Patrick Massot]

Of course the dream solution would be to put mapsto everywhere, but putting it where it works is already a great improvement.

[Mario Carneiro]

I have in the past complained that lean is inconsistent about whether to use := or =>, and \mapsto is yet another possibility which is used in not quite the same positions

[Matthew Ballard]

I can see the merits of both arguments but I think it’s a bad idea to move in either direction until there is some consensus. This is not mission critical.

[Eric Wieser]

I mentioned it on the PR, but; the cost of merging a PR that touches 20k lines is that there are 20k opportunities for conflicts with other open PRs

[Michael Rothgang]

I just did an analysis of all open PRs which split or move files: there seem to be about 20 of them, of which perhaps 10 would conflict with that PR. If these operational aspects are an issue, I'd be happy to split the PR into smaller pieces or wait for file splitting PRs to go in first.

[Michael Rothgang]

One data point on the status quo: currently, there are about 54000 uses of "=>" with fun (imperfect count: rg --fixed-strings "=>" | rg "fun" | wc -l), compared to 22646 uses of "\mapsto" (should-be-accurate count: rg --fixed-strings "↦" | wc -l). rg is a Rust rewrite of grep.

[Michael Rothgang]

(I also started writing a summary comment for the discussion so far: hopefully, I can finish this tonight.)

[Mario Carneiro]

both counts are distorted though by automated tools (mathport uses => and I think there has been at least one large scale conversion pass to ↦ in the past)