Lecture 2.3: Functional Programming — Monads

We take a look at an important functional programming abstraction: monads

We will explain the concept from the ground up and see how it is used in Lean

Demo (Part 1)



Monads generalize computation with side effects

Haskell showed that monads can be used very successful to write imperative programs

In Lean, they are used to write imperative programs, but also to reason about them via the so-called monadic laws

Type Effect
option α failure when none; some a is the concrete result
set α nondeterministic behavior
t → α reading (i.e. read elements of type t, e.g. configuration)
ℕ × α adjoin running time (e.g. for modeling algorithmic complexity)
string × α adjoin text output (e.g. logging)
prob α probability (i.e. using random number generators)
io α interaction with the operating system
tactic α interaction with the prover (i.e. Lean)

All these are type constructors M parameterized by a type α (e.g. M := option)

Some effects can be combined, e.g. option (t → α)

Some effects (e.g. set α, prob α) are not executable; they are only for modeling programs abstractly in the logic

Monads are a mathematical structure, so we use class to add them as a type class

Constant Description
pure a no side effect, just the value a (also called return)
bind f g execute f then execute g with the result of f

Specific Ms may provide further operators, e.g. ways to extract the value stored in M

Monads are useful

Demo (Part 2)


Newly introduced syntax


Syntax Description
do indicates the start of a monadic program
bind, >>= combines effectful computations
kleisli, >=> combines effectful computations of type α → M β


Syntax Description
class declares a structure to be a type class
attribute adds an attribute (e.g. simp) to an already defined constant
variable, variables declares variables, which are added to a definition when they are used


Name Description
funext function extensionality


Further reading:


These notes are largely inspired by Programming in Lean