From: Jim Pryor <profjim@jimpryor.net>
Date: Thu, 2 Dec 2010 16:29:03 +0000 (-0500)
Subject: changed my unit_M to Chris' convention of M_unit, for consistency
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=bf8d964cc93f6b0b44a432bca8c94b1374c05e1f

changed my unit_M to Chris' convention of M_unit, for consistency

Signed-off-by: Jim Pryor <profjim@jimpryor.net>
---

diff --git a/code/tree_monadize.ml b/code/tree_monadize.ml
index 6dff768d..16d06106 100644
--- a/code/tree_monadize.ml
+++ b/code/tree_monadize.ml
@@ -72,8 +72,8 @@ end;;
 type env = int -> int;;
 
 type 'a reader = env -> 'a;;
-let unit_reader a : 'a reader = fun e -> a;;
-let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
+let reader_unit a : 'a reader = fun e -> a;;
+let reader_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
   fun e -> f (u e) e;;
 
 (* Now we supply the Reader monad as a parameter to Tree_monadizer.
@@ -81,35 +81,35 @@ let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
  * the monadize function specialized to the Reader monad *)
 module TreeReader = Tree_monadizer(struct
   type 'a m = 'a reader
-  let unit = unit_reader
-  let bind = bind_reader
+  let unit = reader_unit
+  let bind = reader_bind
 end);;
 
 
 type store = int;;
 
 type 'a state = store -> 'a * store;;
