I/O

• Every program eventually has to talk to the world
• But pure functions always return the same result for the same arguments, so how do we handle something like reading from a file?
• The answer is complex in theory but simple(r) in practice

What Is IO?

• A function that does I/O has IO in its return type
  • String means "a string, computed purely"
  • IO String means "an action that, when run, produces a string"
  • This pattern's formal name is a monad
• The compiler enforces that I/O only happens where you say it does
  • Pure functions are guaranteed not to have side effects
  • You can test and reason about them without worrying about hidden state
• This is like Python's async def: an async function must return an Awaitable
  • You cannot accidentally run an async function from sync code
  • Lean's IO type is the same idea: the compiler prevents I/O from leaking into pure functions
• Separately, do and ← (left arrow) are how you sequence effectful actions
  • Type \leftarrow in the editor
  • This is the monad part: chaining steps where each depends on the last
  • Like await lets you write sequential-looking code asynchronously, ← does the same for IO
• You do not need to understand the theory of monads to use IO in Lean
  • But we describe it briefly in an appendix

Hello World

-- Every Lean program starts with main
def main : IO Unit :=
  IO.println "Hello, world!"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
Hello, world!

• main is the entry point for Lean programs
  • Like Python's if __name__ == "__main__": block
• IO Unit is the return type: IO means "does input/output", Unit means "no useful return value"
  • Unit is like Python's None: the side effects are the point
• IO.println prints a string followed by a newline
  • Newline plus indentation isn't required, but it helps
• #eval main runs the action during compilation so we can see the output
• Lean's pure functions cannot raise exceptions
  • I/O actions can fail at runtime and are caught with try/catch, which we discuss below
  • Errors in pure code are handled with sum types like Except, which we will also discussed below

Doing More Than One Thing

-- Use `do` to run IO actions one after another
def main : IO Unit := do
  IO.println "Step 1: start"
  IO.println "Step 2: middle"
  IO.println "Step 3: done"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
Step 1: start
Step 2: middle
Step 3: done

• do groups a sequence of IO actions into one
  • Statements run top to bottom
• Without do, we can only write one IO action per function body
• Each line in a do block runs in order and must return IO Unit
  • Unless we capture it: more on that shortly
• If your function body is a single IO action, no do is needed
• If you want two or more actions in sequence, wrap them in do
• ; can be used as an alternative separator inside do blocks
  • E.g., IO.println "Hi"; IO.println "there" is equivalent to two lines
  • Generally avoided to keep code readable

Forgetting do

-- Forgetting `do` is the most common IO mistake
def main : IO Unit :=
  IO.println "Starting..."
  IO.println "Done!"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
missing_do_err.lean:4:2: error: Application type mismatch: The argument
  IO.println
has type
  ?m.3 → IO Unit
but is expected to have type
  Void IO.RealWorld
in the application
  IO.println "Starting..." IO.println
missing_do_err.lean:6:0: error: Aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.

To attempt to evaluate anyway despite the risks, use the '#eval!' command.

• Forgetting do is the most common IO mistake
• Without it, Lean tries to use the second IO.println as an argument to the first
  • That's why the error message mentions "application type mismatch"
• The fix: add do after :=

Pure Values Inside do

-- `let x := expr` binds a pure value inside a do block
def greet (name : String) : String :=
  s!"Hello, {name}!"

def main : IO Unit := do
  let msg := greet "Lean"
  IO.println msg

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
Hello, Lean!

• let x := expr binds a pure (non-IO) value inside a do block
  • Like Python's x = expr inside an async function
• greet is a plain function that returns a String (no I/O)
• You can call pure functions freely inside do
  • Only the final IO.println does I/O
• The compiler will reject let msg ← greet "Lean" because greet does not return an IO
• let _ := expr is the discard pattern
  • It binds a value but throws it away
  • The underscore means "I don't intend to use this"
  • It also suppresses the unused-variable warning from the compiler
