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
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
We get the highly readable do notation
Monads provide many generic operations, e.g. mmap : (α → M β) → list α → M (list β)
Monads can be extended generically with further operations and laws, via new type classes (e.g. monad_with_orelse)
They have lots of applications, beyond imperative programs
| 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