Switch to ↦ (\mapsto) globally

Stream: mathlib4

[Junyan Xu]

The current style guide says:

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.

Should we switch to ↦ globally across mathlib? This is recently raised on Zulip #mathlib4 > linter requests @ 💬 and @Michael Rothgang volunteered to write a linter for it, and I can volunteer for the PR that replaces => with ↦ (there are a few occurences in the style guidelines also). We'll need to modify the wording of this guidline too.

The problem with allowing both is that when you add something to an old file which uses =>, you would be tempted to conform to the convention and keep using the less preferred => spelling, or otherwise switch the whole file to the mathlib style ↦ (which increases the review burden). This happened in #28500 which is the motivation of this post.

Update: after discussions in this thread, I proclaim that "everywhere" in the vote below should mean Mathlib/, Archive/ and Counterexamples/, but exclude meta-oriented directories and files Tactic/, Testing/, Util/, Lean/, Init.lean, and Tactic.lean under Mathlib/, as shown in the replacement script. See #28622 and #28626 for PRs that do the replacements.

[Junyan Xu]

/poll You opinion
Use ↦ everywhere
Use => everywhere
Allow both

[Eric Wieser]

As a reminder, a regex replacement won't work as there are plenty of bits of lean grammar that while analogous to functions, do not support this syntax

[Junyan Xu]

induction, case, match are some keywords to pay attention to (where replacement may not be possible). My plan is to ask Claude to write a script for replacements, compile after replacements, report any error to Claude for it to generate a new script, and iterate. Hopefully after a few iterations only a few manual replacements are necessary. (Maybe there will be false negative which the linter would hopefully help catch.)

[Kenny Lau]

Junyan Xu said:

In mathlib the pretty printer displays ↦

this is actually not true:

import Mathlib

theorem foo : (fun x ↦ x) 3 = 4 := by
  -- ⊢ (fun x => x) 3 = 4
  sorry

[Kenny Lau]

I think we should change the pretty printer to display ↦

[Junyan Xu]

Weird, I'm definitely seeing ↦ most of the time; this is a random file GroupTheory/Perm/Centralizer.lean that happens to be open in my editor.
image.png

[Kenny Lau]

have you tried copying it and seeing what it actually outputs?

[Junyan Xu]

What do you mean? This is a screenshot of the infoview (of the goal).

[Junyan Xu]

The problem with allowing both ↦ and => is that when you add something to an old file which uses =>, you would be tempted to conform to the convention and keep using the less preferred => spelling, or otherwise switch the whole file to the mathlib style ↦ (which increases the review burden). This happened in #28500 which is the motivation of this post.
(Also added to the OP)

[Aaron Liu]

Kenny Lau said:

I think we should change the pretty printer to display ↦

The pretty printer does display ↦, but only when the file you're in is in the Mathlib folder

[Eric Wieser]

Kenny Lau said:

this is actually not true:

import Mathlib

theorem foo : (fun x ↦ x) 3 = 4 := by
  -- ⊢ (fun x => x) 3 = 4
  sorry

I think you are confusing "in mathlib" with "in the web editor"

[Eric Wieser]

Aaron Liu said:

The pretty printer does display ↦, but only when the file you're in is in the Mathlib folder

More accurately, "only when you are in a project that records this desire in the lakefile"

[Kenny Lau]

Eric Wieser said:

I think you are confusing "in mathlib" with "in the web editor"

good point, but I use the web editor a lot too

[Junyan Xu]

The web editor should fix the lakefile then
Gabriel Ebner said:

Yes, it should be enough to add the pp.unicodeFun option to the lakefile now.

[Eric Wieser]

Previous discussion: #mathlib4 > => notation @ 💬

[Junyan Xu]

Most discussions there were before the ↦ notation was implemented and merged. Here I'm not proposing introducing any new syntax, but simply doing some replacements (and adding a linter so you don't have to / no longer can make a choice which one to use).

[Aaron Liu]

What exactly is the advantage of => vs ↦?

[Jovan Gerbscheid]

The advantage of => is that it's faster to type than ↦. And there are cases where ↦ doesn't work, so in general it's safer to just type => without thinking about it. And I've personally gotten used to always writing =>, probably because of all the metaprogramming I've been doing.

[Junyan Xu]

