instance names

Stream: mathlib4

[Henrik Böving]

I'm currently porting Algebra.Ring.Prodwhich starts of with a giant header of declarations of this style:

/-- Product of two distributive types is distributive. -/
instance [Distrib R] [Distrib S] : Distrib (R × S) :=
  { Prod.hasAdd, Prod.hasMul with
    left_distrib := fun a b c => mk.inj_iff.mpr ⟨left_distrib _ _ _, left_distrib _ _ _⟩
    right_distrib := fun a b c => mk.inj_iff.mpr ⟨right_distrib _ _ _, right_distrib _ _ _⟩ }

/-- Product of two `non_unital_non_assoc_semiring`s is a `non_unital_non_assoc_semiring`. -/
instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
    NonUnitalNonAssocSemiring (R × S) :=
  { Prod.addCommMonoid, Prod.mulZeroClass, Prod.distrib with }

/-- Product of two `non_unital_semiring`s is a `non_unital_semiring`. -/
instance [NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S) :=
  { Prod.nonUnitalNonAssocSemiring, Prod.semigroup with }

I'm assuming Lean 3 had some unhygienic instance naming mechanism that made this type of stuff possible? How am I supposed to deal with it in the port, I guess I could just move through the responsible prod files and make the names explicit but having an explicit nonUnitalNonAssocSemiring seems a little over the top?

[Yakov Pechersky]

Use inferInstanceAs?

[Ruben Van de Velde]

Lean 4 also has implicit instance names, but they're even longer. We've not settled on a preferred approach yet

[Mario Carneiro]

