naming convention: "inst" in instance names

Stream: mathlib4

[Kenny Lau]

Loogle search: https://loogle.lean-lang.org/?q=%E2%8A%A2+CommMonoid+_

Under usual circumstances, doing instance : CommMonoid _ in a namespace Foo automatically generates the name Foo.instCommMonoid.

However, some existing mathlib definitions that are manually named do not follow this rule, such as Rat.commMonoid.

For the sake of consistency, I would advocate for changing all these instances to have name starting with inst.

(This encompasses all (algebraic) typeclasses, not just CommMonoid)

[Aaron Liu]

What about non-algebraic typeclasses?

[Kenny Lau]

I seldom interact with them.

[Andrew Yang]

I don’t see what the extra inst tells you. Does it tell you that the def is tagged with @[instance] (in that case are you prepending every simp lemma with simp_?) or that AddCommGroup is a type class?

Regarding the autogenerated name, I think autogenerated name should be intentionally worse to discourage people from mentioning it in production ready code and I don’t think their behavior is an indication of anything.

[Thomas Murrills]

Conversely, does the lack of inst tell us that this instance has been intentionally manually named, and thus indicate something about its (intended) usage? :eyes:

[Kenny Lau]

Well, I think my argument here is that as long as the auto-generated names exist, there will be people who treat it as the standard...

But I think you do have a valid point in that we should actually just never mention instance names at all.

In either case, we should have a standard, and removing inst from all instance names will also be a big PR.

(For reference, the other direction is /(?-i)instance [a-hj-z]\w+ :/)

[Thomas Murrills]

Genuine question: why are these instances manually named? I figured it’s because they’re mentioned somewhere in source—but is that true? And if so, is mentioning them necessary/good style, or can we/should we avoid mentioning them like you say?

[Kenny Lau]

because when there is a standard, people will follow it.

(manually naming also avoids the situation where the auto generated name is 200 characters long)

[Kenny Lau]

@Thomas Murrills I think you're in a better position than me to figure out how many instance mentions exist in mathlib

[Thomas Murrills]

Also I do think there could potentially be a meaningful difference in standard between “how an autogenerated name should look” and “how a manually-created name should look”, precisely to signal the difference! :) I’m not sure autogenerated naming should be construed as a standard for manual naming, if they’re intended to have different usages.

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills I think you're in a better position than me to figure out how many instance mentions exist in mathlib

I could do this! :grinning_face_with_smiling_eyes: But before I go to the trouble, I’d like to hear about the intention behind giving these instances manual names in the first place, and whether mentioning them is even a problem.

[Kenny Lau]

Thomas Murrills said:

Also I do think there could potentially be a meaningful difference in standard between “how an autogenerated name should look” and “how a manually-created name should look”, precisely to signal the difference! :) I’m not sure autogenerated naming should be construed as a standard for manual naming, if they’re intended to have different usages.

I agree with this. As above, I said that it is acceptable to me if the rule is "inst for autogenerated name, no inst for manual names", but if this becomes the rule then it should be standardised!

The only situation not acceptable to me is where there is not a standard rule written down somewhere, and then half of the declarations use inst and half don't.

[Kenny Lau]

But then again as a user for discoverability purposes I would prefer if they all have inst even if I don't end up writing them down in the final proof. It's not a good algorithm to "first try inst and then try without inst"

[Ruben Van de Velde]

Why they're named at all

• they're mentioned somewhere
• the original name is confusing or strange or too long (e.g. #31347)
• cargo-culting

Why they're named without inst

• they weren't an instance before
• they got their name in mathlib3

[Thomas Murrills]

Kenny Lau said:

But then again as a user for discoverability purposes I would prefer if they all have inst even if I don't end up writing them down in the final proof. It's not a good algorithm to "first try inst and then try without inst"

Good point; to my mind discoverability concerns could definitely outweigh the importance of signaling intended usage in the tradeoff here. (Or maybe there’s a way to make them start with inst without being the same as the autogenerated name? But I’ll hold off on crossing that bridge.)

[Kenny Lau]

Thomas Murrills said:

Or maybe there’s a way to make them start with inst without being the same as the autogenerated name?

Not sure what you mean here.

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

Also I do think there could potentially be a meaningful difference in standard between “how an autogenerated name should look” and “how a manually-created name should look”, precisely to signal the difference! :) I’m not sure autogenerated naming should be construed as a standard for manual naming, if they’re intended to have different usages.

