TYPECLASSES IN MATHLIB

Lean Seminar 2026

TYPECLASSES IN MATHLIB

  1. Mathlib, its missions and design considerations

  2. Typeclass use in Mathlib

  3. Optimising typeclass synthesis in Mathlib

  4. Hazards of typeclass use

  5. Type synonyms

TYPECLASSES IN MATHLIB

  1. Mathlib, its missions and design considerations

Mathlib, its mission and design considerations

One of Mathlib's aim is to unify different areas of mathematics into a convenient mathematical library for formalising current research in mathematics.

Examples:

Fermat's Last Theorem.

Carleson's Project.

With this philosophy in mind, we explore some of the usages of typeclasses and the obstacles that might arise.

TYPECLASSES IN MATHLIB

  1. Mathlib, its missions and design considerations

  2. Typeclass use in Mathlib

  3. Optimising typeclass synthesis in Mathlib

  4. Hazards of typeclass use

  5. Type synonyms

TYPECLASSES IN MATHLIB

  1. Typeclass use in Mathlib

2. Typeclass use in Mathlib

In mathematics, it is often the case that objects have similar properties and behave in analogous ways.

Consider the structures Set, Finset, Subgroup, Submonoid, Flag and friends

These structures all share in common lemmas like:

example {S : Type*} {H K : Set S} : H < K ↔ H ≤ K ∧ ∃ x ∈ K, x ∉ H := example {S : Type*} {H K : Finset S} : H < K ↔ H ≤ K ∧ ∃ x ∈ K, x ∉ H := example {G : Type*} [Group G] {H K : Subgroup G} : H < K ↔ H ≤ K ∧ ∃ x ∈ K, x ∉ H := example {M : Type*} [Monoid M] {H K : Submonoid M} : H < K ↔ H ≤ K ∧ ∃ x ∈ K, x ∉ H := example {C : Type*} [LE C] {H K : Flag C} : H < K ↔ H ≤ K ∧ ∃ x ∈ K, x ∉ H :=

This is a lot of duplicated code.

2. Typeclass use in Mathlib

Problem: Maintaining all these lemmas is tedious. If refactors happen, all these lemmas might need to be updated.

Solution: Recall one of the crowning jewels in Mathlib's design.

2. Typeclass use in Mathlib

The Filter structure.

Among other things, the Filter abstraction reduced 512 lemmas involving compositions of limits into a single lemma

theorem Tendsto.comp {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} (hg : Tendsto g y z) (hf : Tendsto f x y) : Tendsto (g ∘ f) x z :=

Dealing with code duplication and capturing an essential pattern in mathematics.

Of course, Filter is a structure, not a typeclass. But we can do the same with typeclasses!

2. Typeclass use in Mathlib

As you probably suspected, all of the structures: Set, Finset, Subgroup, Submonoid, Flag and friends

look very SetLike 🤔

Indeed so! All structures have a registered SetLike instance, so it suffices to prove the desired lemma once.

variable {A B : Type*} [SetLike A B] [PartialOrder A] [IsConcreteLE A B] {p q : A} in theorem lt_iff_le_and_exists : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p := by

Of course we don't register a SetLike instance on Set! Otherwise this would yield a cycle.

2. Typeclass use in Mathlib

We can do the same for morphisms which extend the structures like the MonoidHom structure.

We can create classes like MonoidHomClass, MulHomClass which take the FunLike class as a parameter.

To have lemmas like:

