I/O and Monads

• Every program eventually has to talk to the world

What Is IO? (And What Is a Monad?)

• 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 IO 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 IO from leaking into pure functions
• Separately, do and ← (left arrow) are how you sequence effectful actions
  • 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 to use monads in Lean
  • (DEBT) We will revisit the theory once we are comfortable doing I/O

Hello World

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

#eval main

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 doesn't have exceptions
  • Errors are handled with sum types like Except, which we'll cover later (DEBT)

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

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

Forgetting do

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

#eval main

io/ex_missing_do.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
io/ex_missing_do.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 do, 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

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
  • Warning: 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

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

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()
  • Type \leftarrow in the editor
• 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

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

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

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

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

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

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

#eval main

io/ex_bug_no_do.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 "Hello" IO.println
io/ex_bug_no_do.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.

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

io/ex_bug_let_bind.lean:6:2: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  ToString (IO String)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
io/ex_bug_let_bind.lean:8: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.

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

io/ex_bug_return.lean:4:2: error: Type mismatch
  msg
has type
  String
but is expected to have type
  IO String
io/ex_bug_return.lean:10: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.

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

io/ex_bug_return_type.lean:3:2: error: Type mismatch
  IO.println (toString "Announcing: " ++ toString item)
has type
  IO Unit
but is expected to have type
  IO String
io/ex_bug_return_type.lean:6:2: error: Type mismatch
  announce "Lean 4"
has type
  IO String
but is expected to have type
  IO Unit
io/ex_bug_return_type.lean:8: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.

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

io/ex_bug_arrow.lean:5:15: error: Type mismatch
  double 5
has type
  Int
but is expected to have type
  IO ?m.7
io/ex_bug_arrow.lean:8: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.

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

Step 1: start

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

#eval main

Hello, Lean!

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

hello
world

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

ready

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

Sum is 0

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

again

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

Hello, stranger!