ENnReal

Stream: mathlib4

[Scott Morrison]

This is coming up in comments already: what is the mathlib4 capitalisation of ennreal? I think it is probably ENnReal, but ... It's going to be weird whatever we do.

[Eric Rodriguez]

Shouldn't non-neg get the LT/LE treatment?

[Richard Osborn]

It seems like the naming convention needs to make a distinction between initialisms (such as LT, LE, NE) and abbreviations (such as Eq, Comm). If ENN is an initialism for Extended Non-Negative then it would make sense to capitalize all letters.

[Scott Morrison]

Okay! I like that more.

[Scott Morrison]

maybe one day we can fix the Ne in core. :-)

[Yaël Dillies]

Why not just Ennreal?

[Johan Commelin]

I think you know the reason. You just don't agree with it.

[Eric Wieser]

EnNrEaL /s

[Yaël Dillies]

I understand we have a new naming convention, but we should seriously consider whether it's appropriate when mathlib names are already settled as one atom.

[Marc Huisinga]

Richard Osborn said:

It seems like the naming convention needs to make a distinction between initialisms (such as LT, LE, NE) and abbreviations (such as Eq, Comm). If ENN is an initialism for Extended Non-Negative then it would make sense to capitalize all letters.

One informal rule that I see occasionally in programming is to decapitalize longer initialisms, especially when they can be understood without every letter being capitalized. E.g. IDProvider may stay as such, but JSONProvider is converted to JsonProvider. I believe that this makes it easier to identify the separate words in a name.

Personally, I usually only fully capitalize initialisms of two characters, and decapitalize everything that's longer. However, in Lean 4 core there is a precedent for decapatilizing all initialisms, e.g. JSON, XML and LSP or ID. Types like RBMap are still fully capitalized though, which makes me think that capitalizing initialisms of length 2 is fine.
Applying this rule here would lead to EnnReal.

Edit: Ah, ID is obviously also an abbreviation and not an initialism, so it makes sense that it's capitalized differently from RBMap.

[Eric Wieser]

Usually in programming you don't have initialism which are suffices of one another; the EnnReal and NNReal produced with your heuristic feel rather inconsistent.

[Eric Wieser]

ENNReal/NNReal seems like the best choice to me, since it preserves the fact you can swap between the two by adding/removing a single character

[Andrew Yang]

It is probably just me not accustomed to the new naming convention, but I still find it a bit of a pain to distinguish abbreviations from acronyms and Props from Types when naming and using stuff for a non-native english speaker / non type-theorist.

[Yaël Dillies]

What exactly does this new convention bring us? It seems like it makes clashes much less likely, but we were not running out of names.

[Jireh Loreaux]

I actually prefer ENNReal to ennreal or any other variant. When I was new to mathlib I was trying to familiarize myself with the library and the initialism didn't immediately jump out to me, so it would probably be helpful for newcomers (or those with only a passing interest) to more easily distinguish this.

[Kevin Buzzard]

Types start with capital letters, terms start with small letters. The type/term distinction is something which new users have to learn and this makes it easier

[Yaël Dillies]

But what does initialism bring us? This is a linguistically blurry line. I'm sure "radar" is some maths object out there and we'll want to call it Radar (assuming it's a type), but the new convention argues for RaDAR.

[Yaël Dillies]

Similarly, it wants us to call a "laser" type LASER, not Laser.

[Kevin Buzzard]

I'm just not interested in this argument. Telling the core Lean people that their ideas are not what you want is not a helpful way to proceed. We have a port to do.

[Yaël Dillies]

How is what the core Lean people's opinion relevant here? We are deciding on a mathlib naming convention, not a Lean naming convention.

[Yaël Dillies]

My opinion is that we should resynthesize all initials in type names as being part of the radical.

[Andrew Yang]

But many times whether something is a Type or a Prop is an implementation detail. For example, full is a Type, faithful is a Prop, is_limit is a Type, is_pullback is a Prop, is_split_mono is a Prop, is_left_adjoint is a Type etc.

[Andrew Yang]

Do we really want FullSpec and faithful_spec?

[Jireh Loreaux]

Yaël, we should definitely align mathlib naming conventions (at least overall) with Lean core.

[Yaël Dillies]

Why though? There's no shame in admitting that a naming convention used by the core library doesn't scale to a million lines maths library.

[Jireh Loreaux]

A few reasons:

1. Consistency
2. We use things from Core and Std
3. It helps with disambiguation

If at certain points we need to make exceptions, then that can be considered.

[Richard Osborn]

Andrew Yang said:

But many times whether something is a Type or a Prop is an implementation detail. For example, full is a Type, faithful is a Prop, is_limit is a Type, is_pullback is a Prop, is_split_mono is a Prop, is_left_adjoint is a Type etc.

This seems like a separate naming issue. To me, it makes sense to have faithful renamed to is_faithful precisely since it is a Prop. Similarly, is_limit should just be named limit (or Limit in mathlib4). It seems reasonable to have a distinction between Type and Prop.

[Johan Commelin]

Andrew Yang said:

Do we really want FullSpec and faithful_spec?

The big benefit is that we will be able to tell from the name whether it is a type or a prop!

[Arien Malec]

"Standards are like toothbrushes. Everybody wants one but nobody wants to use anyone else's." -- Connie Morella

[Richard Osborn]

I should probably mention that under the current naming convention all the examples listed are classes, so they would be translated into Full, Faithful, Limit, Pullback, SplitMono, and LeftAdjoint.

[Johan Commelin]

Does it not matter whether the class is a predicate or data-carrying? That's a pity.

[Reid Barton]

It doesn't make sense to remove is from is_noun. It changes the meaning completely and the noun version is probably already in use for the other thing.

[Reid Barton]

e.g. docs#category_theory.left_adjoint, docs#category_theory.is_left_adjoint

[Andrew Yang]

But it seems like this is the naming convention used by the core, and we seem to have decided to follow it no matter what.

[Andrew Yang]

In your example, they will be named CategoryTheory.leftAdjoint and CategoryTheory.LeftAdjoint, so there won't be a name collision in this case.

[Scott Morrison]

No, that doesn't sound right.

[Scott Morrison]

My understanding was that these were just changing to LeftAdjoint and IsLeftAdjoint, and then if you wanted to construct a LeftAdjoint for a Foo it would probably be called Foo.leftAdjoint.

[Scott Morrison]

What is the suggestion that category_theory.left_adjoint should become CategoryTheory.leftAdjoint based on?

[Andrew Yang]

It is (D ⥤ C) -> (C ⥤ D) which is a term and should be lowerCamelCase if I didn't misunderstand the naming convention?

[Reid Barton]

There are even two things left_adjoint could mean:

• left_adjoint C D = type of all left adjoints from C to D
• left_adjoint F = the left adjoint of a functor F

Distinguishing these through capitalization could be sensible. But the is_ prefix is an important part of the English meaning, we can't just drop it.

[Reid Barton]

In is_adjective, the is_ is redundant.

[Scott Morrison]

Oh, sorry, I'm wrong, and didn't actually read the examples.

[Scott Morrison]

I agree about category_theory.left_adjoint changing to CategoryTheory.leftAdjoint. It is not a type, but a thing you do to a functor equipped with a typeclass. (Yes, crappy design, but that's not the topic today. :-)

[Reid Barton]

I don't mind left_adjoint becoming leftAdjoint, but is_left_adjoint cannot be called LeftAdjoint.

[Reid Barton]

Same for is_limit

[Reid Barton]

(I guess "adjoint" maybe isn't the best possible example, considering that in ordinary English it is actually an adjective.)

[Scott Morrison]

Where did this "we're getting rid of is_" start? We're getting rid of has_ for notational typeclasses to match core, but I'm not sure that there was any plan to go beyond that.

[Andrew Yang]

examples being docs#is_lawful_monad -> docs4#LawfulMonad I guess?

[Reid Barton]

I think the category theory library is a bit special in that it uses nouns as types for bundled structures, as in normal mathematical English, rather than as classes containing only structure. For example M : category_theory.monad C means that M is a monad (docs#category_theory.monad; compare docs#monad).

[Arien Malec]

Lean 4 is sort of inconsistent here: is_lawful_foo mostly maps to LawfulFoo, but IsLawfulSingleton is a thing

[Arien Malec]

Is there a clean standard for when is_foo/has_foo should/should not be replaced by Foo?

[Reid Barton]

I kind of think is_lawful_foo is a Foo-scoped version of is_lawful.

[Reid Barton]

If you're already writing foo X to mean "X is a foo" (e.g. foo = group) then LawfulFoo X seems fine.

[Andrew Yang]

By the way, is_limit will be translated to IsLimit regardless. It is not a typeclass.

[Reid Barton]

Oh it never occurred to me that is_left_adjoint might be a type class.

[Thomas Murrills]

If you're already writing foo X to mean "X is a foo" (e.g. foo = group) then LawfulFoo X seems fine.

In those cases, does Foo X mean that X carries a Foo structure, and g : Foo X is the actual Foo as data? If so I think that’s qualitatively different than LawfulFoo X : Prop (which is what we see in e.g. LawfulMonad)

[Thomas Murrills]

(if not, though, then I agree :) )

[Richard Osborn]

There are around 40 classes already ported as "IsThing", so there isn't a strong push to drop "is" from class names. It sounds like there are arguments for both sides.

[Reid Barton]

I agree that for classes it's a bit murkier as you don't tend to name inhabitants of a class.

[Arien Malec]

I made updates in the wiki to clarify the case of def Foo: Type := sorry, and toned down the Lean 4 typeclass section. It would be helpful to replace the "<?>" there.

[Sebastian Ullrich]

LawfulMonad is a mistake we haven't corrected yet. It should definitely have an Is.