refine again
authorjim <jim@web>
Mon, 6 Apr 2015 13:33:28 +0000 (09:33 -0400)
committerLinux User <ikiwiki@localhost.members.linode.com>
Mon, 6 Apr 2015 13:33:28 +0000 (09:33 -0400)
topics/week8_reader_monad.mdwn

index 07bba89..492f7a3 100644 (file)
@@ -1,12 +1,10 @@
-<!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ¢ ⇧ -->
+<!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
 
 
-[[!toc levels=2]]
 
 
-The Reader Monad
-================
+[[!toc levels=2]]
 
 
-The goal for this part is to introduce the Reader Monad, and present
-two linguistics applications: binding and intensionality. Along the
+The goal for these notes is to introduce the Reader Monad, and present
+two linguistic applications: binding and intensionality. Along the
 way, we'll continue to think through issues related to order, and a
 related notion of flow of information.
 
 way, we'll continue to think through issues related to order, and a
 related notion of flow of information.
 
@@ -54,35 +52,36 @@ _|__    ___|___
 No matter what order we evaluate it in, this computation
 should eventually reduce to `13`. Given a specific reduction strategy,
 we can watch the order in which the computation proceeds. Following
 No matter what order we evaluate it in, this computation
 should eventually reduce to `13`. Given a specific reduction strategy,
 we can watch the order in which the computation proceeds. Following
-on the lambda evaluator developed during the previous homework, let's
+on the evaluator developed during the previous homework, let's
 adopt the following reduction strategy:
 
 > In order to reduce an expression of the form (head arg), do the following in order:
 adopt the following reduction strategy:
 
 > In order to reduce an expression of the form (head arg), do the following in order:
-> 1. Reduce head to h'
-> 2. Reduce arg to a'.
-> 3. If (h' a') is a redex, reduce it.
+
+> 1. Reduce `head` to `head'`
+> 2. Reduce `arg` to `arg'`.
+> 3. If `(head' arg')` is a redex, reduce it.
 
 There are many details left unspecified here, but this will be enough
 for today. The order in which the computation unfolds will be
 
 
 There are many details left unspecified here, but this will be enough
 for today. The order in which the computation unfolds will be
 
-> 1.  Reduce head (+ 1) to itself
-> 2.  Reduce arg ((* ((/ 6) 2)) 4)
->     1.  Reduce head (* ((/ 6) 2))
->         1.  Reduce head * to itself
->         2.  Reduce arg ((/ 6) 2)
->             1.  Reduce head (/ 6) to itself
->             2.  Reduce arg 2 to itself
->             3.  Reduce ((/ 6) 2) to 3
->         3.  Reduce (* 3) to itself
->     2.  Reduce arg 4 to itself
->     3.  Reduce ((* 3) 4) to 12
-> 3.  Reduce ((+ 1) 12) to 13
+> 1.  Reduce head `(+ 1)` to itself
+> 2.  Reduce arg `((* ((/ 6) 2)) 4)`
+>     1.  Reduce head `(* ((/ 6) 2))`
+>         1.  Reduce head `*` to itself
+>         2.  Reduce arg `((/ 6) 2)`
+>             1.  Reduce head `(/ 6)` to itself
+>             2.  Reduce arg `2` to itself
+>             3.  Reduce `((/ 6) 2)` to `3`
+>         3.  Reduce `(* 3)` to itself
+>     2.  Reduce arg `4` to itself
+>     3.  Reduce `((* 3) 4)` to `12`
+> 3.  Reduce `((+ 1) 12)` to `13`
 
 This reduction pattern follows the structure of the original
 expression exactly, at each node moving first to the left branch,
 processing the left branch, then moving to the right branch, and
 finally processing the results of the two subcomputation. (This is
 
 This reduction pattern follows the structure of the original
 expression exactly, at each node moving first to the left branch,
 processing the left branch, then moving to the right branch, and
 finally processing the results of the two subcomputation. (This is
-called depth-first postorder traversal of the tree.)
+called depth-first postorder traversal of the tree.)
 
 [diagram with arrows traversing the tree]
 
 
 [diagram with arrows traversing the tree]
 
@@ -96,7 +95,7 @@ Never mind that these types will allow us to construct silly
 arithmetric trees such as `+ *` or `2 3`. Note that during the
 reduction sequence, the result of reduction was in every case a
 well-formed subtree. So the process of reduction could be animated by
 arithmetric trees such as `+ *` or `2 3`. Note that during the
 reduction sequence, the result of reduction was in every case a
 well-formed subtree. So the process of reduction could be animated by
