Error Handling

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

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}"

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

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

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"

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 safeSqrt (n : Nat) : Except String Nat :=
13  if n < 0 then .error "Negative number"
14  else .ok (Nat.sqrt n)  -- Simplified
15
16def compute (x y : Nat) : Except String Nat := do
17  let quotient ← divide x y
18  safeSqrt quotient

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"

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

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: Option.toExcept
14#check Option.toExcept

1-- Handle all errors uniformly
2def orElse (x : Option α) (y : Option α) : Option α :=
3  match x with
4  | some a => some a
5  | none => y
6
7#eval orElse none (some 5)        -- some 5
8#eval orElse (some 3) (some 5)    -- some 3
9
10-- Collect successes, ignore failures
11def filterMap (f : α → Option β) (xs : List α) : List β :=
12  xs.filterMap f
13
14def parseNat? (s : String) : Option Nat := s.toNat?
15
16#eval ["1", "hello", "3"].filterMap parseNat?  -- [1, 3]
17
18-- Require all to succeed
19def sequence (xs : List (Option α)) : Option (List α) :=
20  xs.mapM id
21
22#eval sequence [some 1, some 2, some 3]  -- some [1, 2, 3]
23#eval sequence [some 1, none, some 3]    -- none