theorem map_mul [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y := MulHomClass.map_mul f x y theorem map_mul_eq_one [MulOne M] [MulOne N] [FunLike F M N] [MonoidHomClass F M N] (f : F) {a b : M} (h : a * b = 1) : f a * f b = 1 := by rw [← map_mul, h, map_one]

OUTLINE - TYPECLASSES IN MATHLIB

  1. Mathlib, its missions and design considerations

  2. Typeclass use in Mathlib

  3. Optimising typeclass synthesis in Mathlib

  4. Hazards of typeclass use

  5. Type synonyms

TYPECLASSES IN MATHLIB

  1. Optimising typeclass synthesis in Mathlib

Bundling vs. Unbundling

3. Optimising typeclass synthesis in Mathlib

Indeed, typeclasses like SetLike, FunLike, EquivLike, MonoidHomClass are extremely convenient and reduce a lot of code duplication.

However, challenges arise as Mathlib scales.

Mathlib must be fast.

Instance synthesis accounts for 10 to 25 percent of the build time for a typical Mathlib file.

Instance synthesis algorithm to fail, it must have explored the entire search space.

3. Optimising typeclass synthesis in Mathlib

For instance, consider the following code snippet:

inductive P inductive Q example (p : P) : Q := p

As expected this example results an error.

But what was surprising at the time, is that this took 250ms to fail.

At the time, classes like MulHomClass were set up in the following way:

class MulHomClass (F : Type*) (M N : outParam (Type*)) [Mul M] [Mul N]
  extends DFunLike F M fun _ => N where
  ...

3. Optimising typeclass synthesis in Mathlib

When peaking under the hood to see what was taking so long, we see that after triggering a typeclass search for CoeT P p Q.

Typeclass search goes crazy once it applies the FunLike.hasCoeToFun.

[tryResolve] ✅ CoeFun P fun x ↦ (a : ?m.146) → ?m.147 a ≟ CoeFun P fun x ↦ (a : ?m.146) → ?m.147 a
[] new goal FunLike P _tc.2 _tc.3 ▼
  [instances] #[@ZeroHomClass.toFunLike, @AddHomClass.toFunLike, @OneHomClass.toFunLike, @MulHomClass.toFunLike, @EmbeddingLike.toFunLike, @RelHomClass.toFunLike, @StarHomClass.toFunLike, @SMulHomClass.toFunLike, @TopHomClass.toFunLike, @BotHomClass.toFunLike, @SupHomClass.toFunLike, @InfHomClass.toFunLike, @NonnegHomClass.toFunLike, @SubadditiveHomClass.toFunLike, @SubmultiplicativeHomClass.toFunLike, @MulLEAddHomClass.toFunLike, @NonarchimedeanHomClass.toFunLike, @sSupHomClass.toFunLike, @sInfHomClass.toFunLike, @ContinuousMapClass.toFunLike, @LocallyBoundedMapClass.toFunLike, @SpectralMapClass.toFunLike, @DilationClass.toFunLike, @SlashInvariantFormClass.toFunLike]

3. Optimising typeclass synthesis in Mathlib

The solution:

class MulHomClass (F : Type*) (M N : outParam Type*) [Mul M] [Mul N] [FunLike F M N] : Prop where

This refactor resulted in a 33 percent speed up for typeclass instance synthesis.

and an overall 19 percent decrease in build instructions.

3. Optimising typeclass synthesis in Mathlib

In case you were left wondering

The code snippet shown before fails much faster:

#time example (p : P) : Q := p

3. Optimising typeclass synthesis in Mathlib

Consider now the mathematical objects with varying levels of structure:

Mul < Semigroup < Monoid < Group

Preorder < PartialOrder < Lattice < LinearOrder

Last week, we saw that these hierarchies are set up through forgetful inheritance.

But how should these hierarchies interact?

3. Optimising typeclass synthesis in Mathlib

Consider we have to synthesize a CommMonoid instance.

Let's think about two ways we could set up the interaction between the algebraic and order hierarchy:

3. Optimising typeclass synthesis in Mathlib

Bundled

Semi-bundled

[LinearOrdered(Add)CommMonoid α]

[(Add)CommMonoid α] [LinearOrder α] [IsOrdered(Add)Monoid α]

[LinearOrderedCancel(Add)CommMonoid α]

[(Add)CommMonoid α] [LinearOrder α] [IsOrderedCancel(Add)Monoid α]

3. Optimising typeclass synthesis in Mathlib

[Ordered(Add)CommGroup α]

[(Add)CommGroup α] [PartialOrder α] [IsOrdered(Add)Monoid α]

[LinearOrdered(Add)CommGroup]

[(Add)CommGroup α] [LinearOrder α] [IsOrdered(Add)Monoid α]

[OrderedSemiring α]

[Semiring α] [PartialOrder α] [IsOrderedRing α]

3. Optimising typeclass synthesis in Mathlib

[OrderedCommSemiring α]

[CommSemiring α] [PartialOrder α] [IsOrderedRing α]

[OrderedRing α]

[Ring α] [PartialOrder α] [IsOrderedRing α]

[OrderedCommRing α]

[CommRing α] [PartialOrder α] [IsOrderedRing α]

3. Optimising typeclass synthesis in Mathlib

[StrictOrderedSemiring α]

[Semiring α] [PartialOrder α] [IsStrictOrderedRing α]

[StrictOrderedCommSemiring α]

[CommSemiring α] [PartialOrder α] [IsStrictOrderedRing α]

[StrictOrderedRing α]

[Ring α] [PartialOrder α] [IsStrictOrderedRing α]

3. Optimising typeclass synthesis in Mathlib

[StrictOrderedCommRing α]

[CommRing α] [PartialOrder α] [IsOrderedRing α]

[LinearOrderedSemiring α]

[Semiring α] [LinearOrder α] [IsStrictOrderedRing α]

[LinearOrderedCommSemiring α]

[CommSemiring α] [LinearOrder α] [IsStrictOrderedRing α]

3. Optimising typeclass synthesis in Mathlib

[LinearOrderedRing α]

[Ring α] [LinearOrder α] [IsStrictOrderedRing α]

[LinearOrderedCommRing α]

[CommRing α] [LinearOrder α] [IsStrictOrderedRing α]

[LinearOrderedSemifield α]

[Semifield α] [LinearOrder α] [IsStrictOrderedRing α]

3. Optimising typeclass synthesis in Mathlib

[LinearOrderedField α]

[Field α] [LinearOrder α] [IsStrictOrderedRing α]

[NormedLatticeAddCommGroup α]

[NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α]

[NormedOrdered(Add)Group α]

[Normed(Add)CommGroup α] [PartialOrder α] [IsOrdered(Add)Monoid α]

3. Optimising typeclass synthesis in Mathlib

[NormedLinearOrdered(Add)Group α]

[Normed(Add)CommGroup α] [LinearOrder α] [IsOrdered(Add)Monoid α]

[NormedLinearOrderedField α]

[NormedField α] [LinearOrder α] [IsStrictOrderedRing α]

3. Optimising typeclass synthesis in Mathlib

This refactor partitioned the instance search space.

When trying to synthesize a CommMonoid instance.

Before, Lean would try infer this instance by searching through declarations like NormedLinearOrderedField or NormedOrderedGroup.

Now, Lean will only go as far as NormedField and Group.

3. Optimising typeclass synthesis in Mathlib

This decoupling yielded a 20% speedup to typeclass inference time.

Resulting in a 6% overall speedup to Mathlib.

But it does result in more verbose parameters.

Which raises the question:

Should the normed hierarchy be decoupled from the algebraic hierarchy?

And in general, when should one use a bundled or unbundled typeclass design?

TYPECLASSES IN MATHLIB

  1. Mathlib, its missions and design considerations

  2. Typeclass use in Mathlib

  3. Optimising typeclass synthesis in Mathlib

  4. Hazards of typeclass use

  5. Type synonyms

TYPECLASSES IN MATHLIB

  1. Optimising typeclass synthesis in Mathlib

Priorities

3. Optimising typeclass synthesis in Mathlib

As illustrated last week, many hierarchies present diamonds.

Algebraic hierarchy

Diamonds are not always bad. But there are performance considerations to keep in mind.

3. Optimising typeclass synthesis in Mathlib

Consider the toy example covered last week.

Diamond

3. Optimising typeclass synthesis in Mathlib

In code this corresponds to:

set_option linter.unusedVariables false class Base (B : Type u) where base : String class LeftBranch (B : Type u) extends Base B class RightBranch (B : Type u) extends Base B class Diamond (B : Type u) extends LeftBranch B, RightBranch B

3. Optimising typeclass synthesis in Mathlib

Let us define a type which has a Diamond instance

inductive D instance : Diamond D where base := "base"

On the right hand, if we now ask the instance synthesis algorithm to infer that the type D with a Diamond instance has the Base instance, we get the following path:

set_option trace.Meta.synthInstance true in #synth Base D

3. Optimising typeclass synthesis in Mathlib

On the left hand, if we now tweak the priority of the LeftBranch instance

instance (priority := high) {α : Type u} [LeftBranch α] : Base α := inferInstance set_option trace.Meta.synthInstance true in #synth Base D

3. Optimising typeclass synthesis in Mathlib

So far so good.

Our toy example was not too interesting.

But it does illustrate how priorities tell the instance synthesis algorithm to consider certain instances before others.

Consider the "random" definition found in Mathlib

def RestrictScalars.lsmul [Module S M] : S →ₐ[R] Module.End R (RestrictScalars R S M) := -- We use `RestrictScalars.moduleOrig` in the implementation, -- but not in the type letI : Module S (RestrictScalars R S M) := RestrictScalars.moduleOrig R S M Algebra.lsmul R R (RestrictScalars R S M)

3. Optimising typeclass synthesis in Mathlib

def RestrictScalars.lsmul [Module S M] : S →ₐ[R] Module.End R (RestrictScalars R S M) := -- We use `RestrictScalars.moduleOrig` in the implementation, -- but not in the type letI : Module S (RestrictScalars R S M) := RestrictScalars.moduleOrig R S M Algebra.lsmul R R (RestrictScalars R S M)

When we peek into the trace of the instance synthesis algorithm we keep seeing Algebra.id

This is not by chance!

But first, let's do a loogle search.

3. Optimising typeclass synthesis in Mathlib

Algebra Instances

The list indeed goes on.

3. Optimising typeclass synthesis in Mathlib

As we saw, there are many instances of the from Algebra ?R ?S.

As anticipated, Algebra.id has a high priority.

Why?

If it is to fail, it generally fails fast.

If it is to be successful, it is almost surely the instance we want.

3. Optimising typeclass synthesis in Mathlib

Dually, we can also set low priorities for instances which are most likely not going to succeed.

Considering that when searching for algebraic instances we often do not need to search for the Normed hierarchy.

We can set

attribute [instance 200] ESeminormedAddMonoid.toAddMonoid

To have the instance synthesis algorithm explore the Normed hierarchy last.

3. Optimising typeclass synthesis in Mathlib

Summarising,

Set high priorities for instances that are cheap to fail and are often what one wants, as seen with Algebra.id

Set low priorities for instances which are less likely to apply, as seen with ESeminormedAddMonoid.toAddMonoid

However, there are rumours that the typeclass system will be redesigned in some way which will render priority twiddling obsolete.

TYPECLASSES IN MATHLIB

  1. Mathlib, its missions and design considerations

  2. Typeclass use in Mathlib

  3. Optimising typeclass synthesis in Mathlib

  4. Hazards of typeclass use

  5. Type synonyms

TYPECLASSES IN MATHLIB

  1. Hazards of typeclass use

4. Hazards of typeclass use

It is often the case that one deals with diamond like hierarchies when building up mathematical structures.

We saw this for example with the algebraic hierarchy.

Algebraic hierarchy

4. Hazards of typeclass use

If different paths are definitionally equal, this is not a problem.

However, in the following diamond:

Demo image

It is easy to set up the typeclasses in such a way that a bad diamond is produced.

4. Hazards of typeclass use

Consider synthesizing a TopologicalSpace instance on α × β, given two MetricSpace instances.

Consider the "natural" set up for the MetricSpace typeclass.

class BadMetricSpace (α : Type u) : Type u extends Dist α where dist_self : ∀ x : α, dist x x = 0 dist_comm : ∀ x y : α, dist x y = dist y x dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y

4. Hazards of typeclass use

Consider the paths:

MetricSpace α → TopologicalSpace α → TopologicalSpace (α × β)

MetricSpace α → MetricSpace (α × β) → TopologicalSpace (α × β) where d((a_1,b_1) , (a_2, b_2)) = d_{\alpha}(a_1, a_2) \sqcup d_{\beta}(b_1, b_2)

The two topologies are the same mathematically, but not definitionally.

This is a problem.

4. Hazards of typeclass use

The fix.

Inspired by the algebraic hierarchy's forgetful inheritance.

A metric space contains both a distance, a topology, and a proof that the topology coincides with the one coming from the distance.

Furthermore, define the instance MetricSpace α × β with the supremum distance, the product topology and the proof that the topology induced by the metric coincides with the product topology.

Both definitionally equal paths yield the product topology on the product space.

4. Hazards of typeclass use

We set up PseudoMetricSpaces to contain a UniformSpace which in turn contains a TopologicalSpace.

class PseudoMetricSpace (α : Type u) : Type u extends Dist α where dist_self : ∀ x : α, dist x x = 0 dist_comm : ∀ x y : α, dist x y = dist y x dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z /-- Extended distance between two points -/ edist : α → α → ENNReal := fun x y => ENNReal.ofNNReal (.mk (dist x y) (dist_nonneg' _ ‹_› ‹_› ‹_›)) edist_dist : ∀ x y : α, edist x y = ENNReal.ofReal (dist x y) := by intro x y; exact ENNReal.coe_nnreal_eq _ toUniformSpace : UniformSpace α := .ofDist dist dist_self dist_comm dist_triangle uniformity_dist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | dist p.1 p.2 < ε } := by intros; rfl toBornology : Bornology α := Bornology.ofDist dist dist_comm dist_triangle cobounded_sets : (Bornology.cobounded α).sets = { s | ∃ C : ℝ, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C } := by intros; rfl

TYPECLASSES IN MATHLIB

  1. Mathlib, its missions and design considerations

  2. Typeclass use in Mathlib

  3. Optimising typeclass synthesis in Mathlib

  4. Hazards of typeclass use

  5. Registering multiple instances

TYPECLASSES IN MATHLIB

  1. Registering multiple instances

5. Registering multiple instances

Typically, when deciding between whether a mathematical notion should be a class or a structure.

The decision to make it a typeclass often comes down to recognizing whether:

  • We are dealing with a property on a type which we want to use implicitly → class

  • Or whether we are working with an object that belongs to a family of objects → structure

5. Registering multiple instances

Think about Group and Subgroup:

We use Group when we want to work with properties of groups.

We use Subgroup when we want to talk about the Lattice of subgroups of a Group.

But what if:

We want to equip a same type with different properties?

Or, we want to explore the interactions between these properties?

5. Registering multiple instances

In topology, we generally fix a specific topology.

But sometimes we want to reason about non-standard topologies on a type and even, their interactions.

def indiscreteTopology : TopologicalSpace ℕ := ⊤ def discreteTopology : TopologicalSpace ℕ := ⊥ example : ¬ IsOpen[indiscreteTopology] {1} := by intro contr have := TopologicalSpace.isOpen_top_iff {1} simp only [singleton_ne_empty, singleton_ne_univ, or_self, iff_false] at this contradiction example : IsOpen[discreteTopology] {1} := by exact trivial

5. Registering multiple instances

In a similar fashion, consider the natural numbers, ℕ.

One can use the usual ordering on the natural numbers.

example : (0 : ℕ) ≤ (1 : ℕ) := by decide

5. Registering multiple instances

But it is also possible to equip the same type with the dual order.

We do not want competing instances on a same type.

Solution: we use type synonyms such as OrderDual with handy notation to differentiate between them.

example : (1 : ℕᵒᵈ) ≤ (0 : ℕᵒᵈ) := by decide

5. Registering multiple instances

Similarly, we can use type synonyms when using Group actions.

variable {G : Type*} [Group G] /- Left action -/ example (g x : G) : g • x = g * x := rfl open MulOpposite /- Right action -/ example (g : Gᵐᵒᵖ) (x : G) : (g) • x = x * (unop g) := rfl

Conclusion

When working with typeclasses in Mathlib, think of the following things:

Typeclasses can be used to reduce code duplication and capture essential patterns in mathematics as was seen with SetLike and MonoidHomClass.

But we have to be careful with how we (set up)/(declare) our typeclasses for optimisation reasons as was seen:

  • (Bundled/Unbundled) When integrating the algebra, order (, topology, normed, etc.) hierarchies

  • (Priorities) When registering instances like Algebra.id and ESeminormedAddMonoid.toAddMonoid

Conclusion

Furthermore, we have to watch out for bad diamonds like that encountered in the interaction between TopologicalSpace, MetricSpace and Prod.

In this case we should stick as much as we can to forgetful inheritance when extending poorer typeclasses to richer typeclasses.

Finally, one should be aware of type synonyms like OrderDual, MulOpposite and IsOpen[ · ].

References

Anne Baanen et al. “Growing Mathlib: maintenance of a large scale mathematical library”.

Anne Baanen. “Use and Abuse of Instance Parameters in the Lean Mathematical Library”.

Eric Wieser. “Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies”.