PMA Publisher: Published from the Principia Machina source

2026-10-15T19:35:22Z

Published from the Principia Machina source

← Older revision		Revision as of 19:35, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:Monads and do-notation}}		{{DISPLAYTITLE:Monads and do-notation}}
	{{Plebeian\|Lean theorem prover/Explainers/Programs and proofs in one language}}		{{Plebeian\|Lean theorem prover/Explainers/Programs and proofs in one language}}
			{{Lean theorem prover map}}

	Lean is a purely functional language: a function's result depends only on its arguments,		Lean is a purely functional language: a function's result depends only on its arguments,

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:01:10Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:Monads and do-notation}}
{{Plebeian|Lean theorem prover/Explainers/Programs and proofs in one language}}

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
<code>Monad</code> class, the monad <code>IO</code>, and the features of do-notation, and
then prints what Lean 4.34.1 turns a <code>do</code> 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 <code>m</code>, such as <code>Option</code> or
<code>IO</code>, with two operations. <code>pure</code> makes a value into a computation that
has no effect, and <code>bind</code>, written <code>>>=</code>, runs one computation and
passes its result to the next.

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
#check @pure
#check @bind
</pre>

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">@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 β</pre>

The class <code>Monad</code> brings these together, as a
[[Lean theorem prover/System/Type classes and instance resolution|type class]], with the
related classes <code>Functor</code> and <code>Applicative</code>. The reference manual
notes that these classes follow the use of functors and monads in programming, which is
narrower than the general mathematical notion.<ref name="rm-monads">"Functors, Monads and do-Notation", chapter of ''The Lean Language Reference'' (edition covering Lean 4.34.0), introduction and section 18.3 "Syntax". [https://lean-lang.org/doc/reference/4.34.0/Functors___-Monads-and--do--Notation/ lean-lang.org/doc/reference/4.34.0/Functors___-Monads-and--do--Notation/]; [https://lean-lang.org/doc/reference/4.34.0/Functors___-Monads-and--do--Notation/Syntax/ …/Syntax/]</ref>
An instance is not required to obey the monad laws; the separate class
<code>LawfulMonad</code> records that it does, and proofs about monadic programs use
it.<ref name="rm-monads" /><ref name="do">Sebastian Ullrich and Leonardo de Moura, "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)", ''Proceedings of the ACM on Programming Languages'' 6 (ICFP), article 109, August 2022, 28 pp. doi:[https://doi.org/10.1145/3547640 10.1145/3547640]; author's copy [https://lean-lang.org/papers/do.pdf lean-lang.org/papers/do.pdf].</ref>

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

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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
</pre>

The two evaluations print <code>some 30</code> and <code>none</code>. The
<code>example</code> states what the <code>do</code> block means, and <code>rfl</code>
proves it: the block is, by definition, a chain of <code>bind</code>s. The basic rules are
few. A block consisting of one expression is that expression. <code>let x ← e</code>
followed by the rest becomes <code>e >>= fun x => …</code>; an expression whose result is
not named becomes <code>e >>= fun () => …</code>; and <code>let x := e</code> is an ordinary
local definition.<ref name="fpil-do">David Thrane Christiansen, ''Functional Programming in Lean'', online book (code tested with Lean 4.33.0), section 4.4 "<code>do</code>-Notation for Monads". [https://lean-lang.org/functional_programming_in_lean/Monads/do--Notation-for-Monads/ lean-lang.org/functional_programming_in_lean/Monads/do--Notation-for-Monads/]</ref><ref name="rm-monads" />

A '''nested action''' saves naming a result used once: <code>(← e)</code> inside an
expression is lifted out and bound just before the statement that contains it, within the
enclosing <code>do</code> block.<ref name="do" />

<pre class="lean lean-cont" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
def halfPlusOne (a : Nat) : Option Nat := do
return (← safeDiv a 2) + 1

#eval halfPlusOne 10
</pre>

This prints <code>some 6</code>.

== IO ==

Input and output are effects of the same kind. Lean prints the definition of
<code>IO</code>:

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
#print IO
#print EIO
</pre>

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">@[reducible] def IO : Type → Type :=
EIO IO.Error
def EIO : Type → Type → Type :=
fun ε α => EST ε IO.RealWorld α</pre>

An <code>IO</code> action is a computation that may fail with an <code>IO.Error</code> and
that takes and returns a token whose type is built from <code>IO.RealWorld</code> (in 4.34.1,
<code>Void IO.RealWorld</code>).<ref name="fpil-io" /> 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.<ref name="fpil-io">David Thrane Christiansen, ''Functional Programming in Lean'', online book (code tested with Lean 4.33.0), section 4.5 "The IO Monad". [https://lean-lang.org/functional_programming_in_lean/Monads/The-IO-Monad/ lean-lang.org/functional_programming_in_lean/Monads/The-IO-Monad/]</ref>
Seen from inside the logic, an <code>IO</code> action is a value like any other; seen from
outside, it is a set of instructions that the run-time system carries out (see
[[Lean theorem prover/System/The compiler and runtime|the compiler and runtime]]). The
metaprogramming monads described in
[[Lean theorem prover/System/Metaprogramming in Lean|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 <code>for</code> loops with <code>break</code> and
<code>continue</code>. 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.<ref name="do" />

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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]
</pre>

This prints <code>7</code>. <code>Id</code> is the monad with no effect, and
<code>Id.run</code> extracts the result, so <code>sumUntilZero</code> is a pure function
written in imperative style. A mutable variable is local to its <code>do</code> block and
cannot be changed from outside it.<ref name="rm-monads" />

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

<pre class="lean lean-cont" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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]
</pre>

The results are <code>some 12</code> and <code>none</code>. The same features work in
<code>IO</code>:

<pre class="lean lean-cont" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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"]
</pre>

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">1: alpha
2: beta
2 non-empty lines</pre>

== 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 <code>StateT</code> layer, initialised with its
first value; a reassignment sets that state. An early return becomes an exception in an
<code>ExceptT</code> layer, caught at the edge of the block. A <code>for</code> loop becomes
a call to a loop function over the collection, with <code>break</code> and
<code>continue</code> as two further exceptions, one caught outside the loop and one around
its body.<ref name="do" /> 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 <code>ForIn</code>.<ref name="rm-monads" />

Lean's own implementation differs in its details from the paper's reference
rules.<ref name="do" /> Since version 4.32.0, the default is a new elaborator for
<code>do</code>; the earlier one is still available with <code>set_option
backward.do.legacy true</code>.<ref name="rn432">"Lean 4.32.0", in "Release Notes", ''The Lean Language Reference'' (edition covering Lean 4.34.0), Highlights and Language sections. [https://lean-lang.org/doc/reference/4.34.0/releases/v4.32.0/ lean-lang.org/doc/reference/4.34.0/releases/v4.32.0/]</ref>
What it produces can be printed.

<pre class="lean lean-cont" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
#print sumUntilZero
</pre>

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">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</pre>

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

<pre class="lean lean-cont" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
#print findBig
</pre>

<pre class="lean-output" style="background: #ffffff; border: 1px dashed #a2a9b1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">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</pre>

Here the early return travels in the loop's state. The first component is
<code>none</code> while the loop runs normally and <code>some v</code> once
<code>return v</code> has been executed; after the loop, a <code>match</code> 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 <code>bind</code>,
<code>pure</code>, <code>forIn</code> and local definitions. Nothing about it is special to
the Lean kernel, and a theorem about a <code>do</code> program is a theorem about that term.

<pre class="lean lean-cont" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
theorem sumUntilZero_nil : sumUntilZero [] = 0 := rfl

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

theorem findBig_nil : findBig [] = none := rfl
</pre>

All three are accepted. Ullrich and de Moura prove more general facts in the same way, for
example that a block with two nested <code>for</code> loops and an early return equals a
search function defined by recursion, for every monad satisfying <code>LawfulMonad</code>,
using induction and the simplifier.<ref name="do" /> 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 ==

[[Lean theorem prover/History/Automath|Automath]] begins the history, with the first system
for checking mathematics by computer. Within this section, the page on
[[Lean theorem prover/System/Syntax extension and hygienic macros|syntax
extension and hygienic macros]] shows how notation of this kind is defined.

== References ==

<references />

Lean theorem prover/System/Monads and do-notation - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source