author Chris Sat, 14 Mar 2015 19:46:15 +0000 (15:46 -0400) committer Chris Sat, 14 Mar 2015 19:46:15 +0000 (15:46 -0400)

index 9a3d04c..2e4f704 100644 (file)
@@ -112,3 +112,38 @@ our scorecard.  On the simple-minded view, we would replace it with
`w`.  But that's not the right result, because `w` itself has been
mapped onto 2.

`w`.  But that's not the right result, because `w` itself has been
mapped onto 2.

+
+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) -> (R->MS) 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).  It turns out that 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.  Then the
+obvious singleton for the Option monad is \p.Just p.  What is the