toType capitalization

Stream: mathlib4

[Violeta Hernández]

We have docs#Multiset.ToType but docs#Ordinal.toType. Which one is correct?

[Michael Rothgang]

Rule 2 in #naming says "ToType" --- the real question is whether this should be a special exception. In any case, these should be consistent.

[Eric Wieser]

Maybe using To at all is wrong, and we should instead use a a name like docs#Set.Elem

[Yury G. Kudryashov]

A loosely related question: should we stop using raw Subtype for coercion of, e.g., Submodules to Type*? It's annoying when simp simplifies x \in LinearMap.ker f to f x = 0 in the type.

[Violeta Hernández]

Ordinal.Elem seems very wrong to me. It feels like overextending the set-theoretic convention of "an ordinal is the set of smaller ordinals" to a setting where it's not even true.

[Violeta Hernández]

Multiset.Elem seems a bit questionable but perhaps justifiable through analogy

[Violeta Hernández]

I've opened #32449 for the ordinal rename

[Matt Diamond]

but the naming docs have Semifield.toIsField as a correct example... wouldn't that indicate that it should be Ordinal.toType?

[Violeta Hernández]

IsField is a Prop, while Type is... a Type

[Matt Diamond]

right, but why capitalize "to"?

[Matt Diamond]

docs#Subfield.toField

[Violeta Hernández]

hmm, I don't know.

[Matt Diamond]

there are a ton of .toX methods where X is a type... docs#Fin.toNat

[Matt Diamond]

there does seem to be a lot of inconsistency in the codebase, where we have some .To methods and some .to methods... maybe someone could write a script that tallies both sides?

[Matt Diamond]

I mean you guys can do what you want but .toX seems more natural and is used by countless .to methods across mathlib that convert between types... I get the sense that .ToX is the outlier here

[Violeta Hernández]

Yeah, you've convinced me

[Violeta Hernández]

I'd like to hear feedback from others, though

[Andrew Yang]

Rule 2 in #naming says that "Props and Types (or Sort) (inductive types, structures, classes) are in UpperCamelCase".

Subfield.toField F is not a Type. Ordinal.toType X is a Type so it should be ToType instead.

[Violeta Hernández]

Oh, I see. So you specifically need an output of type Type

[Matt Diamond]

ah, so the idea is that since Ordinal.ToType returns a Type, it is a type and the whole thing is capitalized?

[Matt Diamond]

perhaps this is just me coming from my software engineering background, where I would consider Ordinal.toType a function that returns a type and not a type itself, but I guess there's really no distinction

[Matt Diamond]

still feels a bit odd to consider Ordinal.ToType as the same kind of thing as Nat or Real

[Andrew Yang]

The idea is that if o : Ordinal then o.ToType should be considered as the same kind of thing as Nat: something that could appear to the right of a :.

[Matt Diamond]

I mean it's really a def that takes an ordinal and returns a type, not the name of a type itself

[Matt Diamond]

I could sort of see it as a type constructor, since it takes in an Ordinal and returns a Type

[Eric Wieser]

By that argument Fin and List are not types

[Matt Diamond]

like I said, I can sort of see it as a type constructor

[Matt Diamond]

though with o.ToType you've already violated the capitalization rule since o is lowercase (and in general you can't control how someone is going to name the ordinal)... so now the rule is "types should be capitalized as much as possible"

[Aaron Liu]

I feel like o.ToType doesn't violate the capitalization rule

[Aaron Liu]

you can tell by the last component of the name that this is a type

[Aaron Liu]

I guess you can also tell by the fact that it's called to type and so would therefore output a type

[Matt Diamond]

I can't think of any other type which can be specified via generalized field notation except for ToType in the codebase (e.g. we can't do n.Fin instead of Fin n)... it feels like a special case

[Matt Diamond]

anyway I can see the arguments for ToType... whatever the outcome is, I think the naming conventions doc should be more explicit about how dot notation factors in

[Aaron Liu]

I feel like there's a lot though

[Aaron Liu]

like docs#Polynomial.Splits

[Aaron Liu]

or docs#Nat.Prime

[Matt Diamond]

Do you have an example that's a Type instead of a Prop? I see your point though

[Aaron Liu]

I think I remember a docs#Con.Quotient or something like that

[Matt Diamond]

alright, that's fair, that's a good example... you could do c.Quotient

[Matt Diamond]

perhaps I would be less opposed if it was Ordinal.Type

[Matt Diamond]

it's having "to" in the name of a type that seems off to me

[Violeta Hernández]

I think it was Ordinal.Type in Lean 3, but got renamed during porting

[Violeta Hernández]

Nope! This is all my fault. #16161

[Andrew Yang]