-replacing subtrees with the result of reduction on that subtree, till
+replacing subtrees with the result of reduction on that subtree, until
 the entire tree is replaced by a single integer (namely, `13`).
 
 Now we replace the number `2` with `0`:
 the entire tree is replaced by a single integer (namely, `13`).
 
 Now we replace the number `2` with `0`:
@@ -121,21 +120,21 @@ _|__    ___|___
 When we reduce, we get quite a ways into the computation before things
 break down:
 
 When we reduce, we get quite a ways into the computation before things
 break down:
 
-> 1.  Reduce head (+ 1) to itself
-> 2.  Reduce arg ((* ((/ 6) 0)) 4)
->     1.  Reduce head (* ((/ 6) 0))
->         1.  Reduce head * to itself
->         2.  Reduce arg ((/ 6) 0)
->             1.  Reduce head (/ 6) to itself
->             2.  Reduce arg 0 to itself
->             3.  Reduce ((/ 6) 0) to ACKKKK
+> 1.  Reduce head `(+ 1)` to itself
+> 2.  Reduce arg `((* ((/ 6) 0)) 4)`
+>     1.  Reduce head `(* ((/ 6) 0))`
+>         1.  Reduce head `*` to itself
+>         2.  Reduce arg `((/ 6) 0)`
+>             1.  Reduce head `(/ 6)` to itself
+>             2.  Reduce arg `0` to itself
+>             3.  Reduce `((/ 6) 0)` to ACKKKK
 
 This is where we replace `/` with `safe_div`. `safe_div` returns not an `int`, but an `int option`.  If the division goes
 through, the result is `Some n`, where `n` is the integer result.
 But if the division attempts to divide by zero, the result is `None`.
 
 We could try changing the type of the arithmetic operators from `int
 
 This is where we replace `/` with `safe_div`. `safe_div` returns not an `int`, but an `int option`.  If the division goes
 through, the result is `Some n`, where `n` is the integer result.
 But if the division attempts to divide by zero, the result is `None`.
 
 We could try changing the type of the arithmetic operators from `int
--> int -> int` at least to `int -> int -> int option`; but since we now have to
+-> int -> int` to `int -> int -> int option`; but since we now have to
 anticipate the possibility that *any* argument might involve division by
 zero inside of it, it would be better to prepare for the possibility
 that any subcomputation might return `None` here. So our operators should have
 anticipate the possibility that *any* argument might involve division by
 zero inside of it, it would be better to prepare for the possibility
 that any subcomputation might return `None` here. So our operators should have
@@ -153,15 +152,15 @@ over `int option`s.
 At this point, we bring in the monadic machinery. In particular, here
 is the `⇧` and the `map2` function from the notes on safe division:
 
 At this point, we bring in the monadic machinery. In particular, here
 is the `⇧` and the `map2` function from the notes on safe division:
 
