edits

[lambda.git] / topics / _week7_monads.mdwn

diff --git a/topics/_week7_monads.mdwn b/topics/_week7_monads.mdwn
index 32f7ac0..b9be5ba 100644 (file)
--- a/topics/_week7_monads.mdwn
+++ b/topics/_week7_monads.mdwn
@@ -74,13 +74,14 @@ if `α List` is our box type, we can write the second arrow as
 
 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
 
 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:
+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>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 (/maeptu/): (P -> Q -> R) -> <u>P</u> -> <u>Q</u> -> <u>R</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>mapply (/&epsilon;m@plai/): <u>P -> Q</u> -> <u>P</u> -> <u>Q</u></code>
 


@@ -108,8 +109,8 @@ if there is a `map` function defined for that box type with the type given above
        if there are in addition `map2`, `mid`, and `mapply`.  (With
        `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.)
 
        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 an `mcompose` and a `join` such that `mid` is be
+* ***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:
 
        a left and right identity for `mcompose`, and `mcompose` is
        associative.  That is, the following "laws" must hold:
 


@@ -124,26 +125,26 @@ Identity box type is a completly invisible box.  With the following
 definitions
 
     mid ≡ \p.p
 definitions
 
     mid ≡ \p.p

-    mcompose ≡ \f\g\x.f(gx)
+    mcompose ≡ \fgx.f(gx)

 
 Id is a monad.  Here is a demonstration that the laws hold:
 
 
 Id is a monad.  Here is a demonstration that the laws hold:
 

-    mcompose mid k == (\f\g\x.f(gx)) (\p.p) k
+    mcompose mid k == (\fgx.f(gx)) (\p.p) k

                    ~~> \x.(\p.p)(kx)
                    ~~> \x.kx
                    ~~> k
                    ~~> \x.(\p.p)(kx)
                    ~~> \x.kx
                    ~~> k

-    mcompose k mid == (\f\g\x.f(gx)) k (\p.p)
+    mcompose k mid == (\fgx.f(gx)) k (\p.p)

                    ~~> \x.k((\p.p)x)
                    ~~> \x.kx
                    ~~> k
                    ~~> \x.k((\p.p)x)
                    ~~> \x.kx
                    ~~> k

-    mcompose (mcompose j k) l == mcompose ((\f\g\x.f(gx)) j k) l
+    mcompose (mcompose j k) l == mcompose ((\fgx.f(gx)) j k) l

                               ~~> mcompose (\x.j(kx)) l
                               ~~> mcompose (\x.j(kx)) l

-                              == (\f\g\x.f(gx)) (\x.j(kx)) l
+                              == (\fgx.f(gx)) (\x.j(kx)) l

                               ~~> \x.(\x.j(kx))(lx)
                               ~~> \x.j(k(lx))
                               ~~> \x.(\x.j(kx))(lx)
                               ~~> \x.j(k(lx))

-    mcompose j (mcompose k l) == mcompose j ((\f\g\x.f(gx)) k l)
+    mcompose j (mcompose k l) == mcompose j ((\fgx.f(gx)) k l)

                               ~~> mcompose j (\x.k(lx))
                               ~~> mcompose j (\x.k(lx))

-                              == (\f\g\x.f(gx)) j (\x.k(lx))
+                              == (\fgx.f(gx)) j (\x.k(lx))

                               ~~> \x.j((\x.k(lx)) x)
                               ~~> \x.j(k(lx))
 
                               ~~> \x.j((\x.k(lx)) x)
                               ~~> \x.j(k(lx))
 


@@ -157,10 +158,15 @@ consider the box type `α List`, with the following operations:
  
     mcompose-crossy: (β -> [γ]) -> (α -> [β]) -> (α -> [γ])
     mcompose-crossy f g a = [c | b <- g a, c <- f b]
  
     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
 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.
+list of γs.
+
+The final result is the concatenation of those lists of γs.

 For example, 
 
     let f b = [b, b+1] in
 For example, 
 
     let f b = [b, b+1] in


@@ -169,12 +175,11 @@ For example,
 
 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,
+There can be multiple monads for any given box type.  For instance,

 using the same box type and the same mid, we can define
 
 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
+    mcompose-zippy f g a = foldr (\b -> \gs -> f b ++ gs) (g a) []

 
 

+so that 

 
 

+    mcompose-zippy f g 7 = [49, 14]