RFC: reimplementing `class abbrev`

Need for class abbrev in Mathlib

Some definitions are naturally expressed with a single type class, such as VectorSpace or PID. But, they are implemented as multiple separate type classes, in order to better fit in with the Mathlib type class hierarchy.

This is a problem for people new to Mathlib, because searching for VectorSpace or PID doesn't give any results, and instead you need to remember which exact combination of type classes needs to be used. For more experienced users this is also a problem, because it means that theorems and definitions become longer and more difficult to read. Instead, we can use class abbrev to define them as follows:

class abbrev VectorSpace (K V : Type*) [Semiring K] :=
  AddCommGroup V
  Module K V

class abbrev PID (P : Type*) :=
  CommRing P
  IsDomain P
  IsPrincipalIdealRing P

So then we can write [VectorSpace K V] instead of [AddCommGroup V] [Module K V], and [PID P] instead of [CommRing P] [IsDomain P] [IsPrincipalIdealRing P].

Additionally, Mathlib is moving away from some bundled type classes, with changes like [OrderedRing R] -> [Ring R] [PartialOrder R] [IsOrderedRing R]. Although this gives faster type class search, it is unfortunate that this comes at the cost of readability. With class abbrev, we can again write [OrderedRing R], and in the future similar type class refactors can be done much more easily. In this example:

class abbrev OrderedRing (R : Type*) :=
  Ring R
  PartialOrder R
  IsOrderedRing R

Inefficiency of class abbrev

class abbrev causes inefficient type class search:

class A (n : Nat) where
  x : Nat
class B (n : Nat) where
  y : Nat
class abbrev C (n : Nat) :=
  A n
  B n

instance [A n] : A (n+1) where

#synth B 100000

Here, the search for B 100000 triggers a search for A 100000, which causes an timeout. For class abbrev to be usable in Mathlib, it is important that defining class abbrev C does not significantly slow down the type class search for any other class.

Proposal

I propose that when declaring a class abbrev, the structure projection functions do not get added as instances. This means that a search for B n does not trigger a search for C n (and hence not for A n). Instead, I propose that we maintain the invariant that for any local instance of C n, there are corresponding local instances for A n and B n. The LocalInstances are an array of free variables (as an Expr) that are be considered by type class search (and invisible to the user). This RFC asks to loosen the restriction that the entries have to be a free variable. Instead, for [inst : C n], we would add inst, inst.toA and inst.toB to the LocalInstances.

We should not allow global instances of C n, except for the constructor C.mk, which is tagged as an instance by the class abbrev command.

To implement this, we should define an insertion function for LocalInstances which checks if the className corresponds to a class abbrev. If so, it should recursively insert the projections of the class abbrev into the LocalInstances.

Community Feedback

This RFC was recently discussed at #PR reviews > #28803 refactor: unbundle algebra from `ENormed*`

Some related things were discussed here:

#mathlib4 > Comm vs non-Comm instance design

#mathlib4 > Normed modules @ 💬

Mathlib also has the variable? command which attempts to solve the same problem.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

No files or tests are named. Start by tracing the class abbrev command and LocalInstances handling described in the RFC, then determine how local projections should be inserted without adding global projection instances. Done means class abbrev improves notation while avoiding the demonstrated type-class search timeout.