# 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_