-let unit_state a : 'a state  = fun s -> (a, s);;
-let bind_state (u : 'a state) (f : 'a -> 'b state) : 'b state =
+let state_unit a : 'a state  = fun s -> (a, s);;
+let state_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
   fun s -> (let (a, s') = u s in (f a) s');;
 
 (* Make a TreeState module containing monadize specialized to the State monad *)
 module TreeState =  Tree_monadizer(struct
   type 'a m = 'a state
-  let unit = unit_state
-  let bind = bind_state
+  let unit = state_unit
+  let bind = state_bind
 end);;
 
 
-let unit_list a = [a];;
-let bind_list (u: 'a list) (f : 'a -> 'b list) : 'b list =
+let list_unit a = [a];;
+let list_bind (u: 'a list) (f : 'a -> 'b list) : 'b list =
   List.concat(List.map f u);;
 
 (* Make a TreeList module containing monadize specialized to the List monad *)
 module TreeList =  Tree_monadizer(struct
   type 'a m = 'a list
-  let unit = unit_list
-  let bind = bind_list
+  let unit = list_unit
+  let bind = list_bind
 end);;
 
 
@@ -135,15 +135,15 @@ end) = struct
 end;;
 
 type ('a,'r) cont = ('a -> 'r) -> 'r;;
-let unit_cont a : ('a,'r) cont = fun k -> k a;;
-let bind_cont (u: ('a,'r) cont) (f: 'a -> ('b,'r) cont) : ('b,'r) cont =
+let cont_unit a : ('a,'r) cont = fun k -> k a;;
+let cont_bind (u: ('a,'r) cont) (f: 'a -> ('b,'r) cont) : ('b,'r) cont =
   fun k -> u (fun a -> f a k);;
 
 (* Make a TreeCont module containing monadize specialized to the Cont monad *)
 module TreeCont =  Tree_monadizer2(struct
   type ('a,'r) m = ('a,'r) cont
-  let unit = unit_cont
-  let bind = bind_cont
+  let unit = cont_unit
+  let bind = cont_bind
 end);;
 
 
@@ -191,7 +191,7 @@ TreeList.monadize (fun i -> [ [i;i*i] ]) t1;;
 
 (* do nothing *)
 let initial_continuation = fun t -> t in
-TreeCont.monadize unit_cont t1 initial_continuation;;
+TreeCont.monadize cont_unit t1 initial_continuation;;
 
 (* convert tree to list of leaves *)
 let initial_continuation = fun t -> [] in
@@ -210,3 +210,26 @@ let initial_continuation = fun t -> 0 in
 TreeCont.monadize (fun a k -> 1 + k a) t1 initial_continuation;;
 
 
+
+
+(* Tree monad *)
+
+(* type 'a tree defined above *)
+let tree_unit (a: 'a) : 'a tree = Leaf a;;
+let rec tree_bind (u : 'a tree) (f : 'a -> 'b tree) : 'b tree =
+    match u with
+    | Leaf a -> f a
+    | Node (l, r) -> Node (tree_bind l f, tree_bind r f);;
+
+type 'a, treeTC_reader =
+		'a tree reader;;
+
+	let unit (a: 'a) : 'a tree reader =
+		M.unit (Leaf a);;
+
+	let rec bind (u : ('a, M) tree) (f : 'a -> ('b, M) tree) : ('b, M) tree =
+	    match u with
+	    | Leaf a -> M.bind (f a) (fun b -> M.unit (Leaf b))
+	    | Node (l, r) -> M.bind (bind l f) (fun l' ->
+							M.bind (bind r f) (fun r' ->
+								M.unit (Node (l', r'));;
diff --git a/hints/assignment_7_hint_2.mdwn b/hints/assignment_7_hint_2.mdwn
index d1736b32..29f6f05b 100644
--- a/hints/assignment_7_hint_2.mdwn
+++ b/hints/assignment_7_hint_2.mdwn
@@ -20,9 +20,9 @@
 
 	Since `dpm`s are to be a monad, we have to define a unit and a bind. These are just modeled on the unit and bind for the State monad:
 
-		let unit_dpm (value : 'a) : 'a dpm = fun (r, h) -> (value, r, h);;
+		let dpm_unit (value : 'a) : 'a dpm = fun (r, h) -> (value, r, h);;
 
-		let bind_dpm (u : 'a dpm) (f : 'a -> 'b dpm) : 'b dpm =
+		let dpm_bind (u : 'a dpm) (f : 'a -> 'b dpm) : 'b dpm =
 			fun (r, h) ->
 				let (a, r', h') = u (r, h)
 				in let u' = f a
diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn
index 2e4df05d..9789d4a2 100644
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -8,9 +8,9 @@
 	As I said, for simplicity, we'll represent sets using lists:
 
 		type 'a set = 'a list;;
-		let empty_set : 'a set = [];;
-		let unit_set (value: 'a) : 'a set = [value];;
-		let bind_set (u: 'a set) (f: 'a -> 'b set) : 'b set =
+		let set_empty : 'a set = [];;
+		let set_unit (value: 'a) : 'a set = [value];;
+		let set_bind (u: 'a set) (f: 'a -> 'b set) : 'b set =
 			List.concat (List.map f u);;
 
 
diff --git a/hints/assignment_7_hint_4.mdwn b/hints/assignment_7_hint_4.mdwn
index 6b33b7a5..046a45b9 100644
--- a/hints/assignment_7_hint_4.mdwn
+++ b/hints/assignment_7_hint_4.mdwn
@@ -17,13 +17,13 @@
 						then let obj = List.nth h (r 'x') in q obj
 						else false
 					in (truth_value', r, h)
-		in bind_set u (fun one_dpm -> unit_set (bind_dpm one_dpm eliminator))
+		in set_bind u (fun one_dpm -> set_unit (dpm_bind one_dpm eliminator))
 
-	The first seven lines here just perfom the operation we described: return a `bool dpm` computation that only yields `true` when its input `(r, h)` associates variable `x` with the right sort of entity. The last line performs the `bind_set` operation. This works by taking each `dpm` in the set and returning a `unit_set` of a filtered `dpm`. The definition of `bind_set` takes care of collecting together all of the `unit_set`s that result for each different set element we started with.
+	The first seven lines here just perfom the operation we described: return a `bool dpm` computation that only yields `true` when its input `(r, h)` associates variable `x` with the right sort of entity. The last line performs the `set_bind` operation. This works by taking each `dpm` in the set and returning a `set_unit` of a filtered `dpm`. The definition of `set_bind` takes care of collecting together all of the `set_unit`s that result for each different set element we started with.
 
 	We can call the `(fun one_dpm -> ...)` part \[[Qx]] and then updating `u` with \[[Qx]] will be:
 
-		bind_set u \[[Qx]]
+		set_bind u \[[Qx]]
 
 	or as it's written using Haskell's infix notation for bind:
 
@@ -39,11 +39,11 @@
 
 *	Now what do we do with predicates? As before, we suppose we have a function `q` that maps entities to `bool`s. We want to turn it into a function that maps `entity dpm`s to `bool dpm`s. Eventually we'll need to operate not just on single `dpm`s but on sets of them, but first things first. We'll begin by lifting `q` into a function that takes `entity dpm`s as arguments and returns `bool dpm`s:
 
-		fun entity_dpm -> bind_dpm entity_dpm (fun e -> unit_dpm (q e))
+		fun entity_dpm -> dpm_bind entity_dpm (fun e -> dpm_unit (q e))
 
-	Now we have to transform this into a function that again takes single `entity dpm`s as arguments, but now returns a `bool dpm set`. This is easily done with `unit_set`:
+	Now we have to transform this into a function that again takes single `entity dpm`s as arguments, but now returns a `bool dpm set`. This is easily done with `set_unit`:
 
-		fun entity_dpm -> unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (q e)))
+		fun entity_dpm -> set_unit (dpm_bind entity_dpm (fun e -> dpm_unit (q e)))
 
 	Finally, we realize that we're going to have a set of `bool dpm`s to start with, and we need to monadically bind \[[Qx]] to them. We don't want any of the monadic values in the set that wrap `false` to become `true`; instead, we want to apply a filter that checks whether values that formerly wrapped `true` should still continue to do so.
 
@@ -53,9 +53,9 @@
 			let eliminator : bool -> bool dpm =
 				fun truth_value ->
 					if truth_value = false
-					then unit_dpm false
-					else bind_dpm entity_dpm (fun e -> unit_dpm (q e))
-			in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+					then dpm_unit false
+					else dpm_bind entity_dpm (fun e -> dpm_unit (q e))
+			in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 
 	Applied to an `entity_dpm`, that yields a function that we can bind to a `bool dpm set` and that will transform the doubly-wrapped `bool` into a new `bool dpm set`.
 
@@ -67,9 +67,9 @@
 		in let entity_dpm = getx
 		in let eliminator = fun truth_value ->
 			if truth_value = false
-			then unit_dpm false
-			else bind_dpm entity_dpm (fun e -> unit_dpm (q e))
-		in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+			then dpm_unit false
+			else dpm_bind entity_dpm (fun e -> dpm_unit (q e))
+		in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 
 	<!--
 	or, simplifying:
@@ -79,12 +79,12 @@
 			in (obj, r, h)
 		in let eliminator = fun truth_value ->
 			if truth_value
-			then bind_dpm getx (fun e -> unit_dpm (q e))
-			else unit_dpm false
-		in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+			then dpm_bind getx (fun e -> dpm_unit (q e))
+			else dpm_unit false
+		in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 	-->
 
-	If we simplify and unpack the definition of `bind_dpm`, that's equivalent to:
+	If we simplify and unpack the definition of `dpm_bind`, that's equivalent to:
 
 		let getx = fun (r, h) ->
 			let obj = List.nth h (r 'x')
@@ -93,10 +93,10 @@
 			if truth_value
 			then (fun (r, h) ->
 					let (a, r', h') = getx (r, h)
-					in let u' = (fun e -> unit_dpm (q e)) a
+					in let u' = (fun e -> dpm_unit (q e)) a
 					in u' (r', h')
-			) else unit_dpm false
-		in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+			) else dpm_unit false
+		in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 
 	which can be further simplified to:
 
@@ -106,19 +106,19 @@
 			then (fun (r, h) ->
 					let obj = List.nth h (r 'x')
 					let (a, r', h') = (obj, r, h)
-					in let u' = (fun e -> unit_dpm (q e)) a
+					in let u' = (fun e -> dpm_unit (q e)) a
 					in u' (r', h')
-			) else unit_dpm false
-		in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+			) else dpm_unit false
+		in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 
 		let eliminator = fun truth_value ->
 			if truth_value
 			then (fun (r, h) ->
 					let obj = List.nth h (r 'x')
-					in let u' = unit_dpm (q obj)
+					in let u' = dpm_unit (q obj)
 					in u' (r, h)
-			) else unit_dpm false
-		in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+			) else dpm_unit false
+		in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 	-->
 
 		let eliminator = fun truth_value ->
@@ -126,8 +126,8 @@
 			then (fun (r, h) ->
 					let obj = List.nth h (r 'x')
 					in (q obj, r, h)
-			) else unit_dpm false
-		in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+			) else dpm_unit false
+		in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 
 	This is a function that takes a `bool dpm` as input and returns a `bool dpm set` as output.
 
@@ -140,13 +140,13 @@
 					then let obj = List.nth h (r 'x') in q obj
 					else false
 				in (truth_value', r, h))
-		in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+		in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
 
 	Can you persuade yourself that these are equivalent?)	
 
 *	Reviewing: now we've determined how to define \[[Q]] and \[[x]] such that \[[Qx]] can be the result of applying the function \[[Q]] to the `entity dpm` \[[x]]. And \[[Qx]] in turn is now a function that takes a `bool dpm` as input and returns a `bool dpm set` as output. We monadically bind this operaration to whatever `bool dpm set` we already have on hand:
 
-		bind_set u \[[Qx]]
+		set_bind u \[[Qx]]
 
 	or:
 
diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn
index de1bbe68..d44f824b 100644
--- a/hints/assignment_7_hint_5.mdwn
+++ b/hints/assignment_7_hint_5.mdwn
@@ -29,8 +29,8 @@ purely dealing with nondeterminism.
 
 	<pre><code>u updated with \[[&exist;x]] &equiv;
 		let extend one_dpm (d : entity) =
-			bind_dpm one_dpm (new_peg_and_assign 'x' d)
-		in bind_set u (fun one_dpm -> List.map (fun d -> extend one_dpm d) domain)
+			dpm_bind one_dpm (new_peg_and_assign 'x' d)
+		in set_bind u (fun one_dpm -> List.map (fun d -> extend one_dpm d) domain)
 	</code></pre>
 
 	where `new_peg_and_assign` is the operation we defined in [hint 3](/hints/assignment_7_hint_3):
@@ -58,7 +58,7 @@ purely dealing with nondeterminism.
 
 	or, being explicit about which "bind" operation we're representing here with `>>=`, that is:
 
-	<pre><code>bind_set (bind_set u \[[&exist;x]]) \[[Px]]
+	<pre><code>set_bind (set_bind u \[[&exist;x]]) \[[Px]]
 	</code></pre>
 
 *	Let's compare this to what \[[&exist;xPx]] would look like on a non-dynamic semantics, for example, where we use a simple Reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week7](
@@ -67,9 +67,9 @@ purely dealing with nondeterminism.
 		type assignment = char -> entity;;
 		type 'a reader = assignment -> 'a;;
 
-		let unit_reader (value : 'a) : 'a reader = fun r -> value;;
+		let reader_unit (value : 'a) : 'a reader = fun r -> value;;
 
-		let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
+		let reader_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
 			fun r ->
 				let a = u r
 				in let u' = f a
@@ -89,7 +89,7 @@ purely dealing with nondeterminism.
 			fun entity_reader ->
 				fun r ->
 					let obj = entity_reader r
-					in unit_reader (predicate obj)
+					in reader_unit (predicate obj)
 
 	The meaning of \[[Qx]] would then be:
 
@@ -98,7 +98,7 @@ purely dealing with nondeterminism.
 	\[[Qx]] &equiv; \[[Q]] \[[x]] &equiv;
 		fun r ->
 			let obj = getx r
-			in unit_reader (q obj)
+			in reader_unit (q obj)
 	</code></pre>
 
 	Recall also how we defined \[[lambda x]], or as [we called it before](/reader_monad_for_variable_binding), \\[[who(x)]]:
@@ -115,7 +115,7 @@ purely dealing with nondeterminism.
 
 		fun (lifted_predicate : lifted_unary) ->
 			fun r -> exists (fun (obj : entity) ->
-				lifted_predicate (unit_reader obj) r)
+				lifted_predicate (reader_unit obj) r)
 			
 	That would be the meaning of \[[&exist;]], which we'd use like this:
 
@@ -136,7 +136,7 @@ purely dealing with nondeterminism.
 				in clause r'
 		in let lifted_exists =
 			fun lifted_predicate ->
-				fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+				fun r -> exists (fun obj -> lifted_predicate (reader_unit obj) r)
 		in fun bool_reader -> lifted_exists (shift 'x' bool_reader)
 
 	which we can simplify to:
@@ -149,7 +149,7 @@ purely dealing with nondeterminism.
 				in clause r'
 		in let lifted_exists =
 			fun lifted_predicate ->
-				fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+				fun r -> exists (fun obj -> lifted_predicate (reader_unit obj) r)
 		in fun bool_reader -> lifted_exists (shifted bool_reader)
 
 		fun bool_reader ->
@@ -158,11 +158,11 @@ purely dealing with nondeterminism.
 					let new_value = entity_reader r
 					in let r' = fun var -> if var = 'x' then new_value else r var
 					in bool_reader r'
-			in fun r -> exists (fun obj -> shifted' (unit_reader obj) r)
+			in fun r -> exists (fun obj -> shifted' (reader_unit obj) r)
 
 		fun bool_reader ->
 			let shifted'' r obj =
-					let new_value = (unit_reader obj) r
+					let new_value = (reader_unit obj) r
 					in let r' = fun var -> if var = 'x' then new_value else r var
 					in bool_reader r'
 			in fun r -> exists (fun obj -> shifted'' r obj)
diff --git a/hints/assignment_7_hint_6.mdwn b/hints/assignment_7_hint_6.mdwn
index e513284b..fd8f55d4 100644
--- a/hints/assignment_7_hint_6.mdwn
+++ b/hints/assignment_7_hint_6.mdwn
@@ -19,12 +19,12 @@
                 let new_dpm = fun (r, h) ->
 					(* if one_dpm isn't already false at (r, h),
 					   we want to check its behavior when updated with phi
-					   bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *)
+					   set_bind (set_unit one_dpm) phi === phi one_dpm; do you remember why? *)
 				    let (truth_value, r', h') = one_dpm (r, h)
 					in let truth_value' = truth_value && (truths (phi one_dpm) (r, h) = [])
 					(* new_dpm must return a (bool, r, h) *)
                     in (truth_value', r', h')
-				in unit_set new_dpm;;
+				in set_unit new_dpm;;
 
 
 	**Thanks to Simon Charlow** for catching a subtle error in previous versions of this function. Fixed 1 Dec.
@@ -32,7 +32,7 @@
 *	Representing \[[and &phi; &psi;]] is simple:
 
 		let and_op (phi : clause) (psi : clause) : clause =
-			fun one_dpm -> bind_set (phi one_dpm) psi;;
+			fun one_dpm -> set_bind (phi one_dpm) psi;;
 		(* now u >>= and_op phi psi === u >>= phi >>= psi; do you remember why? *)
 		
 
@@ -41,15 +41,15 @@
 	(These probably still manifest the bug Simon spotted.)
 
 		let or_op (phi : clause) (psi : clause) =
-            fun one_dpm -> unit_set (
+            fun one_dpm -> set_unit (
                 fun (r, h) ->
 					let truth_value' = (
 						truths (phi one_dpm) (r, h) <> [] ||
-						truths (bind_set (negate_op phi one_dpm) psi) (r, h) <> []
+						truths (set_bind (negate_op phi one_dpm) psi) (r, h) <> []
 					) in (truth_value', r, h))
 
 		let if_op (phi : clause) (psi : clause) : clause =
-            fun one_dpm -> unit_set (
+            fun one_dpm -> set_unit (
               fun (r, h) ->
 					let truth_value' = List.for_all (fun one_dpm ->
 							let (truth_value, _, _) = one_dpm (r, h)
@@ -65,17 +65,17 @@
 		type assignment = char -> int;;
 		type store = entity list;;
 		type 'a dpm = assignment * store -> 'a * assignment * store;;
-		let unit_dpm (x : 'a) : 'a dpm = fun (r, h) -> (x, r, h);;
-		let bind_dpm (u: 'a dpm) (f : 'a -> 'b dpm) : 'b dpm =
+		let dpm_unit (x : 'a) : 'a dpm = fun (r, h) -> (x, r, h);;
+		let dpm_bind (u: 'a dpm) (f : 'a -> 'b dpm) : 'b dpm =
 			fun (r, h) ->
 				let (a, r', h') = u (r, h)
 				in let u' = f a
 				in u' (r', h')
 
 		type 'a set = 'a list;;
-		let empty_set : 'a set = [];;
-		let unit_set (x : 'a) : 'a set = [x];;
-		let bind_set (u : 'a set) (f : 'a -> 'b set) : 'b set =
+		let set_empty : 'a set = [];;
+		let set_unit (x : 'a) : 'a set = [x];;
+		let set_bind (u : 'a set) (f : 'a -> 'b set) : 'b set =
 			List.concat (List.map f u);;
 
 		type clause = bool dpm -> bool dpm set;;
@@ -93,18 +93,18 @@
 			fun entity_dpm ->
 				let eliminator = fun truth_value ->
 					if truth_value = false
-					then unit_dpm false
-					else bind_dpm entity_dpm (fun e -> unit_dpm (f e))
-				in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator);;
+					then dpm_unit false
+					else dpm_bind entity_dpm (fun e -> dpm_unit (f e))
+				in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator);;
 
 		(* doing the same thing for binary predicates *)
 		let lift_predicate2 (f : entity -> entity -> bool) : entity dpm -> entity dpm -> clause =
 			fun entity1_dpm entity2_dpm ->
 				let eliminator = fun truth_value ->
 					if truth_value = false
-					then unit_dpm false
-					else bind_dpm entity1_dpm (fun e1 -> bind_dpm entity2_dpm (fun e2 -> unit_dpm (f e1 e2)))
-				in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator);;
+					then dpm_unit false
+					else dpm_bind entity1_dpm (fun e1 -> dpm_bind entity2_dpm (fun e2 -> dpm_unit (f e1 e2)))
+				in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator);;
 
 		let new_peg_and_assign (var_to_bind : char) (d : entity) : bool -> bool dpm =
 		  fun truth_value ->
@@ -118,7 +118,7 @@
 		(* from hint 5 *)
 		let exists var : clause =
 			let extend one_dpm (d : entity) =
-				bind_dpm one_dpm (new_peg_and_assign var d)
+				dpm_bind one_dpm (new_peg_and_assign var d)
 			in fun one_dpm -> List.map (fun d -> extend one_dpm d) domain
 
 		(* include negate_op, and_op, or_op, and if_op as above *)
@@ -126,7 +126,7 @@
 *	More:
 
 		(* some handy utilities *)
-		let (>>=) = bind_set;;
+		let (>>=) = set_bind;;
 		let getx = get 'x';;
 		let gety = get 'y';;
 		let initial_set = [fun (r,h) -> (true,r,h)];;
diff --git a/manipulating_trees_with_monads.mdwn b/manipulating_trees_with_monads.mdwn
index 445722be..315cb68a 100644
--- a/manipulating_trees_with_monads.mdwn
+++ b/manipulating_trees_with_monads.mdwn
@@ -498,7 +498,7 @@ Okay, now let's do the same thing for our Tree monad.
 
 	let rec bind (u : 'a tree) (f : 'a -> 'b tree) : 'b tree =
 	    match u with
-	    | Leaf a -> (fun b -> Leaf b) (f a)
+	    | Leaf a -> (fun b -> b) (f a) (* see below *)
 	    | Node (l, r) -> (fun l' r' -> Node (l', r')) (bind l f) (bind r f);;
 
 	(* monadic operations for the TreeT monadic transformer *)
diff --git a/week9.mdwn b/week9.mdwn
index 546b2d2c..c6dd9e83 100644
--- a/week9.mdwn
+++ b/week9.mdwn
@@ -446,9 +446,9 @@ Here's the implementation of the State monad, together with an implementation of
 	(* alternatively, an env could be implemented as type char -> int *)
 
 	type 'a reader = env -> 'a;;
-	let unit_reader (value : 'a) : 'a reader =
+	let reader_unit (value : 'a) : 'a reader =
 		fun e -> value;;
-	let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
+	let reader_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
 		fun e -> let a = u e
 				 in let u' = f a
 				 in u' e;;
@@ -458,9 +458,9 @@ Here's the implementation of the State monad, together with an implementation of
 	(* this corresponds to having only a single mutable variable *)
 
 	type 'a state = store -> ('a, store);;
-	let unit_state (value : 'a) : 'a state =
+	let state_unit (value : 'a) : 'a state =
 		fun s -> (value, s);;
-	let bind_state (u : 'a state) (f : 'a -> 'b state) : 'b state =
+	let state_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
 		fun s -> let (a, s') = u s
 				 in let u' = f a
 				 in u' s';;