• Be careful: let _ := someIOAction stores the action without running it
  • Use ← for IO

Functions That Return IO Actions

-- Functions can return IO actions, not just plain values
def printTwice (msg : String) : IO Unit := do
  IO.println msg
  IO.println msg

def main : IO Unit := do
  printTwice "echo!"
  printTwice "again"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
echo!
echo!
again
again

• A function can return an IO Unit: a reusable IO action
  • Like Python's async def, calling it gives you something you still have to run
• printTwice "echo!" runs two IO.println calls in sequence
• IO functions compose: main calls printTwice twice

Capturing Results from IO

-- Use ← to capture the result of an IO action
def makeGreeting : IO String := do
  IO.println "Building greeting..."
  return "Hello from IO!"

def main : IO Unit := do
  let msg ← makeGreeting
  IO.println msg

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
Building greeting...
Hello from IO!

• Use let x ← ioAction (the left-arrow ←) to capture the result of an IO action
  • Like Python's x = await some_coroutine()
• makeGreeting has type IO String: it is an action that produces a String
• return expr wraps a pure value as an IO result
  • This is not the same as Python's return, which exits the function immediately
  • Lean's return stays in the do block: it just marks a value as an IO result
  • Yes, this is confusing…
• let msg ← makeGreeting runs the action and binds the resulting String to msg
• Two binding forms to remember:
  • let x := expr is a pure expression, no IO
  • let x ← action is an I/O action, captures its result

Reading Input

-- IO.getStdin gives access to standard input
def main : IO Unit := do
  IO.println "Enter your name:"
  let stdin ← IO.getStdin
  let name ← stdin.getLine
  IO.println s!"Hello, {name.trimAscii}!"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
Enter your name:
Hello, !

• IO.getStdin returns an IO.FS.Stream connected to standard input
• stdin.getLine reads one line and returns it as an IO String
• Both require ← because they are IO actions that produce values
• String.trimAscii removes leading and trailing whitespace, including the trailing newline
  • Without .trimAscii, getLine returns the newline character as part of the string
  • This would make s!"Hello, {name}!" print an unwanted line break
• The output above shows an empty name because #eval runs inside the Lean compiler process
  • The compiler claims stdin for its own use, so stdin.getLine returns an empty string
  • This is a limitation of #eval, not of Lean's IO system
  • In the next lesson we will compile and run programs as proper executables, where stdin works correctly

Chaining IO Actions

-- Chain multiple ← binds in a single do block
def main : IO Unit := do
  IO.println "Enter your first name:"
  let stdin ← IO.getStdin
  let first ← stdin.getLine
  IO.println "Enter your last name:"
  let last ← stdin.getLine
  IO.println s!"Hello, {first.trimAscii} {last.trimAscii}!"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
Enter your first name:
Enter your last name:
Hello,  !

• do blocks compose naturally: you can chain as many ← binds as you need
• Each ← runs the action and captures its result for the next step
• Here getLine is called twice: once for the first name, once for the last name
  • Both captures are combined in a single IO.println
• Like writing multiple await calls in one async function

For Loops in do Blocks

-- Iterate over a list in a do block with for
def main : IO Unit := do
  let fruits := ["apple", "banana", "cherry"]
  for fruit in fruits do
    IO.println fruit

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
apple
banana
cherry

• for x in list do iterates over a list inside a do block
  • Like Python's for x in list: but the body is an IO action
• Each iteration runs in sequence, top to bottom
• Works with List, Array, and any type that implements ForIn
  • Including the results of IO.FS.readDir (used in archive)
• The loop is syntactic sugar for recursion: there is no mutable loop variable by default

For Loops Elsewhere

• for with let mut also works in pure functions that do not involve IO
  • Lean implicitly uses the identity monad and compiles the loop to a pure fold
  • The syntax is identical: for x in xs do body

