naming conventions: natCast vs nat_cast

Stream: mathlib4

[Thomas Murrills]

Ooo, there are a lot of nat_casts which should be natCasts spread around mathlib4. :eyes: (A fair number of int_casts, and some rat_casts.)

[Eric Wieser]

In lemma names shouldn't they be nat_cast?

[Eric Wieser]

This is confusing because we have both natCast and Nat.cast; but the latter is the canonical spelling

[Thomas Murrills]

Hmm, I guess the question is: how does . factor into a lemma name? Should the two things either side be viewed as part of the same whole being referenced, and therefore the whole thing is a single unit in lowerCamelCase? Or should they be viewed as separate identifiers?

[Eric Wieser]

I think this belongs in the naming thread now

[Notification Bot]

5 messages were moved here from #mathlib4 > Complex.Basic by Thomas Murrills.

[Eric Wieser]

As a data point, docs4#map_multiset_sum

[Thomas Murrills]

Hmm, good data point. If we're considering making a conscious choice, though, we might ask: would what that lemma name referred to be epsilon clearer if it were map_multisetSum?

[Eric Wieser]

I think it's confusing for a lowercase name (sum) to become uppercase when included in a lemma name when usually the rule is the reverse

[Eric Wieser]

But I agree it's not clear a conscious choice was made

[Thomas Murrills]

True, it might be less clear than otherwise!

Pros to lowerCamelCasing so far: keeps it as a distinctive unit, _-separation is a bit more ambiguous in terms of what each "chunk" of the name is.

Cons: a lowercase name is now uppercase, so you now might not even recognize the chunk in the first place! And there's still ambiguity about where the . should be.

[Thomas Murrills]

Maybe I'm just suggesting this because I'm insanely sleep deprived right now, but:

it would be unambiguous to use ' as an intraname translation for . in lemmas. E.g. map_multiset'sum.

[Thomas Murrills]

' is generally only used at the end of names, and dots are generally only in the middle, meaning that iff ' was part of the original thing the lemma was about, it would be at an underscore boundary and thus distinguishable from a ' which used to be a ..

[Floris van Doorn]

Eric Wieser said:

As a data point, docs4#map_multiset_sum

Personally, I like the name Multiset.map_sum better, especially since there is an explicit Multiset argument.

[Floris van Doorn]

But if we stick we the current name, I probably prefer map_multisetSum, since Multiset.sum is a single operation.

[Eric Wieser]

Floris van Doorn said:

Personally, I like the name Multiset.map_sum better, especially since there is an explicit Multiset argument.

I don't think Multiset.map_sum is great here because it sounds like map refers to Multiset.map, and all the other map_* lemmas are in either the root or morphism namespaces

[Eric Wieser]

Thomas Murrills said:

Maybe I'm just suggesting this because I'm insanely sleep deprived right now, but:

it would be unambiguous to use ' as an intraname translation for . in lemmas. E.g. map_multiset'sum.

If we want to go down that route, map_«Multiset.sum» seems less bad...

[Eric Wieser]

Oh, that's not legal any more in Lean4; map_«Multiset.sum» is now parsed as map_ «Multiset.sum» instead of «map_Multiset.sum»

[Eric Wieser]

