Module 3 · Lesson 5

Error Handling

Lean uses types to make failure explicit. No null pointers, no exceptions—justOption and Except.

The Problem with Null

In languages with null, any value might secretly be null. This leads to runtime crashes. Lean's type system prevents this entirely.

lean

1-- In many languages: head([]) crashes or returns null
2-- In Lean: we must handle the empty case
3
4def safeHead (xs : List α) : Option α :=
5  match xs with
6  | [] => none
7  | x :: _ => some x
8
9#eval safeHead [1, 2, 3]  -- some 1
10#eval safeHead ([] : List Nat)  -- none

Option: Maybe There's a Value

Option α represents a value that might be missing:

lean

1inductive Option (α : Type) where
2  | none : Option α          -- No value
3  | some : α → Option α      -- Has a value
4
5-- Examples
6def maybeNumber : Option Nat := some 42
7def noNumber : Option Nat := none
8
9-- Access with pattern matching
10def showOption (opt : Option Nat) : String :=
11  match opt with
12  | none => "Nothing"
13  | some n => s!"Got {n}"

Working with Option

Instead of pattern matching everywhere, Option provides convenient methods for common operations. These methods make working with optional values concise and composable.

lean

1-- getD: get with default
2#eval (some 5).getD 0     -- 5
3#eval none.getD 0         -- 0
4
5-- map: transform inner value
6#eval (some 5).map (· * 2)   -- some 10
7#eval none.map (· * 2)       -- none
8
9-- bind: chain optional operations
10def half (n : Nat) : Option Nat :=
11  if n % 2 == 0 then some (n / 2) else none
12
13#eval (some 10).bind half  -- some 5
14#eval (some 7).bind half   -- none
15#eval none.bind half       -- none

ℹ

bind is also written as >>=. It chains operations that might fail—if any step fails, the whole chain fails.

Option in Practice

lean

1-- Find an element
2def find (p : α → Bool) : List α → Option α
3  | [] => none
4  | x :: xs => if p x then some x else find p xs
5
6#eval find (· > 5) [1, 3, 7, 2]  -- some 7
7#eval find (· > 10) [1, 3, 7, 2]  -- none
8
9-- Dictionary lookup
10def lookup (key : String) (pairs : List (String × α)) : Option α :=
11  match pairs with
12  | [] => none
13  | (k, v) :: rest => if k == key then some v else lookup key rest
14
15def env := [("x", 1), ("y", 2)]
16#eval lookup "x" env  -- some 1
17#eval lookup "z" env  -- none

Designing with Error Types

Use Option when the absence of a value is expected and unremarkable. Use Except when you need to explain why something failed.

Except: Errors with Context

Except ε α is like Option but carries error information:

lean

1inductive Except (ε α : Type) where
2  | error : ε → Except ε α   -- Failed with error
3  | ok : α → Except ε α      -- Succeeded with value
4
5-- Example: division with error message
6def divide (x y : Nat) : Except String Nat :=
7  if y == 0 
8  then Except.error "Division by zero"
9  else Except.ok (x / y)
10
11#eval divide 10 2   -- Except.ok 5
12#eval divide 10 0   -- Except.error "Division by zero"

Working with Except

Like Option, Except supports mapand bind operations. These let you transform success values or chain fallible operations without manual error propagation.

lean

1-- Pattern matching
2def showResult (r : Except String Nat) : String :=
3  match r with
4  | .error e => s!"Error: {e}"
5  | .ok n => s!"Success: {n}"
6
7-- map and bind work similarly to Option
8#eval (Except.ok 5 : Except String Nat).map (· * 2)  -- ok 10
9#eval (Except.error "oops" : Except String Nat).map (· * 2)  -- error "oops"
10
11-- Chain fallible operations
12def smallEnough (n : Nat) : Except String Nat :=
13  if n > 100 then .error s!"{n} is too large"
14  else .ok n
15
16def compute (x y : Nat) : Except String Nat := do
17  let quotient ← divide x y
18  smallEnough quotient
19
20#eval compute 10 2      -- Except.ok 5
21#eval compute 10 0      -- Except.error "Division by zero"
22#eval compute 1000 2    -- Except.error "500 is too large"

⚠

A trap worth naming: a guard like if n < 0 then .error "negative" for n : Nat is dead code — a Nat is never negative, so the branch can never be taken. Lean will not warn you. Validate the things that can actually go wrong, and if you need negatives, use Int.

Do Notation for Error Handling

The do notation makes chaining fallible operations clean:

lean

1-- Without do notation (messy)
2def processWithoutDo (x y z : Nat) : Except String Nat :=
3  match divide x y with
4  | .error e => .error e
5  | .ok a => match divide a z with
6    | .error e => .error e
7    | .ok b => .ok (b * 2)
8
9-- With do notation (clean)
10def processWithDo (x y z : Nat) : Except String Nat := do
11  let a ← divide x y
12  let b ← divide a z
13  return b * 2
14
15#eval processWithDo 100 5 2   -- ok 20
16#eval processWithDo 100 0 2   -- error "Division by zero"
17#eval processWithDo 100 5 0   -- error "Division by zero"

Key Takeaway

The ← syntax extracts values from Except(or Option). If extraction fails, the whole doblock short-circuits and returns the error.

Custom Error Types

lean

1-- Define specific errors
2inductive ValidationError where
3  | tooShort : Nat → ValidationError
4  | invalidChar : Char → ValidationError
5  | reserved : String → ValidationError
6
7def validateUsername (name : String) : Except ValidationError String :=
8  if name.length < 3 then
9    .error (.tooShort name.length)
10  else if name.any (· == ' ') then
11    .error (.invalidChar ' ')
12  else if name == "admin" then
13    .error (.reserved name)
14  else
15    .ok name

Converting Between Option and Except

lean

1-- Option to Except
2def optionToExcept (opt : Option α) (err : ε) : Except ε α :=
3  match opt with
4  | none => .error err
5  | some a => .ok a
6
7-- Except to Option (loses error info)
8def exceptToOption (ex : Except ε α) : Option α :=
9  match ex with
10  | .error _ => none
11  | .ok a => some a
12
13-- Built-in the other way round:
14#check @Except.toOption   -- Except ε α → Option α
15
16-- Going Option → Except has no single built-in name, because you must
17-- supply the error. The idiom is a one-liner:
18def Option.toExcept (opt : Option α) (err : ε) : Except ε α :=
19  opt.elim (.error err) .ok
20
21#eval (some 5).toExcept "missing"          -- Except.ok 5
22#eval (none : Option Nat).toExcept "missing"  -- Except.error "missing"

Deep Dive: Why No Exceptions?

Exceptions in languages like Java or Python are problematic:

They're invisible in function signatures
They bypass the type system
They make reasoning about code harder
They complicate theorem proving

With Option and Except, failure is:

Visible in the type: Except Error Value
Checked by the compiler
Composable with do notation
Provable (you can prove code handles all errors)

The Escape Hatches: get!, panic!, and IO Exceptions

Everything above keeps failure in the types. Lean also gives you ways out of that discipline. They are legitimate in the right place — and a design smell everywhere else.

lean

1-- get! : "I know this is some". Crashes at runtime if it is not.
2#eval (some 5).get!               -- 5
3-- #eval (none : Option Nat).get! -- PANIC: value is none
4
5-- panic! : deliberately crash with a message. Requires Inhabited.
6def mustBePositive (n : Int) : Nat :=
7  if n > 0 then n.toNat else panic! s!"expected positive, got {n}"
8
9-- IO has real exceptions, because the outside world does
10#eval show IO Unit from do
11  try
12    let _ ← IO.FS.readFile "does-not-exist.txt"
13    IO.println "read it"
14  catch e =>
15    IO.println s!"caught: {e}"
16
17-- throw raises one
18#eval show IO Unit from do
19  try
20    throw (IO.userError "something went wrong")
21  catch e =>
22    IO.println s!"caught: {e}"

⚠

get! and panic! do not make your function partial in the type system — the signature still claims it always returns a value. What actually happens is that panic! returns the Inhabited default and logs to stderr, so a proof about the function sees a plausible-but-wrong value rather than a crash. That mismatch between what runs and what you proved is exactly why these should be rare.

💡

A good rule: Option/Except for anything a caller might reasonably handle; IO exceptions for genuine environment failures (missing files, network); and panic! only for invariants you believe are impossible, as documentation of that belief.

Common Patterns

lean

1-- Fallbacks: <|> takes the first success (this is Alternative.orElse)
2#eval (some 3) <|> (some 5)             -- some 3
3#eval (none : Option Nat) <|> (some 5)  -- some 5
4
5-- Written out, that is:
6def orElse (x : Option α) (y : Option α) : Option α :=
7  match x with
8  | some a => some a
9  | none => y
10
11#eval orElse none (some 5)        -- some 5
12#eval orElse (some 3) (some 5)    -- some 3
13
14-- Collect successes, ignore failures
15def filterMap (f : α → Option β) (xs : List α) : List β :=
16  xs.filterMap f
17
18def parseNat? (s : String) : Option Nat := s.toNat?
19
20#eval ["1", "hello", "3"].filterMap parseNat?  -- [1, 3]
21
22-- Require all to succeed
23def sequence (xs : List (Option α)) : Option (List α) :=
24  xs.mapM id
25
26#eval sequence [some 1, some 2, some 3]  -- some [1, 2, 3]
27#eval sequence [some 1, none, some 3]    -- none

Exercise: Validate Age

Create a validator that accepts ages 0–120 and returns a helpful error otherwise.

lean

1def validateAge (n : Nat) : Except String Nat :=
2  if n <= 120 then .ok n else .error "age out of range"
3
4#eval validateAge 25   -- ok 25
5#eval validateAge 200  -- error "age out of range"

Higher-Order Functions Next: Type Classes