Lean theorem prover/System/Monads and do-notation

Plain-language version: Programs and proofs in one language

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Lean is a purely functional language: a function's result depends only on its arguments, and evaluating it changes nothing else. Programs still need failure, state, input and output. Lean represents these effects as values, using monads, and provides do-notation so that programs using them can be written in an imperative style, with sequencing, mutable local variables, loops and early return. This page shows the Monad class, the monad IO, and the features of do-notation, and then prints what Lean 4.34.1 turns a do block into. The result is an ordinary term, which is why programs written this way can still be reasoned about.

The Monad class

A monad is a type constructor m, such as Option or IO, with two operations. pure makes a value into a computation that has no effect, and bind, written >>=, runs one computation and passes its result to the next.

#check @pure
#check @bind

@pure : {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
@bind : {m : Type u_1 → Type u_2} → [self : Bind m] → {α β : Type u_1} → m α → (α → m β) → m β

The class Monad brings these together, as a type class, with the related classes Functor and Applicative. The reference manual notes that these classes follow the use of functors and monads in programming, which is narrower than the general mathematical notion. An instance is not required to obey the monad laws; the separate class LawfulMonad records that it does, and proofs about monadic programs use it.

Option is the simplest useful case. A computation of type Option α either produces a value (some a) or fails (none), and bind stops at the first failure.

def safeDiv (a b : Nat) : Option Nat :=
  if b == 0 then none else some (a / b)

def compute (a b c : Nat) : Option Nat := do
  let x ← safeDiv a b
  let y ← safeDiv x c
  return x + y

#eval compute 100 5 2
#eval compute 100 0 2

example (a b c : Nat) :
    compute a b c =
      (safeDiv a b >>= fun x => safeDiv x c >>= fun y => pure (x + y)) := rfl

The two evaluations print some 30 and none. The example states what the do block means, and rfl proves it: the block is, by definition, a chain of binds. The basic rules are few. A block consisting of one expression is that expression. let x ← e followed by the rest becomes e >>= fun x => …; an expression whose result is not named becomes e >>= fun () => …; and let x := e is an ordinary local definition.

A nested action saves naming a result used once: (← e) inside an expression is lifted out and bound just before the statement that contains it, within the enclosing do block.

def halfPlusOne (a : Nat) : Option Nat := do
  return (← safeDiv a 2) + 1

#eval halfPlusOne 10

This prints some 6.

IO

Input and output are effects of the same kind. Lean prints the definition of IO:

#print IO
#print EIO

@[reducible] def IO : Type → Type :=
EIO IO.Error
def EIO : Type → Type → Type :=
fun ε α => EST ε IO.RealWorld α

An IO action is a computation that may fail with an IO.Error and that takes and returns a token whose type is built from IO.RealWorld (in 4.34.1, Void IO.RealWorld). Christiansen's Functional Programming in Lean explains the device: an action receives a token standing for the world and returns the changed world, and this is safe as long as no token is used twice. Seen from inside the logic, an IO action is a value like any other; seen from outside, it is a set of instructions that the run-time system carries out (see the compiler and runtime). The metaprogramming monads described in metaprogramming in Lean are built on the same base.

Mutable variables, loops and early return

Haskell's do-notation provides sequencing and little more. Ullrich and de Moura's paper "‘do’ Unchained" extends it with three features from imperative languages: local mutable variables, early return, and for loops with break and continue. The paper gives translation rules from each feature back to pure code, implements them in Lean 4, and proves in Lean that the rules preserve the meaning of the program with respect to a simple semantics.

def sumUntilZero (xs : List Nat) : Nat := Id.run do
  let mut total := 0
  for x in xs do
    if x == 0 then break
    total := total + x
  return total

#eval sumUntilZero [3, 4, 0, 10]

This prints 7. Id is the monad with no effect, and Id.run extracts the result, so sumUntilZero is a pure function written in imperative style. A mutable variable is local to its do block and cannot be changed from outside it.

Early return leaves the whole block, from inside a loop if need be:

def findBig (xs : List Nat) : Option Nat := Id.run do
  for x in xs do
    if x > 10 then return some x
  return none

#eval findBig [3, 12, 40]
#eval findBig [1, 2]

The results are some 12 and none. The same features work in IO:

def report (lines : List String) : IO Unit := do
  let mut count := 0
  for line in lines do
    if line.isEmpty then continue
    count := count + 1
    IO.println s!"{count}: {line}"
  IO.println s!"{count} non-empty lines"

#eval report ["alpha", "", "beta"]

1: alpha
2: beta
2 non-empty lines

How they are translated

In the paper's rules, each feature becomes a monad transformer wrapped around the block. A mutable variable becomes the state of a StateT layer, initialised with its first value; a reassignment sets that state. An early return becomes an exception in an ExceptT layer, caught at the edge of the block. A for loop becomes a call to a loop function over the collection, with break and continue as two further exceptions, one caught outside the loop and one around its body. The reference manual describes the implementation in the same terms: the effects are produced by transforming the whole block "in a manner akin to monad transformers", not by rewriting each statement locally, and a loop requires the collection's type to implement the class ForIn.

Lean's own implementation differs in its details from the paper's reference rules. Since version 4.32.0, the default is a new elaborator for do; the earlier one is still available with set_option backward.do.legacy true. What it produces can be printed.

#print sumUntilZero

def sumUntilZero : List Nat → Nat :=
fun xs =>
  (have total := 0;
    do
    let __s ←
      forIn xs total fun x __s =>
          have total := __s;
          if (x == 0) = true then pure (ForInStep.done total)
          else
            have total := total + x;
            pure (ForInStep.yield total)
    have total : Nat := __s
    pure total).run

The loop has become a call to forIn, the method of ForIn. The mutable variable total is the loop's state: each pass of the body receives it as __s and returns the new value. break has become ForInStep.done, which tells forIn to stop, and the normal end of the body has become ForInStep.yield, which tells it to go on. "Mutation" is rebinding a name with have.

#print findBig

def findBig : List Nat → Option Nat :=
fun xs =>
  (do
      let __s ←
        forIn xs (none, ()) fun x __s =>
            if x > 10 then pure (ForInStep.done (some (some x), ())) else pure (ForInStep.yield (none, ()))
      have __r : Option (Option Nat) × Unit := __s
      match __r.fst with
        | some r => pure r
        | none => pure none).run

Here the early return travels in the loop's state. The first component is none while the loop runs normally and some v once return v has been executed; after the loop, a match either returns that value or continues with the rest of the block. This is the exception path of the paper's rules, encoded directly.

Why it matters for proofs

The output of the translation is an ordinary Lean term built from bind, pure, forIn and local definitions. Nothing about it is special to the Lean kernel, and a theorem about a do program is a theorem about that term.

theorem sumUntilZero_nil : sumUntilZero [] = 0 := rfl

example : sumUntilZero [1, 2, 3, 0, 5] = 6 := by decide

theorem findBig_nil : findBig [] = none := rfl

All three are accepted. Ullrich and de Moura prove more general facts in the same way, for example that a block with two nested for loops and an early return equals a search function defined by recursion, for every monad satisfying LawfulMonad, using induction and the simplifier. Local imperativity is therefore a matter of notation. The programs remain pure functions, and the reasoning about them is the reasoning used for any other Lean definition.

Next

Automath begins the history, with the first system for checking mathematics by computer. Within this section, the page on syntax extension and hygienic macros shows how notation of this kind is defined.