tree that is ready to accept any `int -> int` function and produce the
updated tree.
+\tree (. (. (f2) (f3))(. (f5) (.(f7)(f11))))
\f .
_____|____
interesting functions for the first argument of `treemonadizer`:
(* Simulating the tree reader: distributing a operation over the leaves *)
- # treemonadizer (fun a c -> c (square a)) t1 (fun i -> i);;
+ # treemonadizer (fun a k -> k (square a)) t1 (fun i -> i);;
- : int tree =
Node (Node (Leaf 4, Leaf 9), Node (Leaf 25, Node (Leaf 49, Leaf 121)))
(* Simulating the int list tree list *)
- # treemonadizer (fun a c -> c [a; square a]) t1 (fun i -> i);;
+ # treemonadizer (fun a k -> k [a; square a]) t1 (fun i -> i);;
- : int list tree =
Node
(Node (Leaf [2; 4], Leaf [3; 9]),
Node (Leaf [5; 25], Node (Leaf [7; 49], Leaf [11; 121])))
(* Counting leaves *)
- # treemonadizer (fun a c -> 1 + c a) t1 (fun i -> 0);;
+ # treemonadizer (fun a k -> 1 + k a) t1 (fun i -> 0);;
- : int = 5
We could simulate the tree state example too, but it would require
generalizing the type of the continuation monad to
- type ('a -> 'b -> 'c) continuation = ('a -> 'b) -> 'c;;
+ 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