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