-- for with let mut works in pure functions, not just IO do blocks
def countPositive (xs : List Int) : Nat :=
  let mut count := 0
  for x in xs do
    if x > 0 then count := count + 1
  count

#eval countPositive [-3, 1, -1, 4, 1, 5, -9, 2, -6]

5

Accumulating Results with for

-- Accumulate a result across loop iterations using let mut
def main : IO Unit := do
  let words := ["hello", "world", "from", "Lean"]
  let mut count := 0
  for w in words do
    if w.length > 4 then
      count := count + 1
  IO.println s!"Words longer than 4 chars: {count}"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
Words longer than 4 chars: 2

• let mut count := 0 declares a mutable variable in a do block
  • Only valid inside do: pure functions cannot use mut
• count := count + 1 updates it
  • Without :=, the variable is read-only
• Like Python's count = 0; for w in words: if …: count += 1
• Lean guarantees mut variables don't escape the do block

What let mut Really Does

-- let mut looks like mutation but compiles to state-passing under the hood
-- The compiler rewrites mutable variables into function arguments
def countEvens (xs : List Int) : IO Nat := do
  let mut count := 0
  for x in xs do
    if x % 2 == 0 then
      count := count + 1
  return count

-- The same logic as a pure function using foldl (no IO, no mutation)
def countEvensPure (xs : List Int) : Nat :=
  xs.foldl (fun acc x => if x % 2 == 0 then acc + 1 else acc) 0

#eval countEvens [1, 2, 3, 4, 5, 6]
#eval countEvensPure [1, 2, 3, 4, 5, 6]

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
3
3

• let mut is syntactic sugar
  • The compiler rewrites mutable variables as extra function arguments threaded through each step
  • The generated code is purely functional: data structures are not mutated in place
  • This is why pure functions can remain efficient even without mutable state
  • The compiler handles the bookkeeping
• The pure foldl version and the let mut loop produce the same result
  • For straightforward accumulation, the pure form is often shorter
  • For complex logic with multiple conditions or early exit, let mut is usually easier to read
• Both approaches have the same run time

Summary

• do and ← let you chain IO actions in sequence
• The practical rules are:
  • Use do to sequence actions
  • Use let x ← action to capture an IO result
  • Use let x := expr for pure computation
  • Use return expr to produce an IO result from a pure value
• Lean's IO is more than just files and sockets
• It also manages random number generation and any other effectful computation

Errors Without Exceptions

-- Except carries either a success value or an error message
def safeDivide (a b : Int) : Except String Int :=
  if b == 0 then Except.error "division by zero"
  else Except.ok (a / b)

#eval match safeDivide 10 2 with
  | Except.ok n    => s!"result: {n}"
  | Except.error e => s!"error: {e}"

#eval match safeDivide 10 0 with
  | Except.ok n    => s!"result: {n}"
  | Except.error e => s!"error: {e}"

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
"result: 5"
"error: division by zero"

• Except String Int is a sum type with two constructors:
  • Except.ok n: success, carrying a value of type Int
  • Except.error e: failure, carrying a message of type String
• Like the (value, error) convention of other languages, but the compiler forces you to check both cases
• match on an Except is exhaustive: you cannot forget the error case
• Use Except for pure functions that can fail with a reason
  • Use Option when absence is normal and no explanation is needed

I/O Can Fail

-- try/catch wraps IO actions that might fail
def readFileSafe (path : String) : IO (Option String) := do
  try
    let content ← IO.FS.readFile path
    return some content
  catch _ =>
    return none

def main : IO Unit := do
  -- hello_world.lean exists in this directory
  match ← readFileSafe "hello_world.lean" with
  | some _ => IO.println "File found"
  | none   => IO.println "File not found"
  -- no_such_file.txt does not exist
  match ← readFileSafe "no_such_file.txt" with
  | some _ => IO.println "Unexpected success"
  | none   => IO.println "Missing file handled gracefully"

