Error Handling and IO

Except and IO

Except ε α represents a computation that either succeeds with .ok v or fails with .error msg
Unlike Option, the failure case carries a message that explains what went wrong
do notation works for Except the same way it does for Option: ← short-circuits on .error and the message propagates automatically
IO α is the type of a computation that can perform side effects and return a value of type α; it cannot be called from pure code
Inside an IO do block, let x ← action runs action and binds its result; return v wraps a pure value
IO.FS.readFile and IO.FS.writeFile read and write text files; IO.println writes to standard output
A reliable pattern: write the core logic as a pure function returning Except, test it with #guard, then call it from a thin IO wrapper

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

#guard safeDivide 10 2 == .ok 5
#guard safeDivide 10 0 == .error "division by zero"

-- do notation with Except: <- short-circuits on .error
def compute (a b c : Int) : Except String Int := do
  let x ← safeDivide a b
  let y ← safeDivide x c
  return x + y

#guard compute 10 2 1 == .ok 10
#guard compute 10 0 1 == .error "division by zero"

-- Pure core: validate and transform data
def parseAge (s : String) : Except String Nat :=
  match s.toNat? with
  | none   => .error s!"not a number: {s}"
  | some n => if n > 150 then .error s!"unrealistic age: {n}" else .ok n

#guard parseAge "25"  == .ok 25
#guard parseAge "abc" == .error "not a number: abc"
#guard parseAge "200" == .error "unrealistic age: 200"

-- Pure helper: parse one "name,age" line
def parseLine (line : String) : Except String (String × Nat) :=
  match line.splitOn "," with
  | [name, age] => parseAge age.trim |>.map fun n => (name.trim, n)
  | _           => .error s!"bad format: {line}"

#guard parseLine "Alice, 30" == .ok ("Alice", 30)
#guard parseLine "Bob, abc"  == .error "not a number: abc"

-- IO wrapper: read, process each line, write results
-- Pure logic above is already tested; IO here is a thin shell
def processFile (inPath outPath : String) : IO Unit := do
  let text ← IO.FS.readFile inPath
  let results := text.splitOn "\n" |>.filterMap fun line =>
    match parseLine line with
    | .ok (name, age) => some s!"{name} is {age} years old"
    | .error _        => none
  let output := results.foldl (fun acc s => acc ++ s ++ "\n") ""
  IO.FS.writeFile outPath output

Exercises

Safe Square Root

Write safeSqrt : Float → Except String Float that returns .error "negative input" for values below zero
Verify on 4.0, 0.0, and -1.0

Parse and Add

Write parseAndAdd : String → String → Except String Int that converts two strings to integers using String.toInt? and returns their sum
Convert the Option result to Except with a descriptive error message when parsing fails

File Line Count

Write an IO function that reads a file and prints the number of lines it contains
Use String.splitOn "\n" to split the contents

Validate and Chain

Write validateName : String → Except String String that returns .error when the name is empty or longer than 50 characters
Chain it with parseAge from the lesson using do notation to validate both a name and an age from strings
Return a formatted greeting on success