Do Notation

1def lookup (key : String) (env : List (String × Nat)) : Option Nat :=
2  env.lookup key
3
4-- Without do notation: deeply nested
5def compute (env : List (String × Nat)) : Option Nat :=
6  match lookup "x" env with
7  | none => none
8  | some x => match lookup "y" env with
9    | none => none
10    | some y => match lookup "z" env with
11      | none => none
12      | some z => some (x + y + z)

1-- With do notation: flat and readable
2def compute' (env : List (String × Nat)) : Option Nat := do
3  let x ← lookup "x" env
4  let y ← lookup "y" env
5  let z ← lookup "z" env
6  return x + y + z
7
8def env := [("x", 1), ("y", 2), ("z", 3)]
9#eval compute' env  -- some 6

1-- This do block:
2def example1 : Option Nat := do
3  let x ← some 5
4  let y ← some 3
5  return x + y
6
7-- Is equivalent to:
8def example2 : Option Nat :=
9  (some 5).bind fun x =>
10  (some 3).bind fun y =>
11  pure (x + y)
12
13-- Or using >>= operator:
14def example3 : Option Nat :=
15  some 5 >>= fun x =>
16  some 3 >>= fun y =>
17  pure (x + y)

1def safeDivide (x y : Nat) : Option Nat :=
2  if y == 0 then none else some (x / y)
3
4def calculation : Option Nat := do
5  let a ← safeDivide 10 2   -- a = 5
6  let b ← safeDivide a 0    -- Fails! Returns none
7  let c ← safeDivide b 1    -- Never reached
8  return c

1-- return wraps a pure value
2def justFive : Option Nat := do
3  return 5  -- same as: some 5
4
5-- Can be anywhere in the block
6def example : Option Nat := do
7  let x ← some 3
8  if x > 10 then
9    return 0  -- Early return
10  return x * 2

1def example : Option Nat := do
2  let x ← some 5      -- ← extracts from Option
3  let y = x * 2       -- = is pure computation
4  let z = y + 1       -- no Option involved
5  return z            -- some 11

1def optionExample : Option String := do
2  let x ← some "hello"
3  let y ← some "world"
4  return s!"{x} {y}"

1def divide (x y : Int) : Except String Int :=
2  if y == 0 then .error "division by zero" else .ok (x / y)
3
4def exceptExample : Except String Int := do
5  let a ← divide 10 2
6  let b ← divide a 0   -- Fails with error message
7  return b

1-- For List, do represents all combinations
2def pairs : List (Nat × Nat) := do
3  let x ← [1, 2]
4  let y ← [10, 20]
5  return (x, y)
6
7#eval pairs  -- [(1, 10), (1, 20), (2, 10), (2, 20)]

1def greet : IO Unit := do
2  IO.println "What's your name?"
3  let name ← IO.getLine
4  IO.println s!"Hello, {name}!"

1def classify (n : Nat) : IO Unit := do
2  if n == 0 then
3    IO.println "zero"
4  else if n < 10 then
5    IO.println "small"
6  else
7    IO.println "large"

1def printNumbers : IO Unit := do
2  for i in [1, 2, 3, 4, 5] do
3    IO.println s!"Number: {i}"
4
5def sumList (xs : List Nat) : IO Nat := do
6  let mut sum := 0
7  for x in xs do
8    sum := sum + x
9  return sum

1def countdown : IO Unit := do
2  let mut n := 5
3  while n > 0 do
4    IO.println s!"{n}..."
5    n := n - 1
6  IO.println "Liftoff!"

1-- This doesn't work:
2-- def bad : IO Nat := do
3--   let x ← some 5    -- Option, not IO!
4--   return x
5
6-- Convert Option to IO by handling the failure:
7def good : IO Nat := do
8  let opt : Option Nat := some 5
9  match opt with
10  | none => return 0
11  | some x => return x