-    ⇧ (a: 'a) = Some a;;
+    ⇧ (x : 'a) = Some x
 
 
-    map2 (g : 'a -> 'b -> 'c) (xx : 'a option) (yy : 'b option) =
+    map2 (f : 'a -> 'b -> 'c) (xx : 'a option) (yy : 'b option) =
       match xx with
       | None -> None
       | Some x ->
           (match yy with
           | None -> None
       match xx with
       | None -> None
       | Some x ->
           (match yy with
           | None -> None
-          | Some y -> Some (g x y));;
+          | Some y -> Some (f x y))
 
 Then we lift the entire computation into the monad by applying `⇧` to
 the integers, and by applying `map2` to the operators. Only, we will replace `/` with `safe_div`, defined as follows:
 
 Then we lift the entire computation into the monad by applying `⇧` to
 the integers, and by applying `map2` to the operators. Only, we will replace `/` with `safe_div`, defined as follows:
@@ -173,7 +172,7 @@ the integers, and by applying `map2` to the operators. Only, we will replace `/`
           (match yy with
           | None -> None
           | Some 0 -> None
           (match yy with
           | None -> None
           | Some 0 -> None
-          | Some y -> Some ((/) x y));;
+          | Some y -> Some ((/) x y))
 
 <!--
 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
 
 <!--
 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
@@ -194,20 +193,20 @@ map2 +  ⇧1    _____|_____  ⇧4
 
 With these adjustments, the faulty computation now completes smoothly:
 
 
 With these adjustments, the faulty computation now completes smoothly:
 
-> 1.  Reduce head ((map2 +) ⇧1)
-> 2.  Reduce arg (((map2 *) ((safe_div ⇧6) ⇧0)) ⇧4)
->     1.  Reduce head ((map2 *) ((safe_div ⇧6) ⇧0))
->         1.  Reduce head (map2 *)
->         2.  Reduce arg ((safe_div ⇧6) ⇧0)
->             1.  Reduce head (safe_div ⇧6)
->             2.  Reduce arg ⇧0
->             3.  Reduce ((safe_div ⇧6) ⇧0) to None
->         3.  Reduce ((map2 *) None)
->     2.  Reduce arg ⇧4
->     3.  Reduce (((map2 *) None) ⇧4) to None
-> 3.  Reduce (((map2 +) ⇧1) None) to None
-
-As soon as we try to divide by 0, `safe_div` returns `None`.
+> 1.  Reduce head `((map2 +) ⇧1)`
+> 2.  Reduce arg `(((map2 *) ((safe_div ⇧6) ⇧0)) ⇧4)`
+>     1.  Reduce head `((map2 *) ((safe_div ⇧6) ⇧0))`
+>         1.  Reduce head `(map2 *)`
+>         2.  Reduce arg `((safe_div ⇧6) ⇧0)`
+>             1.  Reduce head `(safe_div ⇧6)`
+>             2.  Reduce arg `⇧0`
+>             3.  Reduce `((safe_div ⇧6) ⇧0)` to `None`
+>         3.  Reduce `((map2 *) None)`
+>     2.  Reduce arg `⇧4`
+>     3.  Reduce `(((map2 *) None) ⇧4)` to `None`
+> 3.  Reduce `(((map2 +) ⇧1) None)` to `None`
+
+As soon as we try to divide by `0`, `safe_div` returns `None`.
 Thanks to the details of `map2`, the fact that `None` has been returned
 by one of the arguments of a `map2`-ed operator guarantees that the
 `map2`-ed operator will pass on the `None` as its result. So the
 Thanks to the details of `map2`, the fact that `None` has been returned
 by one of the arguments of a `map2`-ed operator guarantees that the
 `map2`-ed operator will pass on the `None` as its result. So the
@@ -225,7 +224,7 @@ So at this point, we can see how the Option/Maybe monad provides
 plumbing that allows subcomputations to send information from one part
 of the computation to another. In this case, the `safe_div` function
 can send the information that division by zero has been attempted
 plumbing that allows subcomputations to send information from one part
 of the computation to another. In this case, the `safe_div` function
 can send the information that division by zero has been attempted
-throughout the rest of the computation. If you think of the plumbing
+upwards to the rest of the computation. If you think of the plumbing
 as threaded through the tree in depth-first, postorder traversal, then
 `safe_div` drops `None` into the plumbing half way through the
 computation, and that `None` travels through the rest of the plumbing
 as threaded through the tree in depth-first, postorder traversal, then
 `safe_div` drops `None` into the plumbing half way through the
 computation, and that `None` travels through the rest of the plumbing
@@ -235,7 +234,7 @@ till it comes out of the result faucet at the top of the tree.
 ## Information flowing in the other direction: top to bottom
 
 We can think of this application as facilitating information flow.
 ## Information flowing in the other direction: top to bottom
 
 We can think of this application as facilitating information flow.
-In the save-div example, a subcomputation created a message that
+In the `safe_div` example, a subcomputation created a message that
 propagated upwards to the larger computation:
 
 <pre>
 propagated upwards to the larger computation:
 
 <pre>
@@ -261,7 +260,7 @@ information available at the top of the computation available to the
 subcomputations: 
 
 <pre>
 subcomputations: 
 
 <pre>
-                    [λx]  
+                    [λn]  
  ___________          |
  |         |          |
 _|__    ___|___       |
  ___________          |
  |         |          |
 _|__    ___|___       |
@@ -270,7 +269,7 @@ _|__    ___|___       |
       |    |          |
       *  __|___       |
          |    |       |
       |    |          |
       *  __|___       |
          |    |       |
-        _|__  x  <----|
+        _|__  n  <----|
         |  |
         /  6
 </pre>
         |  |
         /  6
 </pre>
@@ -281,6 +280,7 @@ embedded position. Whatever the value of the argument that the lambda
 form combines with, that is what will be substituted in for free
 occurrences of that variable within the body of the lambda.
 
 form combines with, that is what will be substituted in for free
 occurrences of that variable within the body of the lambda.
 
+
 ## Binding
 
 So our next step is to add a (primitive) version of binding to our
 ## Binding
 
 So our next step is to add a (primitive) version of binding to our
@@ -308,7 +308,8 @@ type <u>α</u> = int -> α
 ⇧x = \n. x
 xx >>= k = \n. k (xx n) n
 map  f xx = \n. f (xx n)
 ⇧x = \n. x
 xx >>= k = \n. k (xx n) n
 map  f xx = \n. f (xx n)
-map2 f xx yy = \n. f (xx n) (yy n)
+ff ¢ xx = \n. (ff n) (xx n)
+map2 f xx yy = map f xx ¢ yy = \n. f (xx n) (yy n)
 </pre>
 
 A boxed type in this monad will be a function from an integer to an
 </pre>
 
 A boxed type in this monad will be a function from an integer to an
@@ -318,15 +319,14 @@ integer and returns `x` instead (most values in the computation don't
 depend on the input integer).
 
 The `mbind`/`>>=` function in this monad takes a monadic value `xx`, a function
 depend on the input integer).
 
 The `mbind`/`>>=` function in this monad takes a monadic value `xx`, a function
-`k` lifting non-monadic objects into the monad, and returns a function
+`k` taking non-monadic values into the monad, and returns a function
 that expects an integer `n`. It feeds `n` to `xx`, which delivers a
 result in the orginal type, which is fed in turn to `k`. `k` returns
 that expects an integer `n`. It feeds `n` to `xx`, which delivers a
 result in the orginal type, which is fed in turn to `k`. `k` returns
-a monadic value, which upon being fed an integer, also delivers a value
+a monadic value, which upon being fed an integer, also delivers a result
 in the orginal type.
 
 in the orginal type.
 
-The `map2` function corresponding to this bind operation is given
-above. It may look familiar --- we'll be commenting on this
-familiarity in a moment.
+The `map`, `¢`, and `map2` functions corresponding to this `mbind` are given
+above. They may look familiar --- we'll comment on this in a moment.
 
 Lifing the computation into the monad, we have the following adjusted
 types:
 
 Lifing the computation into the monad, we have the following adjusted
 types:
@@ -354,14 +354,14 @@ map2 +  ⇧1    ____|_____  ⇧4
                map2 /  ⇧6
 </pre>
 
                map2 /  ⇧6
 </pre>
 
-It remains only to decide how the variable `x` will access the input value supplied
+It remains only to decide how the variable `n` will access the input value supplied
 at the top of the tree. The input value is supposed to be the
 at the top of the tree. The input value is supposed to be the
-value that gets used for the variable `x`. Like every leaf in the tree
+value that gets used for the variable `n`. Like every leaf in the tree
 in argument position, the code we want in order to represent the
 variable will have the type of a boxed `int`, namely, `int -> int`. So
 we have the following:
 
 in argument position, the code we want in order to represent the
 variable will have the type of a boxed `int`, namely, `int -> int`. So
 we have the following:
 
-    varx = fun (n : int) -> n
+    var_n = fun (n : int) -> n
 
 That is, variables in this system denote the identity function!
 
 
 That is, variables in this system denote the identity function!
 
@@ -370,7 +370,8 @@ from any integer `n` to `(+ 1 (* (/ 6 n)) 4)`.
 
 Take a look at the definition of the Reader monad again. The
 `mid` takes some object `x` and returns `\n. x`. In other words,
 
 Take a look at the definition of the Reader monad again. The
 `mid` takes some object `x` and returns `\n. x`. In other words,
-`⇧x = Kx`, for our familiar combinator **K**, so `⇧ = K`. Likewise, the reason the `map2` function looked familiar is that it seems to involve the `S` combinator. In fact, the `mapply`/`¢` operator for the Reader monad is exactly `\ff xx n -> (ff n) (xx n)`, or the **S** combinator. `map2 f xx yy` for the Reader monad is `(f ○ xx) ¢ yy`, where `○` is function composition, which implements `map` for the Reader monad. So in other words, `map2 f xx yy` is `S (f ○ xx) yy`.
+`⇧x = Kx`, for our familiar combinator **K**, so `⇧ = K`. Likewise, the `map` operation
+is just function composition, and the `mapply`/`¢` operation is our friend the **S** combinator. `map2 f xx yy` for the Reader monad is `(f ○ xx) ¢ yy` or `S (f ○ xx) yy`.
 
 We've seen this before as a strategy for translating a binding
 construct into a set of combinators. To remind you, here is a part of
 
 We've seen this before as a strategy for translating a binding
 construct into a set of combinators. To remind you, here is a part of
@@ -388,8 +389,7 @@ scheme is that we're making the simplifying assumption that there is
 at most a single lambda involved. So once again we have the identity
 function **I** as the translation of the bound variable, **K** as the function
 governing expressions that don't contain an instance of the bound
 at most a single lambda involved. So once again we have the identity
 function **I** as the translation of the bound variable, **K** as the function
 governing expressions that don't contain an instance of the bound
-variable, **S** as an operation that manages the applicative combination of complex
-expressions.
+variable, **S** as an operation that manages `¢`, that is, the applicative combination of complex expressions.
 
 
 ## Jacobson's Variable Free Semantics as a Reader Monad
 
 
 ## Jacobson's Variable Free Semantics as a Reader Monad
@@ -398,11 +398,11 @@ We've designed the presentation above to make it as easy as possible
 to show that Jacobson's Variable Free Semantics (e.g., Jacobson 1999,
 [Towards a Variable-Free
 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
 to show that Jacobson's Variable Free Semantics (e.g., Jacobson 1999,
 [Towards a Variable-Free
 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
-implements a reader monad.
+implements a Reader monad.
 
 More specifically, it will turn out that Jacobson's geach combinator
 
 More specifically, it will turn out that Jacobson's geach combinator
-*g* is exactly our `lift` operator, and her binding combinator *z* is
-exactly our `bind` (though with the arguments reversed).
+*g* is exactly our `map` operator, and her binding combinator *z* is
+exactly our `mbind` (though with the arguments reversed).
 
 Jacobson's system contains two main combinators, *g* and *z*. She
 calls *g* the Geach rule, and *z* performs binding. Here is a typical
 
 Jacobson's system contains two main combinators, *g* and *z*. She
 calls *g* the Geach rule, and *z* performs binding. Here is a typical
@@ -411,14 +411,14 @@ Charlow, with beta reduction as performed by the on-line evaluator:
 
 <pre>
 ; Jacobson's analysis of "Everyone_i thinks he_i left"
 
 <pre>
 ; Jacobson's analysis of "Everyone_i thinks he_i left"
-let g = \f u. \x. f (u x) in
-let z = \f u. \x. f (u x) x in
-let he = \x. x in
-let everyone = \P. FORALL x (P x) in
+let g = \f xx. \n. f (xx n) in ; or `f ○ xx`
+let z = \k xx. \n. k (xx n) n in ; or `S (flip k) xx`, or `Reader.(>>=) xx k`
+let he = \n. n in
+let everyone = \P. FORALL i (P i) in
 
 everyone (z thinks (g left he))
 
 
 everyone (z thinks (g left he))
 
-~~>  FORALL x (thinks (left x) x)
+~~>  FORALL i (thinks (left i) i)
 </pre>
 
 Two things to notice: First, pronouns once again denote identity
 </pre>
 
 Two things to notice: First, pronouns once again denote identity
@@ -433,19 +433,22 @@ before you are about to combine with the binder, when you finish off
 with *z*. Here is an example with a longer chain of *g*'s:
 
 <pre>
 with *z*. Here is an example with a longer chain of *g*'s:
 
 <pre>
-everyone (z thinks (g (t bill) (g said (g left he))))
+; "Everyone_i thinks that Bill said he_i left"
+
+everyone (z thinks (g (T bill) (g said (g left he))))
+; or `everyone (thinks =<< T bill ○ said ○ left ○ I)`
 
 
-~~> FORALL x (thinks (said (left x) bill) x)
+~~> FORALL i (thinks (said (left i) bill) i)
 </pre>
 
 If you compare Jacobson's values for *g* and *z* to the functions in
 the reader monad given above, you'll see that Jacobson's *g*
 combinator is exactly our `map` operator. Furthermore, Jacobson's *z*
 </pre>
 
 If you compare Jacobson's values for *g* and *z* to the functions in
 the reader monad given above, you'll see that Jacobson's *g*
 combinator is exactly our `map` operator. Furthermore, Jacobson's *z*
-combinator is identital to `>>=`, except with the order of the
-arguments reversed (i.e., `(z f u) == (u >>= f)`).
+combinator is identical to our Reader `>>=`, except with the order of the
+arguments reversed (i.e., `(z k xx) == (xx >>= k)`).
 
 
-(The `t` combinator in the derivations above is given by `t x =
-\xy.yx`; it handles situations in which English word order reverses
+(The `T` combinator in the derivations above is given by `T x <~~> \f. f x`;
+it handles situations in which English word order reverses
 the usual function/argument order.)
 
 In other words, 
 the usual function/argument order.)
 
 In other words, 
@@ -460,10 +463,6 @@ argument, here, *thinks*.
 
 ## The Reader monad for intensionality
 
 
 ## The Reader monad for intensionality
 
-[This section has not been revised since 2010, so there may be a few
-places where it doesn't follow the convetions we've adopted this time;
-nevertheless, it should be followable.]
-
 Now we'll look at using the Reader monad to do intensional function application.
 
 In Shan (2001) [Monads for natural
 Now we'll look at using the Reader monad to do intensional function application.
 
 In Shan (2001) [Monads for natural
@@ -485,10 +484,10 @@ Note the extra `#` attached to the directive `use`.
 
 First, the familiar linguistic problem:
 
 
 First, the familiar linguistic problem:
 
-       Bill left.  
-          Cam left.
-          Ann believes [Bill left].
-          Ann believes [Cam left].
+    Bill left.  
+    Cam left.
+    Ann believes that Bill left.
+    Ann believes that Cam left.
 
 We want an analysis on which the first three sentences can be true at
 the same time that the last sentence is false. If sentences denoted
 
 We want an analysis on which the first three sentences can be true at
 the same time that the last sentence is false. If sentences denoted
@@ -520,10 +519,10 @@ individuals rather than to generalized quantifiers.
 
 The main difference between the intensional types and the extensional
 types is that in the intensional types, the arguments are functions
 
 The main difference between the intensional types and the extensional
 types is that in the intensional types, the arguments are functions
-from worlds to extensions: intransitive verb phrases like "left" now
-take so-called "individual concepts" as arguments (type s->e) rather than plain
-individuals (type e), and attitude verbs like "think" now take
-propositions (type s->t) rather than truth values (type t).
+from worlds to extensions: intransitive verb phrases like *left* now
+take so-called "individual concepts" as arguments (type `s->e`) rather than plain
+individuals (type `e`), and attitude verbs like *think* now take
+propositions (type `s->t`) rather than truth values (type `t`).
 In addition, the result of each predicate is an intension.
 This expresses the fact that the set of people who left in one world
 may be different than the set of people who left in a different world.
 In addition, the result of each predicate is an intension.
 This expresses the fact that the set of people who left in one world
 may be different than the set of people who left in a different world.
@@ -535,7 +534,7 @@ in the way that the intensionality monad makes most natural.
 
 The intensional types are more complicated than the extensional
 types. Wouldn't it be nice to make the complicated types available
 
 The intensional types are more complicated than the extensional
 types. Wouldn't it be nice to make the complicated types available
-for those expressions like attitude verbs that need to worry about
+for expressions like attitude verbs that need to worry about
 intensions, and keep the rest of the grammar as extensional as
 possible? This desire is parallel to our earlier desire to limit the
 concern about division by zero to the division function, and let the
 intensions, and keep the rest of the grammar as extensional as
 possible? This desire is parallel to our earlier desire to limit the
 concern about division by zero to the division function, and let the
@@ -544,22 +543,22 @@ division-by-zero problems as much as possible.
 
 So here's what we do:
 
 
 So here's what we do:
 
-In OCaml, we'll use integers to model possible worlds. Characters (characters in the computational sense, i.e., letters like `'a'` and `'b'`, not Kaplanian characters) will model individuals, and OCaml booleans will serve for truth values:
+In OCaml, we'll use integers to model possible worlds. `char`s (characters in the computational sense, i.e., letters like `'a'` and `'b'`, not Kaplanian characters) will model individuals, and OCaml `bool`s will serve for truth values:
 
 
-       type s = int;;
-       type e = char;;
-       type t = bool;;
+       type s = int
+       type e = char
+       type t = bool
 
 
-       let ann = 'a';;
-       let bill = 'b';;
-       let cam = 'c';;
+       let ann = 'a'
+       let bill = 'b'
+       let cam = 'c'
 
 
-       let left1 (x:e) = true;; 
-       let saw1 (x:e) (y:e) = y < x;; 
+       let left1 (x : e) = true 
+       let saw1 (y : e) (x : e) = x < y 
 
 
-       left1 ann;; (* true *)
-       saw1 bill ann;; (* true *)
-       saw1 ann bill;; (* false *)
+       left1 ann (* true *)
+       saw1 bill ann (* true *)
+       saw1 ann bill (* false *)
 
 So here's our extensional system: everyone left, including Ann;
 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
 
 So here's our extensional system: everyone left, including Ann;
 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
@@ -569,9 +568,9 @@ Now we add intensions. Because different people leave in different
 worlds, the meaning of *leave* must depend on the world in which it is
 being evaluated:
 
 worlds, the meaning of *leave* must depend on the world in which it is
 being evaluated:
 
-    let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
-    left ann 1;; (* true: Ann left in world 1 *)
-    left cam 2;; (* false: Cam didn't leave in world 2 *) 
+    let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true
+    left ann 1 (* true: Ann left in world 1 *)
+    left cam 2 (* false: Cam didn't leave in world 2 *) 
 
 This new definition says that everyone always left, except that 
 in world 2, Cam didn't leave.
 
 This new definition says that everyone always left, except that 
 in world 2, Cam didn't leave.
@@ -583,7 +582,7 @@ the chart above, which was `(s->e)->s->t`. This is because
 making the subject an individual concept. In semantics jargon, we say
 that *leave* is extensional with respect to its first argument.
 
 making the subject an individual concept. In semantics jargon, we say
 that *leave* is extensional with respect to its first argument.
 
-Therefore we will adopt the general strategy of defining predicates
+We will adopt the general strategy of defining predicates
 in a way that they take arguments of the lowest type that will allow
 us to make all the distinctions the predicate requires. When it comes
 time to combine this predicate with monadic arguments, we'll have to
 in a way that they take arguments of the lowest type that will allow
 us to make all the distinctions the predicate requires. When it comes
 time to combine this predicate with monadic arguments, we'll have to
@@ -592,9 +591,9 @@ make use of various lifting predicates.
 Likewise, although *see* depends on the world of evaluation, it is
 extensional in both of its syntactic arguments:
 
 Likewise, although *see* depends on the world of evaluation, it is
 extensional in both of its syntactic arguments:
 
-    let saw x y w = (w < 2) && (y < x);;
-    saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
-    saw bill ann 2;; (* false: no one saw anyone in world 2 *)
+    let saw (y : e) (x : e) (w : s) = (w < 2) && (x < y)
+    saw bill ann 1 (* true: Ann saw Bill in world 1 *)
+    saw bill ann 2 (* false: no one saw anyone in world 2 *)
 
 This (again, partially) intensionalized version of *see* coincides
 with the `saw1` function we defined above for world 1; in world 2, no
 
 This (again, partially) intensionalized version of *see* coincides
 with the `saw1` function we defined above for world 1; in world 2, no
@@ -612,82 +611,84 @@ Just to keep things straight, let's review the facts:
 Now we are ready for the intensionality monad:
 
 <pre>
 Now we are ready for the intensionality monad:
 
 <pre>
-type 'a intension = s -> 'a;;
-let unit x = fun (w:s) -> x;;
-(* as before, bind can be written more compactly, but having
-   it spelled out like this will be useful down the road *)
-let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
+type 'a intension = s -> 'a
+let mid x = fun (w : s) -> x
+let (>>=) xx k = fun (w : s) -> let x = xx w in let yy = k x in yy w
+                 (* or just `fun w -> k (xx w) w` *)
 </pre>
 
 </pre>
 
-Then the individual concept `unit ann` is a rigid designator: a
+Then the individual concept `mid ann` is a rigid designator: a
 constant function from worlds to individuals that returns `'a'` no
 matter which world is used as an argument. This is a typical kind of
 constant function from worlds to individuals that returns `'a'` no
 matter which world is used as an argument. This is a typical kind of
-thing for a monad unit to do.
+thing for a monadic `mid` to do.
 
 Then combining a predicate like *left* which is extensional in its
 
 Then combining a predicate like *left* which is extensional in its
-subject argument with an intensional subject like `unit ann` is simply bind
+subject argument with an intensional subject like `mid ann` is simply `mbind`
 in action:
 
 in action:
 
-    bind (unit ann) left 1;; (* true: Ann left in world 1 *)
-    bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
+    (mid ann >>= left) 1  (* true: Ann left in world 1 *)
+    (mid cam >>= left) 2  (* false: Cam didn't leave in world 2 *)
 
 
-As usual, bind takes a monad box containing Ann, extracts Ann, and
+As usual, `>>=` takes a monadic box containing Ann, extracts Ann, and
 feeds her to the extensional *left*. In linguistic terms, we take the
 feeds her to the extensional *left*. In linguistic terms, we take the
-individual concept `unit ann`, apply it to the world of evaluation in
+individual concept `mid ann`, apply it to the world of evaluation in
 order to get hold of an individual (`'a'`), then feed that individual
 to the extensional predicate *left*.
 
 We can arrange for a transitive verb that is extensional in both of
 its arguments to take intensional arguments:
 
 order to get hold of an individual (`'a'`), then feed that individual
 to the extensional predicate *left*.
 
 We can arrange for a transitive verb that is extensional in both of
 its arguments to take intensional arguments:
 
-    let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
+    let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> f x y))
 
 
-This is almost the same `lift2` predicate we defined in order to allow
+This is almost the same `map2` predicate we defined in order to allow
 addition in our division monad example. The difference is that this
 variant operates on verb meanings that take extensional arguments but
 addition in our division monad example. The difference is that this
 variant operates on verb meanings that take extensional arguments but
-returns an intensional result. Thus the original `lift2` predicate
-has `unit (f x y)` where we have just `f x y` here.
+returns an intensional result. Thus the original `map2` predicate
+has `mid (f x y)` where we have just `f x y` here.
 
 
-The use of `bind` here to combine *left* with an individual concept,
-and the use of `lift2'` to combine *see* with two intensional
+The use of `>>=` here to combine *left* with an individual concept,
+and the use of `map2'` to combine *see* with two intensional
 arguments closely parallels the two of Montague's meaning postulates
 (in PTQ) that express the relationship between extensional verbs and
 their uses in intensional contexts.
 
 <pre>
 arguments closely parallels the two of Montague's meaning postulates
 (in PTQ) that express the relationship between extensional verbs and
 their uses in intensional contexts.
 
 <pre>
-lift2' saw (unit bill) (unit ann) 1;;  (* true *)
-lift2' saw (unit bill) (unit ann) 2;;  (* false *)
+map2' saw (mid bill) (mid ann) 1  (* true *)
+map2' saw (mid bill) (mid ann) 2  (* false *)
 </pre>
 
 </pre>
 
-Ann did see bill in world 1, but Ann didn't see Bill in world 2.
+Ann did see Bill in world 1, but Ann didn't see Bill in world 2.
 
 Finally, we can define our intensional verb *thinks*. *Think* is
 intensional with respect to its sentential complement, though still extensional
 with respect to its subject. (As Montague noticed, almost all verbs
 in English are extensional with respect to their subject; a possible
 
 Finally, we can define our intensional verb *thinks*. *Think* is
 intensional with respect to its sentential complement, though still extensional
 with respect to its subject. (As Montague noticed, almost all verbs
 in English are extensional with respect to their subject; a possible
-exception is "appear".)
+exception is *appear*.)
 
     let thinks (p:s->t) (x:e) (w:s) = 
 
     let thinks (p:s->t) (x:e) (w:s) = 
-      match (x, p 2) with ('a', false) -> false | _ -> p w;;
+      match (x, p 2) with ('a', false) -> false | _ -> p w
+
+In every world, Ann fails to believe any proposition that is false in world 2.
+Apparently, she stably thinks we may be in world 2. Otherwise, everyone
+believes a proposition iff that proposition is true in the world of evaluation.
+
+    (mid ann >>= thinks (mid bill >>= left)) 1  (* true *)
+
+So in world 1, Ann thinks that Bill left (because in worlds 1 and 2, Bill did leave).
 
 
-Ann disbelieves any proposition that is false in world 2. Apparently,
-she firmly believes we're in world 2. Everyone else believes a
-proposition iff that proposition is true in the world of evaluation.
+But although Cam left in world 1:
 
 
-    bind (unit ann) (thinks (bind (unit bill) left)) 1;;
+    (mid cam >>= left) 1  (* true *)
 
 
-So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
+he didn't leave in world 2, so Ann doesn't in world 1 believe that Cam left:
 
 
-    bind (unit ann) (thinks (bind (unit cam) left)) 1;;
+    (mid ann >>= thinks (mid cam >>= left)) 1  (* false *)
 
 
-But in world 1, Ann doesn't believe that Cam left (even though he
-did leave in world 1: `bind (unit cam) left 1 == true`). Ann's thoughts are hung up on
-what is happening in world 2, where Cam doesn't leave.
 
 
-*Small project*: add intersective ("red") and non-intersective
- adjectives ("good") to the fragment. The intersective adjectives
+**Small project**: add intersective (*red*) and non-intersective
+ adjectives (*good*) to the fragment. The intersective adjectives
  will be extensional with respect to the nominal they combine with
  will be extensional with respect to the nominal they combine with
- (using bind), and the non-intersective adjectives will take
+ (using `mbind`), and the non-intersective adjectives will take
  intensional arguments.
 
 notes: cascade, general env
  intensional arguments.
 
 notes: cascade, general env