<![CDATA[
# Monads
Today we will practice with monads, implement a few, learn about `fmap` and `join`,
and practice proving satisfaction of the Monad Laws.
## Maybe
One of the simplest monads is the Maybe monad, which you might also know as
the Option monad. Recall the definition of `bind` and `return` for the Maybe
monad you saw in lecture:
```
let return x = Some x
let bind m f =
match m with
| Some x -> f x
| None -> None
let (>>=) = bind
```
`return` takes a value and creates a trivial `option` out of it, while `bind`
takes an `option` and a function, and applies the function to the contents of that
`option`, creating a new optional value.
##### Exercise: add [✭]
Complete the definition of `add` according to its specification using `>>=`
and `return`:
```
(*
* Computes the sum of two optional values.
* If both x and y are of the form Some p, [add x y] should be Some(px + py)
* If either x or y are None, [add x y] should be None
*)
let add (x: int option) (y : int option) =
(*Your implementation here*)
```
□
##### Exercise: cleanup [✭✭]
The following code uses some functions that produce optional values, but
whoever wrote it clearly missed last week's lecture on Monads. Rewrite it
more elegantly with `bind` and `return`.
```
val foo : unit -> int option
val bar : int -> string option
val baz : unit -> string option
val print_option : string option -> unit
let a = foo () in
let b = match a with
| Some x -> bar x
| None -> None in
let c = baz () in
let d = match (b, c) with
| Some x, Some y -> print_option (Some (x^y))
| _ -> ()
```
□
## fmap and join
`bind` and `return` are not the only two useful functions for working with monads.
Although `bind` makes it easy to build computation pipelines as you saw in the
previous exercises, sometimes we only want to apply a single pre-existing function
to a monad, and don't want to have to worry about upgrading it as seen in lecture.
The function `fmap` makes this possible:
```
fmap : 'a t -> ('a -> 'b) -> 'b t
```
Notice the similarity in type to `bind`. The key difference to is that the function
does not return a monad type, whereas it does in `bind`.
`fmap` also has an infix operator `(>>|)`. If you wish, you can think of the `|` as
denoting the end of a computation chain.
We can also reverse the order of the arguments to `fmap` as so:
```
fmap' : ('a -> 'b) -> 'a t -> 'b t
```
This is equivalent to:
```
fmap' : ('a -> 'b) -> ('a t -> 'b t)
```
Written this way, it becomes clear that when fully applied, `fmap'` will
take a function and apply it to the contents of its second, monadic argument.
However, when partially applied, it becomes a function that will take
an non-monadic function and 'upgrade' it to a monadic one. Written this way `fmap'`
is more commonly called `lift`.
##### Exercise: fmap [✭]
Implement `fmap` for the Maybe monad.
□
Another useful function is `join`, called such because it has the effect of 'joining'
a doubly 'nested' monad. To use the burrito analogy, `join` takes a burrito wrapped
in two tortillas and returns a new burrito with the same contents, but with only
one tortilla wrapper.
```
join : 'a t t -> 'a t
```
##### Exercise: join [✭]
Implement `join` for the Maybe monad. `join` should be `None` if either of the
two 'layers' of the input `option` are `None`.
□
##### Exercise: bind 2.0 [✭✭]
Part of what makes `fmap` and `join` such useful functions for formulating monads
is that `bind` can be implemented for all monads using only these two functions.
Do so for the Maybe monad. The `Some` and `None` constructors should not appear
in your solution.
□
##### Exercise: fmap 2.0 [✭✭]
Implement `fmap` and `join` using only `bind` and `return`. Your solution
should work for any monad.
□
## Lists and Nondeterminism
Imagine, for a moment, that you had a function with a random effect.
Given an input, it could return a variety of possible outputs, with no
indication of what they would be based solely on the input. Examples
include rolling a die, or reading a value from a network.
In statistics, we often formalize the concept of multiple outcomes using
a set, called a *sample space*. The sample space is the set of all
possible outcomes of an action. For example, when flipping a coin, the
sample space is {head, tails}. When rolling a 4-sided die, the sample
space is {1, 2, 3, 4}.
Sample spaces for sequential actions are simply combined into one set:
the sample space for flipping two coins is {(head, tails), (head, head),
(tails, head), (tails, tails)}, while the sample space for the sum of
two 4-sided die rolls would be {2, 3, 4, 5, 6, 7, 8}.
Since there is no native representation for sets in OCaml, we often
choose to represent sets as lists, so a function to get the sample space
of rolling a die might have the type:
```
val roll : unit -> int list
```
The List monad makes it convenient to work with non-deterministic functions
by treating this list as a monadic value. `return` trivially makes a singleton
list from its argument, while `bind` can be thought of as performing a
non-deterministic computation on each element of its input set.
As an example:
```
# let l1 = roll() in (*[1; 2; 3; 4]*)
# let l2 = roll() in (*[1; 2; 3; 4]*)
# l1 >>= fun x ->
l2 >>= fun y ->
return (x + y);;
- : int list [2; 3; 4; 5; 3; 4; 5; 6; 4; 5; 6; 7; 5; 6; 7; 8]
```
This computes the result of adding two 4-sided dice rolls. Note that the
list representation of the sample space has duplicates, something that
its set counterpart does not.
##### Exercise: list [✭✭✭]
Implement `return` and `bind` for the List monad.
*Hint: List.map and List.concat might be helpful.*
□
##### Exercise: list again [✭✭]
Implement `fmap` and `join` for the List monad. Do not use `return` nor `bind`
that you implemented in the previous exercise.
□
## The Monad Laws
The monad laws are three equations that every monad implementation must satisfy:
```
(1) (return x >>= f) = f x
(2) (m >>= return) = m
(3) ((m >>= f) >>= g) = (m >>= (fun x -> f x >>= g))
```
##### Exercise: maybe coq [✭✭✭]
Here is an implementation of the Maybe monad in Coq, using Coq's
`option` as the representation type:
```
Module MaybeMonad.
Definition maybe (A:Type) : Type := option A.
(* [return] is a keyword in Coq so we use [return'] instead *)
Definition return' {A:Type} (x:A) :=
Some x.
Definition bind {A B:Type} (m : maybe A) (f : A -> maybe B) : maybe B :=
match m with
| Some x => f x
| None => None
end.
Notation "m >>= f" := (bind m f) (right associativity, at level 60).
(* insert theorems here *)
End MaybeMonad.
```
Prove in Coq that the monad laws hold for that implementation of the Maybe monad.
*Hint: these proofs are straightforward; `destruct` is the most complicated
tactic you need.*
□
##### Exercise: list coq [✭✭✭✭]
Implement the List monad in Coq, using Coq's `list` as the representation
type. Prove in Coq that the monad laws hold for your implementation.
*Hints: Make use of the Coq [List standard library][coq-list], both definitions
and theorems. You will need `induction`. There is a [tactic `cbn`][cbn] that is
like `simpl` but is better tuned to the kinds of proofs you are doing here;
use it instead of `simpl` throughout this exercise.*
[coq-list]: https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html
[cbn]: https://coq.inria.fr/doc/tactics.html#hevea_tactic154
□
]]>