From ebed7bf68237f042849d0ebfeed8095a5f7d14a4 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Thu, 2 Dec 2010 09:30:18 -0500 Subject: [PATCH] tweak whole site: caps for Reader monad, etc Signed-off-by: Jim Pryor --- advanced_topics/monads_in_category_theory.mdwn | 4 ++-- assignment6.mdwn | 2 +- code/tree_monadize.ml | 2 +- coroutines_and_aborts.mdwn | 2 +- hints/assignment_7_hint_2.mdwn | 6 +++--- hints/assignment_7_hint_3.mdwn | 2 +- hints/assignment_7_hint_5.mdwn | 2 +- list_monad_as_continuation_monad.mdwn | 22 ++++++++++---------- reader_monad_for_variable_binding.mdwn | 6 +++--- week7.mdwn | 28 +++++++++++++------------- week8.mdwn | 18 ++++++++--------- 11 files changed, 47 insertions(+), 47 deletions(-) diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index da99f402..87c7886d 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -495,12 +495,12 @@ In functional programming, `unit` is sometimes called `return` and the monad law The base category C will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.) -A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions f:C1→C2 to functions M(f):M(C1)→M(C2). This is also known as liftM f for `M`, and is pronounced "function f lifted into the monad M." For example, where `M` is the list monad, `M` maps every type `'t` into the type `'t list`, and maps every function f:x→y into the function that maps `[x1,x2...]` to `[y1,y2,...]`. +A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions f:C1→C2 to functions M(f):M(C1)→M(C2). This is also known as liftM f for `M`, and is pronounced "function f lifted into the monad M." For example, where `M` is the List monad, `M` maps every type `'t` into the type `'t list`, and maps every function f:x→y into the function that maps `[x1,x2...]` to `[y1,y2,...]`. In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad." -A "monadic value" is any member of a type `M('t)`, for any type `'t`. For example, any `int list` is a monadic value for the list monad. We can think of these monadic values as the result of applying some function `phi`, whose type is `F('t) -> M(F'('t))`. `'t` here is any collection of free type variables, and `F('t)` and `F'('t)` are types parameterized on `'t`. An example, with `M` being the list monad, `'t` being `('t1,'t2)`, `F('t1,'t2)` being `char * 't1 * 't2`, and `F'('t1,'t2)` being `int * 't1 * 't2`: +A "monadic value" is any member of a type `M('t)`, for any type `'t`. For example, any `int list` is a monadic value for the List monad. We can think of these monadic values as the result of applying some function `phi`, whose type is `F('t) -> M(F'('t))`. `'t` here is any collection of free type variables, and `F('t)` and `F'('t)` are types parameterized on `'t`. An example, with `M` being the List monad, `'t` being `('t1,'t2)`, `F('t1,'t2)` being `char * 't1 * 't2`, and `F'('t1,'t2)` being `int * 't1 * 't2`: 
 	let phi = fun ((_:char), x, y) -> [(1,x,y),(2,x,y)]
diff --git a/assignment6.mdwn b/assignment6.mdwn
index 30763c1a..5f8c1b65 100644
--- a/assignment6.mdwn
+++ b/assignment6.mdwn
@@ -1,4 +1,4 @@
-1.  **Build a state monad.** Based on the division by zero monad,
+1.  **Build a State monad.** Based on the division by zero monad,
 build a system that will evaluate arithmetic expressions.  Instead of
 returning a simple integer as a result, it will deliver the correct
 answer along with a count of the number of operations performed during
diff --git a/code/tree_monadize.ml b/code/tree_monadize.ml
index d38800a7..6dff768d 100644
--- a/code/tree_monadize.ml
+++ b/code/tree_monadize.ml
@@ -113,7 +113,7 @@ module TreeList =  Tree_monadizer(struct
 end);;
 
 
