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