Or AsType perhaps?

[Matt Diamond]

yeah, that sounds a little better

[Matt Diamond]

but it's okay... we already have CategoryTheory.ToType and so on, I'm not going to complain if we stick to the standard

[Matt Diamond]

at least I understand the decision a bit better now

[Violeta Hernández]

I've been told to make a poll

[Violeta Hernández]

/poll How to call the map Ordinal → Type?
Ordinal.toType
Ordinal.ToType
Ordinal.AsType

[Matt Diamond]

is Ordinal.Type not an option at this point?

[Violeta Hernández]

It would not work without dot notation, but otherwise it seems like a valid identifier name

[Violeta Hernández]

Well this has been a productive poll

[Matt Diamond]

lol

[Matt Diamond]

might as well just go forward with your PR, I didn't mean to gum up the works here

[Jakub Nowak]

I agree with @Matt Diamond that it's not like ToType is some type. It's rather a function that returns a Type.

[Jakub Nowak]

Compare this with e.g. docs#Erased.OutType, where Out is part of the name OutType. Although, maybe out_as_Type (but in lower camel case) makes more sense?

[Kevin Buzzard]

Rule 3 of capitalisation in #naming says that whatever the name is, it needs to be capitalised, so Ordinal.toType is definitely wrong. Explicitly, our established conventions are that functions which return X are capitalised in the same way as X.

[Jakub Nowak]

Rule 3 says they are named as terms of type C. I.e., instances of C. Not as C itself.

[Jakub Nowak]

Ah, wait, instances of Type should be capitalized. So yes, you're right.

[Yaël Dillies]

Kevin Buzzard said:

Explicitly, our established conventions are that functions which return X are capitalised in the same way as X.

But zero : Nat, not Zero : Nat

[Jakub Nowak]

It's zero : Nat, just like you would do n : Nat for any other (instance of) Nat.

[Kevin Buzzard]

Yael you know what I mean -- functions which return a term of type X are capitalised in the same way as terms of type X.

[Yaël Dillies]

Ah, sure, then I agree!

[Jakub Nowak]

But, in my opinion, for rule 3 to make sense, we should also name functions according to what the functions returns, not what the functions does. In which sense toType is wrong, because it describes what the function does, i.e. converting Ordinal to Type.

[Jakub Nowak]

So, in my opinion, we either stick to rule 3 in full, so we name the functions according to what it returns, so the correct name would be Ordinal.Type (or maybe something like Ordinal.EquivType to avoid confusion with Type?), or we make an exception to rule 3, both in naming and styling of the name, in which case Ordinal.toType would be correct.

[Andrew Yang]

ToType also describes what the function returns: The coercion of an ordinal to a type.

[Jakub Nowak]

Andrew Yang said:

ToType also describes what the function returns: The coercion of an ordinal to a type.

And therefore in my opinion it's invalid according to rule 3 of #naming. I don't understand what's your point?

[Kevin Buzzard]

Surely it's valid according to rule 3? What is your logic? It's just the same as e.g. docs#MetricSpace.toEMetricSpace which has a small t because it's returning a term. Here we're using the same word but capitalising because it's returning a type. This is how the naming convention works.

[Jakub Nowak]

"Functions are named the same way as their return values". It means, that the name should be named according to their return value. In toEMetricSpace name, the word to does not have, in any way, relation to it's return value. Rather, it describes the function itself.

[Jakub Nowak]

The rule 3 doesn't solely say, that the name of function should use the same style as the type of the returned value. It says more, it says, to also name the function in a way, that the name of a function describes the return value.

[Jakub Nowak]

So, every to* function in mathlib violates this rule. Now, this is very common, and I don't say to rename all of these functions. Are only say, that it's a valid exception to rule 3, but, because we're making it an exception to rule 3, we should also consider separately the matter of how to style the name in the case of this exception.

[Sébastien Gouëzel]

I don't understand what you say. Rule 3 is only about capitalization. It says: if your function returns a Prop or a Type, use uppercase. Otherwise, use lowercase. No more, no less.

[Jakub Nowak]

Sébastien Gouëzel said:

I don't understand what you say. Rule 3 is only about capitalization. It says: if your function returns a Prop or a Type, use uppercase. Otherwise, use lowercase. No more, no less.

In my opinion, this rule only makes sense, when the name of the function describes the return value.

[Thomas Murrills]

The intent is that the “way” in that rule (and the phrase “named as though it is”) refers only to naming choices that are in scope for the naming convention, i.e. choices about capitalization and underscores. The “meaning” of the name (how it describes the term it refers to) is out of scope for these conventions, and is not intended to be addressed by this rule.

