Module 4 · Lesson 2

Implementing Instances

Instances connect types to type classes. Learn to write them for your own types and understand how Lean resolves them.

Basic Instance Syntax

Declare an instance with instance:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Anonymous instance (most common)
6instance : ToString Point where
7  toString p := s!"({p.x}, {p.y})"
8
9-- Named instance (useful for debugging)
10instance instBEqPoint : BEq Point where
11  beq p1 p2 := p1.x == p2.x && p1.y == p2.y
12
13#eval toString (Point.mk 3.0 4.0)  -- "(3.0, 4.0)"
14#eval Point.mk 1.0 2.0 == Point.mk 1.0 2.0  -- true

Implementing Common Type Classes

BEq: Equality

The BEq type class provides the == operator. You implement the beq method which takes two values and returnstrue if they should be considered equal.

lean

1inductive Color where
2  | red | green | blue
3
4instance : BEq Color where
5  beq c1 c2 := match c1, c2 with
6    | .red, .red => true
7    | .green, .green => true
8    | .blue, .blue => true
9    | _, _ => false
10
11#eval Color.red == Color.red    -- true
12#eval Color.red == Color.blue   -- false

Ord: Ordering

The Ord type class enables the comparison operators<, >, <=, and >=. You implement compare which returns .lt, .eq, or .gt.

lean

1instance : Ord Color where
2  compare c1 c2 := match c1, c2 with
3    | .red, .red => .eq
4    | .red, _ => .lt
5    | .green, .red => .gt
6    | .green, .green => .eq
7    | .green, .blue => .lt
8    | .blue, .blue => .eq
9    | .blue, _ => .gt
10
11#eval compare Color.red Color.blue  -- .lt
12#eval Color.green < Color.blue      -- true

Hashable

The Hashable type class enables using your type as keys inHashMap and elements in HashSet. You must ensure that equal values produce equal hashes.

lean

1instance : Hashable Color where
2  hash c := match c with
3    | .red => 0
4    | .green => 1
5    | .blue => 2

Repr: Debug Representation

The Repr type class controls how values appear in #evaloutput and debugging. Unlike ToString, Repr typically shows the constructor form so you can copy-paste the output back as valid code.

lean

1instance : Repr Point where
2  reprPrec p _ := s!"Point.mk {p.x} {p.y}"
3
4#eval (Point.mk 1.0 2.0 : Point)  -- Point.mk 1.0 2.0

Instances for Parameterized Types

When your type has parameters, instances can require constraints on those parameters:

lean

1structure Pair (α β : Type) where
2  fst : α
3  snd : β
4
5-- Require both types to have BEq
6instance [BEq α] [BEq β] : BEq (Pair α β) where
7  beq p1 p2 := p1.fst == p2.fst && p1.snd == p2.snd
8
9-- Now this works for any Pair of equatable types
10#eval Pair.mk 1 "a" == Pair.mk 1 "a"   -- true
11#eval Pair.mk 1 "a" == Pair.mk 2 "a"   -- false

Key Takeaway

Instance constraints propagate: if Pair needs BEqfor its elements, then Pair Nat String works becauseNat and String have BEq instances.

Recursive Instances

lean

1-- Instance for List requires instance for elements
2instance [BEq α] : BEq (List α) where
3  beq xs ys := match xs, ys with
4    | [], [] => true
5    | x :: xs, y :: ys => x == y && beq xs ys
6    | _, _ => false
7
8#eval [1, 2, 3] == [1, 2, 3]   -- true
9#eval [1, 2] == [1, 2, 3]     -- false

Using deriving

For simple types, deriving generates instances automatically:

lean

1-- Derive multiple instances at once
2structure Person where
3  name : String
4  age : Nat
5  deriving Repr, BEq, Hashable
6
7-- Works immediately
8#eval Person.mk "Alice" 30 == Person.mk "Alice" 30  -- true
9#eval repr (Person.mk "Bob" 25)  -- Person.mk "Bob" 25
10
11-- For inductive types too
12inductive Status where
13  | pending
14  | active
15  | completed
16  deriving Repr, BEq, Hashable, Ord

💡

Use deriving when possible—it's less error-prone than manual instances. Write manual instances for custom behavior.

Default Method Implementations

Type classes can provide default implementations:

lean

1class Printable (α : Type) where
2  format : α → String
3  -- Default implementation using format
4  print : α → IO Unit := fun x => IO.println (format x)
5
6-- Only need to implement format
7instance : Printable Nat where
8  format n := s!"Number: {n}"
9
10-- print comes for free
11#eval (Printable.print 42 : IO Unit)  -- prints "Number: 42"

Instance Priority

When multiple instances could apply, priority determines which wins:

lean

1-- Lower number = higher priority (tried first)
2instance (priority := high) : ToString Bool where
3  toString b := if b then "yes" else "no"
4
5instance (priority := low) : ToString Bool where
6  toString b := if b then "1" else "0"
7
8-- The high priority instance wins
9#eval toString true  -- "yes"

Debugging Instance Search

If Lean can't find an instance, the error message points to the missing class. Check whether you forgot to import a module or define an instance.

Deep Dive: Instance Search

When Lean sees x == y, it:

Determines the type of x
Searches for a BEq instance for that type
If the type has parameters, recursively finds instances for them
Uses the found instance to call BEq.beq

This happens at compile time, so there's no runtime overhead.

Orphan Instances

An "orphan instance" is an instance for a type you don't own, in a module that doesn't define the type or the class. Use with caution:

lean

1-- In your module: instance for external type
2-- This is an "orphan" - can cause conflicts
3
4instance : ToString (List Nat) where
5  toString xs := s!"[{String.intercalate ", " (xs.map toString)}]"
6
7-- Better: wrap in your own type
8structure MyList (α : Type) where
9  items : List α
10
11instance [ToString α] : ToString (MyList α) where
12  toString xs := s!"MyList: {xs.items}"

⚠

Orphan instances can conflict if another library defines the same instance. Prefer wrapping types or defining instances where the type is defined.

Exercise: BEq for a Structure

Define a BEq instance for a simple structure.

lean

1structure User where
2  id : Nat
3  name : String
4
5instance : BEq User where
6  beq a b := a.id == b.id && a.name == b.name
7
8#eval ({ id := 1, name := "A" } : User) == { id := 1, name := "A" }

The Concept Next: Custom Type Classes