-(* since the continuation monad is parameterized on two types---it's
+(* since the Continuation monad is parameterized on two types---it's
  * ('a,'r) cont not ('a) cont---we can't match the type ('a) m that
  * Tree_monadizer expects in its parameter. So we have to make a different
  * Tree_monadizer2 that takes a ('a,'x) m type constructor in its
diff --git a/coroutines_and_aborts.mdwn b/coroutines_and_aborts.mdwn
index ca1b2e81..69e96683 100644
--- a/coroutines_and_aborts.mdwn
+++ b/coroutines_and_aborts.mdwn
@@ -603,7 +603,7 @@ into this:
 
 Code written in the latter form is said to be written in **explicit continuation-passing style** or CPS. Later we'll talk about algorithms that mechanically convert an entire program into CPS.
 
-There are also different kinds of "syntactic sugar" we can use to hide the continuation plumbing. Of course we'll be talking about how to manipulate continuations **with a continuation monad.** We'll also talk about a style of working with continuations where they're **mostly implicit**, but special syntax allows us to distill the implicit continuaton into a first-class value (the `k` in `(let/cc k ...)` and `(shift k ...)`.
+There are also different kinds of "syntactic sugar" we can use to hide the continuation plumbing. Of course we'll be talking about how to manipulate continuations **with a Continuation monad.** We'll also talk about a style of working with continuations where they're **mostly implicit**, but special syntax allows us to distill the implicit continuaton into a first-class value (the `k` in `(let/cc k ...)` and `(shift k ...)`.
 
 Various of the tools we've been introducing over the past weeks are inter-related. We saw coroutines implemented first with zippers; here we've talked in the abstract about their being implemented with continuations. Oleg says that "Zipper can be viewed as a delimited continuation reified as a data structure." Ken expresses the same idea in terms of a zipper being a "defunctionalized" continuation---that is, take something implemented as a function (a continuation) and implement the same thing as an inert data structure (a zipper).
 
diff --git a/hints/assignment_7_hint_2.mdwn b/hints/assignment_7_hint_2.mdwn
index 9c1079c3..d1736b32 100644
--- a/hints/assignment_7_hint_2.mdwn
+++ b/hints/assignment_7_hint_2.mdwn
@@ -1,9 +1,9 @@
 
-*	GS&V's semantics involves elements from several different monads we've been looking at. First, they're working with (epistemic) modalities, so there are worlds playing a role like they did in [[Reader Monad for Intensionality]]. But we're going to ignore the modal element for this exercise. There's also variable binding, which calls for [another reader monad](/reader_monad_for_variable_binding). Next, there is a notion of a store, which some operations add new reference cells to. We implement this with a state monad (and so too, in effect, do they---though they don't conceive of what they're doing in those terms). So we'll be working with a combination of both a reader monad for the variable binding and a state monad to keep track of the new "pegs" or reference cells.
+*	GS&V's semantics involves elements from several different monads we've been looking at. First, they're working with (epistemic) modalities, so there are worlds playing a role like they did in [[Reader Monad for Intensionality]]. But we're going to ignore the modal element for this exercise. There's also variable binding, which calls for [another Reader monad](/reader_monad_for_variable_binding). Next, there is a notion of a store, which some operations add new reference cells to. We implement this with a State monad (and so too, in effect, do they---though they don't conceive of what they're doing in those terms). So we'll be working with a combination of both a Reader monad for the variable binding and a State monad to keep track of the new "pegs" or reference cells.
 
 	There are systematic ways to layer different monads together. If you want to read about these, a keyword is "monad transformers." Ken Shan discusses them in [his paper](http://arxiv.org/abs/cs/0205026v1) that we recommended earlier.
 
-	However, since we haven't studied these, we will just combine the reader monad and the state monad in an ad hoc way. The easiest way to do this is to think of the assignment function and the store of reference cells as a combined state, which gets threaded through the computations in the same way that simple states did in your earlier homeworks.
+	However, since we haven't studied these, we will just combine the Reader monad and the State monad in an ad hoc way. The easiest way to do this is to think of the assignment function and the store of reference cells as a combined state, which gets threaded through the computations in the same way that simple states did in your earlier homeworks.
 
 	We'll call these "discourse possibility monads," or `dpm`s, and type them as follows:
 
@@ -18,7 +18,7 @@
 
 	Although we're leaving worlds out of the picture, each of these monadic values still represents a different *discourse* possibility: which entities might be being talked about, using which variables.
 
-	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:
+	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);;
 
diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn
index 4aa9180f..2e4df05d 100644
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -3,7 +3,7 @@
 
 	Now some of the `dpm`s we work with will be `bool dpm`s, which are functions from discourse possibilities to `bool`s (and discourse possibilities). It's tempting to think we might just work with `bool dpm`s instead of sets of possibilities. However, I don't think this can work. The reason why is that at a crucial point in GS&Vs semantics, we have to work with not just a *single* way of mutating or "extending" a discourse possibility, but a *range* of different ways to mutate the live discourse possibilities. So we do need to work with sets, after all.
 
-	A set is just another monadic layer. We've already talked about list monads, and we can for these purposes just use list monads to represent set monads. Instead of sets of possibilities, let's work with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities.
+	A set is just another monadic layer. We've already talked about List monads, and we can for these purposes just use List monads to represent set monads. Instead of sets of possibilities, let's work with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities.
 
 	As I said, for simplicity, we'll represent sets using lists:
 
diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn
index 779fb2ed..de1bbe68 100644
--- a/hints/assignment_7_hint_5.mdwn
+++ b/hints/assignment_7_hint_5.mdwn
@@ -61,7 +61,7 @@ purely dealing with nondeterminism.
 	
bind_set (bind_set u \[[∃x]]) \[[Px]]
 	

 
-*	Let's compare this to what \[[∃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](
+*	Let's compare this to what \[[∃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](
 /reader_monad_for_variable_binding).)
  
 		type assignment = char -> entity;;
diff --git a/list_monad_as_continuation_monad.mdwn b/list_monad_as_continuation_monad.mdwn
index 438e2a80..53bbde1a 100644
--- a/list_monad_as_continuation_monad.mdwn
+++ b/list_monad_as_continuation_monad.mdwn
@@ -2,9 +2,9 @@
 
 We're going to come at continuations from three different directions, and each
 time we're going to end up at the same place: a particular monad, which we'll
-call the continuation monad.
+call the Continuation monad.
 
-Rethinking the list monad
+Rethinking the List monad
 -------------------------
 
 To construct a monad, the key element is to settle on how to implement its type, and
@@ -16,7 +16,7 @@ pattern for the new discussion further below, and it will tie together
 some previously unconnected elements of the course (more specifically,
 version 3 lists and monads).
 
-For instance, take the **Reader Monad**.  Once we decide to define its type as:
+For instance, take the **Reader monad**.  Once we decide to define its type as:
 
 	type 'a reader = env -> 'a
 
@@ -28,7 +28,7 @@ The reason this is a fairly natural choice is that because the type of
 an `'a reader` is `env -> 'a` (by definition), the type of the
 `r_unit` function is `'a -> env -> 'a`, which is an instance of the
 type of the **K** combinator.  So it makes sense that **K** is the unit
-for the reader monad.
+for the Reader monad.
 
 Since the type of the `bind` operator is required to be
 
@@ -70,7 +70,7 @@ constructions we provided in earlier lectures.  We use the condensed
 version here in order to emphasize similarities of structure across
 monads.]
 
-The **State Monad** is similar.  Once we've decided to use the following type constructor:
+The **State monad** is similar.  Once we've decided to use the following type constructor:
 
 	type 'a state = store -> ('a, store)
 
