Module 4 · Lesson 1

The Concept of Type Classes

Type classes enable ad-hoc polymorphism—writing functions that work with any type that provides certain operations.

The Problem: Ad-Hoc Polymorphism

Consider printing values. Different types need different printing logic:

lean

1-- We want one "show" function that works for many types
2-- But each type has different logic:
3
4def showNat (n : Nat) : String := toString n
5def showBool (b : Bool) : String := if b then "true" else "false"
6def showList (xs : List Nat) : String := s!"[{xs}]"
7
8-- Tedious! We want:
9-- show 42        → "42"
10-- show true      → "true"
11-- show [1,2,3]   → "[1, 2, 3]"

The issue: we want show to work on any type, but with type-specific behavior. This is called ad-hoc polymorphism.

Type Classes: The Solution

A type class declares an interface. Types implement that interface via instances:

lean

1-- Define what it means to be "showable"
2class Show (α : Type) where
3  show : α → String
4
5-- Implement for specific types
6instance : Show Nat where
7  show n := toString n
8
9instance : Show Bool where
10  show b := if b then "true" else "false"
11
12-- Now we can use show generically
13#eval Show.show 42      -- "42"
14#eval Show.show true    -- "true"

Key Takeaway

Type classes separate what operations exist (the class) from howthey're implemented (the instances). This enables generic programming.

Using Type Classes in Functions

Functions can require types to have certain instances:

lean

1-- [Show α] means "α must have a Show instance"
2def greet [Show α] (x : α) : String :=
3  s!"Hello, {Show.show x}!"
4
5#eval greet 42       -- "Hello, 42!"
6#eval greet true     -- "Hello, true!"
7
8-- Multiple constraints
9def compare [Ord α] [Show α] (x y : α) : String :=
10  match Ord.compare x y with
11  | .lt => s!"{Show.show x} < {Show.show y}"
12  | .eq => s!"{Show.show x} = {Show.show y}"
13  | .gt => s!"{Show.show x} > {Show.show y}"

Standard Type Classes

ToString

lean

1-- Built-in, used by string interpolation
2class ToString (α : Type) where
3  toString : α → String
4
5-- This is why s!"x = {x}" works
6#eval s!"value: {42}"        -- "value: 42"
7#eval s!"flag: {true}"       -- "flag: true"

BEq (Boolean Equality)

lean

1class BEq (α : Type) where
2  beq : α → α → Bool
3
4-- Enables == operator
5#eval 5 == 5     -- true
6#eval "a" == "b" -- false

Ord (Ordering)

lean

1class Ord (α : Type) where
2  compare : α → α → Ordering
3
4-- Ordering is: .lt, .eq, or .gt
5-- Enables <, >, <=, >= operators
6#eval compare 5 3    -- .gt
7#eval 5 < 3          -- false

Hashable

lean

1class Hashable (α : Type) where
2  hash : α → UInt64
3
4-- Used by HashMap, HashSet
5#eval hash "hello"   -- some UInt64

Instance Resolution

Lean automatically finds the right instance based on types:

lean

1-- Lean figures out which Show instance to use
2#eval Show.show 42      -- Uses Show Nat
3#eval Show.show "hi"    -- Uses Show String
4
5-- This happens at compile time
6def printTwice [Show α] (x : α) : String :=
7  let s := Show.show x  -- Lean picks the instance
8  s ++ ", " ++ s

ℹ

Instance resolution is automatic. You don't pass instances explicitly—Lean finds them based on the types involved.

Deriving Instances

Many instances can be auto-generated:

lean

1-- deriving generates instances automatically
2structure Point where
3  x : Int
4  y : Int
5  deriving Repr, BEq, Hashable
6
7-- Now these work:
8#eval repr (Point.mk 1 2)            -- Shows the structure
9#eval Point.mk 1 2 == Point.mk 1 2   -- true

Deep Dive: Type Classes vs Interfaces

Type classes are similar to interfaces in OOP but more powerful:

Retroactive conformance: You can add instances for types you don't own
Multi-parameter: Classes can involve multiple types
Associated types: Classes can have type members
Default implementations: Classes can provide default methods

Where Instances Come From

lean

1-- 1. Built-in instances (Nat, Bool, String, etc.)
2#eval (5 : Nat) == 5   -- BEq Nat exists
3
4-- 2. Derived instances
5structure RGB where
6  r : UInt8
7  g : UInt8
8  b : UInt8
9  deriving BEq
10
11-- 3. Your own instances
12instance : ToString RGB where
13  toString c := s!"rgb({c.r}, {c.g}, {c.b})"
14
15-- 4. Instances from libraries
16-- (Importing a library may bring instances into scope)

Error Handling Next: Implementing Instances