Do-Notation for Monadic and IO Programming in Lean 4

Lean 4’s do-notation provides a clean, imperative-looking syntax for sequencing monadic computations. Under the hood every do block desugars to a sequence of monadic bind (>>=) operations, but the notation reads naturally as a series of statements. do works with any monad — IO, Option, Except, StateT, and more.

The Basics of `do`

A do block is a sequence of statements. Each statement is one of:

A bind let x ← action — runs action and binds the result to x
A plain let let x := expr — binds a pure value
A mutable let let mut x := expr — introduces a mutable local variable
A discarding bind action — runs action and discards the result
Control flow: if, for, while, return, break, continue

def greet : IO Unit := do
  let name ← IO.getLine       -- bind: read a line from stdin
  let greeting := "Hello, " ++ name.trim ++ "!"
  IO.println greeting          -- sequence: print and discard result

Desugaring

The snippet above desugars to:

def greet' : IO Unit :=
  IO.getLine >>= fun name =>
  let greeting := "Hello, " ++ name.trim ++ "!"
  IO.println greeting

Binding with `←`

The left-arrow ← extracts the value from a monadic action:

def readTwo : IO (String × String) := do
  let first  ← IO.getLine
  let second ← IO.getLine
  return (first.trim, second.trim)

If the monad is Option or Except, a failing action short-circuits the rest of the do block:

def safeDivide (n : Nat) (d : Nat) : Option Nat := do
  if d == 0 then none
  let q ← some (n / d)      -- ← extracts from Option
  return q

`let` and `let mut`

let in a do block is immutable. let mut introduces a mutable local variable that can be updated with :=:

def sumTo (n : Nat) : IO Nat := do
  let mut total := 0
  for i in List.range (n + 1) do
    total := total + i
  return total

Mutable variables only exist inside the do block in which they are declared. Lean still compiles them to purely functional code using monadic state behind the scenes — there is no shared mutable state.

`if` / `else` in `do` Blocks

Standard if/else works naturally inside do:

def classify (n : Int) : IO Unit := do
  if n > 0 then
    IO.println s!"{n} is positive"
  else if n < 0 then
    IO.println s!"{n} is negative"
  else
    IO.println "zero"

`for` Loops

for x in collection do iterates over any type with a ForIn instance (arrays, lists, ranges, etc.):

def printList (xs : List String) : IO Unit := do
  for x in xs do
    IO.println x

def sumArray (arr : Array Nat) : Nat := Id.run do
  let mut total := 0
  for x in arr do
    total := total + x
  return total

Id.run runs a do block in the identity monad, yielding a pure value. Use it when you want for/while loops without any IO.

`while` Loops

while condition do repeats the body as long as the condition holds:

def countDown (n : Nat) : IO Unit := do
  let mut i := n
  while i > 0 do
    IO.println s!"T-minus {i}"
    i := i - 1
  IO.println "Liftoff!"

`return`, `break`, and `continue`

return x exits the current do block immediately with value x
break exits the nearest enclosing for or while loop
continue skips the rest of the current loop iteration

def findFirst (xs : List Nat) (pred : Nat → Bool) : Option Nat := do
  for x in xs do
    if pred x then return x
  return none

def printEven (xs : List Nat) : IO Unit := do
  for x in xs do
    if x % 2 ≠ 0 then continue
    IO.println s!"{x} is even"

def printUpTo10 (xs : List Nat) : IO Unit := do
  for x in xs do
    if x > 10 then break
    IO.println x

IO: Reading Input and Printing Output

The IO monad represents computations that interact with the outside world. Key IO actions:

Printing
Files
Reading Input

-- IO.println : [ToString α] → α → IO Unit
-- IO.print   : [ToString α] → α → IO Unit  (no newline)
-- IO.eprint  : [ToString α] → α → IO Unit  (stderr)

def main : IO Unit := do
  IO.print "Enter your name: "
  let name ← IO.getLine
  IO.println s!"Hello, {name.trim}!"

-- String interpolation with s!
IO.println s!"2 + 2 = {2 + 2}"

-- Read an entire file as a String
def readFileContents (path : String) : IO String := do
  IO.FS.readFile path

