Type Classes

Type classes let Lean infer behaviour automatically. They are the machinery behind +, ==, #eval's printing, and deriving— and once you can write your own, a lot of Lean stops looking like magic.

Learning Goals

• Declare a class and provide instances for several types.
• Write functions that work for any type satisfying a constraint.
• Implement the standard classes: ToString, BEq, Inhabited, Add.
• Give a class a default method and override it.
• Explain what deriving was doing all along.

The Problem Type Classes Solve

You want + to work on Nat, Int, Float, matrices, and your own types. Defining addNat, addInt, addFloat separately means every generic function must be written once per type. A type class instead declares an interface, and lets each type say how it satisfies that interface. Lean then finds the right implementation for you.

Defining a Class

1class Summable (α : Type) where
2  zero : α
3  add  : α → α → α
4
5instance : Summable Nat where
6  zero := 0
7  add := Nat.add
8
9instance : Summable String where
10  zero := ""
11  add := String.append

The class says “a type is Summableif it has a zero and a way to combine two values”. Each instance is the evidence that a particular type qualifies.

Using Instances

Square brackets in a signature mean “require an instance, and find it for me”. You never pass it explicitly.

1def sumPair [Summable α] (x y : α) : α :=
2  Summable.add x y
3
4#eval sumPair 3 4          -- 7
5#eval sumPair "Lean" " 4"  -- "Lean 4"

One definition, two types, no overloading table to maintain. Add an instance for a new type tomorrow and sumPair starts working on it without being touched.

1def sumAll [Summable α] : List α → α
2  | [] => Summable.zero
3  | x :: xs => Summable.add x (sumAll xs)
4
5#eval sumAll [1, 2, 3]           -- 6
6#eval sumAll ["a", "b", "c"]     -- "abc"

The Standard Classes

Most of what felt built-in earlier in the course is an instance of a class you can implement yourself. Here is the same structure gaining printing, equality, a default, and arithmetic.

ToString and Repr

1structure Point where
2  x : Nat
3  y : Nat
4
5instance : ToString Point where
6  toString p := s!"({p.x}, {p.y})"
7
8#eval toString (Point.mk 1 2)          -- "(1, 2)"
9#eval s!"the point is {Point.mk 3 4}"  -- "the point is (3, 4)"
10
11instance : Repr Point where
12  reprPrec p _ := s!"Point({p.x}, {p.y})"
13
14#eval Point.mk 5 6                     -- Point(5, 6)

BEq and Inhabited

1instance : BEq Point where
2  beq a b := a.x == b.x && a.y == b.y
3
4#eval Point.mk 1 2 == Point.mk 1 2   -- true
5#eval Point.mk 1 2 == Point.mk 9 9   -- false
6
7instance : Inhabited Point where
8  default := Point.mk 0 0
9
10#eval (default : Point)              -- Point(0, 0)

Overloading operators

+ is notation for the Add class. Provide the instance and the operator starts working on your type.

1instance : Add Point where
2  add a b := Point.mk (a.x + b.x) (a.y + b.y)
3
4#eval Point.mk 1 2 + Point.mk 10 20   -- Point(11, 22)

The heterogeneous variants let the two operands have different types — scalar multiplication, for instance, where the left side is a Nat and the right is a Point.

1instance : HMul Nat Point Point where
2  hMul k p := Point.mk (k * p.x) (k * p.y)
3
4#eval 3 * Point.mk 1 2   -- Point(3, 6)

Default Methods

A class can supply a default implementation, defined in terms of the other fields. Instances get it for free but may override it.

1class Greeter (α : Type) where
2  name : α → String
3  greet : α → String := fun a => s!"Hello, {name a}!"
4
5structure Dog where
6  nick : String
7
8-- Only supplies name; greet comes from the default
9instance : Greeter Dog where
10  name d := d.nick
11
12#eval Greeter.greet (Dog.mk "Rex")   -- "Hello, Rex!"
13
14structure Robot where
15  id : Nat
16
17-- Overrides the default
18instance : Greeter Robot where
19  name r := s!"unit-{r.id}"
20  greet r := s!"BEEP. UNIT-{r.id} ONLINE."
21
22#eval Greeter.greet (Robot.mk 7)     -- "BEEP. UNIT-7 ONLINE."

