tree monads

[lambda.git] / zipper-lists-continuations.mdwn

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index d16a24e..052bdf6 100644 (file)
--- a/zipper-lists-continuations.mdwn
+++ b/zipper-lists-continuations.mdwn
@@ -642,11 +642,11 @@ generalizing the type of the continuation monad to
 
     type ('a -> 'b -> 'c) continuation = ('a -> 'b) -> 'c;;
 
-The tree monad
---------------
+The binary tree monad
+---------------------
 
 Of course, by now you may have realized that we have discovered a new
-monad, the tree monad:
+monad, the binary tree monad:
 
 <pre>
 type 'a tree = Leaf of 'a | Node of ('a tree) * ('a tree);;
@@ -661,7 +661,7 @@ 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
 
 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
+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`:
@@ -696,7 +696,7 @@ As for the associative law,
     Associativity: bind (bind u f) g = bind u (\a. bind (fa) g)
 
 we'll give an example that will show how an inductive proof would
-have to proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then
+proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then
 
 \tree (. (. (. (. (a1)(a2)))))
 \tree (. (. (. (. (a1) (a1)) (. (a1) (a1)))  ))