#Typeclasses

Typeclasses are (parametrized) types that can be used as implicit arguments. Terms of such types are called instances.

What is special about these are:

• Instances can be synthesized by Lean.
• It is expected that an instance, if it exists, is unique for a given type.

Formally, a class is a type defined with the same syntax as a structure, but with the class keyword. The instances are defined with the instance keyword.

class Alone : Type

• alone : Bool

instance instAlone : Alone

Equations

• instAlone = { alone := true }

At its simplest, typeclass synthesis is just search.

instance extra : Alone

Equations

• extra = { alone := false }

def myAlone {alone : Alone} : Bool

Equations

• myAlone = Alone.alone

Parameters with type typeclasses can be inferred. This is stronger than implicit arguments. Implicit arguments are inferred from the type.

The class syntax is just a shorthand for defining a structure with one field and annotating it. Annotations modify the environment, but do not affect the elaboration process. More precisely, they modify environmental extensions.

class Alone' : Type

• alone : Bool

instance instAlone' : Alone'

Equations

• instAlone' = { alone := true }

We can also have inductive typeclasses.

class inductive Alone'' : Type

• mk : Bool → Alone''

BasePoint class

This associates a basepoint to a type.

class BasePoint (α : Type u) : Type u

• basePoint : α

instance instBasePointString : BasePoint String

Equations

• instBasePointString = { basePoint := "hello" }

def basePoint (α : Type u) [BasePoint α] : α

Gives the basepoint of a type with a BasePoint instance.

Equations

• basePoint α = BasePoint.basePoint

instance instBasePointList {α : Type u} : BasePoint (List α)

Equations

• instBasePointList = { basePoint := [] }

instance prodBasePoint {α β : Type u} [BasePoint α] [BasePoint β] : BasePoint (α × β)

Equations

• prodBasePoint = { basePoint := (basePoint α, basePoint β) }

instance basePointZero {α : Type u} [Zero α] : BasePoint α

Equations

• basePointZero = { basePoint := Zero.zero }

instance idBasePoint {α : Type u} : BasePoint (α → α)

Equations

• idBasePoint = { basePoint := id }

@[instance 100]

instance codomainBasePoint {α β : Type u} [BasePoint β] : BasePoint (α → β)

Equations

• codomainBasePoint = { basePoint := fun (x : α) => basePoint β }

Useful typeclasses

instance instHAddStringBool_pfsProgs25 : HAdd String Bool String

Equations

• instHAddStringBool_pfsProgs25 = { hAdd := fun (s : String) (b : Bool) => if b = true then s else "Did you really mean: " ++ s }

def instHAddOfAdd_pfsProgs25 {α : Type} [Add α] : HAdd α α α

Equations

• instHAddOfAdd_pfsProgs25 = { hAdd := Add.add }