week11 tweaks

[lambda.git] / manipulating_trees_with_monads.mdwn

diff --git a/manipulating_trees_with_monads.mdwn b/manipulating_trees_with_monads.mdwn
index a05fa25..d0897ef 100644 (file)
--- a/manipulating_trees_with_monads.mdwn
+++ b/manipulating_trees_with_monads.mdwn
@@ -92,6 +92,7 @@ a reader monad---is to have the treemap function return a (monadized)
 tree that is ready to accept any `int -> int` function and produce the
 updated tree.
 
 tree that is ready to accept any `int -> int` function and produce the
 updated tree.
 

+\tree (. (. (f 2) (f 3)) (. (f 5) (. (f 7) (f 11))))

 
        \f      .
           _____|____
 
        \f      .
           _____|____


@@ -280,7 +281,7 @@ interesting functions for the first argument of `treemonadizer`:
 We could simulate the tree state example too, but it would require
 generalizing the type of the continuation monad to
 
 We could simulate the tree state example too, but it would require
 generalizing the type of the continuation monad to
 

-       type ('a -> 'b -> 'k) continuation = ('a -> 'b) -> 'k;;
+       type ('a, 'b, 'c) continuation = ('a -> 'b) -> 'c;;

 
 The binary tree monad
 ---------------------
 
 The binary tree monad
 ---------------------


@@ -297,29 +298,29 @@ monad, the binary tree monad:
 
 For once, let's check the Monad laws.  The left identity law is easy:
 
 
 For once, let's check the Monad laws.  The left identity law is easy:
 

-    Left identity: bind (unit a) f = bind (Leaf a) f = fa
+    Left identity: bind (unit a) f = bind (Leaf a) f = f a

 
 To check the other two laws, we need to make the following
 observation: it is easy to prove based on `tree_bind` by a simple
 induction on the structure of the first argument that the tree
 resulting from `bind u f` is a tree with the same strucure as `u`,
 
 To check the other two laws, we need to make the following
 observation: it is easy to prove based on `tree_bind` by a simple
 induction on the structure of the first argument that the tree
 resulting from `bind u f` is a tree with the same strucure as `u`,

-except that each leaf `a` has been replaced with `fa`:
+except that each leaf `a` has been replaced with `f a`:

 
 

-\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
+\tree (. (f a1) (. (. (. (f a2) (f a3)) (f a4)) (f a5)))

 
                        .                         .
                      __|__                     __|__
                      |   |                     |   |
 
                        .                         .
                      __|__                     __|__
                      |   |                     |   |

-                     a1  .                    fa1  .
+                     a1  .                   f a1  .

                         _|__                     __|__
                         |  |                     |   |
                         _|__                     __|__
                         |  |                     |   |

-                        .  a5                    .  fa5
+                        .  a5                    .  f a5

           bind         _|__       f   =        __|__
                        |  |                    |   |
           bind         _|__       f   =        __|__
                        |  |                    |   |

-                       .  a4                   .  fa4
+                       .  a4                   .  f a4

                      __|__                   __|___
                      |   |                   |    |
                      __|__                   __|___
                      |   |                   |    |

-                     a2  a3                 fa2  fa3
+                     a2  a3                f a2  f a3

 
 Given this equivalence, the right identity law
 
 
 Given this equivalence, the right identity law
 


@@ -336,26 +337,26 @@ As for the associative law,
 we'll give an example that will show how an inductive proof would
 proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then
 
 we'll give an example that will show how an inductive proof would
 proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then
 

-\tree (. (. (. (. (a1)(a2)))))
-\tree (. (. (. (. (a1) (a1)) (. (a1) (a1)))  ))
+\tree (. (. (. (. (a1) (a2)))))
+\tree (. (. (. (. (a1) (a1)) (. (a1) (a1)))))

 
                                                   .
                                               ____|____
                  .               .            |       |
        bind    __|__   f  =    __|_    =      .       .
                |   |           |   |        __|__   __|__
 
                                                   .
                                               ____|____
                  .               .            |       |
        bind    __|__   f  =    __|_    =      .       .
                |   |           |   |        __|__   __|__

-               a1  a2         fa1 fa2       |   |   |   |
+               a1  a2        f a1 f a2      |   |   |   |

                                             a1  a1  a1  a1
 
 Now when we bind this tree to `g`, we get
 
                                             a1  a1  a1  a1
 
 Now when we bind this tree to `g`, we get
 

-                  .
-              ____|____
-              |       |
-              .       .
-            __|__   __|__
-            |   |   |   |
-           ga1 ga1 ga1 ga1
+                   .
+              _____|______
+              |          |
+              .          .
+            __|__      __|__
+            |   |      |   |
+          g a1 g a1  g a1 g a1

 
 At this point, it should be easy to convince yourself that
 using the recipe on the right hand side of the associative law will
 
 At this point, it should be easy to convince yourself that
 using the recipe on the right hand side of the associative law will