I agree with this. As above, I said that it is acceptable to me if the rule is "inst for autogenerated name, no inst for manual names", but if this becomes the rule then it should be standardised!

The only situation not acceptable to me is where there is not a standard rule written down somewhere, and then half of the declarations use inst and half don't.

Oh, for sure! :grinning_face_with_smiling_eyes: Are there manually-named instances that start with inst? (I wasn’t aware of these when saying what I said.)

[Kenny Lau]

Thomas Murrills said:

Are there manually-named instances that start with inst?

/(?-i)instance inst[A-Z][a-z]/

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

Or maybe there’s a way to make them start with inst without being the same as the autogenerated name?

Not sure what you mean here.

E.g. use a manual name of something like Rat.inst.commMonoid, Rat.instanceCommMonoid, which would be distinct from an autogenerated-esque Rat.instCommMonoid…

[Kenny Lau]

Then there would still be the same discoverability issue, where I would then need to try Rat.instCommMonoid and then try Rat.instanceCommMonoid. Discoverability means consistency and one single rule.

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

Are there manually-named instances that start with inst?

/(?-i)instance inst[A-Z][a-z]/

Ah, okay, sorry, missed that. On mobile for a couple more minutes; about how many hits are there?

[Kenny Lau]

440 files

[Thomas Murrills]

Kenny Lau said:

Then there would still be the same discoverability issue, where I would then need to try Rat.instCommMonoid and then try Rat.instanceCommMonoid. Discoverability means consistency and one single rule.

Fair, my thought was that both would be able to come up in autocomplete when you typed instCommMonoid thanks to partial matching.

[Kenny Lau]

indeed, but that's not good enough

[Thomas Murrills]

Ruben Van de Velde said:

Why they're named at all

• they're mentioned somewhere
• the original name is confusing or strange or too long (e.g. #31347)
• cargo-culting

Why they're named without inst

• they weren't an instance before
• they got their name in mathlib3

Ok, great! So it seems like we have four reasons for manual naming of instances in general:

• mentioning/usage
• “correcting” the autogenerated name
• historical accident
• cargo culting

I’d like to understand “usage”/“they’re mentioned somewhere” better. Why do instances get mentioned, typically? And should we really be doing so? Why not synthesize it?

Also, my sense is that the primary intention for manual naming without inst for mentioning here is to signal intention and reduce code smell at the point of use (“it’s okay to mention this instance explicitly”). Do people find that to be their experience?

[Kenny Lau]

Thomas Murrills said:

Also, my sense is that the primary intention for manual naming without inst for mentioning here is to signal intention and reduce code smell at the point of use (“it’s okay to mention this instance explicitly”). Do people find that to be their experience?

Not necessarily, sometimes I just do it because I don't trust the auto generator (i.e. it might generate a name that is too long, or it might be fragile in some way (which is related))

[Thomas Murrills]

Okay, but it seems like that falls under “correcting the autogenerated name”. I’m specifically asking about the reason for {manual naming without inst for mentioning}. :)

[Kenny Lau]

ah, my apologies

[Thomas Murrills]

No problem! :)

[Kenny Lau]

for the mentioning part, it might not be for future mentions (i.e. in other files), it might be aimed towards the same file, where I define instMonoid : Monoid ?a under some assumptions, and then under some other assumptions,

instance : CommMonoid ?a where
  __ := instMonoid
  mul_comm := ?b

[Thomas Murrills]

Ok, maybe we can group a mention like that under “mentioning the instance in the typeclass hierarchy” more generally. (Because my guess is that using inst in instance names when it’s used only within other instances would be generally palatable!)

So, the above question is of course refined to: why do we mention instances outside of other instances, and should we really be doing so instead of synthesizing them?

