4. Classes and Typeclasses🔗

4.1. Classes and Typeclasses🔗

A class is a structure that supports typeclass inference.

class DummyClass (α : Type) where
  dummy_object : α

def getDummyObject (α : Type) [DummyClass α] : α :=
  DummyClass.dummy_object

instance : DummyClass Nat where
  dummy_object := 0

0#eval getDummyObject Nat

Mathlib class hierarchy examples:

variable {M : Type} [Monoid M]
variable (a b c : M)

mul_assoc a b c : a * b * c = a * (b * c)#check mul_assoc a b c
one_mul a : 1 * a = a#check one_mul a
mul_one a : a * 1 = a#check mul_one a

variable {M : Type} [CommMonoid M]
variable (a b : M)

mul_comm a b : a * b = b * a#check mul_comm a b

variable {A : Type} [AddCommMonoid A]
variable (x y z : A)

add_assoc x y z : x + y + z = x + (y + z)#check add_assoc x y z
zero_add x : 0 + x = x#check zero_add x
add_zero x : x + 0 = x#check add_zero x
add_comm x y : x + y = y + x#check add_comm x y

variable {R : Type} [Semiring R]
variable (a b c : R)

add_assoc a b c : a + b + c = a + (b + c)#check add_assoc a b c
mul_assoc a b c : a * b * c = a * (b * c)#check mul_assoc a b c
left_distrib a b c : a * (b + c) = a * b + a * c#check left_distrib a b c
right_distrib a b c : (a + b) * c = a * c + b * c#check right_distrib a b c
zero_mul a : 0 * a = 0#check zero_mul a
mul_zero a : a * 0 = 0#check mul_zero a

4.2. Exercises🔗

Define a typeclass DefaultElem with a field defaultElem.
Create an instance DefaultElem Bool.
Define getDefault (α : Type) [DefaultElem α] : α and test it with Bool.