@@ -95,18 +95,18 @@ Abstracting over the `s` and adjusting the types gives the result:
 	let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
 	    fun (s : store) -> let (a, s') = u s in f a s'
 
-The **Option/Maybe Monad** doesn't follow the same pattern so closely, so we
+The **Option/Maybe monad** doesn't follow the same pattern so closely, so we
 won't pause to explore it here, though conceptually its unit and bind
 follow just as naturally from its type constructor.
 
-Our other familiar monad is the **List Monad**, which we were told
+Our other familiar monad is the **List monad**, which we were told
 looks like this:
 
 	(* type 'a list = ['a];; *)
 	l_unit (a : 'a) = [a];;
 	l_bind u f = List.concat (List.map f u);;
 
-Thinking through the list monad will take a little time, but doing so
+Thinking through the List monad will take a little time, but doing so
 will provide a connection with continuations.
 
 Recall that `List.map` takes a function and a list and returns the
@@ -141,7 +141,7 @@ the object returned by the second argument of `bind` to always be of
 type `('something list) list`.  We can eliminate that restriction by flattening
 the list of lists into a single list: this is
 just `List.concat` applied to the output of `List.map`.  So there is some logic to the
-choice of unit and bind for the list monad.
+choice of unit and bind for the List monad.
 
 Yet we can still desire to go deeper, and see if the appropriate bind
 behavior emerges from the types, as it did for the previously
@@ -367,14 +367,14 @@ and:
 		(* an intermediate version, and the fully eta-reduced: *)
 	    fun k -> u (fun a -> f a k)
 
-Consider the most eta-reduced versions of `l'_unit` and `l'_bind`. They're the same as the unit and bind for the Montague continuation monad! In other words, the behavior of our v3-list monad and the behavior of the continuations monad are
+Consider the most eta-reduced versions of `l'_unit` and `l'_bind`. They're the same as the unit and bind for the Montague Continuation monad! In other words, the behavior of our v3-List monad and the behavior of the continuations monad are
 parallel in a deep sense.
 
 Have we really discovered that lists are secretly continuations?  Or
 have we merely found a way of simulating lists using list
 continuations?  Well, strictly speaking, what we have done is shown
 that one particular implementation of lists---the right fold
-implementation---gives rise to a continuation monad fairly naturally,
+implementation---gives rise to a Continuation monad fairly naturally,
 and that this monad can reproduce the behavior of the standard list
 monad.  But what about other list implementations?  Do they give rise
 to monads that can be understood in terms of continuations?
diff --git a/reader_monad_for_variable_binding.mdwn b/reader_monad_for_variable_binding.mdwn
index b9fd816d..ce4d087c 100644
--- a/reader_monad_for_variable_binding.mdwn
+++ b/reader_monad_for_variable_binding.mdwn
@@ -148,7 +148,7 @@ Here we'll use a different monad. It's called the **Reader monad**. We define it
 	(* we assume we've settled on some implementation of the environment *)
 	type env = (char * int) list;;
 
-	(* here's the type of our reader monad *)
+	(* here's the type of our Reader monad *)
 	type 'a reader = env -> 'a;;
 
 	(* here's our unit operation; it creates a reader-monad value that
@@ -190,7 +190,7 @@ Now if we try:
 	# let result = eval (Let('x',Constant 1,Addition(Variable 'x',Constant 2)));;
 	- : int reader = 
 
-How do we see what integer that evaluates to? Well, it's an int-reader monad, which is a function from an `env` to an `int`, so we need to give it some `env` to operate on. We can give it the empty environment:
+How do we see what integer that evaluates to? Well, it's an int-Reader monad, which is a function from an `env` to an `int`, so we need to give it some `env` to operate on. We can give it the empty environment:
 
 	# result [];;
 	- : int = 3
@@ -286,7 +286,7 @@ Substituting in the definition of `shift`, this is:
 		= fun v -> (fun e -> S (lookup i ((i, v e) :: e)) Alice)
 		= fun v -> (fun e -> S (v e) Alice)
 
-In other words, it's a function from entity reader monads to a function from assignment functions to the result of applying S to the value of that entity reader-monad under that assignment function, and to Alice. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[i]] and \[[Alice]].
+In other words, it's a function from entity-Reader monads to a function from assignment functions to the result of applying S to the value of that entity reader-monad under that assignment function, and to Alice. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[i]] and \[[Alice]].
 
 What's not to like?
 
diff --git a/week7.mdwn b/week7.mdwn
index abb6cfe8..961b024a 100644
--- a/week7.mdwn
+++ b/week7.mdwn
@@ -164,7 +164,7 @@ theory of accommodation, and a theory of the situations in which
 material within the sentence can satisfy presuppositions for other
 material that otherwise would trigger a presupposition violation; but,
 not surprisingly, these refinements will require some more
-sophisticated techniques than the super-simple option monad.]
+sophisticated techniques than the super-simple Option monad.]
 
 
 Monads in General
@@ -227,7 +227,7 @@ that provides at least the following three elements:
 
 	So `unit` is a way to put something inside of a monadic box. It's crucial
 	to the usefulness of monads that there will be monadic boxes that
-	aren't the result of that operation. In the option/maybe monad, for
+	aren't the result of that operation. In the Option/Maybe monad, for
 	instance, there's also the empty box `None`. In another (whimsical)
 	example, you might have, in addition to boxes merely containing integers,
 	special boxes that contain integers and also sing a song when they're opened. 
@@ -238,7 +238,7 @@ that provides at least the following three elements:
 
 *	Thirdly, an operation that's often called `bind`. As we said before, this is another
 	unfortunate name: this operation is only very loosely connected to
-	what linguists usually mean by "binding." In our option/maybe monad, the
+	what linguists usually mean by "binding." In our Option/Maybe monad, the
 	bind operation is:
 
 		let bind u f = match u with None -> None | Some x -> f x;;
@@ -260,7 +260,7 @@ that provides at least the following three elements:
 
 	The guts of the definition of the `bind` operation amount to
 	specifying how to unbox the monadic value `u`.  In the `bind`
-	operator for the option monad, we unboxed the monadic value by
+	operator for the Option monad, we unboxed the monadic value by
 	matching it with the pattern `Some x`---whenever `u`
 	happened to be a box containing an integer `x`, this allowed us to
 	get our hands on that `x` and feed it to `f`.
@@ -281,7 +281,7 @@ that provides at least the following three elements:
 	For each new monadic type, this has to be worked out in an
 	useful way.
 
-So the "option/maybe monad" consists of the polymorphic `option` type, the
+So the "Option/Maybe monad" consists of the polymorphic `option` type, the
 `unit`/return function, and the `bind` function.
 
 
@@ -318,7 +318,7 @@ OCaml. In fact, the `<-` symbol already means something different in OCaml,
 having to do with mutable record fields. We'll be discussing mutation someday
 soon.)
 
-As we proceed, we'll be seeing a variety of other monad systems. For example, another monad is the list monad. Here the monadic type is:
+As we proceed, we'll be seeing a variety of other monad systems. For example, another monad is the List monad. Here the monadic type is:
 
 	# type 'a list
 
@@ -345,7 +345,7 @@ of `'b list`s into a single `'b list`:
 	# List.concat [[1]; [1;2]; [1;3]; [1;2;4]]
 	- : int list = [1; 1; 2; 1; 3; 1; 2; 4]
 
-So now we've seen two monads: the option/maybe monad, and the list monad. For any
+So now we've seen two monads: the Option/Maybe monad, and the List monad. For any
 monadic system, there has to be a specification of the complex monad type,
 which will be parameterized on some simpler type `'a`, and the `unit`/return
 operation, and the `bind` operation. These will be different for different
@@ -407,7 +407,7 @@ them from hurting the people that use them or themselves.
 	If you don't understand why the lambda form is necessary (the
 	"fun x -> ..." part), you need to look again at the type of `bind`.
 
-	Some examples of associativity in the option monad (bear in
+	Some examples of associativity in the Option monad (bear in
 	mind that in the Ocaml implementation of integer division, 2/3
 	evaluates to zero, throwing away the remainder):
 
@@ -428,7 +428,7 @@ them from hurting the people that use them or themselves.
 
 Of course, associativity must hold for *arbitrary* functions of
 type `'a -> 'b m`, where `m` is the monad type.  It's easy to
-convince yourself that the `bind` operation for the option monad
+convince yourself that the `bind` operation for the Option monad
 obeys associativity by dividing the inputs into cases: if `u`
 matches `None`, both computations will result in `None`; if
 `u` matches `Some x`, and `f x` evalutes to `None`, then both
@@ -505,7 +505,7 @@ The `lift` operation we asked you to define for last week's homework is a common
 	# let even x = (x mod 2 = 0);;
 	val g : int -> bool = 
 
-`even` has the type `int -> bool`. Now what if we want to convert it into an operation on the option/maybe monad?
+`even` has the type `int -> bool`. Now what if we want to convert it into an operation on the Option/Maybe monad?
 
 	# let lift g = fun u -> bind u (fun x -> Some (g x));;
 	val lift : ('a -> 'b) -> 'a option -> 'b option = 
@@ -518,7 +518,7 @@ also define a lift operation for binary functions:
 
 `lift2 (+)` will now be a function from `int option`s  and `int option`s to `int option`s. This should look familiar to those who did the homework.
 
-The `lift` operation (just `lift`, not `lift2`) is sometimes also called the `map` operation. (In Haskell, they say `fmap` or `<$>`.) And indeed when we're working with the list monad, `lift f` is exactly `List.map f`!
+The `lift` operation (just `lift`, not `lift2`) is sometimes also called the `map` operation. (In Haskell, they say `fmap` or `<$>`.) And indeed when we're working with the List monad, `lift f` is exactly `List.map f`!
 
 Wherever we have a well-defined monad, we can define a lift/map operation for that monad. The examples above used `Some (g x)` and so on; in the general case we'd use `unit (g x)`, using the specific `unit` operation for the monad we're working with.
 
@@ -545,7 +545,7 @@ and so on. Here are the laws that any `ap` operation can be relied on to satisfy
 	ap (unit f) (unit x) = unit (f x)
 	ap u (unit x) = ap (unit (fun f -> f x)) u
 
-Another general monad operation is called `join`. This is the operation that takes you from an iterated monad to a single monad. Remember when we were explaining the `bind` operation for the list monad, there was a step where
+Another general monad operation is called `join`. This is the operation that takes you from an iterated monad to a single monad. Remember when we were explaining the `bind` operation for the List monad, there was a step where
 we went from:
 
 	[[1]; [1;2]; [1;3]; [1;2;4]]
@@ -583,7 +583,7 @@ Continuation monad.
 But first, we'll look at several linguistic applications for monads, based
 on what's called the *Reader monad*.
 
-##[[Reader monad for Variable Binding]]##
+##[[Reader Monad for Variable Binding]]##
 
-##[[Reader monad for Intensionality]]##
+##[[Reader Monad for Intensionality]]##
 
diff --git a/week8.mdwn b/week8.mdwn
index d3b5c1b7..e285451a 100644
--- a/week8.mdwn
+++ b/week8.mdwn
@@ -9,7 +9,7 @@ Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
 uses combinators to impose binding relationships between argument
 positions.  The system does not make use of assignment functions or
 variables.  We'll see that from the point of view of our discussion of
-monads, Jacobson's system is essentially a reader monad in which the
+monads, Jacobson's system is essentially a Reader monad in which the
 assignment function threaded through the computation is limited to at
 most one variable.  It will turn out that Jacobson's geach combinator
 *g* is exactly our `lift` operator, and her binding combinator *z* is
@@ -53,7 +53,7 @@ dependence of a pronoun upwards through the tree using *g* until just
 before you are about to combine with the binder, when you finish off
 with *z*.  (There are examples with longer chains of *g*'s below.)
 
-Last week we saw a reader monad for tracking variable assignments:
+Last week we saw a Reader monad for tracking variable assignments:
 
 
 type env = (char * int) list;;
@@ -74,7 +74,7 @@ an assignemnt function was implemented as a list of `char * int`.  The
 idea is that a list like `[('a', 2); ('b',5)]` associates the variable
 `'a'` with the value 2, and the variable `'b'` with the value 5.
 
-Combining this reader monad with ideas from Jacobson's approach, we
+Combining this Reader monad with ideas from Jacobson's approach, we
 can consider the following monad:
 
 
@@ -89,7 +89,7 @@ let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
 

 
 I've called this the *link* monad, because it links (exactly one)
-pronoun with a binder, but it's a kind of reader monad.  (Prove that
+pronoun with a binder, but it's a kind of Reader monad.  (Prove that
 `ap`, the combinator for applying a linked functor to a linked object,
 can be equivalently defined in terms of `bind` and `unit`.)
 
@@ -98,7 +98,7 @@ kind of value that can be linked into a structure is an individual of
 type `e`.  It is easy to make the monad polymorphic in the type of the
 linked value, which will be necessary to handle, e.g., paycheck pronouns.
 
-In the standard reader monad, the environment is an assignment
+In the standard Reader monad, the environment is an assignment
 function.  Here, instead this monad provides a single value.  The idea
 is that this is the value that will be used to replace the pronoun
 linked to it by the monad.
@@ -122,7 +122,7 @@ link`, and returns a `'b link`, i.e., the result is in the link monad.
 order), but returns something that is not in the monad.  Rather, it
 will be a function from individuals to a computation in which the
 pronoun in question is bound to that individual.  We could emphasize
-the parallel with the reader monad even more by writing a `shift`
+the parallel with the Reader monad even more by writing a `shift`
 operator that used `unit` to produce a monadic result, if we wanted to.
 
 The monad version of *Everyone_i thinks he_i left*, then (remembering
@@ -140,16 +140,16 @@ everyone (z thinks (g (t bill) (g said (g left he))))
 
 So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
 is exactly `bind` with the arguments reversed.  It appears that
-Jacobson's variable-free semantics is essentially a reader monad.
+Jacobson's variable-free semantics is essentially a Reader monad.
 
-One of Jacobson's main points survives: restricting the reader monad
+One of Jacobson's main points survives: restricting the Reader monad
 to a single-value environment eliminates the need for variable names.
 
 Binding more than one variable at a time
 ----------------------------------------
 
 It requires some cleverness to use the link monad to bind more than
-one variable at a time.  Whereas in the standard reader monad a single
+one variable at a time.  Whereas in the standard Reader monad a single
 environment can record any number of variable assignments, because
 Jacobson's monad only tracks a single dependency, binding more than
 one pronoun requires layering the monad.  (Jacobson provides some
-- 
2.11.0