author Chris Barker Sun, 28 Nov 2010 14:35:36 +0000 (09:35 -0500) committer Chris Barker Sun, 28 Nov 2010 14:35:36 +0000 (09:35 -0500)

index d16a24e..052bdf6 100644 (file)
@@ -642,11 +642,11 @@ generalizing the type of the continuation monad to

type ('a -> 'b -> 'c) continuation = ('a -> 'b) -> 'c;;

type ('a -> 'b -> 'c) continuation = ('a -> 'b) -> 'c;;

---------------
+---------------------

Of course, by now you may have realized that we have discovered a new

Of course, by now you may have realized that we have discovered a new

<pre>
type 'a tree = Leaf of 'a | Node of ('a tree) * ('a tree);;

<pre>
type 'a tree = Leaf of 'a | Node of ('a tree) * ('a tree);;
@@ -661,7 +661,7 @@ 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

To check the other two laws, we need to make the following
Left identity: bind (unit a) f = bind (Leaf a) f = fa

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
+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`:
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`:
@@ -696,7 +696,7 @@ As for the associative law,
Associativity: bind (bind u f) g = bind u (\a. bind (fa) g)

we'll give an example that will show how an inductive proof would
Associativity: bind (bind u f) g = bind u (\a. bind (fa) g)

we'll give an example that will show how an inductive proof would
-have to proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then
+proceed.  Let `f a = Node (Leaf a, Leaf a)`.  Then

\tree (. (. (. (. (a1)(a2)))))
\tree (. (. (. (. (a1) (a1)) (. (a1) (a1)))  ))

\tree (. (. (. (. (a1)(a2)))))
\tree (. (. (. (. (a1) (a1)) (. (a1) (a1)))  ))