Module 4 · Lesson 3

Custom Type Classes

Define your own type classes to create reusable abstractions over different types.

Defining a Type Class

Use class to define a new type class:

lean

1-- A class for types that can be serialized to JSON
2class ToJson (α : Type) where
3  toJson : α → String
4
5-- Instances for basic types
6instance : ToJson Nat where
7  toJson n := toString n
8
9instance : ToJson String where
10  toJson s := s!""{s}""
11
12instance : ToJson Bool where
13  toJson b := if b then "true" else "false"
14
15#eval ToJson.toJson 42        -- "42"
16#eval ToJson.toJson "hello"   -- ""hello""
17#eval ToJson.toJson true      -- "true"

Classes with Multiple Methods

A type class can require multiple methods. Instances must implement all of them, ensuring that any type claiming to be Serializable provides both serialization and deserialization.

lean

1class Serializable (α : Type) where
2  serialize : α → String
3  deserialize : String → Option α
4
5instance : Serializable Nat where
6  serialize n := toString n
7  deserialize s := s.toNat?
8
9#eval Serializable.serialize 123          -- "123"
10#eval Serializable.deserialize "456"      -- some 456
11#eval (Serializable.deserialize "abc" : Option Nat)  -- none

Classes with Laws

Some classes imply laws that instances should satisfy:

lean

1-- A Monoid has an identity and an associative operation
2class Monoid (α : Type) where
3  empty : α
4  append : α → α → α
5  -- Laws (not enforced, but expected):
6  -- append empty x = x
7  -- append x empty = x
8  -- append (append x y) z = append x (append y z)
9
10instance : Monoid String where
11  empty := ""
12  append := String.append
13
14instance : Monoid (List α) where
15  empty := []
16  append := List.append
17
18-- Generic function using Monoid
19def concat [Monoid α] (xs : List α) : α :=
20  xs.foldl Monoid.append Monoid.empty
21
22#eval concat ["a", "b", "c"]       -- "abc"
23#eval concat [[1,2], [3], [4,5]]   -- [1, 2, 3, 4, 5]

Key Takeaway

Monoid laws aren't checked by the type system here, but in Lean's math library (Mathlib), you can prove that instances satisfy their laws.

Designing Minimal Interfaces

Keep type classes small. Prefer a few core methods plus derived helpers rather than many overlapping operations. This reduces instance burden and improves reuse.

Extending Type Classes

Classes can extend other classes:

lean

1-- Semigroup: just append
2class Semigroup (α : Type) where
3  append : α → α → α
4
5-- Monoid extends Semigroup with identity
6class Monoid' (α : Type) extends Semigroup α where
7  empty : α
8
9-- Instances must provide all methods
10instance : Monoid' Nat where
11  empty := 0
12  append := Nat.add
13
14-- Functions can use parent class methods
15def reduce [Monoid' α] (xs : List α) : α :=
16  xs.foldl Semigroup.append Monoid'.empty

Multi-Parameter Type Classes

Type classes can involve multiple types. This is useful for encoding relationships between types, such as conversions or compatibility constraints.

lean

1-- Convert between types
2class Convertible (α β : Type) where
3  convert : α → β
4
5instance : Convertible Nat Int where
6  convert n := Int.ofNat n
7
8instance : Convertible Int String where
9  convert i := toString i
10
11#eval (Convertible.convert 42 : Int)     -- 42
12#eval (Convertible.convert (42 : Int) : String)  -- "42"

Outparams: Functional Dependencies

Use outParam when one type determines another:

lean

1-- The element type determines the collection type uniquely
2class Collection (elem : Type) (coll : outParam Type) where
3  empty : coll
4  insert : elem → coll → coll
5  toList : coll → List elem
6
7-- For Nat, the collection is List Nat
8instance : Collection Nat (List Nat) where
9  empty := []
10  insert := List.cons
11  toList := id
12
13-- Lean infers coll from elem
14def build [Collection α coll] (xs : List α) : coll :=
15  xs.foldl (fun c x => Collection.insert x c) Collection.empty

Deep Dive: Why outParam?

Without outParam, Lean can't figure out the collection type from just the element type. With it, the instance search knows: "If elem is Nat, then coll must be List Nat."

This is similar to "functional dependencies" in Haskell.

Default Implementations

Type classes can provide default implementations for methods. This reduces the burden on instance authors—they only need to implement the core methods, and the rest come for free.

lean

1class Printable (α : Type) where
2  -- Required method
3  repr : α → String
4  
5  -- Optional with defaults
6  print : α → IO Unit := fun x => IO.println (repr x)
7  printList : List α → IO Unit := fun xs => 
8    xs.forM (fun x => print x)
9
10-- Only need to implement repr
11instance : Printable Nat where
12  repr := toString
13
14-- print and printList work automatically
15#eval (Printable.print 42 : IO Unit)

Practical Example: A DSL for Expressions

lean

1-- Expression type class
2class Expr (α : Type) where
3  lit : Int → α
4  add : α → α → α
5  mul : α → α → α
6
7-- Evaluator instance
8instance : Expr Int where
9  lit n := n
10  add := Int.add
11  mul := Int.mul
12
13-- Pretty printer instance
14instance : Expr String where
15  lit n := toString n
16  add x y := s!"({x} + {y})"
17  mul x y := s!"({x} * {y})"
18
19-- One expression, multiple interpretations
20def expr [Expr α] : α :=
21  Expr.add (Expr.lit 1) (Expr.mul (Expr.lit 2) (Expr.lit 3))
22
23#eval (expr : Int)     -- 7
24#eval (expr : String)  -- "(1 + (2 * 3))"

💡

This pattern—one definition, multiple interpretations—is called "tagless final" style. It's powerful for building DSLs.

When to Create Type Classes

Create a type class when you have:

Multiple types with the same operations (equality, ordering, serialization)
A common interface that different types implement differently
Algorithms that work generically over types with certain capabilities

Exercise: Simple Pretty Printer

Define a type class for pretty-printing and implement it for a pair.

lean

1class Pretty (α : Type) where
2  pretty : α → String
3
4instance [Pretty α] [Pretty β] : Pretty (α × β) where
5  pretty p := s!"({Pretty.pretty p.1}, {Pretty.pretty p.2})"
6
7instance : Pretty Nat where
8  pretty := toString
9
10#eval Pretty.pretty (1, 2)

Avoid type classes when:

A simple function would suffice
There's only one type that will ever implement it
The abstraction doesn't provide meaningful reuse

Implementing Instances Next: Do Notation