edits

[lambda.git] / topics / _week7_monads.mdwn

diff --git a/topics/_week7_monads.mdwn b/topics/_week7_monads.mdwn
index 75bc205..b9be5ba 100644 (file)
--- a/topics/_week7_monads.mdwn
+++ b/topics/_week7_monads.mdwn
@@ -1,4 +1,5 @@
-<!-- λ Λ ∀ ≡ α β ρ ω Ω -->
+<!-- λ Λ ∀ ≡ α β γ ρ ω Ω -->
+<!-- Loved this one: http://www.stephendiehl.com/posts/monads.html -->

 
 Monads
 ======
 
 Monads
 ======


@@ -7,7 +8,7 @@ The [[tradition in the functional programming
 literature|https://wiki.haskell.org/Monad_tutorials_timeline]] is to
 introduce monads using a metaphor: monads are spacesuits, monads are
 monsters, monads are burritos.  We're part of the backlash that
 literature|https://wiki.haskell.org/Monad_tutorials_timeline]] is to
 introduce monads using a metaphor: monads are spacesuits, monads are
 monsters, monads are burritos.  We're part of the backlash that

-prefers to say that monads are monads.  
+prefers to say that monads are (Just) monads.  

 
 The closest we will come to metaphorical talk is to suggest that
 monadic types place objects inside of *boxes*, and that monads wrap
 
 The closest we will come to metaphorical talk is to suggest that
 monadic types place objects inside of *boxes*, and that monads wrap


@@ -16,22 +17,22 @@ any case, the emphasis will be on starting with the abstract structure
 of monads, followed by instances of monads from the philosophical and
 linguistics literature.
 
 of monads, followed by instances of monads from the philosophical and
 linguistics literature.
 

-### Boxes: type expressions with one free type variable
+## Box types: type expressions with one free type variable

 
 Recall that we've been using lower-case Greek letters
 
 Recall that we've been using lower-case Greek letters

-<code>&alpha;, &beta;, &gamma;, ...</code> to represent types.  We'll
+<code>&alpha;, &beta;, &gamma;, ...</code> as variables over types.  We'll

 use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a
 type schema is a type expression that may or may not contain unbound
 type variables.  For instance, we might have
 
 use `P`, `Q`, `R`, and `S` as metavariables over type schemas, where a
 type schema is a type expression that may or may not contain unbound
 type variables.  For instance, we might have
 

-    P ≡ Int
-    P ≡ α -> α
-    P ≡ ∀α. α -> α
-    P ≡ ∀α. α -> β 
+    P_1 ≡ Int
+    P_2 ≡ α -> α
+    P_3 ≡ ∀α. α -> α
+    P_4 ≡ ∀α. α -> β 

 
 etc.
 
 
 etc.
 

-A box type will be a type expression that contains exactly one free
+A *box type* will be a type expression that contains exactly one free

 type variable.  Some examples (using OCaml's type conventions):
 
     α Maybe
 type variable.  Some examples (using OCaml's type conventions):
 
     α Maybe


@@ -48,5 +49,137 @@ We'll often write box types as a box containing the value of the free
 type variable.  So if our box type is `α List`, and `α == Int`, we
 would write
 
 type variable.  So if our box type is `α List`, and `α == Int`, we
 would write
 

-<table border=2px><td>Int</td></table>
+<u>Int</u>

 
 

+for the type of a boxed Int.
+
+## Kleisli arrows
+
+At the most general level, we'll talk about *Kleisli arrows*:
+
+P -> <u>Q</u>
+
+A Kleisli arrow is the type of a function from objects of type P to
+objects of type box Q, for some choice of type expressions P and Q.
+For instance, the following are arrows:
+
+Int -> <u>Bool</u>
+
+Int List -> <u>Int List</u>
+
+Note that the left-hand schema can itself be a boxed type.  That is,
+if `α List` is our box type, we can write the second arrow as
+
+<u>Int</u> -> <u><u>Int</u></u>
+
+We'll need a number of classes of functions to help us maneuver in the
+presence of box types.  We will want to define a different instance of
+each of these for whichever box type we're dealing with.  (This will
+become clearly shortly.)
+
+<code>mid (/&epsilon;maid&epsilon;nt@tI/ aka unit, return, pure): P -> <u>P</u></code>
+
+<code>map (/maep/): (P -> Q) -> <u>P</u> -> <u>Q</u></code>
+
+<code>map2 (/m&ash;ptu/): (P -> Q -> R) -> <u>P</u> -> <u>Q</u> -> <u>R</u></code>
+
+<code>mapply (/&epsilon;m@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
+
+<code>mcompose (aka <=<): (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
+
+<code>mbind (aka >>=): (     <u>Q</u>) -> (Q -> <u>R</u>) -> (     <u>R</u>)</code>
+
+<code>mflipcompose (aka >=>): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
+
+<code>mflipbind (aka =<<) (     <u>Q</u>) -> (Q -> <u>R</u>) -> (     <u>R</u>)</code>
+
+<code>mjoin: <u><u>P</u></u> -> <u>P</u></code> 
+
+The managerie isn't quite as bewildering as you might suppose.  For
+one thing, `mcompose` and `mbind` are interdefinable: <code>u >=> k ≡
+\a. (ja >>= k)</code>.
+
+In most cases of interest, instances of these types will provide
+certain useful guarantees.
+
+*   ***Mappable*** ("functors") At the most general level, box types are *Mappable*
+if there is a `map` function defined for that box type with the type given above.
+
+*   ***MapNable*** ("applicatives") A Mappable box type is *MapNable*
+       if there are in addition `map2`, `mid`, and `mapply`.  (With
+       `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.)
+
+* ***Monad*** ("composables") A MapNable box type is a *Monad* if there
+       is in addition an `mcompose` and a `join` such that `mid` is 
+       a left and right identity for `mcompose`, and `mcompose` is
+       associative.  That is, the following "laws" must hold:
+
+        mcompose mid k = k
+        mcompose k mid = k
+        mcompose (mcompose j k) l = mcompose j (mcompose k l)
+
+To take a trivial (but, as we will see, still useful) example,
+consider the identity box type Id: `α -> α`.  So if α is type Bool,
+then a boxed α is ... a Bool.  In terms of the box analogy, the
+Identity box type is a completly invisible box.  With the following
+definitions
+
+    mid ≡ \p.p
+    mcompose ≡ \fgx.f(gx)
+
+Id is a monad.  Here is a demonstration that the laws hold:
+
+    mcompose mid k == (\fgx.f(gx)) (\p.p) k
+                   ~~> \x.(\p.p)(kx)
+                   ~~> \x.kx
+                   ~~> k
+    mcompose k mid == (\fgx.f(gx)) k (\p.p)
+                   ~~> \x.k((\p.p)x)
+                   ~~> \x.kx
+                   ~~> k
+    mcompose (mcompose j k) l == mcompose ((\fgx.f(gx)) j k) l
+                              ~~> mcompose (\x.j(kx)) l
+                              == (\fgx.f(gx)) (\x.j(kx)) l
+                              ~~> \x.(\x.j(kx))(lx)
+                              ~~> \x.j(k(lx))
+    mcompose j (mcompose k l) == mcompose j ((\fgx.f(gx)) k l)
+                              ~~> mcompose j (\x.k(lx))
+                              == (\fgx.f(gx)) j (\x.k(lx))
+                              ~~> \x.j((\x.k(lx)) x)
+                              ~~> \x.j(k(lx))
+
+Id is the favorite monad of mimes everywhere.  
+
+To take a slightly less trivial (and even more useful) example,
+consider the box type `α List`, with the following operations:
+
+    mid: α -> [α]
+    mid a = [a]
+ 
+    mcompose-crossy: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
+    mcompose-crossy f g a = [c | b <- g a, c <- f b]
+    mcompose-crossy f g a = foldr (\b -> \gs -> (f b) ++ gs) [] (g a) 
+    mcompose-crossy f g a = concat (map f (g a))
+
+These three definitions are all equivalent.
+In words, `mcompose f g a` feeds the a (which has type α) to g, which
+returns a list of βs; each β in that list is fed to f, which returns a
+list of γs.
+
+The final result is the concatenation of those lists of γs.
+For example, 
+
+    let f b = [b, b+1] in
+    let g a = [a*a, a+a] in
+    mcompose-crossy f g 7 = [49, 50, 14, 15]
+
+It is easy to see that these definitions obey the monad laws (see exercises).
+
+There can be multiple monads for any given box type.  For instance,
+using the same box type and the same mid, we can define
+
+    mcompose-zippy f g a = foldr (\b -> \gs -> f b ++ gs) (g a) []
+
+so that 
+
+    mcompose-zippy f g 7 = [49, 14]