-- Write a String to a file
def writeContents (path : String) (contents : String) : IO Unit := do
  IO.FS.writeFile path contents

-- Line-by-line reading
def printLines (path : String) : IO Unit := do
  let contents ← IO.FS.readFile path
  for line in contents.splitOn "\n" do
    IO.println line

-- IO.getLine reads a line from stdin (including newline)
def promptNumber : IO Nat := do
  IO.print "Enter a number: "
  let line ← IO.getLine
  match line.trim.toNat? with
  | some n => return n
  | none   => do
    IO.println "Not a number, defaulting to 0"
    return 0

`try` / `catch` for Exceptions

The IO monad can throw exceptions of type IO.Error. Use try/catch to handle them:

def safeReadFile (path : String) : IO String := do
  try
    IO.FS.readFile path
  catch e =>
    IO.println s!"Error reading file: {e}"
    return ""

-- throw raises an exception explicitly
def mustBePositive (n : Int) : IO Unit := do
  if n ≤ 0 then
    throw (IO.userError s!"Expected positive, got {n}")
  IO.println s!"{n} is positive"

For a typed error channel, use EIO ε or ExceptT ε IO:

inductive AppError where
  | notFound : String → AppError
  | parseError : String → AppError

def loadConfig (path : String) : EIO AppError String := do
  let contents ← (IO.FS.readFile path).toEIO
    (fun _ => AppError.notFound path)
  return contents

`dbg_trace` for Debugging

dbg_trace prints a message to stderr during elaboration (in tactic proofs) or at runtime (in programs). It is useful for debugging without modifying the program’s result.

-- In a tactic proof
theorem debug_example (p q : Prop) (h : p ∧ q) : p := by
  dbg_trace "Starting proof..."
  exact h.1

-- At runtime in a do block (use IO.println for IO code)
def factorial (n : Nat) : Nat :=
  dbg_trace "computing factorial of {n}"
  if n = 0 then 1 else n * factorial (n - 1)

At runtime, dbg_trace writes to stderr and always returns Unit. It is available even in pure code and does not affect the type or value of an expression.

A Complete `do` Example

def main : IO Unit := do
  IO.println "=== Number Guessing Game ==="
  let secret := 42
  let mut attempts := 0
  let mut found := false
  while !found do
    IO.print "Your guess: "
    let line ← IO.getLine
    match line.trim.toNat? with
    | none =>
      IO.println "Please enter a valid number."
    | some guess =>
      attempts := attempts + 1
      if guess < secret then
        IO.println "Too low!"
      else if guess > secret then
        IO.println "Too high!"
      else do
        IO.println s!"Correct! You got it in {attempts} attempts."
        found := true

How do blocks desugar

let x ← m desugars to m >>= fun x => ... (monadic bind).let x := e desugars to let x := e; ... (pure let).return x desugars to pure x.for x in xs do body desugars using ForIn.forIn which iterates and accumulates via a state machine.break and continue are tunneled through BreakT/ContinueT wrapper monads that wrap OptionT, defined in Init.Control.Do.

Introduction

Language Basics

Theorem Proving

Functional Programming

Do-Notation for Monadic and IO Programming in Lean 4

The Basics of `do`

Desugaring

Binding with `←`

`let` and `let mut`

`if` / `else` in `do` Blocks

`for` Loops

`while` Loops

`return`, `break`, and `continue`

IO: Reading Input and Printing Output

`try` / `catch` for Exceptions

`dbg_trace` for Debugging

A Complete `do` Example

Build docs developers (and LLMs) love

Introduction

Language Basics

Theorem Proving

Functional Programming

Documentation Index

​The Basics of do

​Desugaring

​Binding with ←

​let and let mut

​if / else in do Blocks

​for Loops

​while Loops

​return, break, and continue

​IO: Reading Input and Printing Output

​try / catch for Exceptions

​dbg_trace for Debugging

​A Complete do Example

Build docs developers (and LLMs) love

The Basics of `do`

Desugaring

Binding with `←`

`let` and `let mut`

`if` / `else` in `do` Blocks

`for` Loops

`while` Loops

`return`, `break`, and `continue`

IO: Reading Input and Printing Output

`try` / `catch` for Exceptions

`dbg_trace` for Debugging

A Complete `do` Example