15
$\begingroup$

In the Lean mathlib, I see some places where a typeclass argument is included in a class definition, such as locally_finite_order. In other places, I see the "extends" keyword used, such as ring. What are the differences and tradeoffs between these two ways of doing things?

$\endgroup$

1 Answer 1

13
$\begingroup$

Section 2.2 of Anne Baanen's recent paper Use and abuse of instance parameters in the Lean mathematical library gives a very nice explanation of this, referring to them as "unbundled subclasses" (like locally_finite_order) and "bundled subclasses" (like ring). This paper discusses, in various places, situations where we might prefer one over the other.

One example is in section 5.1. Defining a class

class module (R M : Type) extends add_comm_monoid M := ...

would automatically create an instance that says, "in order to show add_comm_monoid T, it suffices to show module ?x T." Instances like this can lead to huge performance issues, so the preferred pattern here is the unbundled definition:

class module (R M : Type) [add_comm_monoid M] := ...

In the other direction, overuse of unbundled subclasses can lead to performance problems of a different kind (Baanen section 10, or a blog post by Ralf Jung). Full unbundling leads to exponential blowup in the number of type class arguments (and thus searches) needed as you climb a hierarchy of classes. Baanen gives the example:

instance prod.comm_monoid
  [has_one M] [has_one N] [has_mul M] [has_mul N]
  [semigroup M] [semigroup N] [mul_one_class M] [mul_one_class N]
  [monoid M] [monoid N] [comm_semigroup M] [comm_semigroup N]
  [comm_monoid M] [comm_monoid N] :
comm_monoid (M × N) := ...
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.