#eval main

warning: failed to query latest release, using existing version 'leanprover/lean4:v4.30.0'
File found
Missing file handled gracefully

• try action catch _ => fallback catches any IO exception
  • The _ discards the exception value
  • Inspect it with catch e => ... if needed
• IO operations like IO.FS.readFile throw on failure (file not found, permission denied, etc.)
• Wrapping in try/catch converts an exception into a safe Option or Except value
• Like Python's try: ... except OSError: ... but typed
  • The return type shows the fallback
• Pure Except (from the previous section) and IO try/catch are complementary:
  • Pure functions use Except to report errors without side effects
  • IO functions use try/catch to handle runtime failures

Three Ways to Do It

Lean splits failure across three mechanisms where Python uses exceptions for all of them:

1. Use Option in pure functions when absence is normal and no explanation needed, e.g., looking up a key that may not exist.

2. Use Except e a in pure functions when failure needs a reason, e.g., parsing a string that may be malformed.

3. Use try/catch in IO actions when runtime failure outside your control, e.g., file not found, or a network error.

4. Option and Except appear in function signatures, so the compiler forces callers to handle failure

5. try/catch is only available in IO: you cannot silently ignore an IO exception
6. When migrating from Python:
   • Replace None returns with Option
   • Replace ValueError/KeyError in pure logic with Except
   • Replace OSError/IOError with try/catch around IO actions

-- This should print two lines but has a bug. Fix it.
def main : IO Unit :=
  IO.println "Hello"
  IO.println "World"

#eval main

-- Should print the greeting, but has a bug. Fix it.
def makeMsg : IO String := return "Hello, Lean!"

def main : IO Unit := do
  let msg := makeMsg
  IO.println msg

#eval main

-- This function should return a greeting, but has a bug. Fix it.
def getGreeting : IO String := do
  let msg := "Hello!"
  msg

def main : IO Unit := do
  let g ← getGreeting
  IO.println g

#eval main

-- This function should print a message, but its return type is wrong. Fix it.
def announce (item : String) : IO String := do
  IO.println s!"Announcing: {item}"

def main : IO Unit := do
  announce "Lean 4"

#eval main

-- Should print the doubled value, but has a bug. Fix it.
def double (n : Int) : Int := n * 2

def main : IO Unit := do
  let result ← double 5
  IO.println s!"Result: {result}"

#eval main

-- Should print both lines, but only prints one. Fix it.
def main : IO Unit := do
  IO.println "Step 1: start"
  let _ := IO.println "Step 2: done"

#eval main

-- Add a second line so main prints "Hello, Lean!" then "Ready to go!"
def main : IO Unit := do
  IO.println "Hello, Lean!"

#eval main

-- Fix printLoud so it prints the message in uppercase.
-- Hint: String.toUpper converts a String to all caps.
def printLoud (msg : String) : IO Unit :=
  IO.println msg

def main : IO Unit := do
  printLoud "hello"
  printLoud "world"

#eval main

-- Fix buildMsg so it returns "Message: " ++ text (using return).
def buildMsg (text : String) : IO String :=
  return text

def main : IO Unit := do
  let msg ← buildMsg "ready"
  IO.println msg

#eval main

-- Fix main so it computes and prints the sum of the list (should be 15).
def addUp (xs : List Int) : Int := xs.foldl (· + ·) 0

def main : IO Unit := do
  IO.println "Sum is 0"

#eval main

-- Fix repeat3 so it calls IO.println with msg exactly three times.
def repeat3 (msg : String) : IO Unit := do
  IO.println msg

def main : IO Unit := do
  repeat3 "again"

#eval main

-- Fix main to read a name from stdin and print "Hello, <name>!"
-- instead of always printing "Hello, stranger!"
def main : IO Unit := do
  let stdin ← IO.getStdin
  let _name ← stdin.getLine
  IO.println "Hello, stranger!"

#eval main