-Mappables (functors), MapNables (applicatives functors), and Monads
-(composables) are ways of lifting computations from unboxed types into
-boxed types. Here, a "boxed type" is a type function with one missing
-piece, which we can think of as a function from a type to a type.
-Call this type function M, and let P, Q, R, and S be variables over types.
-
-Recall that a monad requires a singleton function 1:P-> MP, and a
-composition operator >=>: (P->MQ) -> (Q->MR) -> (P->MR) [the type for
-the composition operator given here corrects a "type"-o from the class handout]
-that obey the following laws:
-
- 1 >=> k = k
- k >=> 1 = k
- j >=> (k >=> l) = (j >=> k) >=> l
-
-For instance, the identity monad has the identity function I for 1
-and ordinary function composition (o) for >=>. It is easy to prove
-that the laws hold for any expressions j, k, and l whose types are
-suitable for 1 and >=>:
-
- 1 >=> k == I o k == \p. I (kp) ~~> \p.kp ~~> k
- k >=> 1 == k o I == \p. k (Ip) ~~> \p.kp ~~> k
-
- (j >=> k) >=> l == (\p.j(kp)) o l == \q.(\p.j(kp))(lq) ~~> \q.j(k(lq))
- j >=> (k >=> l) == j o (k o l) == j o \p.k(lp) == \q.j(\p.k(lp)q) ~~> \q.j(k(lq))
-
-1. On a number of occasions, we've used the Option type to make our
-conceptual world neat and tidy (for instance, think of the discussion
-of Kaplan's Plexy). As we learned in class, there is a natural monad
-for the Option type. Borrowing the notation of OCaml, let's say that
-"`'a option`" is the type of a boxed `'a`, whatever type `'a` is.
+1. On a number of occasions, we've used the Option/Maybe type to make our
+conceptual world neat and tidy (for instance, think of [[our discussion
+of Kaplan's Plexy|topics/week6_plexy]]). As we learned in class, there is a natural monad
+for the Option type. Using the vocabulary of OCaml, let's say that
+`'a option` is the type of a boxed `'a`, whatever type `'a` is.