We could simulate the tree state example too, but it would require
generalizing the type of the continuation monad to
- type ('a -> 'b -> 'k) continuation = ('a -> 'b) -> 'k;;
+ type ('a, 'b, 'c) continuation = ('a -> 'b) -> 'c;;
The binary tree monad
---------------------
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
+ Left identity: bind (unit a) f = bind (Leaf a) f = f a
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`:
+except that each leaf `a` has been replaced with `f a`:
\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
. .
__|__ __|__
| | | |
- a1 . fa1 .
+ a1 . f a1 .
_|__ __|__
| | | |
- . a5 . fa5
+ . a5 . f a5
bind _|__ f = __|__
| | | |
- . a4 . fa4
+ . a4 . f a4
__|__ __|___
| | | |
- a2 a3 fa2 fa3
+ a2 a3 f a2 f a3
Given this equivalence, the right identity law
. . | |
bind __|__ f = __|_ = . .
| | | | __|__ __|__
- a1 a2 fa1 fa2 | | | |
+ a1 a2 f a1 f a2 | | | |
a1 a1 a1 a1
Now when we bind this tree to `g`, we get
- .
- ____|____
- | |
- . .
- __|__ __|__
- | | | |
- ga1 ga1 ga1 ga1
+ .
+ _____|______
+ | |
+ . .
+ __|__ __|__
+ | | | |
+ g a1 g a1 g a1 g a1
At this point, it should be easy to convince yourself that
using the recipe on the right hand side of the associative law will