Polymorphism and Type Classes
On September 23, 1999, the Mars Climate Orbiter disintegrated in the Martian atmosphere because one piece of software produced thrust data in pound-force seconds while another expected newton-seconds. A \$327 million spacecraft, destroyed by a unit conversion error that any undergraduate physics student could catch. The software worked. The math was correct. The types simply failed to express the constraints that mattered.
This is what motivates the machinery in this article. Type classes and phantom types let you encode dimensional constraints directly in the type system. You cannot add meters to seconds because the compiler will not let you. You cannot pass thrust in the wrong units because the function signature forbids it. These constraints cost nothing at runtime, they compile away completely, but they catch at compile time the very class of error that destroyed a spacecraft. By the end of this article, you will see how to build such a system yourself.
But safety is only half the story. Polymorphism is also about not writing the same code twice. A sorting algorithm should not care whether it sorts integers, strings, or financial instruments. A data structure should not be rewritten for each type it might contain. The alternative is copying code and changing types by hand, which is how bugs are born and how programmers lose their minds. Polymorphism is the machinery that makes abstraction possible without sacrificing type safety.
In 1967, Christopher Strachey drew a distinction that would shape programming languages for decades: parametric polymorphism, where code works uniformly for all types, versus ad-hoc polymorphism, where the behavior changes based on the specific type involved. The first gives you reverse : List α → List α, a function blissfully ignorant of what the list contains. The second gives you +, which does quite different things to integers, floats, and matrices. Lean provides both, unified under a type class system that traces its lineage through Haskell back to Wadler and Blott’s 1989 paper How to Make Ad-Hoc Polymorphism Less Ad Hoc. The result is generic code that is simultaneously flexible and precise.
Parametric Polymorphism
Functions can take type parameters, allowing them to work with any type without knowing or caring what that type is. The function length : List α → Nat counts elements whether they are integers, strings, or proof terms. The curly braces indicate implicit arguments that Lean infers automatically, sparing you the tedium of writing length (α := Int) myList everywhere.
def identity {α : Type} (x : α) : α := x
#eval identity 42 -- 42
#eval identity "hello" -- "hello"
#eval identity [1, 2, 3] -- [1, 2, 3]
def compose {α β γ : Type} (g : β → γ) (f : α → β) : α → γ :=
fun x => g (f x)
def addOne (x : Nat) : Nat := x + 1
def double (x : Nat) : Nat := x * 2
#eval compose double addOne 5 -- 12
def flip {α β γ : Type} (f : α → β → γ) : β → α → γ :=
fun b a => f a b
#eval flip Nat.sub 3 10 -- 7
Polymorphic Data Types
Data types can also be parameterized, creating generic containers that work with any element type. You define List α once and get lists of integers, lists of strings, and lists of lists for free. The alternative, writing IntList, StringList, and ListOfLists separately, is how Java programmers spent the 1990s.
def Pair (α β : Type) := α × β
def makePair {α β : Type} (a : α) (b : β) : Pair α β := (a, b)
#eval makePair 1 "one" -- (1, "one")
inductive Either (α β : Type) where
| left : α → Either α β
| right : β → Either α β
deriving Repr
def mapEither {α β γ : Type} (f : β → γ) : Either α β → Either α γ
| .left a => .left a
| .right b => .right (f b)
#eval mapEither (· + 1) (Either.right 5 : Either String Nat)
Implicit Arguments
Implicit arguments in curly braces are inferred by Lean from context. When inference fails or you want to override it, the @ prefix makes everything explicit. This escape hatch is rarely needed, but when you need it, you really need it.
def listLength {α : Type} (xs : List α) : Nat :=
match xs with
| [] => 0
| _ :: rest => 1 + listLength rest
#eval listLength [1, 2, 3] -- 3
#eval listLength ["a", "b"] -- 2
#eval @listLength Nat [1, 2, 3] -- explicit type argument
def firstOrDefault {α : Type} (xs : List α) (default : α) : α :=
match xs with
| [] => default
| x :: _ => x
#eval firstOrDefault [1, 2, 3] 0 -- 1
#eval firstOrDefault ([] : List Nat) 0 -- 0
Instance Arguments
Square brackets denote instance arguments, resolved through type class inference. When you write [Add α], you are saying “give me any type that knows how to add.” The compiler finds the right implementation automatically. This is the mechanism that lets + work on integers, floats, vectors, and anything else with an Add instance.
def printTwice {α : Type} [ToString α] (x : α) : String :=
s!"{x} and {x}"
#eval printTwice 42 -- "42 and 42"
#eval printTwice true -- "true and true"
#eval printTwice "hi" -- "hi and hi"
def maximum {α : Type} [Ord α] (xs : List α) : Option α :=
xs.foldl (init := none) fun acc x =>
match acc with
| none => some x
| some m => if compare x m == .gt then some x else some m
#eval maximum [3, 1, 4, 1, 5, 9] -- some 9
#eval maximum ["b", "a", "c"] -- some "c"
Defining Type Classes
Type classes define interfaces that types can implement, but unlike object-oriented interfaces, the implementation is external to the type. You can add new capabilities to existing types without modifying them. This is how Lean can make + work for types defined in libraries you do not control.
class Printable (α : Type) where
format : α → String
instance : Printable Nat where
format n := s!"Nat({n})"
instance : Printable Bool where
format b := if b then "yes" else "no"
instance : Printable String where
format s := s!"\"{s}\""
def showValue {α : Type} [Printable α] (x : α) : String :=
Printable.format x
#eval showValue 42 -- "Nat(42)"
#eval showValue true -- "yes"
#eval showValue "test" -- "\"test\""
Tip
A type class constraint like
[Add α]is a proof obligation. The compiler must find evidence thatαsupports addition. Instance resolution is proof search. This connection between “finding implementations” and “finding proofs” is not a metaphor; it is the same mechanism. When you reach the Proofs article, you will see the compiler searching for proofs exactly as it searches for instances here.
Polymorphic Instances
Instances themselves can be polymorphic, building complex instances from simpler ones. If you can print an α, you can print a List α. This compositionality is the quiet superpower of type classes: small building blocks assemble into sophisticated behavior without explicit wiring.
instance {α : Type} [Printable α] : Printable (List α) where
format xs :=
let items := xs.map Printable.format
"[" ++ ", ".intercalate items ++ "]"
instance {α β : Type} [Printable α] [Printable β] : Printable (α × β) where
format p := s!"({Printable.format p.1}, {Printable.format p.2})"
#eval showValue [1, 2, 3] -- "[Nat(1), Nat(2), Nat(3)]"
#eval showValue (42, true) -- "(Nat(42), yes)"
#eval showValue [(1, true), (2, false)]
Numeric Type Classes
Type classes excel at abstracting over numeric operations. Write your algorithm once against an abstract Mul and Add, and it works for integers, rationals, complex numbers, matrices, and polynomials. The abstraction costs nothing at runtime because instance resolution happens at compile time. The generic code specializes to concrete operations in the generated code.
class Addable (α : Type) where
add : α → α → α
zero : α
instance : Addable Nat where
add := Nat.add
zero := 0
instance : Addable Int where
add := Int.add
zero := 0
instance : Addable Float where
add := Float.add
zero := 0.0
def sumList {α : Type} [Addable α] (xs : List α) : α :=
xs.foldl Addable.add Addable.zero
#eval sumList [1, 2, 3, 4, 5] -- 15
#eval sumList [1.5, 2.5, 3.0] -- 7.0
#eval sumList ([-1, 2, -3] : List Int) -- -2
Extending Classes
Type classes can extend other classes, inheriting their operations while adding new ones. An Ord instance gives you compare, and from that you get <, ≤, >, ≥, min, and max for free. The hierarchy of algebraic structures in Mathlib, from magmas through groups to rings and fields, is built this way.
class Eq' (α : Type) where
eq : α → α → Bool
class Ord' (α : Type) extends Eq' α where
lt : α → α → Bool
instance : Eq' Nat where
eq := (· == ·)
instance : Ord' Nat where
eq := (· == ·)
lt := (· < ·)
def sortedInsert {α : Type} [Ord' α] (x : α) (xs : List α) : List α :=
match xs with
| [] => [x]
| y :: ys => if Ord'.lt x y then x :: y :: ys else y :: sortedInsert x ys
#eval sortedInsert 3 [1, 2, 4, 5] -- [1, 2, 3, 4, 5]
Functor
The Functor pattern captures the idea of mapping a function over a structure while preserving its shape. Lists, options, arrays, trees, and IO actions are all functors. Once you see the pattern, you see it everywhere: any context that wraps a value and lets you transform that value without escaping the context.
class Functor' (F : Type → Type) where
map : {α β : Type} → (α → β) → F α → F β
instance : Functor' List where
map := List.map
instance : Functor' Option where
map f
| none => none
| some x => some (f x)
def doubleAll {F : Type → Type} [Functor' F] (xs : F Nat) : F Nat :=
Functor'.map (· * 2) xs
#eval doubleAll [1, 2, 3] -- [2, 4, 6]
#eval doubleAll (some 21) -- some 42
#eval doubleAll (none : Option Nat) -- none
Multiple Constraints
Functions can require multiple type class constraints, combining capabilities from different classes. A sorting function needs Ord; a function that sorts and prints needs [Ord α] [Repr α]. The constraints document exactly what your function requires, nothing more, nothing less.
def showCompare {α : Type} [ToString α] [Ord α] (x y : α) : String :=
let result := match compare x y with
| .lt => "less than"
| .eq => "equal to"
| .gt => "greater than"
s!"{x} is {result} {y}"
#eval showCompare 3 5 -- "3 is less than 5"
#eval showCompare "b" "a" -- "b is greater than a"
def sortAndShow {α : Type} [ToString α] [Ord α] (xs : List α) : String :=
let sorted := xs.toArray.qsort (compare · · == .lt) |>.toList
s!"{sorted}"
#eval sortAndShow [3, 1, 4, 1, 5] -- "[1, 1, 3, 4, 5]"
Deriving Instances
Many standard type classes can be automatically derived, saving you from writing boilerplate that follows predictable patterns. The deriving clause generates instances for Repr, BEq, Hashable, and others. Let the machine do the mechanical work; save your creativity for the parts that require thought.
structure Point' where
x : Nat
y : Nat
deriving Repr, BEq, Hashable
#eval Point'.mk 1 2 == Point'.mk 1 2 -- true
#eval Point'.mk 1 2 == Point'.mk 3 4 -- false
inductive Color where
| red | green | blue
deriving Repr, DecidableEq
#eval Color.red == Color.red -- true
#eval Color.red == Color.blue -- false
structure Person where
name : String
age : Nat
deriving Repr, BEq
def alice : Person := { name := "Alice", age := 30 }
def bob : Person := { name := "Bob", age := 25 }
#eval alice == bob -- false
#eval repr alice -- { name := "Alice", age := 30 }
Semigroups and Monoids
Algebraic structures like semigroups and monoids capture patterns that recur across mathematics and programming. A semigroup has an associative operation; a monoid adds an identity element. String concatenation, list append, function composition, and integer addition are all monoids. Recognizing the common structure lets you write code once and apply it to all of them.
class Semigroup (α : Type) where
append : α → α → α
class Monoid' (α : Type) extends Semigroup α where
empty : α
def concat {α : Type} [Monoid' α] (xs : List α) : α :=
xs.foldl Semigroup.append Monoid'.empty
instance : Monoid' String where
append := String.append
empty := ""
instance {α : Type} : Monoid' (List α) where
append := List.append
empty := []
#eval concat ["Hello", " ", "World"] -- "Hello World"
#eval concat [[1, 2], [3], [4, 5]] -- [1, 2, 3, 4, 5]
Units of Measurement: Safety for Free
Here is the payoff for all the type class machinery. We can prevent the Mars Orbiter bug entirely, not through runtime checks but through types that make the error inexpressible. Consider representing physical quantities with phantom types:
/-!
# Type-Safe Units of Measurement
A demonstration of using phantom types and type classes to enforce dimensional
correctness at compile time with zero runtime overhead. The types exist only
in the compiler's mind; the generated code manipulates raw floats.
-/
-- Phantom types representing physical dimensions
-- These have no constructors and no runtime representation
structure Meters
structure Seconds
structure Kilograms
structure MetersPerSecond
structure MetersPerSecondSquared
structure Newtons
structure NewtonSeconds
-- A quantity is a value tagged with its unit type
-- At runtime, this is just a Float
structure Quantity (unit : Type) where
val : Float
deriving Repr
-- Type class for multiplying quantities with compatible units
class UnitMul (u1 u2 result : Type) where
-- Type class for dividing quantities with compatible units
class UnitDiv (u1 u2 result : Type) where
-- Define the dimensional relationships
instance : UnitDiv Meters Seconds MetersPerSecond where
instance : UnitDiv MetersPerSecond Seconds MetersPerSecondSquared where
instance : UnitMul Kilograms MetersPerSecondSquared Newtons where
instance : UnitMul Newtons Seconds NewtonSeconds where
-- Arithmetic operations that preserve dimensional correctness
def Quantity.add {u : Type} (x y : Quantity u) : Quantity u :=
⟨x.val + y.val⟩
def Quantity.sub {u : Type} (x y : Quantity u) : Quantity u :=
⟨x.val - y.val⟩
def Quantity.mul {u1 u2 u3 : Type} [UnitMul u1 u2 u3] (x : Quantity u1) (y : Quantity u2) : Quantity u3 :=
⟨x.val * y.val⟩
def Quantity.div {u1 u2 u3 : Type} [UnitDiv u1 u2 u3] (x : Quantity u1) (y : Quantity u2) : Quantity u3 :=
⟨x.val / y.val⟩
def Quantity.scale {u : Type} (x : Quantity u) (s : Float) : Quantity u :=
⟨x.val * s⟩
-- Smart constructors for readability
def meters (v : Float) : Quantity Meters := ⟨v⟩
def seconds (v : Float) : Quantity Seconds := ⟨v⟩
def kilograms (v : Float) : Quantity Kilograms := ⟨v⟩
def newtons (v : Float) : Quantity Newtons := ⟨v⟩
def newtonSeconds (v : Float) : Quantity NewtonSeconds := ⟨v⟩
-- Example: Computing velocity from distance and time
-- This compiles because Meters / Seconds = MetersPerSecond
def computeVelocity (distance : Quantity Meters) (time : Quantity Seconds)
: Quantity MetersPerSecond :=
distance.div time
-- Example: Computing force from mass and acceleration
-- This compiles because Kilograms * MetersPerSecondSquared = Newtons
def computeForce (mass : Quantity Kilograms) (accel : Quantity MetersPerSecondSquared)
: Quantity Newtons :=
mass.mul accel
-- Example: Computing impulse from force and time
-- This compiles because Newtons * Seconds = NewtonSeconds
def computeImpulse (force : Quantity Newtons) (time : Quantity Seconds)
: Quantity NewtonSeconds :=
force.mul time
-- The Mars Climate Orbiter scenario:
-- One team computes impulse in Newton-seconds
-- Another team expects the same units
-- The type system ensures they match
def thrusterImpulse : Quantity NewtonSeconds :=
let force := newtons 450.0
let burnTime := seconds 10.0
computeImpulse force burnTime
-- This would NOT compile - you cannot add NewtonSeconds to Meters:
-- def nonsense := thrusterImpulse.add (meters 100.0)
-- This would NOT compile - you cannot pass Meters where Seconds expected:
-- def badVelocity := computeVelocity (meters 100.0) (meters 50.0)
-- The key insight: all the Quantity wrappers and phantom types vanish at runtime.
-- The generated code is just floating-point arithmetic.
-- The safety is free.
def main : IO Unit := do
let distance := meters 100.0
let time := seconds 9.58 -- Usain Bolt's 100m record
let velocity := computeVelocity distance time
IO.println s!"Distance: {distance.val} m"
IO.println s!"Time: {time.val} s"
IO.println s!"Velocity: {velocity.val} m/s"
let mass := kilograms 1000.0
let accel : Quantity MetersPerSecondSquared := ⟨9.81⟩
let force := computeForce mass accel
IO.println s!"Mass: {mass.val} kg"
IO.println s!"Acceleration: {accel.val} m/s²"
IO.println s!"Force: {force.val} N"
let impulse := computeImpulse force (seconds 5.0)
IO.println s!"Impulse: {impulse.val} N·s"
The Quantity type wraps a Float but carries a phantom type parameter representing its unit. You cannot add meters to seconds because Quantity.add requires both arguments to have the same unit type. You cannot pass thrust in the wrong units because the function signature encodes the dimensional requirements.
The crucial insight is that these phantom types vanish at runtime. The Meters and Seconds types have no constructors, no fields, no runtime representation whatsoever. The generated code manipulates raw floats with raw floating-point operations. The type checker enforces dimensional correctness; the compiled program pays no cost for it. This is the dream of static typing: safety that exists only in the compiler’s mind, free at runtime, catching at compile time the very class of error that destroyed a spacecraft.
There is a broader lesson here about the direction of software. The mathematics that physicists scribble on whiteboards, the dimensional analysis that engineers perform by hand, the invariants that programmers hold in their heads and document in comments: these are all pseudocode. They are precise enough for humans to follow but not precise enough for machines to verify. The project of programming language research, from Curry and Howard through ML and Haskell to Lean and dependent types, has been to formalize this pseudocode. To turn informal reasoning into machine-checked artifacts.
As code generation by large language models becomes routine, this formalization becomes essential. A neural network can produce syntactically correct code that passes tests yet harbors subtle unit errors, off-by-one mistakes, and violated invariants. The guardrails cannot be more tests, more code review, more human attention. The guardrails must be formalisms that make entire categories of errors unrepresentable. Type classes, phantom types, dependent types: these are not academic curiosities but safety controls for a future where most code is synthesized. The Mars Climate Orbiter was written by humans who made a human error. The code that replaces them must be held to a higher standard. (For more on this trajectory, see Artificial Intelligence.)
Build and run with:
lake exe units