[Kenny Lau]

well, one use case I can imagine is if we have two instances on the same type, on the rare occasion that we want to prove some sort of uniqueness of instances. (To be clear, this is clearly a rare situation, and normally should be avoided at all costs, but some theorems like that still have their usefulness.)

Outside of that use case, I can't see why one would want to mention instance name.

[Andrew Yang]

Kenny Lau said:

for the mentioning part, it might not be for future mentions (i.e. in other files), it might be aimed towards the same file, where I define instMonoid : Monoid ?a under some assumptions, and then under some other assumptions,

instance : CommMonoid ?a where
  __ := instMonoid
  mul_comm := ?b

I assume the right thing to use here is inferInstanceAs (Monoid _)? At least I personally think referring to an instance by its name is a code smell.

[Aaron Liu]

The right thing to do here would to not put the instance there at all and just let Lean infer it (though this doesn't always work)

[Michael Rothgang]

I'm arriving late to the bikeshed, and see 30-something messages, mostly (but not exclusively) by just two users. On a generic open source mailing list, one heuristic would be "side discussion, ignore" --- which I don't want to do since the content seems relevant and I respect both Kenny and Thomas' expertise. However, going over this in detail is not efficient:

@Kenny Lau @Thomas Murrills can you help me by creating a summary of the discussion so far? What did you cover, what conclusions did the two of you arrive at so far?

[Kenny Lau]

@Michael Rothgang

• Issue: currently both instance instGroup : ... and instance group : ... exist, and I want to standardise.
• My opinion: I think instGroup should be chosen for consistency with auto-generated names for the sake of discoverability. It's inefficient for the user to have to first try instGroup and then try group.
• Thomas's opinion: he agrees with me on the discoverability point, but he's also waiting to explore why anyone would manually name instances in the first place.

[Yaël Dillies]

I bother naming instances by hand because, like any declaration in mathlib, following the naming convention makes the declaration more searchable (and, no, the autogenerated instance names are not consistent enough to be their own convention).

[Thomas Murrills]

And to add some context why I want to know: if it turns out there’s a good reason to want to be able to mention manually named instances, there might be a good reason to signal that they are distinct from autogenerated names. Then we can actually analyze the tradeoff between discoverability and distinct manual names.

[Thomas Murrills]

(More generally, I think we shouldn’t change things (e.g. impose a standardization convention) without first fully understanding why things are the way they are in the first place! :) )

[Yaël Dillies]

People have historically replied to my argument above by saying that "It's infer_instance's job to find an instance". But there are many ways in which that can fail (missing assumption, missing import, no cache, not even a lean environment), and an analogous argument could be made of lemmas: "It's exact?'s job to find a lemma", which is (currently) ludicrous given all the constraints on what and how exact? can find something, constraints which aren't unlike those of infer_instance.

[Kenny Lau]

ok, I would like to derail slightly this conversation: should we do def instCommGroup : ... for "local instances"?

[Eric Wieser]

I don't see this mentioned above; a lot of instances are named monoid because they were mathported and that's what we named them in Lean 3

[Thomas Murrills]

Hmm, I don’t think exact? is at all analogous to typeclass synthesis. Shouldn’t instances be set up precisely so that you can access them via typeclass synthesis (as opposed to lemmas, which don’t work that way)?

Also, @Yaël Dillies, is your position then that

1. all instances ought to be named by hand, in an ideal world
2. a name without inst is more discoverable than one with inst (actually, sorry, you didn’t opine on this! What is your position here?)

I’m also trying to understand the circumstances you’re talking about that make it helpful to mention an instance name. Are we talking just about the writing experience (autocomplete, etc.), or are there circumstances where instance names should remain mentioned in Mathlib source?

[Aaron Liu]

sometimes I want to find the instance used to derive something and before I set up a Lean environment and wait 10~30sec for import Mathlib to go through so I can #synth usually I do two or three searches with #loogle first

[Thomas Murrills]

And to emphasize the question about source: the primary reason I could see for not using inst in the name of instances is to signal “this instance name, without inst, is okay to mention in (final, contributed) source with no code smell”.

