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, both definitions and theorems. You will need induction. There is a tactic 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.

□