manip trees: tweaks
authorJim Pryor <profjim@jimpryor.net>
Wed, 1 Dec 2010 08:46:37 +0000 (03:46 -0500)
committerJim Pryor <profjim@jimpryor.net>
Wed, 1 Dec 2010 08:46:37 +0000 (03:46 -0500)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
manipulating_trees_with_monads.mdwn

index a05fa25..69b5131 100644 (file)
@@ -280,7 +280,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 +297,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 (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
 
                        .                         .
                      __|__                     __|__
                      |   |                     |   |
-                     a1  .                    fa1  .
+                     a1  .                   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
 
@@ -344,18 +344,18 @@ proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then
                  .               .            |       |
        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