Zulip Chat Archive

Stream: mathlib4

Topic: Coding style: <| vs $

Yury G. Kudryashov (Dec 28 2023 at 17:54):

Hi, do we officially prefer one of <| or $ to another?

Eric Wieser (Dec 28 2023 at 17:54):

Yes, #style says <|:

Note: while $ is a synonym for <|, its use in mathlib is disallowed in favor of <| for consistency as well as because of the symmetry with |>.

Yury G. Kudryashov (Dec 28 2023 at 17:55):

I'm going to search for $s and change them to <|s then.

Yaël Dillies (Dec 28 2023 at 18:19):

Out of all style decisions, this is the one I just can't stand with. <| don't stick out visually for me, so readability is very poor, and the symmetry argument with|> doesn't make sense to me since I never use it (certainly, if you're doing dot notation on a lemma with underscores, that usually means you've messed up implicitness of the arguments). How come we like ASCII art now? :frowning:

Yaël Dillies (Dec 28 2023 at 18:19):

Anyway, I see no reason to not let everyone do their own thing.

Mario Carneiro (Dec 28 2023 at 18:27):

FWIW I use a programmer font with nice ligatures so it actually does look like a big triangle to me. You should consider using one to improve the look of the other ascii art aspects of lean code like := and =>

Mario Carneiro (Dec 28 2023 at 18:28):

We could use a unicode triangle, but I think it is better to leave that as an available operator for mathsy stuff

Yaël Dillies (Dec 28 2023 at 18:29):

▸ is famously already used

Yaël Dillies (Dec 28 2023 at 18:29):

Also using a programmer font will probably conflict with the fact that we want a lot of unicode available

Mario Carneiro (Dec 28 2023 at 18:30):

believe it or not the ▸ operator actually did come from the math (well, type theory) literature

Yaël Dillies (Dec 28 2023 at 18:30):

I should also mention that typing <| is 1 + 2 keystrokes while $ is a single one. I'm a big (ab)user of $ so that matters.

Junyan Xu (Dec 28 2023 at 18:31):

the symmetry argument with|> doesn't make sense to me since I never use it (certainly, if you're doing dot notation on a lemma with underscores, that usually means you've messed up implicitness of the arguments

It doesn't seem any implicit argument should be made explicit in

theorem finRange_succ (n : ℕ) :
    finRange n.succ = (finRange n |>.map Fin.castSucc |>.concat (.last _))

(and certainly nested ( are avoided using |> here.) You can see more examples how |> is used in mathlib here.

Mario Carneiro (Dec 28 2023 at 18:32):

Yaël Dillies said:

I should also mention that typing <| is 1 + 2 keystrokes while $ is a single one. I'm a big (ab)user of $ so that matters.

This depends a lot on your keyboard layout. What if your keyboard has a € key instead?

Yaël Dillies (Dec 28 2023 at 18:32):

In fact, mine does!

Mario Carneiro (Dec 28 2023 at 18:33):

in any case, if number of keystrokes was our top optimization criterion we would be an ascii shop

Yaël Dillies (Dec 28 2023 at 18:34):

Junyan Xu said:

It doesn't seem any implicit argument should be made explicit in

theorem finRange_succ (n : ℕ) :
    finRange n.succ = (finRange n |>.map Fin.castSucc |>.concat (.last _))

Maybe I'm the minority, but

theorem finRange_succ (n : ℕ) :
    finRange n.succ = ((finRange n).map Fin.castSucc).concat (.last _)

actually looks better to me? No outside bracket needed, and you clearly see what happens first and what happens last.

Yaël Dillies (Dec 28 2023 at 18:35):

... not to mention it's shorter

Mario Carneiro (Dec 28 2023 at 18:36):

and $ meaning application doesn't really make any sense at all - the only thing it has going for it is that it's one of the ascii punctuation characters (which is a powerful force in programming language design)

Mario Carneiro (Dec 28 2023 at 18:39):

@ would make more sense as an application operator

Junyan Xu (Dec 28 2023 at 18:39):

Yaël Dillies said:

Maybe I'm the minority, but
theorem finRange_succ (n : ℕ) :
    finRange n.succ = ((finRange n).map Fin.castSucc).concat (.last _)
actually looks better to me? No outside bracket needed, and you clearly see what happens first and what happens last.

Yes in this case, but I would prefer |> when there are three or more nested (. Also you usually don't need to go back to add parentheses if you use |> (except maybe the outermost one for precedence reasons).

Adam Topaz (Dec 28 2023 at 18:52):

It’s not just about looking nice or being shorter… I think readability is much more important and personally I think the version with |> makes it much easier to immediately see what’s going on with the code.

Yaël Dillies (Dec 28 2023 at 18:54):

I too am fighting for readability, and I think <|/|> are terrible for that! Sure I can use a programming font in my VScode, but that still doesn't stop the code ~~looking terrible~~ being unreadable on Github, Zulip, Discord...

Mario Carneiro (Dec 28 2023 at 18:58):

reminder, "looking good/terrible" is not synonymous with "readability"

Yaël Dillies (Dec 28 2023 at 19:00):

Sure, let me edit my message.

Mario Carneiro (Dec 28 2023 at 19:00):

what is the argument that $ is more readable than <|?

Mario Carneiro (Dec 28 2023 at 19:01):

I'm sorry but I can't see this as anything other than "I'm used to $ from lean 3 code"

Yaël Dillies (Dec 28 2023 at 19:01):

Less ASCII art, no kerning issue, no height issue.

Mario Carneiro (Dec 28 2023 at 19:01):

they are both ascii art

Mario Carneiro (Dec 28 2023 at 19:02):

and the other two are aesthetic concerns not readability concerns

Mario Carneiro (Dec 28 2023 at 19:02):

again, see my previous message

Mario Carneiro (Dec 28 2023 at 19:02):

readability is about being able to look at the text and understand what it says

Yaël Dillies (Dec 28 2023 at 19:02):

For me specifically, I think the matter is that $ is more visually "one thing" than <|.

Kyle Miller (Dec 28 2023 at 19:04):

I'm not arguing for using it, but my mnemonic was that $ is a ( and a ) pinned together

Kyle Miller (Dec 28 2023 at 19:06):

I see <| as a little cliff that raises the height of nesting. I think it's supposed to be arrow-like, pointing toward the function it's feeding

Mario Carneiro (Dec 28 2023 at 19:08):

I think part of the motivation for the directionality is the idea of a "pipeline", x |> f |> g |> h takes x, applies f then g then h in that order

Mario Carneiro (Dec 28 2023 at 19:09):

it's trying to fight against the traditional function application order h (g (f x)) which puts the functions in the wrong order compared to the order of operations

Mario Carneiro (Dec 28 2023 at 19:10):

but it also so happens that when writing proofs because things are goal directed you often want to work backward from the end, hence the reverse pipeline h <| g <| f <| x turns out to be even more useful

Mario Carneiro (Dec 28 2023 at 19:11):

the use of pipe symbols derive from the | symbol in unix pipes, which again pull from the idea of a pipeline

Newell Jensen (Dec 28 2023 at 19:12):

Kyle Miller said:

I see <| as a little cliff that raises the height of nesting. I think it's supposed to be arrow-like, pointing toward the function it's feeding

This is how I view it, pointing toward the function it's feeding, which makes more sense than $. <| is harder to type for sure so I understand that. Is there a way in VSCode to set notation so that you don't have to use local notation for each lean file and VSCode would treat the ascii of $ as <|? No idea if this is possible or not but if so you could have a sed script that then was used before pushing PRs to replace all the $ by <|. I personally wouldn't use this but might be a workaround for those that love the $ :wink:

Mario Carneiro (Dec 28 2023 at 19:13):

you can just use $ in vscode, it's already legal notation

Mario Carneiro (Dec 28 2023 at 19:13):

As for autofix, I would love that but it seems like something to bundle together with other formatting tooling

Newell Jensen (Dec 28 2023 at 19:25):

Yes, agreed. Do we do any auto-formatting now? Something like python-black for mathlib to handle the autofixing and code conventions would be nice so you didn't have to run the linters locally and it was just part of the design cycle.

Newell Jensen (Dec 28 2023 at 19:27):

But there are probably "larger fish to fry"....

Eric Rodriguez (Dec 28 2023 at 20:11):

I will agree with Yael that sometimes the backwards pipeline sometimes looks weird when applying dot notation, although it's very context dependent.

Yury G. Kudryashov (Dec 28 2023 at 20:15):

I opened #9319 but I won't insist on merging it.

Eric Rodriguez (Dec 28 2023 at 20:27):

like lack of spaces before \l, I think regardless of opinions it's best to merge this ASAP to stop rotting and bikeshed later, fixing this with tools when we have that possibility

Alex J. Best (Dec 29 2023 at 00:36):

Yaël Dillies said:

Also using a programmer font will probably conflict with the fact that we want a lot of unicode available

I'm not sure this is true, someone here did a very nice comparison of the many fonts available (personally I'm very happy with julia mono for ligatures and unicode support)

Eric Wieser (Dec 29 2023 at 16:39):

Though it's slightly confusing having the <| ligature when working with code that also does whiskering with ◁. Julia Mono can be used with them disabled, thankfully.

Adam Topaz (Dec 29 2023 at 17:18):

I've never really confused the two, and I've been using the julia mono ever since Alex told me about it last summer.

Yury G. Kudryashov (Dec 30 2023 at 20:12):

So, what's the plan about #9319?

Yury G. Kudryashov (Dec 30 2023 at 20:13):

I merged master. IMHO, we should either merge it soon or reject it soon.

Yury G. Kudryashov (Dec 30 2023 at 20:24):

#9361 should be the non-controversal part of #9319

Johan Commelin (Dec 30 2023 at 20:25):

If you want to merge #9319 and have <| everywhere, then vote with :thumbs_up:
If you want to keep $ around, vote with :thumbs_down:

Mario Carneiro (Dec 30 2023 at 20:27):

do we have any means to prevent backsliding or is this just something we are going to do periodically?

Yury G. Kudryashov (Dec 30 2023 at 20:27):

Disable the $ notation?

Mario Carneiro (Dec 30 2023 at 20:28):

I suppose we could... we add a macro_rules for the f $ x notation which prints a warning

Henrik Böving (Dec 30 2023 at 20:28):

Cant this be part of a linter?

Mario Carneiro (Dec 30 2023 at 20:28):

(with a linter option to disable it for downstream users that disagree with the policy)

Mario Carneiro (Dec 30 2023 at 20:29):

oh, you mean just a post hoc linter that looks at the syntax ... sure

Yury G. Kudryashov (Dec 30 2023 at 20:29):

Note: I have no opinion about $ vs <| but I (a) don't want to merge master in this PR again; (b) prefer to have consistent style in the library.