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:
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
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>