This is really a mess; we have 336 matches for _(nat|int|rat)Cast and 404 matches for _(nat|int|rat)_cast (on some random branch I'm on)

[Eric Wieser]

(multisetSum has 0 matches to multiset_sums 161)

[Eric Wieser]

theorem.*_(nat|int|rat)_cast has 85 matches, theorem.*_(nat|int|rat)Cast has 91

[Jireh Loreaux]

We actually did talk about this at some point and I think the _ separator was determined. I believe the conversation was even about Nat.cast specifically.

[Eric Wieser]

There's a single message here:

Floris van Doorn said:

I've been using natCast if the Lean 3 name was nat_cast and keep it as cast otherwise.

[Jireh Loreaux]

I just found that too. I guess I fabricated that memory?

[Jireh Loreaux]

Sorry

[Eric Wieser]

A similar data point is the lemmas about docs4#Int.ceil etc, such as docs#Nat.cast_ceil_eq_int_ceil

[Floris van Doorn]

These data points are mostly an indication of what mathport is automatically generating as lemma names (i.e. what it was in Lean 3), not necessarily what we want.

[Eric Wieser]

Sure; though having an example of lemmas that would be renamed helps us decide which convention to choose

[Thomas Murrills]

Just as one final avenue: are there any other potential solutions of the form "translate the dot explicitly"? This would eliminate all ambiguity and make lemmas easy to find and recognize as the one you're looking for (once you know about it), but might be more verbose/less pretty. So it might come down to what our naming convention prioritizes.

' is the only one I could think of which is 1) easy to type/ASCII 2) brief 3) admissible in an identifier, but it does look weird as of now. frobenius_nat'cast (n : ℕ). map_multiset'sum. hmm.

Another option in this vein is translating the dot to a word, like _foo_, but I'm not sure what word we'd use.

__ is technically a possibility, but makes the two parts of the name look less associated with each other, so imo that's not great.

Any other "unambiguous translation" possibilities anyone can think of (or other ideas/comments) before we make a poll?

[Notification Bot]

29 messages were moved here from #mathlib4 > naming conventions by Eric Wieser.

[Eric Wieser]

/poll What should lemma about Foo.bar (Nat.cast x) be called?

• Foo.bar_nat_cast
• Foo.bar_natCast
• fooBar_natCast
• foo_bar_nat_cast

[Eric Wieser]

/poll What should lemma about Nat.cast (Bar.baz x) be called?

• Nat.cast_bar_baz
• Nat.cast_barBaz
• natCast_barBaz
• nat_cast_bar_baz

[Eric Wieser]

(if adding a new option, please add it to both polls in a way that is consistent, even if you don't vote for both)

[Eric Wieser]

To some extent the question boils down to whether .s in namespaced names collapse into _s or single tokens

[Eric Wieser]

Declaring natCast/intCast/ratCast as exceptions to the rules is probably also not unreasonable

[Reid Barton]

What are the Lean 3 names of these hypothetical lemmas?

[Eric Wieser]

Usually foo.bar_nat_cast and nat.cast_bar_baz

[Eric Wieser]

:ping_pong:, to get some more opinions on the poll. I forgot to bring this up in the porting meeting.

[Eric Wieser]

:ping_pong:, since as far as I can tell this isn't covered yet by #naming

[Yury G. Kudryashov]

This came up again in @Yaël Dillies 's #9619
I'm OK with either convention but I think that we should choose one.

[Michael Stoll]

I was just wondering about this in the context of #10029 and #10034. Should I use "nat_cast" or "natCast" there?

[Michael Stoll]

I think these lemmas are about NatCast, so I would assume the convention calls for "natCast" in the names?

[Emilie (Shad Amethyst)]

Yeah:

When something named with UpperCamelCase is part of something named with snake_case, it is referenced in lowerCamelCase.
https://leanprover-community.github.io/contribute/naming.html

[Michael Stoll]

OK; changed to "natCast" now.

[Eric Wieser]

That rule doesn't apply here, Foo.bar is not UpperCamelCase

[Eric Wieser]

(unfortunately we don't have a rule that applies here, which is why we have a problem)

[Yaël Dillies]

The entire point of making things camel case is that _ now separates declaration names into parts that each correspond to a single element of its type. As such, nat_cast would go against the spirit since the element appearing in the statements is Nat.cast, not Nat and cast separately.

[Yury G. Kudryashov]

I think that we have at least natCast, nat, nat_cast, coe_nat, and coe (in the Nat` namespace) in the library. it would be nice to have some consistency, I don't care which one.

[Yury G. Kudryashov]

I think that we have at least natCast, nat, nat_cast, coe_nat, and coe (in the Nat` namespace) in the library. it would be nice to have some consistency, I don't care which one.

[Eric Wieser]

#11486 tries to push the needle strongly towards natCast; it would be nice to get more poll votes before merging it

[Eric Wieser]

@Johan Commelin, can you explain why you voted differently between the two polls?

[Eric Wieser]

One "easy" (were it not in core) way out here is to rename docs#Nat.cast to natCast, which would make the naming scheme obvious

[Kim Morrison]

Eric Wieser said:

One "easy" (were it not in core) way out here is to rename docs#Nat.cast to natCast, which would make the naming scheme obvious

If there's consensus on this it's easy to rename.

[Eric Wieser]

I guess the hope is nothing refers to it by name, so there's not actually much downstream breakage to cleanup

[Kim Morrison]

Integrated Mathlib testing is working again, so if you want to make a PR, based off nightly-with-mathlib the CI results should show us how much breakage there is.

[Eric Wieser]

Maybe the FRO should just make a BDFL-style decision on this; the main consequence of choosing one or the other is whether we want autocomplete / doc-gen search to gain support for this style of naming, which needs to either learn to strip .s and case-fold, or replace .s with _.

[Eric Wieser]

(that is, if i search for Nat.cast_ I should also be shown suggestions for natCast_/nat_cast, depending on what we pick)

[Yaël Dillies]

Eric Wieser said:

One "easy" (were it not in core) way out here is to rename docs#Nat.cast to natCast, which would make the naming scheme obvious

An issue with this proposition is that after #11499 there will be lemmas named Namespace.natCast

[Yaël Dillies]

Apart from this issue, I don't really mind renaming Nat.cast to natCast, but note that this is not a sustainable solution for all the other Foo.bar definitions that we need to refer to in lemma names. So basically I don't want to rename Nat.cast to natCast because that would set precedent for many more dubious renames later.

[Kevin Buzzard]

Don't you get suggestions for both natCast_ and nat_cast if you just search for natcast?

[Yaël Dillies]

In the docs, yes. In the vscode autocomplete, no

[Kevin Buzzard]

autcomplete.png

Seems to work for me fine in vs code autocomplete?

[Yaël Dillies]

Uh, interesting. Maybe my autocomplete was tired

[Kevin Buzzard]

I always search for all-small-letters-with-no-underscores for this reason

[Johan Commelin]

Eric Wieser said:

Johan Commelin, can you explain why you voted differently between the two polls?

Oops, I messed up. Adjusted my vote. (This came up during dinner at CIRM, but I forgot to go online afterwards and make the fix.)

[Jireh Loreaux]

Dinner at CIRM I think you mean! :laughing:

[Johan Commelin]

Thanks! Fixed

[Floris van Doorn]

Looking at this thread, the main argument I saw for nat_cast is that it would be confusing to spell "cast" as upper case, and the main argument for natCast is that we use _ to separate definition names, and should not use it within a definition name.

The poll is not as decisive as I would like, but since this poll is over a year old, we should make a decision. Since consistency is important and we're currently mixing all kinds of naming conventions, I'm merging #11637 as a step towards the (slightly) more popular option.

[Yaël Dillies]

Let me remind you that #11486 and #11499 are still up

[Yaël Dillies]

Nevermind I see Floris is a mind-reader :grinning: