TC `extends` vs instance-implicit binders

Stream: mathlib4

[Alex Keizer]

I noticed mathlib uses 2 ways to have one typeclass Foo depend on another typeclass Bar: using extends, as in class Foo (a : Type) extends Bar a or to use an instance binder, as in class Foo (a : Type) [Bar a].
I was wondering what the considerations are for when to use either option?
In particular, I noticed some classes that seem to use both, like:

class GMonoid [AddMonoid ι] extends GMul A, GOne A where

[Eric Wieser]

A more understandable case is docs4#Module

[Eric Wieser]

Or docs4#ContinuousMul

[Anne Baanen]

That is a great question! I call the first one "bundled inheritance" and the second "unbundled inheritance" in my paper on classes in mathlib3. To avoid telling you just to RTFM, I'll try and write the summary:

[Anne Baanen]

Bundled inheritance is generally cleaner to read and write: instead of [Semiring R] [AddCommMonoid M] [Module R M] it would be nicer to just write [SemiModule R M]. The shorter notation also has practical advantages beyond aesthetics: unbundled inheritance causes exponential blowup of term size as your algebraic hierarchy grows deeper. So the rule of thumb in mathlib is to bundle by default, unless there is a good reason to avoid it:

Bundled inheritance requires that the parameter list of the subclass is a subset of the superclass's: Module R M depends on both R and M, so the hypothetical instance Module R M → AddCommMonoid M generated by extends cannot apply reliably since Lean would have to guess a suitable value for R. This is the main reason for unbundling.

The secondary reason for unbundling is that you'd get a combinatorial explosion of potential bundled classes: a multiplication operator could be Comm or not, Assoc or not, Cancel or not, etc... So we use unbundled mixins like docs4#IsDomain (replacing, back in mathlib3 the previous domain and integral_domain class with one is_domain class).

A final consideration new for Lean 4 is that the handling of outParam is different (IMO, worse), so classes like docs4#SetLike will have unbundled subclasses like docs4#SubmonoidClass. (Once the port is done I plan to do the same for docs4#FunLike which currently still uses bundled inheritance.)

[Gabriel Ebner]

A final consideration new for Lean 4 is that the handling of outParam is different (IMO, worse)

Can you elaborate on that remark? Little has changed in outParams specifically. (Or do you mean the whole {} vs. [] thing?)

[Gabriel Ebner]

There's another crucial feature of ("semi"-)unbundled classes that I don't think you mentioned explicitly in the ITP paper. Namely that when have [SemiModule R M] [SemiModule R N], we want the same semiring structure on R and R. If the semiring structure is unbundled, then we get this for free because we only have a single [Semiring R] argument. But if SemiModule was fully bundled then those would be two unrelated (and possibly different) semiring structures.

[Eric Wieser]

I think this probably falls into the "combinatorial explosion" argument, in that you can fix it with [SemiModule2 R M N]

[Gabriel Ebner]

A related issue is that we can't define a [SemiModule2 R M N] : SemiModule R M instance.

[Eric Wieser]

Ah, but that issue _is_ mentioned in Anne's post above :)

[Alex Keizer]

The typeclass that prompted this question from me is

class MvQPF {n : ℕ} (F : TypeVec.{u} n → Type _) [MvFunctor F] where

There aren't many other typeclasses that apply to TypeVec n -> Type _, and the MvFunctor typeclass has the same parameter as MvQPF, so this seems like a prime example of where bundling would be appropriate, right?

[Yury G. Kudryashov]

Anne Baanen said:

Once the port is done I plan to do the same for docs4#FunLike which currently still uses bundled inheritance.

What do you think about my proposal !4#2202?

[Yury G. Kudryashov]

I saw that you've reacted to my Zulip message but I'm bad at translating smiles into words.

[Anne Baanen]

Gabriel Ebner said:

A final consideration new for Lean 4 is that the handling of outParam is different (IMO, worse)

Can you elaborate on that remark? Little has changed in outParams specifically. (Or do you mean the whole {} vs. [] thing?)

This is the {} vs [] thing, specifically taking an instance depending on an outParam that can't be found through unification.

[Anne Baanen]

Yury G. Kudryashov said:

Anne Baanen said:

Once the port is done I plan to do the same for docs4#FunLike which currently still uses bundled inheritance.

What do you think about my proposal !4#2202?

Thank you for the reminder! It looks very interesting and neat, specifically the approach to moving design patterns (bundled morphisms and their associated typeclasses) into code (the BundledHom structure). I have not had a chance to test it out yet, so I can't tell whether my initial thoughts apply in practice, and you have thought of most of my concerns.

Still, I'm somewhat wary of the (p : (A → B) → Prop) predicates as parameters to the classes. These can have quite nontrivial equalities and equivalences that typeclasses cannot see through, or see through only very slowly. For example: if someone writes a monoid hom when an additive hom is expected, will Lean end up trying to unify * with +? This tends to get expensive quite quickly. Quite probably, we're okay as long as we stick to predicates of the form structure IsMonoidHom extends IsMulHom, IsOneHom (rather than IsMonoidHom := IsMulHom ∧ IsOneHom; we'd also avoid issues that would arise if someone writes the predicate as IsOneHom ∧ IsMulHom ).

[Yury G. Kudryashov]

Could you please add this concern to the issue?

[Yury G. Kudryashov]

Is*Hom should be structures but we should have automation that runs mk_iff, then use it to define instances for comp/id/whatever.

[Anne Baanen]

Comment added! I'll try and make some time this afternoon to experiment with your proposal, maybe see if I can manage to redefine MonoidHom.