From a7cc796716c8b22e8d39bfd0acd786b830929ddc Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sun, 28 Nov 2010 09:25:50 -0500 Subject: [PATCH] tree monads --- zipper-lists-continuations.mdwn | 91 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) 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: + +
```+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));;
+```
+ +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))) +
```+                .                         .
+              __|__		        __|__
+              |   |		        |   |
+              a1  .		       fa1  .
+                 _|__		          __|__
+                 |  |		          |   |
+                 .  a5		          .  fa5
+   bind         _|__       f   =        __|__
+                |  |		        |   |
+                .  a4		        .  fa4
+              __|__		      __|___
+              |   |		      |    |
+              a2  a3		     fa2  fa3
+```
+ +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))) )) +
```+                                           .
+				       ____|____
+          .               .    	       |       |
+bind    __|__   f  =    __|_    =      .       .
+        |   |	        |   |  	     __|__   __|__
+        a1  a2 	       fa1 fa2 	     |   |   |   |
+				     a1  a1  a1  a1
+```
+ +Now when we bind this tree to `g`, we get + +
```+           .
+       ____|____
+       |       |
+       .       .
+     __|__   __|__
+     |   |   |   |
+    ga1 ga1 ga1 ga1
+```
+ +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. -- 2.11.0