edits

diff --git a/topics/_week7_monads.mdwn b/topics/_week7_monads.mdwn
index 61d5009..32f7ac0 100644 (file)
--- a/topics/_week7_monads.mdwn
+++ b/topics/_week7_monads.mdwn
@@ -1,4 +1,4 @@
-<!-- λ Λ ∀ ≡ α β ρ ω Ω -->
+<!-- λ Λ ∀ ≡ α β γ ρ ω Ω -->

 <!-- Loved this one: http://www.stephendiehl.com/posts/monads.html -->
 
 Monads
 <!-- Loved this one: http://www.stephendiehl.com/posts/monads.html -->
 
 Monads


@@ -8,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


@@ -17,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


@@ -53,6 +53,8 @@ would write
 
 for the type of a boxed Int.
 
 
 for the type of a boxed Int.
 

+## Kleisli arrows
+

 At the most general level, we'll talk about *Kleisli arrows*:
 
 P -> <u>Q</u>
 At the most general level, we'll talk about *Kleisli arrows*:
 
 P -> <u>Q</u>


@@ -70,15 +72,15 @@ if `α List` is our box type, we can write the second arrow as
 
 <u>Int</u> -> <u><u>Int</u></u>
 
 
 <u>Int</u> -> <u><u>Int</u></u>
 

-We'll need a number of schematic 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:
+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:

 
 <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>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 (/maep/): (P -> Q -> R) -> <u>P</u> -> <u>Q</u> -> <u>R</u></code>
+<code>map2 (/maeptu/): (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>mapply (/&epsilon;m@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
 


@@ -92,30 +94,34 @@ these for whichever box type we're dealing with:
 
 <code>mjoin: <u><u>P</u></u> -> <u>P</u></code> 
 
 
 <code>mjoin: <u><u>P</u></u> -> <u>P</u></code> 
 

-Note that `mcompose` and `mbind` are interdefinable: <code>u >=> k ≡ \a. (ja >>= k)</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, the specific instances of these types will
-provide certain useful guarantees.
+In most cases of interest, instances of these types will provide
+certain useful guarantees.

 
 

-*   ***Mappable*** ("functors") At the most general level, some box types are *Mappable*
-if there is a `map` function defined for that boxt type with the type given above.
+*   ***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*
 
 *   ***MapNable*** ("applicatives") A Mappable box type is *MapNable*

-       if there are in addition `map2`, `mid`, and `mapply`.
+       if there are in addition `map2`, `mid`, and `mapply`.  (With
+       `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.)

 
 

-*   ***Monad*** ("composable") A MapNable box type is a *Monad* if
-       there is in addition a `mcompose` and `join`.  In addition, in
-       order to qualify as a monad, `mid` must be a left and right
-       identity for mcompose, and mcompose must be associative.  That
-       is, the following "laws" must hold:
+* ***Monad*** ("composable") A MapNable box type is a *Monad* if there
+       is in addition an `mcompose` and a `join` such that `mid` is be
+       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)
 
 
         mcompose mid k = k
         mcompose k mid = k
         mcompose (mcompose j k) l = mcompose j (mcompose k l)
 

-To take a trivial example (but still useful, as we will see), consider
-the identity box type Id: `α -> α`.  In terms of the box analogy, the
-Identity box type is an invisible box.  With the following definitions
+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 ≡ \f\g\x.f(gx)
 
     mid ≡ \p.p
     mcompose ≡ \f\g\x.f(gx)


@@ -143,18 +149,32 @@ Id is a monad.  Here is a demonstration that the laws hold:
 
 Id is the favorite monad of mimes everywhere.  
 
 
 Id is the favorite monad of mimes everywhere.  
 

-To take a slightly less trivial example, consider the box type `α
-List`, with the following operations:
+To take a slightly less trivial (and even more useful) example,
+consider the box type `α List`, with the following operations:

 
 

-    mcompose f g p = [r | q <- g p, r <- f q]
+    mid: α -> [α]
+    mid a = [a]
+ 
+    mcompose-crossy: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
+    mcompose-crossy f g a = [c | b <- g a, c <- f b]

 
 

-In words, if g maps a P to a list of Qs, and f maps a Q to a list of
-Rs, then mcompose f g maps a P to a list of Rs by first feeding the P
-to g, then feeding each of the Qs delivered by g to f.  For example,
+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 q = [q, q+1] in
-    let g p = [p*p, p+p] in
-    mcompose f g 7 = [49, 50, 14, 15]
+    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).
 
 
 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 isntance,
+using the same box type and the same mid, we can define
+
+    mcompose-zippy f g a = match (f,g) with
+      ([],_) -> []
+      (_,[]) -> []
+      (f:ftail, g:gtail) -> f(ga) && mcompoze-zippy ftail gtail a
+
+