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 earlyReturn : 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 := instead of ←. This is an ordinary local binding — the same let you use outside a do block.

lean

1def pureBinding : 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

⚠

It is :=, not =. Writing let y = x * 2 gives unexpected token, expected ':='. The single = is equality (a proposition), never assignment — that is true everywhere in Lean, inside do blocks included.

ℹ

Use ← when the right-hand side is in the monad(Option Nat, IO String) and you want the value inside. Use := when it is already a plain value. If you get type mismatch on a let, you almost certainly picked the wrong one.

(← e) : Arrows Inside Expressions

You do not need a let for every extraction. An ← can appear anywhere inside an expression; Lean lifts it out into a binding for you, left to right.

lean

1def verbose : Option Nat := do
2  let x ← some 5
3  let y ← some 3
4  return x + y
5
6-- Same thing, no intermediate names
7def concise : Option Nat := do
8  return (← some 5) + (← some 3)
9
10#eval concise   -- some 8
11
12-- Very common in IO
13#eval show IO Unit from do
14  IO.println s!"cwd: {← IO.currentDir}"

⚠

The lifting happens at the nearest enclosing do, and in evaluation order. That matters when the effects are not commutative: f (← a) (← b) runs a then b, always. If the order is important to a reader, write the lets out — clarity beats brevity here.

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)

In many languages List is a monad, and do over it means "all combinations". Lean core deliberately does not ship that instance — writing a do block over a list fails with failed to synthesize Pure List. Use flatMap directly, which is what the desugaring would have produced anyway:

lean

1-- What "do over List" would mean, written out:
2def pairs : List (Nat × Nat) :=
3  [1, 2].flatMap fun x =>
4  [10, 20].map fun y =>
5  (x, y)
6
7#eval pairs  -- [(1, 10), (1, 20), (2, 10), (2, 20)]
8
9-- The same thing with the standard combinator
10#eval [1, 2].flatMap (fun x => [10, 20].map (fun y => (x, y)))

ℹ

Mathlib and Batteries do provide Monad List. If you have one of them imported, the do version works. Relying on it is fine if you know the instance is in scope — this is a good example of why "instance not found" is so often really "import not present".

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 "\n" with
13  | [] => return "empty file"
14  | 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    throw "expected positive"     -- NOT: return .error "..."
4  return n                        -- NOT: return .ok n
5
6#eval ensurePositive (-1)   -- Except.error "expected positive"
7#eval ensurePositive 5      -- Except.ok 5

⚠

Inside a do block, return ealready wraps e in the monad. So return .ok n means .ok (.ok n) and does not typecheck, and return .error e would build a success containing an error value. To fail, use throw.

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