Extending Classes

extends builds a class that requires everything the parent requires plus more. An instance of the child automatically provides the parent.

1class Shape (α : Type) where
2  area : α → Nat
3
4class NamedShape (α : Type) extends Shape α where
5  shapeName : α → String
6
7structure Sq where
8  side : Nat
9
10instance : NamedShape Sq where
11  area s := s.side * s.side
12  shapeName _ := "square"
13
14#eval Shape.area (Sq.mk 4)             -- 16
15#eval NamedShape.shapeName (Sq.mk 4)   -- "square"

This is how Lean's algebraic hierarchy is organised: a group is a monoid with inverses, a ring is an additive group plus multiplication, and so on. Each layer states only what it adds.

Constraints Compose

A function can demand several instances at once. It then works for every type that satisfies all of them.

1def describeAll [ToString α] (xs : List α) : String :=
2  xs.map toString |>.foldl (· ++ ·) ""
3
4#eval describeAll [Point.mk 1 1, Point.mk 2 2]   -- "(1, 1)(2, 2)"
5
6def maxOf [LE α] [DecidableLE α] (a b : α) : α :=
7  if a <= b then b else a
8
9#eval maxOf 3 9              -- 9
10#eval maxOf "abc" "abd"      -- "abd"

maxOf needs two things: an ordering (LE) and the knowledge that the ordering can actually be computed (DecidableLE) — a direct callback to the Bool versus Prop split from Level 5. a ≤ b is a proposition; running if on it requires a decision procedure.

What deriving Was Doing

Now the Level 4 shortcut makes sense. deriving generates instances of exactly these classes, following the structure of your type.

1structure Vec2 where
2  a : Nat
3  b : Nat
4deriving Repr, BEq, Inhabited
5
6-- Equivalent to writing three instances by hand
7#eval Vec2.mk 1 2                    -- { a := 1, b := 2 }
8#eval Vec2.mk 1 2 == Vec2.mk 1 2     -- true
9#eval (default : Vec2)               -- { a := 0, b := 0 }

Write instances by hand when you want control over the behaviour — a custom display format, or an equality that ignores a cache field. Otherwise derive.

Practice

1structure Money where
2  cents : Nat
3deriving Repr
4
5instance : Add Money where
6  add a b := Money.mk (a.cents + b.cents)
7
8instance : ToString Money where
9  toString m := s!"${m.cents / 100}.{m.cents % 100}"
10
11#eval Money.mk 250 + Money.mk 175   -- { cents := 425 }
12#eval toString (Money.mk 425)       -- "$4.25"

1class Container (f : Type → Type) where
2  empty : f α
3  insert : α → f α → f α
4  toList : f α → List α
5
6instance : Container List where
7  empty := []
8  insert x xs := x :: xs
9  toList xs := xs
10
11#eval Container.toList
12        (Container.insert 1 (Container.insert 2 (Container.empty : List Nat)))
13-- [1, 2]

Common Mistakes

• Using (inst : C α) instead of [C α]. Round brackets make it an ordinary argument you must pass by hand.
• Referring to a sibling field by bare name inside an instance. Qualify it or use the underlying data.
• Defining a second instance for a type that already has one. No error, but the results change depending on which wins.
• Panicking at “failed to synthesize”. It names the exact instance you need. Usually the fix is one deriving clause.

Check Yourself

• What is the difference between [Summable α] and (s : Summable α)?
• How can Lean resolve Summable.zero when it has no arguments to inspect?
• When would you write Repr by hand instead of deriving it?
• Why does maxOf need DecidableLE and not just LE?