projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
a7cc796
)
tree monads
author
Chris Barker
<barker@omega.(none)>
Sun, 28 Nov 2010 14:32:22 +0000
(09:32 -0500)
committer
Chris Barker
<barker@omega.(none)>
Sun, 28 Nov 2010 14:32:22 +0000
(09:32 -0500)
zipper-lists-continuations.mdwn
patch
|
blob
|
history
diff --git
a/zipper-lists-continuations.mdwn
b/zipper-lists-continuations.mdwn
index
48ae04c
..
d16a24e
100644
(file)
--- a/
zipper-lists-continuations.mdwn
+++ b/
zipper-lists-continuations.mdwn
@@
-652,8
+652,8
@@
monad, the tree monad:
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 =
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:
</pre>
For once, let's check the Monad laws. The left identity law is easy:
@@
-668,19
+668,19
@@
except that each leaf `a` has been replaced with `fa`:
\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
<pre>
\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
<pre>
- . .
- __|__ __|__
- | | | |
- a1 . fa1 .
- _|__ __|__
- | | | |
- . a5 . fa5
+ . .
+ __|__
__|__
+ | |
| |
+ a1 .
fa1 .
+ _|__
__|__
+ | |
| |
+ . a5
. fa5
bind _|__ f = __|__
bind _|__ f = __|__
- | | | |
- . a4 . fa4
- __|__
__|___
- | |
| |
- a2 a3 fa2 fa3
+ | |
| |
+ . a4
. fa4
+ __|__
__|___
+ | |
| |
+ a2 a3
fa2 fa3
</pre>
Given this equivalence, the right identity law
</pre>
Given this equivalence, the right identity law
@@
-701,24
+701,24
@@
have to proceed. Let `f a = Node (Leaf a, Leaf a)`. Then
\tree (. (. (. (. (a1)(a2)))))
\tree (. (. (. (. (a1) (a1)) (. (a1) (a1))) ))
<pre>
\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>
</pre>
Now when we bind this tree to `g`, we get
<pre>
- .
- ____|____
- | |
- . .
- __|__ __|__
- | | | |
+ .
+ ____|____
+ | |
+ . .
+ __|__ __|__
+ | | | |
ga1 ga1 ga1 ga1
</pre>
ga1 ga1 ga1 ga1
</pre>