Module 5 · Lesson 2

The IO Monad

IO encapsulates side effects—file I/O, network requests, randomness—while keeping pure functions pure.

Why IO?

Pure functions always return the same output for the same input. But some operations are inherently impure:

Reading user input (different each time)
Writing to a file (changes external state)
Getting current time (depends on when called)
Making HTTP requests (network conditions vary)

The IO type marks functions that perform these effects:

lean

1-- Pure: no IO in type
2def add (x y : Nat) : Nat := x + y
3
4-- Impure: returns IO
5def greet : IO Unit := IO.println "Hello!"
6
7-- The type tells you: this function does I/O

Key Takeaway

If a function's return type includes IO, it might perform side effects. If it doesn't, it's guaranteed pure.

Basic IO Operations

Console I/O

lean

1-- Print to console
2def sayHello : IO Unit := do
3  IO.println "Hello, World!"
4
5-- Read from console
6def askName : IO String := do
7  IO.print "Enter your name: "
8  IO.getLine
9
10-- Put it together
11def interactive : IO Unit := do
12  IO.print "What's your name? "
13  let name ← IO.getLine
14  IO.println s!"Hello, {name.trim}!"

File I/O

lean

1-- Read entire file
2def readConfig : IO String := do
3  IO.FS.readFile "config.txt"
4
5-- Write to file
6def writeLog (msg : String) : IO Unit := do
7  IO.FS.writeFile "log.txt" msg
8
9-- Append to file
10def appendLog (msg : String) : IO Unit := do
11  let handle ← IO.FS.Handle.mk "log.txt" .append
12  handle.putStrLn msg

Command Line Arguments

lean

1def main (args : List String) : IO Unit := do
2  IO.println s!"Got {args.length} arguments"
3  for arg in args do
4    IO.println s!"  - {arg}"

Composing IO Actions

lean

1-- Sequence with do notation
2def program : IO Unit := do
3  IO.println "Step 1"
4  IO.println "Step 2"
5  IO.println "Step 3"
6
7-- Pass results between actions
8def compute : IO Nat := do
9  IO.println "Computing..."
10  let input ← IO.getLine
11  let n := input.trim.toNat!
12  IO.println s!"Got {n}"
13  return n * 2

Error Handling in IO

IO operations can fail. Use try/catch:

lean

1def safeRead (path : String) : IO String := do
2  try
3    IO.FS.readFile path
4  catch e =>
5    IO.println s!"Error reading file: {e}"
6    return ""
7
8-- Or return an option/result
9def tryReadFile (path : String) : IO (Option String) := do
10  try
11    let content ← IO.FS.readFile path
12    return some content
13  catch _ =>
14    return none

⚠

Unlike Except, IO exceptions are actual runtime exceptions. Use try/catch to handle them.

The main Function

Every Lean executable has a main function:

lean

1-- Simplest form
2def main : IO Unit := do
3  IO.println "Hello, World!"
4
5-- With command line arguments
6def main (args : List String) : IO Unit := do
7  match args with
8  | [] => IO.println "No arguments"
9  | _ => IO.println s!"Arguments: {args}"
10
11-- With exit code
12def main : IO UInt32 := do
13  IO.println "Running..."
14  return 0  -- 0 = success

Useful IO Utilities

lean

1-- Get current time
2def showTime : IO Unit := do
3  let now ← IO.monoMsNow
4  IO.println s!"Milliseconds since start: {now}"
5
6-- Environment variables
7def getEnv : IO Unit := do
8  let path ← IO.getEnv "PATH"
9  match path with
10  | none => IO.println "PATH not set"
11  | some p => IO.println s!"PATH = {p}"
12
13-- Current working directory
14def showCwd : IO Unit := do
15  let cwd ← IO.currentDir
16  IO.println s!"Current directory: {cwd}"
17
18-- List directory contents
19def listDir : IO Unit := do
20  let entries ← IO.FS.readDir "."
21  for entry in entries do
22    IO.println entry.fileName

Deep Dive: IO is Lazy

An IO value is a description of an action, not the action itself. The action only runs when the runtime executes it.

lean

1-- This doesn't print anything:
2def action : IO Unit := IO.println "Hello"
3
4-- It's just a value. The printing happens when main runs:
5def main : IO Unit := action

This is why you can pass IO actions around, store them in data structures, and compose them—they're just values.

Mixing Pure and Impure Code

lean

1-- Pure function
2def double (n : Nat) : Nat := n * 2
3
4-- Use pure functions inside IO
5def pureInIO : IO Unit := do
6  let x := double 21  -- Pure computation
7  IO.println s!"Result: {x}"
8
9-- But you can't use IO inside pure functions
10-- def bad : Nat := do
11--   let x ← IO.getLine  -- Error! Can't do IO here
12--   x.length

💡

Keep as much logic as possible in pure functions. Use IOonly at the boundaries—reading input, writing output.

Running IO in #eval

lean

1-- #eval can run IO actions
2#eval IO.println "This prints in the editor"
3
4-- Useful for quick tests
5#eval do
6  IO.println "Line 1"
7  IO.println "Line 2"
8  return 42

Do Notation Next: Mutable State