Signed-off-by: Jim Pryor <profjim@jimpryor.net>
We could simulate the tree state example too, but it would require
generalizing the type of the continuation monad to
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
---------------------
The binary tree monad
---------------------
For once, let's check the Monad laws. The left identity law is easy:
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`,
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)))
. .
__|__ __|__
| | | |
\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
. .
__|__ __|__
| | | |
bind _|__ f = __|__
| | | |
bind _|__ f = __|__
| | | |
Given this equivalence, the right identity law
Given this equivalence, the right identity law
. . | |
bind __|__ f = __|_ = . .
| | | | __|__ __|__
. . | |
bind __|__ f = __|_ = . .
| | | | __|__ __|__
+ a1 a2 f a1 f a2 | | | |
a1 a1 a1 a1
Now when we bind this tree to `g`, we get
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
At this point, it should be easy to convince yourself that
using the recipe on the right hand side of the associative law will