6.1. Class Declarations🔗

Type classes are declared with the Lean.Parser.Command.declaration : commandclass keyword.

syntax

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      class `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId bracketedBinder*
          (extends term,*)? (: term)? where
        (`declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident ::)?
        structFields
      (deriving ident,*)?

Declares a new type class.

The Lean.Parser.Command.declaration : commandclass declaration creates a new single-constructor inductive type, just as if the Lean.Parser.Command.declaration : commandstructure command had been used instead. In fact, the results of the Lean.Parser.Command.declaration : commandclass and Lean.Parser.Command.declaration : commandstructure commands are almost identical, and features such as default values may be used the same way in both. Please refer to the documentation for structures for more information about default values, inheritance, and other features of structures. The differences between structure and class declarations are:

Methods instead of fields: Instead of creating field projections that take a value of the structure type as an explicit parameter, methods are created. Each method takes the corresponding instance as an instance-implicit parameter.
Instance-implicit parent classes: The constructor of a class that extends other classes takes its class parents' instances as instance-implicit parameters, rather than explicit parameters. When instances of this class are defined, instance synthesis is used to find the values of inherited fields. Parents that are not classes are still explicit parameters to the underlying constructor.
Parent projections via instance synthesis: Structure field projections make use of inheritance information to project parent structure fields from child structure values. Classes instead use instance synthesis: given a child class instance, synthesis will construct the parent; thus, methods are not added to child classes in the same way that projections are added to child structures.
Registered as class: The resulting inductive type is registered as a type class, for which instances may be defined and that may be used as the type of instance-implicit arguments.
Out and semi-out parameters are considered: The outParam and semiOutParam gadgets have no meaning in structure definitions, but they are used in class definitions to control instance search.

While Lean.Parser.Command.declaration : commandderiving clauses are allowed for class definitions to maintain the parallel between class and structure elaboration, they are not frequently used and should be considered an advanced feature.

No Instances of Non-Classes

Lean rejects instance-implicit parameters of types that are not classes:

def f [n : invalid binder annotation, type is not a class instance
  Nat
use the command `set_option checkBinderAnnotations false` to disable the checkNat] : n = n := rfl

invalid binder annotation, type is not a class instance
  Nat
use the command `set_option checkBinderAnnotations false` to disable the check

Class vs Structure Constructors

A very small algebraic hierarchy can be represented either as structures (S.Magma, S.Semigroup, and S.Monoid below), a mix of structures and classes (C1.Monoid), or only using classes (C2.Magma, C2.Semigroup, and C2.Monoid):

namespace S
structure Magma (α : Type u) where
  op : α → α → α

structure Semigroup (α : Type u) extends Magma α where
  op_assoc : ∀ x y z, op (op x y) z = op x (op y z)

structure Monoid (α : Type u) extends Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end S

namespace C1
class Monoid (α : Type u) extends S.Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end C1

namespace C2
class Magma (α : Type u) where
  op : α → α → α

class Semigroup (α : Type u) extends Magma α where
  op_assoc : ∀ x y z, op (op x y) z = op x (op y z)

class Monoid (α : Type u) extends Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end C2

S.Monoid.mk and C1.Monoid.mk have identical signatures, because the parent of the class C1.Monoid is not itself a class:

S.Monoid.mk.{u} {α : Type u}
  (toSemigroup : S.Semigroup α)
  (ident : α)
  (ident_left : ∀ (x : α), toSemigroup.op ident x = x)
  (ident_right : ∀ (x : α), toSemigroup.op x ident = x) :
  S.Monoid α

C1.Monoid.mk.{u} {α : Type u}
  (toSemigroup : S.Semigroup α)
  (ident : α)
  (ident_left : ∀ (x : α), toSemigroup.op ident x = x)
  (ident_right : ∀ (x : α), toSemigroup.op x ident = x) :
  C1.Monoid α

Similarly, because neither S.Magma nor C2.Magma inherits from another structure or class, their constructors are identical:

S.Magma.mk.{u} {α : Type u} (op : α → α → α) : S.Magma αC2.Magma.mk.{u} {α : Type u} (op : α → α → α) : C2.Magma α

S.Semigroup.mk, however, takes its parent as an ordinary parameter, while C2.Semigroup.mk takes its parent as an instance implicit parameter:

S.Semigroup.mk.{u} {α : Type u}
  (toMagma : S.Magma α)
  (op_assoc : ∀ (x y z : α),
    toMagma.op (toMagma.op x y) z = toMagma.op x (toMagma.op y z)) :
  S.Semigroup α

C2.Semigroup.mk.{u} {α : Type u} [toMagma : C2.Magma α]
  (op_assoc : ∀ (x y z : α),
    toMagma.op (toMagma.op x y) z = toMagma.op x (toMagma.op y z)) :
  C2.Semigroup α

Finally, C2.Monoid.mk takes its semigroup parent as an instance implicit parameter. The references to op become references to the method C2.Magma.op, relying on instance synthesis to recover the implementation from the C2.Semigroup instance-implicit parameter via its parent projection:

C2.Monoid.mk.{u} {α : Type u}
  [toSemigroup : C2.Semigroup α]
  (ident : α)
  (ident_left : ∀ (x : α), C2.Magma.op ident x = x)
  (ident_right : ∀ (x : α), C2.Magma.op x ident = x) :
  C2.Monoid α

Parameters to type classes may be marked with gadgets, which are special versions of the identity function that cause the elaborator to treat a value differently. Gadgets never change the meaning of a term, but they may cause it to be treated differently in elaboration-time search procedures. The gadgets outParam and semiOutParam affect instance synthesis, so they are documented in that section.

Whether a type is a class or not has no effect on definitional equality. Two instances of the same class with the same parameters are not necessarily identical and may in fact be very different.

Instances are Not Unique

This implementation of binary heap insertion is buggy:

structure Heap (α : Type u) where
  contents : Array α
deriving Repr

def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
  if h : i = 0 then xs
  else if h : i ≥ xs.contents.size then xs
  else
    let j := i / 2
    if Ord.compare xs.contents[i] xs.contents[j] == .lt then
      Heap.bubbleUp j {xs with contents := failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.798
inst✝ : Ord α
i : Nat
xs : Heap α
h✝ : ¬i = 0
h : ¬i ≥ xs.contents.size
j : Nat := i / 2
⊢ sorry < xs.contents.sizecould not synthesize default value for parameter 'hi' using tacticscould not synthesize default value for parameter 'hj' using tacticsfailed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.798
inst✝ : Ord α
i : Nat
xs : Heap α
h✝ : ¬i = 0
h : ¬i ≥ xs.contents.size
j : Nat := i / 2
⊢ sorry < xs.contents.sizexs.contents.swapα:Type ?u.798inst✝:Ord αi:Natxs:Heap αh✝:¬i = 0h:¬i ≥ xs.contents.sizej:Nat := i / 2⊢ sorry < xs.contents.size invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor 
  Nat⟨i, by omega⟩ invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor 
  Nat⟨j, by omega⟩}
    else xs

def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
  let i := xs.contents.size
  {xs with contents := xs.contents.push x}.bubbleUp i

The problem is that a heap constructed with one Ord instance may later be used with another, leading to the breaking of the heap invariant.

One way to correct this is to making the heap type depend on the selected Ord instance:

structure Heap' (α : Type u) [Ord α] where
  contents : Array α

def Heap'.bubbleUp [inst : Ord α] (i : Nat) (xs : @Heap' α inst) : @Heap' α inst :=
  if h : i = 0 then xs
  else if h : i ≥ xs.contents.size then xs
  else
    let j := i / 2
    if inst.compare xs.contents[i] xs.contents[j] == .lt then
      Heap'.bubbleUp j {xs with contents := failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.327
