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 := toString 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}"

Implicit Instance Arguments

Instance arguments are implicit. You can pass them explicitly with @when debugging instance resolution.

lean

1def showTwice [Show α] (x : α) : String :=
2  s!"{Show.show x}, {Show.show x}"
3
4#eval showTwice 7

Standard Type Classes

ToString

The ToString type class powers string interpolation. Any type with a ToString instance can be embedded ins!"..." strings.

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)

The BEq type class enables the ==and != operators. It defines a single methodbeq that returns a Bool.

lean

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

Ord (Ordering)

The Ord type class provides comparison operators. Itscompare method returns an Orderingvalue: .lt, .eq, or .gt.

lean

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

Hashable

The Hashable type class is required for using a type as keys in HashMap or elements in HashSet.

lean

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

Functor

Functor provides map for transforming values inside a container:

lean

1class Functor (f : Type → Type) where
2  map : (α → β) → f α → f β
3
4-- map transforms the value inside
5#eval Functor.map (· + 1) (some 5)     -- some 6
6#eval Functor.map (· + 1) [1, 2, 3]    -- [2, 3, 4]
7
8-- Infix operator: <$>
9#eval (· * 2) <$> some 10              -- some 20
10#eval (· * 2) <$> [1, 2, 3]            -- [2, 4, 6]

Applicative

Applicative extends Functor with pure and sequential application:

lean

1class Applicative (f : Type → Type) extends Functor f where
2  pure : α → f α
3  seq : f (α → β) → (Unit → f α) → f β
4
5-- pure wraps a value
6#eval (pure 5 : Option Nat)            -- some 5
7
8-- Apply functions inside containers: <*>
9#eval some (· + 1) <*> some 5          -- some 6
10
11-- Note: Lean core does NOT give List an Applicative instance, so
12--   [(· * 2), (· * 3)] <*> [1, 2]
13-- fails with "failed to synthesize Seq List". Use Option, Except, or IO —
14-- or flatMap, which is what the list version would mean anyway:
15#eval [(· * 2), (· * 3)].flatMap (fun f => [1, 2].map f)  -- [2, 4, 3, 6]

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.

Instances Can Depend on Instances

This is where type classes stop being "interfaces" and become genuinely powerful. An instance can itself require instances, so Lean builds the one you need by composing smaller ones.

lean

1-- "A list is showable IF its elements are showable"
2instance [ToString α] : ToString (List α) where
3  toString xs := "[" ++ ", ".intercalate (xs.map toString) ++ "]"
4
5-- Now Lean can build ToString for arbitrary nesting, with no extra work:
6#eval toString [[1, 2], [3]]      -- "[[1, 2], [3]]"
7#eval toString [some 1, none]     -- needs ToString (Option Nat) too

💡

When an instance is "not found", the missing piece is usually one link down this chain, not the class you asked for. Lean's error names the innermost failure — failed to synthesize ToString MyType while you were asking for ToString (List MyType). Read the type in the error carefully; it tells you exactly which instance to write.

Scoping Instances

Instances are global by default: writing one anywhere makes it visible everywhere that imports the file. That is usually what you want, and occasionally a disaster — two libraries both defining ToString Nat differently would silently change behaviour. Lean offers narrower scopes for that reason.

lean

1namespace Verbose
2
3-- scoped: only active when someone writes "open Verbose"
4scoped instance : ToString Bool where
5  toString b := if b then "affirmative" else "negative"
6
7end Verbose
8
9#eval toString true         -- "true"        (the default instance)
10
11open Verbose in
12#eval toString true         -- "affirmative" (the scoped one wins here)
13
14-- local instance: active only for the rest of the current section/file
15section
16local instance : ToString Unit where
17  toString _ := "<unit>"
18
19#eval toString ()           -- "<unit>"
20end

⚠

Prefer scoped instance for anything opinionated — a formatting choice, a non-obvious ordering, a numeric coercion. A global instance for a type you do not own is a promise that your interpretation is the only reasonable one, and it is very hard for a downstream user to undo.

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)

Exercise: Generic Logger

Write a function that logs any value that has a ToString instance.

lean

1def log [ToString α] (x : α) : String :=
2  s!"value = {x}"
3
4#eval log 123
5#eval log true

Error Handling Next: Implementing Instances