author Jim Pryor Wed, 1 Dec 2010 08:46:37 +0000 (03:46 -0500) committer Jim Pryor Wed, 1 Dec 2010 08:46:37 +0000 (03:46 -0500)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>

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

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

---------------------

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`,
-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)))

.                         .
__|__                     __|__
|   |                     |   |
-                     a1  .                    fa1  .
+                     a1  .                   a1  .
_|__                     __|__
|  |                     |   |
-                        .  a5                    .  fa5
+                        .  a5                    .  f a5
bind         _|__       f   =        __|__
|  |                    |   |
-                       .  a4                   .  fa4
+                       .  a4                   .  f a4
__|__                   __|___
|   |                   |    |
-                     a2  a3                 fa2  fa3
+                     a2  a3                f a2  f a3

Given this equivalence, the right identity law

@@ -344,18 +344,18 @@ proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then
.               .            |       |
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

-                  .
-              ____|____
-              |       |
-              .       .
-            __|__   __|__
-            |   |   |   |
-           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