" " is faster to type than /-- -/ but we still switched to the latter ...
(BTW you only need to type \map for ↦ , no Shift key involved)

[Thomas Murrills]

Purely by aesthetics, I would use ↦ in “math” files and => in “programming” files (metaprogramming, infrastructure), maybe determined by folder. I’m not sure what this would feel like in practice.

[Thomas Murrills]

(By the way, I’ve been recently test-driving some lean code that edits source throughout mathlib in a syntax-aware way—overlapping with Mario’s refactor infrastructure, but with a different implementation—without going through Claude. If we do switch to a different syntax, free to ping me if you’d like to avoid Claude + manual iterations. :) )

[Jovan Gerbscheid]

I agree that ↦ belongs in mathematical expressions, the kinds of expressions that a mathematician might write on paper. But in metaprogramming, and maybe even in proofs, e.g. proving p → p using fun x => x, it's not clear to me that ↦ is better.

[Jovan Gerbscheid]

I presume we don't have a reliable way to automatically differentiate between "math" and "programming" types? Differentiating by folder would be a bit unsatisfactory given that math files often have snippets of meta code, and meta files often prove some lemmas.

[Thomas Murrills]

One point in favor of mirroring familiar mathematical expressions in math files is making mathlib source code feel more approachable for mathematicians. In (meta)programming I agree that it’s unnecessary.

If that’s the motivation, then one reason to differentiate by folder could be to differentiate by “what mathematicians are likely to be looking at.”

(Alternatively, I wonder if the upcoming meta keyword could provide a different criterion? Though I fear that would be too complex; one advantage of going by folder is that it’s simple and predictable. Of course, even simpler is “just use one thing” or “just allow both”… :) )

[Junyan Xu]

As a first approximation we can single out some folders as meta and not touch them. Within Mathlib/ I see Tactic/, Testing/, Util/, Init.lean, and Tactic.lean. Anything else?

[Michael Rothgang]

Lean, right?

[Thomas Murrills]

Probably Lean/, Mathport/, and Std/ as well, I’d say (though for slightly different reasons than because they’re metaprogramming per se)

[Thomas Murrills]

Wait, Mathport only has an .md, and Std has exactly one file?

[Thomas Murrills]

So I suppose those are edge cases. :grinning_face_with_smiling_eyes:

[Junyan Xu]

It looks appropriate to me to replace the single => in Std/Data/HashMap.lean ...

[Thomas Murrills]

Ah, a nontrivial edge case! The best kind…

[Thomas Murrills]

Btw, my thoughts for Std were that its contents “belong somewhere else” and might be upstreamed—hence it might not make sense to impose this particular Mathlib style constraint.

[Robin Arnez]

As far as I'm aware, Mathlib.Std.Data.HashMap is completely redundant (we have Std.HashMap.map even with quite a few lemmas about it)

[Patrick Massot]

Jovan Gerbscheid said:

The advantage of => is that it's faster to type than ↦. And there are cases where ↦ doesn't work, so in general it's safer to just type => without thinking about it. And I've personally gotten used to always writing =>, probably because of all the metaprogramming I've been doing.

It is faster only if your computer is misconfigured. It certainly isn’t for me.

[Patrick Massot]

I need one more key press to type => (3 vs 2).

[Thomas Murrills]

How do you type ↦ in 2 keypresses? :eyes:

[Thomas Murrills]

Robin Arnez said:

As far as I'm aware, Mathlib.Std.Data.HashMap is completely redundant (we have Std.HashMap.map even with quite a few lemmas about it)

Can we deprecate it? #28611 (draft)

[Robin Arnez]

Yes I don't think there's any reason not to

[Junyan Xu]

Since there's now majority support I commissioned Claude Sonnet 4 to write the script. After some iterations to clarify the exact requirements, the following code (produced during our second conversation) works except in a single occasion, where the one-character reduction from => to ↦ breaks the indentation of a by block:

find . -type f \
  -not -path "./Tactic/*" \
  -not -path "./Testing/*" \
  -not -path "./Util/*" \
  -not -path "./Lean/*" \
  -not -name "Init.lean" \
  -not -name "Tactic.lean" \
  -exec perl -i -0777 -pe 's/(?<![a-zA-Z_])(fun (?:(?!=>|↦|\|).)*?)=>/\1↦/gs' {} \;

