Module 5 · Lesson 1

Do Notation

Do notation provides clean syntax for sequencing operations that have effects or might fail. It's essential for practical Lean programming.

The Problem: Nested Binds

Chaining operations that return Option or Exceptgets messy fast:

lean

1def lookup (key : String) (env : List (String × Nat)) : Option Nat :=
2  env.lookup key
3
4-- Without do notation: deeply nested
5def compute (env : List (String × Nat)) : Option Nat :=
6  match lookup "x" env with
7  | none => none
8  | some x => match lookup "y" env with
9    | none => none
10    | some y => match lookup "z" env with
11      | none => none
12      | some z => some (x + y + z)

Do Notation Cleans This Up

lean

1-- With do notation: flat and readable
2def compute' (env : List (String × Nat)) : Option Nat := do
3  let x ← lookup "x" env
4  let y ← lookup "y" env
5  let z ← lookup "z" env
6  return x + y + z
7
8def env := [("x", 1), ("y", 2), ("z", 3)]
9#eval compute' env  -- some 6

Key Takeaway

The ← extracts a value from Option. If any extraction fails (none), the whole block returnsnone.

How Do Notation Works

do desugars to bind operations:

lean

1-- This do block:
2def example1 : Option Nat := do
3  let x ← some 5
4  let y ← some 3
5  return x + y
6
7-- Is equivalent to:
8def example2 : Option Nat :=
9  (some 5).bind fun x =>
10  (some 3).bind fun y =>
11  pure (x + y)
12
13-- Or using >>= operator:
14def example3 : Option Nat :=
15  some 5 >>= fun x =>
16  some 3 >>= fun y =>
17  pure (x + y)

Key Constructs

let ← : Extract Value

The arrow ← unwraps a value from a monadic context. ForOption, it extracts the inner value fromsome; for none, it short-circuits the entire block.

lean

1def safeDivide (x y : Nat) : Option Nat :=
2  if y == 0 then none else some (x / y)
3
4def calculation : Option Nat := do
5  let a ← safeDivide 10 2   -- a = 5
6  let b ← safeDivide a 0    -- Fails! Returns none
7  let c ← safeDivide b 1    -- Never reached
8  return c

return : Wrap Value

The return keyword wraps a pure value back into the monadic type. For Option it produces some; for IO it produces a completed action.

lean

1-- return wraps a pure value
2def justFive : Option Nat := do
3  return 5  -- same as: some 5
4
5-- Can be anywhere in the block
6def example : Option Nat := do
7  let x ← some 3
8  if x > 10 then
9    return 0  -- Early return
10  return x * 2

let = : Pure Binding

When a computation is pure (no effects), use plain = instead of ←. This is just a normal variable binding.

lean

1def example : Option Nat := do
2  let x ← some 5      -- ← extracts from Option
3  let y = x * 2       -- = is pure computation
4  let z = y + 1       -- no Option involved
5  return z            -- some 11

ℹ

Use ← for extracting from monads (Option,IO, etc.). Use = for regular assignments.

Do Works with Many Types

Option

lean

1def optionExample : Option String := do
2  let x ← some "hello"
3  let y ← some "world"
4  return s!"{x} {y}"

Except

lean

1def divide (x y : Int) : Except String Int :=
2  if y == 0 then .error "division by zero" else .ok (x / y)
3
4def exceptExample : Except String Int := do
5  let a ← divide 10 2
6  let b ← divide a 0   -- Fails with error message
7  return b

List (Non-determinism)

lean

1-- For List, do represents all combinations
2def pairs : List (Nat × Nat) := do
3  let x ← [1, 2]
4  let y ← [10, 20]
5  return (x, y)
6
7#eval pairs  -- [(1, 10), (1, 20), (2, 10), (2, 20)]

IO (Side Effects)

lean

1def greet : IO Unit := do
2  IO.println "What's your name?"
3  let name ← IO.getLine
4  IO.println s!"Hello, {name}!"

Control Flow in Do Blocks

if-then-else

lean

1def classify (n : Nat) : IO Unit := do
2  if n == 0 then
3    IO.println "zero"
4  else if n < 10 then
5    IO.println "small"
6  else
7    IO.println "large"

for Loops

lean

1def printNumbers : IO Unit := do
2  for i in [1, 2, 3, 4, 5] do
3    IO.println s!"Number: {i}"
4
5def sumList (xs : List Nat) : IO Nat := do
6  let mut sum := 0
7  for x in xs do
8    sum := sum + x
9  return sum

while Loops

lean

1def countdown : IO Unit := do
2  let mut n := 5
3  while n > 0 do
4    IO.println s!"{n}..."
5    n := n - 1
6  IO.println "Liftoff!"

Unless and When

unless and when provide cleaner conditional execution in do blocks:

lean

1-- when: execute if condition is true
2def maybeLog (verbose : Bool) (msg : String) : IO Unit := do
3  when verbose do
4    IO.println s!"[LOG] {msg}"
5
6-- unless: execute if condition is false  
7def requirePositive (n : Int) : IO Unit := do
8  unless n > 0 do
9    IO.println "Error: expected positive number"
10    return
11  IO.println s!"Processing {n}"
12
13-- Both are cleaner than if-then-else with Unit
14#eval maybeLog true "Hello"   -- prints "[LOG] Hello"
15#eval maybeLog false "Hello"  -- prints nothing

Match Inside Do

Pattern matching integrates naturally with do notation:

lean

1def processResult (r : Except String Nat) : IO Unit := do
2  match r with
3  | .error e => IO.println s!"Error: {e}"
4  | .ok n => 
5    IO.println s!"Got value: {n}"
6    let doubled := n * 2
7    IO.println s!"Doubled: {doubled}"
8
9-- Match with ←
10def processFile (path : String) : IO String := do
11  let content ← IO.FS.readFile path
12  match content.splitOn "
13" with
14  | [] => return "empty file"
15  | first :: _ => return first

Early Exit Patterns

Combine if with return to exit a block early. This keeps control flow clear without deeply nested branches.

lean

1def ensurePositive (n : Int) : Except String Int := do
2  if n <= 0 then
3    return .error "expected positive"
4  return .ok n

Deep Dive: What is a Monad?

do notation works with any type that has aMonad instance. A monad provides:

lean

1class Monad (m : Type → Type) where
2  pure : α → m α              -- Wrap a value
3  bind : m α → (α → m β) → m β  -- Chain operations

Option, Except,List, and IO are all monads.

Combining Different Monads

You can't mix monads directly in one do block:

lean

1-- This doesn't work:
2-- def bad : IO Nat := do
3--   let x ← some 5    -- Option, not IO!
4--   return x
5
6-- Convert Option to IO by handling the failure:
7def good : IO Nat := do
8  let opt : Option Nat := some 5
9  match opt with
10  | none => return 0
11  | some x => return x

Exercise: Option Pipeline

Use do notation to chain two Option computations.

lean

1def parseNat (s : String) : Option Nat := s.toNat?
2
3def sumTwo (a b : String) : Option Nat := do
4  let x ← parseNat a
5  let y ← parseNat b
6  return x + y
7
8#eval sumTwo "3" "4"   -- some 7
9#eval sumTwo "3" "x"   -- none

Custom Type Classes Next: The IO Monad