Lean4

Practise it in the Academy:IO and the proof boundary →

Module 5 · Lesson 2

The IO Monad

IO is the type of actions that affect the outside world: files, the console, the clock, randomness. A function without IO in its type cannot do any of these.

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
Try it
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

Console input and output are the most common IO operations. Use IO.printlnto write a line, IO.print to write without a newline, and(← IO.getStdin).getLine to read user input.

lean
Try it
1-- Print to console
2def sayHello : IO Unit := do
3  IO.println "Hello, World!"
4
5-- Read from console. Note: there is no bare IO.getLine —
6-- you read from a stream, and stdin is one.
7def askName : IO String := do
8  IO.print "Enter your name: "
9  (← IO.getStdin).getLine
10
11-- Put it together
12def interactive : IO Unit := do
13  IO.print "What's your name? "
14  let name ← (← IO.getStdin).getLine
15  IO.println s!"Hello, {name.trimAscii}!"

File I/O

Reading and writing files is straightforward with the IO.FSnamespace. For simple cases, readFile and writeFilehandle the entire file at once.

lean
Try it
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

When your Lean program is compiled and run from the command line, arguments passed to the executable are available as a list of strings in the main function.

lean
Try it
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
Try it
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.getStdin).getLine
11  let n := input.trimAscii.toString.toNat!
12  IO.println s!"Got {n}"
13  return n * 2

Keep a Pure Core

A common pattern is to keep business logic pure and use IO only for input/output. This keeps code testable and reusable.

lean
Try it
1-- Pure function
2def sanitize (s : String) : String := s.trimAscii.toString.toLower
3
4-- IO wrapper
5def greetUser : IO Unit := do
6  IO.print "Name: "
7  let name ← (← IO.getStdin).getLine
8  let clean := sanitize name
9  IO.println s!"Hello, {clean}!"

Error Handling in IO

IO operations can fail. Use try/catch:

lean
Try it
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
15
16-- (These are three ALTERNATIVES — a file may only define main once.)
ℹ
Lean accepts IO Unit, IO UInt32, and either of those taking List String. With IO Unit the exit code is 0 unless an uncaught exception escapes, in which case it is 1. Use IO UInt32 when you need to signal specific failures to a shell script or CI job.

IO, BaseIO, and EIO

IO is not primitive — it is one member of a small family, and you will see the others in signatures and error messages.

lean
Try it
1-- EIO ε α : an IO action that can fail with an error of type ε
2-- IO α     = EIO IO.Error α    ← the usual one
3-- BaseIO α = EIO Empty α       ← cannot fail at all
4
5#check @IO.getStdin      -- BaseIO IO.FS.Stream  — reading stdin never fails
6#check @IO.FS.readFile   -- ... : IO String      — reading a file can
7
8-- A BaseIO action can be used anywhere an IO action is expected
9-- (it just never takes the failure path), but not the other way round.
💡
If a try/catch gives you "no exceptions to catch"-flavoured type errors, check whether the action is BaseIO — it is telling you the failure you are guarding against cannot happen.

Running External Commands

lean
Try it
1-- Run a command and capture its output
2#eval show IO Unit from do
3  let out ← IO.Process.output { cmd := "echo", args := #["hello"] }
4  IO.println s!"exit={out.exitCode} stdout={out.stdout.trimAscii}"
5
6-- Run and just wait for the exit code
7#eval show IO Unit from do
8  let code ← IO.Process.spawn { cmd := "echo", args := #["hi"] } >>= (·.wait)
9  IO.println s!"exited with {code}"

Useful IO Utilities

lean
Try it
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 (readDir lives on FilePath, not IO.FS)
19def listDir : IO Unit := do
20  let entries ← (System.FilePath.mk ".").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
Try it
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 are ordinary values.

Mixing Pure and Impure Code

lean
Try it
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.getStdin).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
Try it
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
Exercise: Read and Compute

Read a line from input, parse it as a Nat, and print double the value.

lean
Try it
1def readDouble : IO Unit := do
2  IO.print "Enter a number: "
3  let input ← (← IO.getStdin).getLine
4  let n := input.trimAscii.toString.toNat!
5  IO.println s!"Double is {n * 2}"
Do NotationNext: Mutable State