What it does is basically

for all files in the current directory or recursive subdirectories, for each occurrence of fun (completely lowercase) followed by some characters (including linebreaks), look for the first => or ↦ or | that appears afterwards, and if it is =>, replace it with ↦. I also want you to exclude the following directories and files: Tactic/, Testing/, Util/, Lean/, Init.lean, and Tactic.lean

and "don't match fun that are immediately preceded by a letter (upper or lowercase) or _"

and the result is #28622 which now builds! :octopus:
(and #28626 for Archive & Counterexamples)

[Kim Morrison]

I don't think that poll above counts as majority support. I think that counts as general disagreement. :-)

[Michael Rothgang]

Note that 4-5 people voted for two options. Is this "accept all options you're fine with" or "pick only your preferred one"?

[David Ang]

I voted for => and \mapsto because I’m fine with either but not both

[Filippo A. E. Nuccio]

I voted for \mapsto and both because I prefer the first but I don't feel like "prohibiting" anything.

[Junyan Xu]

So at the moment there are 48 votes from 41 people and 24 of them are supportive. I guess that counts as majority support? I've now also clarified the scope of "everywhere" in the OP and people might want to recast their votes. :-)

[Junyan Xu]

If you are used to writing => the above script should do a decent job converting your code to "mathlib style" :-)

[Jireh Loreaux]

We don't exactly make changes based on majority rule. The poll above suggests there's still a lot of division, and many still support allowing both. So I don't see a strong reason to disallow one option or the other at the moment.

[(deleted)]

Thomas Murrills said:

How do you type ↦ in 2 keypresses? :eyes:

I recommend that you start using Plover. It's underrated and is very useful when writing Lean code.

[suhr]

I recommend configuring the compose key (or WinCompose on Windows).

[Patrick Massot]

Thomas Murrills said:

How do you type ↦ in 2 keypresses? :eyes:

I’m sorry I dropped the conversation, I’m travelling (I’m currently in China). I use https://github.com/OneDeadKey/kalamine to tweak my keyboard layout. My base layout is QwertyLafayette which has plenty of room on its typography layer (the green letters on the main picture, you access them after pressing the red star key which a special deadkey). I put ↦ on the R key. So I tap what would be the ; key on a US qwerty and then I tap r. Of course I have many more useful Lean symbols configured using Compose but they require some more keypresses (but not more than what you could need using the VSCode or Neovim Lean abbreviations, and the compose key works in every software).

[Patrick Massot]

In any case, there are many ways to type this ↦, including using the editor extensions that you need anyway. So beginners can type it with not more work than the other unicode symbols we use all the time in Lean. And serious users who want to type it more efficiently have lots of options.

[Filippo A. E. Nuccio]

Of course Patrick's answer is the master way to go. A more humble tweak is to add the following lines

"lean4.input.customTranslations":
        {
         "ma": "↦"},

to your .json file, that will add the shortcut ma for the symbol (but this makes it three keystrokes, including the \). You can also use "m" but this will override the default value and will oblige you to type \mu to obtain μ .

[Eric Wieser]

If we strongly believe that's useful we should add it to the defaults rather than telling users to add it

[Yaël Dillies]

\ma currently turns into ♂...

[Aaron Liu]

mars?

[Jovan Gerbscheid]

If \m and \ma would both give ↦, that would be great!

(And I don't really like the idea of telling people to use some special keyboard software, or even to add something to some magic json file, because in practice the vast majority of users simply isn't going to do this)

[Thomas Zhu]

Filippo A. E. Nuccio said:

You can also use "m" but this will override the default value and will oblige you to type \mu to obtain μ .

By the way, on a MacBook you can use Option + M to type µ

[Patrick Massot]

Yes, we definitely need to fix \ma becoming mars instead of ↦, independently of any other discussion about this symbol.

[Patrick Massot]

I guess the issue is that mars is shorter than mapsto, so ma is seen as closer to mars than mapsto. I’m sure @Marc Huisinga will save us anyway.

[Marc Huisinga]

Happy to accept a PR that changes these abbreviations to something more fitting for Mathlib.

[Vasilii Nesterov]

Here's the PR: https://github.com/leanprover/vscode-lean4/pull/667