X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=reader_monad_for_variable_binding.mdwn;h=ce4d087c2889b7745d7d16287b6f21a97fa6255a;hp=3591c24b401ce341aed5292cc42a983c187522d7;hb=2daa38a304aaee91b9d3ac57274cfa7d63977198;hpb=5555d992063202b118a612862085a06291bc6f47

diff --git a/reader_monad_for_variable_binding.mdwn b/reader_monad_for_variable_binding.mdwn
index 3591c24b..ce4d087c 100644
--- a/reader_monad_for_variable_binding.mdwn
+++ b/reader_monad_for_variable_binding.mdwn
@@ -1,3 +1,5 @@
+[[!toc]]
+
 Substitution versus Environment-based Semantics
 -----------------------------------------------
 
@@ -146,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
@@ -188,7 +190,7 @@ Now if we try:
 	# let result = eval (Let('x',Constant 1,Addition(Variable 'x',Constant 2)));;
 	- : int reader = <fun>
 
-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
@@ -284,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?