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);;
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`:
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))) ))