The Option Type

Handling Missing Values

Option α represents a value that may be absent: some v wraps a present value and none signals absence
This is Lean's answer to null; the type system forces every caller to handle both cases explicitly
Pattern match with | some v => ... | none => ... when the two branches need different logic
Option.map f opt applies f to the wrapped value if present; none passes through unchanged
Option.getD opt default extracts the value or returns default when the option is none
do notation for Option lets you sequence option-returning steps; a single none short-circuits the rest of the chain

-- Option α is either (some value) or none; there is no null in Lean
def safeDivide (a b : Int) : Option Int :=
  if b == 0 then none else some (a / b)

#guard safeDivide 10 2 == some 5
#guard safeDivide 10 0 == none

-- map transforms the value if present; none passes through unchanged
#guard (safeDivide 10 2).map (· * 3) == some 15
#guard (safeDivide 10 0).map (· * 3) == none

-- getD supplies a default when the value is absent
#guard (safeDivide 10 0).getD (-1) == -1

-- Explicit pattern match when the two branches need different logic
def describe (a b : Int) : String :=
  match safeDivide a b with
  | some q => s!"{a} / {b} = {q}"
  | none   => "cannot divide by zero"

#eval describe 10 3    -- "10 / 3 = 3"
#eval describe 10 0    -- "cannot divide by zero"

-- do notation: each <- short-circuits the chain if the result is none
def compute (a b c : Int) : Option Int := do
  let x ← safeDivide a b
  let y ← safeDivide x c
  return x + y

#guard compute 10 2 1 == some 10   -- x=5, y=5, x+y=10
#guard compute 10 0 1 == none      -- first step fails; chain stops

Lists and Option

List.find? p xs returns some x for the first element satisfying p, or none if nothing matches
List.filterMap f xs applies f to each element and collects only the some results
List.findSome? f xs applies f and returns the first some result, stopping early
The shorthand (·.1 == key) reads as fun p => p.1 == key, useful for searching lists of pairs
Combine find? and map to implement safe dictionary lookup over List (String × α) without any special data structure

-- find? returns Some of the first element matching the predicate
def lookup (key : String) (pairs : List (String × Int)) : Option Int :=
  (pairs.find? (·.1 == key)).map (·.2)

#guard lookup "b" [("a", 1), ("b", 2), ("c", 3)] == some 2
#guard lookup "z" [("a", 1), ("b", 2)] == none

-- filterMap applies a function and keeps only the Some results
def onlyEvens (xs : List Nat) : List Nat :=
  xs.filterMap fun n => if n % 2 == 0 then some n else none

#guard onlyEvens [1, 2, 3, 4, 5] == [2, 4]

-- findSome? returns the first Some produced by the function
def firstOver (limit : Int) (xs : List Int) : Option Int :=
  xs.findSome? fun x => if x > limit then some x else none

#guard firstOver 3 [1, 2, 4, 5] == some 4
#guard firstOver 10 [1, 2, 4, 5] == none

-- Combine find? with map for safe lookups in association lists
def scores : List (String × Nat) := [("Alice", 95), ("Bob", 80)]

def grade (name : String) : String :=
  match (scores.find? (·.1 == name)).map (·.2) with
  | some s => if s >= 90 then "A" else "B"
  | none   => "unknown"

#eval grade "Alice"    -- "A"
#eval grade "Bob"      -- "B"
#eval grade "Carol"    -- "unknown"

Exercises

Safe Head

Write safeHead : List α → Option α that returns the first element or none for an empty list
Verify it on both an empty list and a non-empty list using #guard

Chain of Divisions

Using do notation, divide 120 by three separate inputs in sequence
Return none if any divisor is zero, or some of the final quotient otherwise
Verify three cases: all non-zero, first divisor zero, third divisor zero

Lookup with Default

Given scores : List (String × Nat), write a function that returns the score for a name formatted as a string
Return "not found" when the name is absent

Parse Rows

Given a list of strings in "name,score" format, use filterMap and String.splitOn to extract valid (String × Nat) pairs
Skip any string that does not contain exactly one comma or whose score is not a valid number
Use String.toNat? for parsing

All Present

Write allPresent : List (Option α) → Option (List α) that returns some of the unwrapped list if every element is some, or none if any element is none
Verify on [some 1, some 2, some 3] and [some 1, none, some 3]