yeah, instance names are not hygienic (unless you declare them in a macro, but that's probably an issue of its own)

[Yury G. Kudryashov]

You can also drop some (sometimes all) dependencies and let Lean automatically find projections from existing instances.

[Eric Wieser]

In the port of Algebra.Ring.Pi we just give explicit names to all the instances

[Eric Wieser]

I think we should do the same for Prod

[Gabriel Ebner]

Mario Carneiro said:

yeah, instance names are not hygienic (unless you declare them in a macro, but that's probably an issue of its own)

They're actively anti-hygienic, even when you have the instance command in a macro. If you give the instance command accessible names, then it will generate an accessible inaccessible instance name:

structure Foo
macro "foo_inst" : command => `(instance : Nonempty Foo := ⟨⟨⟩⟩)
foo_inst
#check instNonemptyFoo -- works (no comment on the prettiness/usefulness of the name)

That seems reasonable enough. But the automatically generated name will always be accessible, even if the names contain macro scopes:

macro "bar_inst" : command => `(structure Bar instance : Nonempty Bar := ⟨⟨⟩⟩)
bar_inst
#check instNonemptyBar -- works too ?!?

[Mario Carneiro]

I assume the instance is hygienic if you actually give it a name though like

structure Foo
macro "foo_inst" : command => `(instance inst : Nonempty Foo := ⟨⟨⟩⟩)
foo_inst

[Gabriel Ebner]

Yes, of course. That's the same as @[instance] def.

[Yury G. Kudryashov]

What "hygienic" means in this context?

[Gabriel Ebner]

"Hygienic" means that you can only access it from the the same macro scope where you defined it. Or put differently, if you have two macros that generate the same name, it won't clash.

macro "foo" : command =>
  `(def n := 42
    #print n)

foo -- 42
foo -- 42
#print n -- unknown constant n

[Yaël Dillies]

Ruben Van de Velde said:

Lean 4 also has implicit instance names, but they're even longer. We've not settled on a preferred approach yet

Any news on that front? image.png

[Eric Wieser]

Can we have a mathlib_instance keyword that uses the old naming heuristic? These long names aren't helpful when debugging typeclass diamonds

[Eric Wieser]

I recently made a (now-merged) PR that added manual names to a lot of Prod algebra instances, because the generated names were so mangled they were actively misleading!

[Arien Malec]

An "unnamed instance" lint would also be helpful...

[Eric Wieser]

Something to consider here; In lean3 instance some_name : some_class was the same as @[instance] protected some_name : some_class. In lean4, it seems the result is no longer protected...

[Yury G. Kudryashov]

If we add mathlib_instance, then it should make the definition protected.

[Scott Morrison]

It's easy to get a list of all the X.Y.instZ declarations in mathlib4. How about we just go through and give them sensible names?

[Scott Morrison]

We could additionally have a linter that forbids giant names under Mathlib..

[Eric Wieser]

By "under Mathlib." I assume you mean "in files under Mathlib/" as opposed to "in namespaces under Mathlib."

[Scott Morrison]

Yes

[Scott Morrison]

The relevant code for looking up where a declaration is defined treats the module as a Name, so you get the dot-separated names you'd use to import the file. Hence Mathlib..

[Scott Morrison]

Okay !4#3122 adds commands #long_instances, which shows you instances with excessively long names, grouped according to the file they are in. It also begins cleaning up some of the >80 character names!

[Eric Wieser]

Before we start expend much more effort manually naming everything; which convention do we prefer?

[Eric Wieser]

/poll What names should we pick for instances?

• MyType.fooBar for FooBar MyType, to match what we did in Lean 3
• MyType.instFooBar for FooBar MyType, to match what Lean 4 does automatically

[Eric Wieser]

One argument for the latter is that after dropping the has prefix on typeclass names, we end up with things called MyType.one which are probably confusing for newcomers who assume that's the spelling of 1.

[Moritz Doll]

is the issue with automatically protecting instances resolved?

[Eric Wieser]

Not yet

[Eric Wieser]

Arguably the need for it disappears with an inst prefix

[Moritz Doll]

I am very much in favor of the first option, but I am afraid that version runs into serious problems without @[protected]

[Eric Wieser]

It's much less problematic than it was in Lean3, because at least the instance name is no longer the same as the instance type

[Jireh Loreaux]

Moritz Doll said:

I am very much in favor of the first option, but I am afraid that version runs into serious problems without @[protected]

Yes, I already ran into this once for docs4#Star, because then it gets named MyType.star (unprotected), which is a problem in the MyType namespace because Star.star is exported.

[Scott Morrison]

Okay, so it does look like we like the inst prefix (and the porting meeting just now seemed in favour, as well).

[Scott Morrison]

I'm finding plenty of examples where I don't know what the best name is (leaving aside the inst prefix). Here are some examples. I've added the namespaces by hand, even though they are not always immediately visible in the source.

instance TrivSqZeroExt.addSemigroup [AddSemigroup R] [AddSemigroup M] : AddSemigroup (TrivSqZeroExt R M)
instance Subalgebra.toSemiring {R A} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Semiring S
instance Associates.uniqueUnits : Unique (Associates α)ˣ
instance Multiset.fintypeCoe : Fintype m
instance addGroupIsAddTorsor (G : Type _) [AddGroup G] : AddTorsor G G
instance Rack.oppositeRack : Rack Rᵐᵒᵖ
instance AlgEquiv.applyMulSemiringAction : MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁
instance AlgHom.coeOutRingHom : CoeOut (A →ₐ[R] B) (A →+* B)
instance AlgHom.coeOutMonoidHom : CoeOut (A →ₐ[R] B) (A →* B)
instance NeZero.one : NeZero (1 : PartENat)
instance Finite.Set.finite_union (s t : Set α) [Finite s] [Finite t] : Finite (s ∪ t : Set α)
instance Sigma.Lex.denselyOrdered_of_noMaxOrder [Preorder ι] [∀ i, Preorder (α i)] [∀ i, DenselyOrdered (α i)] [∀ i, NoMaxOrder (α i)] : DenselyOrdered (Σₗ i, α i)

[Scott Morrison]

The first two, TrivSqZeroExt.addSemigroup and Subalgebra.toSemiring seem uncontroversial to me.

[Scott Morrison]

(Although noting that I think we would plan to add inst to the first but not the second!)

[Scott Morrison]

The next two, Associates.uniqueUnits and Multiset.fintypeCoe I think are correct?

[Scott Morrison]

After that I'm not at all sure.

[Scott Morrison]

If anyone would like to propose preferred names for these, either with or without a rubric that justifies them, that might be useful. :-)

[Eric Wieser]

addGroupIsAddTorsor -> AddGroup.toAddTorsor to match Semiring.toModule

[Eric Wieser]

Rack.oppositeRack -> MulOpposite.(inst)Rack to match MulOpposite.(inst)Monoid

[Eric Wieser]

applyMulSemiringAction is part of a collection of similar names, so whatever we pick all should be renamed together.

[Scott Morrison]

Actually, is Subalgebra.toSemiring correct? It's not really a "should have come from an extends clause" case at all, and arguably would be better as Subalgebra.semiringCoe?

[Eric Wieser]

Not sure how I feel about the Coe suffix, but I agree that the current pattern is bad

[Eric Wieser]

I think elsewhere we insert the word subtype in the instance name (maybe for coerced sets?)

[Scott Morrison]

Maybe this one should just be Subalgebra.semiring. The invisible coercion can be invisible in the name.

[Eric Wieser]

A better example might be to consider the semiring of submodules vs the additive group of submodule subtypes

[Eric Wieser]

I guess the former could be submodule.instSemiring while the latter submodule.addCommGroup, which at least makes them obviously distinct

[Scott Morrison]

Sorry, I don't understand that pair of examples. What is "the additive group of submodule subtypes"?

[Scott Morrison]

Do you just mean the AddCommGroup structure on an individual submodule? (Whereas the first is an instance where the "points" are themselves submodules?)

[Pol'tta / Miyahara Kō]

Oh, I forgot to refer to this thread.
I have been following this convention from now.

[Moritz Doll]

I've stumbled upon quite a few instances that are not named in the Foo.instBar style. Is there an easy way to find all named instances? They are probably quite a lot but hopefully less than the ~4000 unnamed instances

[Eric Wieser]

I would imagine it's straightforward to find all instances with names that don't start with inst. I don't know if you can inspect whether the name was autogenerated.

[Sebastian Ullrich]

I wrote a bit about different potential naming schemes at https://github.com/leanprover/lean4/issues/2343#issuecomment-1652005640. At this point I have two main questions to users on my mind:

• Do we consider referencing unnamed (and more broadly, even named) instances a necessary evil due to various technical limitations? Should we work on lifting these limitations even if we still keep a way to reference these instances as a fallback?
• When a reference is necessary, how do people actually discover the name of an unnamed instance? Is it mostly through the info view/pp.explicit of a working term?

[Eric Wieser]

a necessary evil due to various technical limitations?

It's not really even a technical limitation. If I want to tell someone "yes, mathlib knows the fact that endomorphisms form a ring", I would like to be able to link to the instance in the docs, which means I need to know its name.

[Sebastian Ullrich]

"How do we want to link to unnamed things" is also a great general question. I assume that apart from instances, notations are our most prevalent source of unnamed declarations, which use an entirely different naming heuristic that fortunately does not seem to have led to issues... so far

[Sebastian Ullrich]

It would be great to have a "Copy docgen URL/shortlink" context menu action in the editor that lets us skip the manual name lookup step

[Eric Wieser]

Linking to notations can probably be resolved by having doc-gen show info about a notation under the head symbol of the thing it generates

[Eric Wieser]

When a reference is necessary, how do people actually discover the name of an unnamed instance? Is it mostly through the info view/pp.explicit of a working term?

Putting the cursor over the word instance does the job.

[Sebastian Ullrich]

Ok, if you've already located the instance. I wasn't sure from which end people usually trace back their search to the name of an instance.

[Eric Wieser]

In Lean3 we'd go via the infoview as you suggest with example : Foo := by show_term { apply_instance }. This is useless in Lean 4 since it just prints inferInstance, but obviously #synth works instead.

[Sebastian Ullrich]

At that point aren't you one more hover away from the instance name?

[Eric Wieser]

Yes; though I'd argue that the infer_instance tactic would be more useful if it unfolded the inferInstance term like Lean3 did.

[Jon Eugster]

Sebastian Ullrich said:

• When a reference is necessary, how do people actually discover the name of an unnamed instance? Is it mostly through the info view/pp.explicit of a working term?

Mostly I read instance names while debugging with set_option Meta.trace.synthInstance true (or sth like that) trying to figure out why and where the wrong instances were used or why it couldnt find one at all.
For that it's very useful if the instances have a short, manageable name as the debugging is already hard enough to read as is:face_with_monocle:

I think in any case where I ever needed to use an unamed instance I would rather just explicitely name it instead

[Sebastian Ullrich]

As "naming things" famously is one of the hardest problems of CS and I really don't want to commit to a solution that affects hundreds of lines of mathlib before making sure we never have to do that again, how about attacking a simpler end of the issue first?
image.png

[Eric Wieser]

Even with the better rendering, that still gives a tonne of irrelevant matches just due to the sheer name length

[Sebastian Ullrich]

The matching algorithm really should not consider these relevant matches but I don't know enough about it to judge the complexity of changing it in that way

[Sebastian Ullrich]

Alternatively, anonymous instance names could be hidden from display and search completely in doc-gen if there is agreement that their named use should at least be minimized. That is, they should be displayed closer to how they're actually written down in the source.

[Yury G. Kudryashov]

What's our current policy about instance names: use the autogenerated names? overwrite them with something more readable?

[Yury G. Kudryashov]

@Anatole Dedecker told me to rename instances in #7028. I think that we should have some policy and implement it everywhere.

[Anatole Dedecker]

My personal policy is to rename them if they are bad enough

[Eric Wieser]

I think @Scott Morrison's policy was "if you're ever going to refer to them by name, give them an explicit name"

[Jireh Loreaux]

I think we should just fix the name generator. (to behave more like Lean 3)

[Yaël Dillies]

I'm personally naming all my instances to Type.instTypeclass (for which that pattern applies).

[Eric Wieser]

I think we already established that was the preferred naming

[Yury G. Kudryashov]

It would be nice if the name generator used Type.instTypeclass unless a definition with this name exists.

[Kevin Buzzard]

You should add your comments to the open lean 4 issue about this lean4#2343

[Eric Wieser]

Yury G. Kudryashov said:

It would be nice if the name generator used Type.instTypeclass unless a definition with this name exists.

Checking "does this exist already" doesn't work, because two files that don't import each other would use the same name, and then you'd get an error when you import both

[Yury G. Kudryashov]

So, what should I do in #7028: rename or not? Autogenerated names are long.

[Yury G. Kudryashov]

Renamed.

[Utensil Song]

I was looking at a relatively short long instance name, and it seems to be very redundant:

image.png

then I found this topic and lean4#2343 , am I reading it correctly that such a long name is only for avoiding name clash? So I made a suggestion on the issue, to auto-generate names like doc#LinearMap.instModuleLinearMap_3e71a6e which should remain readable and search-friendly for its prefix and much less likely to clash due to the cryptographic properties of the hash algorithm. Am I missing something?

[Utensil Song]

BTW. I'm curious about where is this name generator implemented, and is this naming convention already started to grow into people's (manual) naming habits?

[Damiano Testa]

I think that the convention is that if you want to refer to the instance by name, then you name it explicitly and you bypass the auto-named monsters.

As you can see from the thread, there are longer term, more automated plans, but human-naming is currently the best automation!

[Eric Wieser]

and is this naming convention already started to grow into people's (manual) naming habits?

Definitely not! The extent is that we agreed that instance names should start with inst. After the word inst, we've been using the lean3 heuristics by hand.

[Utensil Song]

It's just it seems that anywhere I go into a doc or perform a search, the marvelous long names appear. I thought there is a good reason but avoiding name clash is too technically a reason versus quality of life.

[Utensil Song]

leanprover/doc-gen4#156

[Kevin Buzzard]

Yeah, if you misspell or fail to fully-quality something in docs (e.g. Anatole wrote docs#Metrizable recently) then the output is heavily polluted right now; this is one of the reasons that prompted me to open lean4#2343 .