We could perhaps clarify the wording here to make that more explicit. :) (Note: if you were to search far back enough in the zulip, you could see where these naming conventions were discussed, and it would be clear that only capitalization and underscore were meant to be in scope!)

[Jakub Nowak]

I still think, that when people agreed to this rule, they looked at examples of names, where the names described the return value.

[Sébastien Gouëzel]

The wording is already clear: It's in the paragraph General Conventions / Capitalization.

[Thomas Murrills]

Jakub Nowak said:

I still think, that when people agreed to this rule, they looked at examples of names, where the names described the return value.

It’s a reasonable thought based on the wording, but I was there when the rule was written! :) It was in fact just about capitalization and underscores. :grinning_face_with_smiling_eyes:

[Jakub Nowak]

Sébastien Gouëzel said:

The wording is already clear: It's in the paragraph General Conventions / Capitalization.

Yes, you're right. I'm saying, that this rule is wrong in general.

[Jakub Nowak]

It's wrong in general, because it should only be used, when the name of the function describes the return value.

[Sébastien Gouëzel]

That's the rule that has been agreed upon after long discussions. It's not gonna change now.

[Jakub Nowak]

I think there are exceptions to this rules already.

[Thomas Murrills]

Here is a more explicit version of what was intended:

Functions are capitalized the same way as their return values (e.g. a function of type A → B → C is capitalized as though it is a term of type C).

(where we understand “capitalization” to include underscore conventions, of course).

[Andrew Yang]

And therefore in my opinion it's invalid according to rule 3 of #naming. I don't understand what's your point?

I am totally confused. You are saying that "this rule only makes sense, when the name of the function describes the return value." and I am saying that "the name of the function describes the return value".

[Jakub Nowak]

Andrew Yang said:

"the name of the function describes the return value".

Surely it doesn't? If you try to read toEMetricSpace as a sentence, than that sentence cannot be a description of a noun?

[Thomas Murrills]

Jakub Nowak said:

I think there are exceptions to this rules already.

If you find some exceptions (to the intended rules), please bring them up! :) It’s quite possible we’d then want to change those names to bring them in line with the convention (or else mention the exceptions in the convention).

[Jakub Nowak]

Or maybe we should read is x.toEMetricSpace for it to be sentence. But it still doesn't describe the noun.

[Andrew Yang]

As I said, it is the ordinal casted to a type?

[Jakub Nowak]

Ah, yes, you did say it. I understand what you meant now. You might be right, let me think about it.

[Jakub Nowak]

I agree with you @Andrew Yang. I've been trying to read it as just ToType, in which case, I've read it as "cast to type", but I should have read it as Ordinal.ToType or o.ToType, in which case, it's "ordinal casted to type". And with this interpretation, Ordinal.ToType (i.e. with UpperCamelCase) indeed makes sense to me as well.

[Thomas Murrills]

Jakub Nowak said:

Or maybe we should read is x.toEMetricSpace for it to be sentence. But it still doesn't describe the noun.

As a general point, also note that names don’t necessarily have to be sentences when read in full; description is of course a hard problem, so different (classes of) names have to take different strategies to gesture most effectively at their meaning.

In this case, the toB strategy for terms roughly of the form A → B is fairly simple and already widespread, and both of those facts contribute to the effectiveness of its descriptive gesture. It’s also what you get when you say describe the term as “the canonical function from A to B”, so it already appears in some readings of its type; and the information about A is usually redundant in practice (especially given dot notation), so is jettisoned. (At least, those are some factors I can identify at first glance here.) I think you’re right to identify the phrase formed by dot notation as another contributing factor.

I’m glad things all make sense now, though; this message is just some extra thought on the matter. :)

[Andrew Yang]

I agree that if you have defined a function that you would view of mathematically as $C \to \mathbf{Set}$ then there could reasonably be an exception to name it as lower case. However these things doesn't really appear in practice. First of all functions of these kinds are already very rare in mathematics, and in the rare case that they appear, (e.g. the forgetful functor $\mathbf{Ab}\to\mathbf{Set}$), they are usually bundled functions (in this case a docs#CategoryTheory.Functor) so they are automatically lower case (docs#CategoryTheory.forget)

And my point (which I didn't do my best job explaining; but seems like you get it now) was that in this case it is not the function itself that is the main point, we only care about o.ToType for the particular o that we are working on.

[Violeta Hernández]

I don't really want to bikeshed this for too long. Ordinal.ToType works so I'll just go with it.

[Eric Wieser]

What naming do we use for things like docs#ModuleCat ?

[Eric Wieser]

Looks like it's carrier : Type

[Eric Wieser]

For renaming that, it's possibly worth a separate thread that has a title that will attract responses from category theorists.