So, I’m wondering if there are any cases where we want to mention the name of the instance in final source (and not infer it), or if it’s all about discoverability during the writing process.

[Yaël Dillies]

For me, there are two kinds of instances:

• inheritance instances: they are recognisable by the fact that all (important) arguments to their return type are free variables. They are of the form Stronger A -> Weaker A and their name is of the form Stronger.toWeaker, or Stronger.to_weaker if Weaker is Prop-valued.
• structural instances: all the other ones. They are usually of the form ... -> Foo (BarA), where Bar is some kind of functor, and their name is of the form Bar.instFoo. Since this is the "default" kind of instances, not all of them actually have a meaningful Bar to base the name on, but the exceptions are rare (except in category theory).

[Yaël Dillies]

I personally see the instance names in the second category without inst as exceptions that should be gotten rid of, except as always in category theory which does its own thing

[Yaël Dillies]

I also think there is potential to carve out further kinds of instances from the structural ones, to better reflect usage. I do not have a precise suggestion here but, taking category theory again, it seems that a factor for the existing differences is whether the Foo (Bar A) instance is "primarily about" Foo or Bar.

[Eric Wieser]

We also don't have much of a convention for (b : Bar) : SomeClass ↥b at the moment, docs#Submonoid.toMonoid doesn't fit your rule

[Andrew Yang]

I still don't see what the inst tells you. foo (bar A) should just be called foo_bar or foo.bar or bar.foo regardless if foo is a typeclass or not according to the naming convention. If it were an inheritance instance it would be called foo_of_bar or something similar.

[Yaël Dillies]

The issue with Andrew's suggested convention is that usually we're in some namespace (in his example, bar) by the time we want to provide the instance, so foo_bar is out of the question.

[Yaël Dillies]

foo_of_bar for inheritance instances is also not really an option because most such instances are auto-generated with the to name, with no option to rename them

[Robert Maxton]

Personally, I think instances should just follow the same rules as everything else: snake case for prop-valued typeclasses and camel case for typeclasses carrying data.

[Eric Wieser]

I think the purpose of the inst prefix is to explicitly keep names out of the way that users don't want to refer to. Otherwise you end up with a clash between docs#Nat.add and Nat.instAdd (if it existed) etc

[Eric Wieser]

But it's also worth remembering that this inst-prefixing is builtin Lean behavior, and so we should have a stronger argument that perfornal preference for having mathlib choose to diverge from it.

[Eric Wieser]

Of course, you could argue for the Lean behavior to be changed globally, but @Kyle Miller already put a lot of thought into the current naming heuristics, and this would almost certainly just be re-hashing a previous discussion

[Jovan Gerbscheid]

I agree that we should follow the builtin Lean behaviour. That is, start instance names with inst if the autogenerated name also starts with inst. This makes it easy to tell if a definition is an instance or not. And it makes the naming consistent.

[Andrew Yang]

What is the scope of this inst? When Foo (Bar ..) is in the Bar namespace where Bar .. is a type and Foo is a data carrying typeclass, then one names the definition Bar.instFoo?

[Jovan Gerbscheid]

It seems so:

def Bar := Unit

namespace Bar

instance : Add Bar := ⟨fun _ _ => ()⟩

#check Bar.instAdd

[Aaron Liu]

well that's the autogenerated name though the question is what should the manually generated name be

[Jovan Gerbscheid]

The same as the autogenerated name

[Aaron Liu]

but the autogenerated name is sometimes terrible

[Jovan Gerbscheid]

Yes, but I'm talking about this example

[Jovan Gerbscheid]

I don't mind shortening the terribly long names, but I feel like this is orthogonal to the question posed in this thread, namely what the convention is around "inst" in instance names.

[Chris Henson]

Andrew Yang said:

What is the scope of this inst? When Foo (Bar ..) is in the Bar namespace where Bar .. is a type and Foo is a data carrying typeclass, then one names the definition Bar.instFoo?

I think it is reasonable to ask if the manual name should follow the scope of the autogenerated one. I would guess the answer is usually yes, but maybe some exception for scoped instances?