X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=zipper-lists-continuations.mdwn;h=052bdf657a8440d46389f062e2bfb8c7653cf2d4;hb=638a4cb56977ff574d4f8de1ff4ca6faabe7c9d0;hp=48ae04c0c96dba3831a20a4769e3a3ec48270943;hpb=a7cc796716c8b22e8d39bfd0acd786b830929ddc;p=lambda.git

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index 48ae04c0..052bdf65 100644
--- a/zipper-lists-continuations.mdwn
+++ b/zipper-lists-continuations.mdwn
@@ -642,18 +642,18 @@ 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);;
 let tree_unit (x:'a) = Leaf x;;
 let rec tree_bind (u:'a tree) (f:'a -> 'b tree):'b tree = 
-  match u with Leaf x -> f x | Node (l, r) -> Node ((tree_bind l f),
-  (tree_bind r f));;
+  match u with Leaf x -> f x 
+             | Node (l, r) -> Node ((tree_bind l f), (tree_bind r f));;
 </pre>
 
 For once, let's check the Monad laws.  The left identity law is easy:
@@ -661,26 +661,26 @@ 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`:
 
 \tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
 <pre>
-                .                         .	       
-              __|__		        __|__   
-              |   |		        |   |   
-              a1  .		       fa1  .   
-                 _|__		          __|__ 
-                 |  |		          |   | 
-                 .  a5		          .  fa5
+                .                         .       
+              __|__                     __|__   
+              |   |                     |   |   
+              a1  .                    fa1  .   
+                 _|__                     __|__ 
+                 |  |                     |   | 
+                 .  a5                    .  fa5
    bind         _|__       f   =        __|__   
-                |  |		        |   |   
-                .  a4		        .  fa4  
-              __|__		      __|___	   
-              |   |		      |    |	   
-              a2  a3		     fa2  fa3         
+                |  |                    |   |   
+                .  a4                   .  fa4  
+              __|__                   __|___   
+              |   |                   |    |   
+              a2  a3                 fa2  fa3         
 </pre>   
 
 Given this equivalence, the right identity law
@@ -696,29 +696,29 @@ 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)))  ))
 <pre>
-                                           .		
-				       ____|____	
-          .               .    	       |       |	
-bind    __|__   f  =    __|_    =      .       .	 
-        |   |	        |   |  	     __|__   __|__	
-        a1  a2 	       fa1 fa2 	     |   |   |   |	
-				     a1  a1  a1  a1  
+                                           .
+                                       ____|____
+          .               .            |       |
+bind    __|__   f  =    __|_    =      .       .
+        |   |           |   |        __|__   __|__
+        a1  a2         fa1 fa2       |   |   |   |
+                                     a1  a1  a1  a1  
 </pre>
 
 Now when we bind this tree to `g`, we get
 
 <pre>
-           .		
-       ____|____	
-       |       |	
-       .       .	
-     __|__   __|__	
-     |   |   |   |	
+           .
+       ____|____
+       |       |
+       .       .
+     __|__   __|__
+     |   |   |   |
     ga1 ga1 ga1 ga1  
 </pre>