# 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)
[`23_lecture.lean`](23_lecture.lean)
## Monads
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 `M`s may provide further operators, e.g. ways to extract the value stored in `M`
## Monads are useful
* 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
## Demo (Part 2)
[`23_lecture.lean`](23_lecture.lean)
## Newly introduced syntax
### Notations
Syntax | Description
---------------- | -----------
`do` | indicates the start of a monadic program
`bind`, `>>=` | combines effectful computations
`kleisli`, `>=>` | combines effectful computations of type `α → M β`
### Declarations
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
### Axiom
Name | Description
-------- | -----------
`funext` | function extensionality
## References
* [_Programming in Lean_](https://leanprover.github.io/programming_in_lean/#07_Monads.html), Chapter 7
Further reading:
* [_Real World Haskell_](http://book.realworldhaskell.org/read/monads.html), Chapter 14
## Acknowledgment
These notes are largely inspired by _Programming in Lean_