inst : Ord α
i : Nat
xs : Heap' α
h✝ : ¬i = 0
h : ¬i ≥ xs.contents.size
j : Nat := i / 2
⊢ sorry < xs.contents.sizecould not synthesize default value for parameter 'hi' using tacticscould not synthesize default value for parameter 'hj' using tacticsfailed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.327
inst : Ord α
i : Nat
xs : Heap' α
h✝ : ¬i = 0
h : ¬i ≥ xs.contents.size
j : Nat := i / 2
⊢ sorry < xs.contents.sizexs.contents.swapα:Type ?u.327inst:Ord αi:Natxs:Heap' αh✝:¬i = 0h:¬i ≥ xs.contents.sizej:Nat := i / 2⊢ sorry < xs.contents.size invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor 
  Nat⟨i, by omega⟩ invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor 
  Nat⟨j, by omega⟩}
    else xs

def Heap'.insert [Ord α] (x : α) (xs : Heap' α) : Heap' α :=
  let i := xs.contents.size
  {xs with contents := xs.contents.push x}.bubbleUp i
invalid 'end', insufficient scopesend A

In the improved definitions, Heap'.bubbleUp is needlessly explicit; the instance does not need to be explicitly named here because Lean would select the indicated instances nonetheless, but it does bring the correctness invariant front and center for readers.

6.1.1. Sum Types as Classes🔗

Most type classes follow the paradigm of a set of overloaded methods from which clients may choose freely. This is naturally modeled by a product type, from which the overloaded methods are projections. Some classes, however, are sum types: they require that the recipient of the synthesized instance first check which of the available instance constructors was provided. To account for these classes, a class declaration may consist of an arbitrary inductive type, not just an extended form of structure declaration.

syntax

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      class inductive `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig)*
      (deriving ident,*)?

Class inductive types are just like other inductive types, except they may participate in instance synthesis. The paradigmatic example of a class inductive is Decidable: synthesizing an instance in a context with free variables amounts to synthesizing the decision procedure, but if there are no free variables, then the truth of the proposition can be established by instance synthesis alone (as is done by the decide tactic).

6.1.2. Class Abbreviations🔗

In some cases, many related type classes may co-occur throughout a codebase. Rather than writing all the names repeatedly, it would be possible to define a class that extends all the classes in question, contributing no new methods itself. However, this new class has a disadvantage: its instances must be declared explicitly.

The Lean.Parser.Command.classAbbrev : commandExpands ``` class abbrev C <params> := D_1, ..., D_n ``` into ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ```class abbrev command allows the creation of class abbreviations in which one name is short for a number of other class parameters. Behind the scenes, a class abbreviation is represented by a class that extends all the others. Its constructor is additionally declared to be an instance so the new class can be constructed by instance synthesis alone.

Class Abbreviations

Both plusTimes1 and plusTimes2 require that their parameters' type have Add and Mul instances:

class abbrev AddMul (α : Type u) := Add α, Mul α

def plusTimes1 [AddMul α] (x y z : α) := x + y * z

class AddMul' (α : Type u) extends Add α, Mul α

def plusTimes2 [AddMul' α] (x y z : α) := x + y * z

Because AddMul is a Lean.Parser.Command.classAbbrev : commandExpands ``` class abbrev C <params> := D_1, ..., D_n ``` into ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ```class abbrev, no additional declarations are necessary to use plusTimes1 with Nat:

37#eval plusTimes1 2 5 7

However, plusTimes2 fails, because there is no AddMul' Nat instance—no instances whatsoever have yet been declared:

#eval failed to synthesize
  AddMul' ?m.22
Additional diagnostic information may be available using the `set_option diagnostics true` command.plusTimes2 2 5 7

failed to synthesize
  AddMul' ?m.22
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Declaring an very general instance takes care of the problem for Nat and every other type:

instance [Add α] [Mul α] : AddMul' α where

37#eval plusTimes2 2 5 7