From: Chris Barker <barker@omega.(none)>
Date: Sun, 28 Nov 2010 14:25:50 +0000 (-0500)
Subject: tree monads
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=a7cc796716c8b22e8d39bfd0acd786b830929ddc;hp=9273d85724c80393c8ec4dea26705c47ccdf10c8

tree monads
---

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index 8858a893..48ae04c0 100644
--- a/zipper-lists-continuations.mdwn
+++ b/zipper-lists-continuations.mdwn
@@ -642,3 +642,94 @@ generalizing the type of the continuation monad to
 
     type ('a -> 'b -> 'c) continuation = ('a -> 'b) -> 'c;;
 
+The tree monad
+--------------
+
+Of course, by now you may have realized that we have discovered a new
+monad, the 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));;
+</pre>
+
+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
+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
+   bind         _|__       f   =        __|__   
+                |  |		        |   |   
+                .  a4		        .  fa4  
+              __|__		      __|___	   
+              |   |		      |    |	   
+              a2  a3		     fa2  fa3         
+</pre>   
+
+Given this equivalence, the right identity law
+
+    Right identity: bind u unit = u
+
+falls out once we realize that
+
+    bind (Leaf a) unit = unit a = Leaf a
+
+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
+
+\tree (. (. (. (. (a1)(a2)))))
+\tree (. (. (. (. (a1) (a1)) (. (a1) (a1)))  ))
+<pre>
+                                           .		
+				       ____|____	
+          .               .    	       |       |	
+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>
+
+At this point, it should be easy to convince yourself that
+using the recipe on the right hand side of the associative law will
+built the exact same final tree.
+
+So binary trees are a monad.
+
+Haskell combines this monad with the Option monad to provide a monad
+called a
+[SearchTree](http://hackage.haskell.org/packages/archive/tree-monad/0.2.1/doc/html/src/Control-Monad-SearchTree.html#SearchTree)
+that is intended to 
+represent non-deterministic computations as a tree.