9bbc0152c3f20c4d2512a7588f1b9e4145fc4f8e
1 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ¢ ⇧ -->
3 The Reader Monad
4 ================
6 The goal for this part is to introduce the Reader Monad, and present
7 two linguistics applications: binding and intensionality.  Along the
8 way, we'll continue to think through issues related to order, and a
9 related notion of flow of information.
11 At this point, we've seen monads in general, and three examples of
12 monads: the identity monad (invisible boxes), the Maybe monad (option
13 types), and the List monad.
15 We've also seen an application of the Maybe monad to safe division.
16 The starting point was to allow the division function to return an int
17 option instead of an int.  If we divide 6 by 2, we get the answer Just
18 3.  But if we divide 6 by 0, we get the answer Nothing.
20 The next step was to adjust the other arithmetic functions to know how
21 to handle receiving Nothing instead of a (boxed) integer.  This meant
22 changing the type of their input from ints to int options.  But we
23 didn't need to do this piecemeal; rather, we could "lift" the ordinary
24 arithmetic operations into the monad using the various tools provided
25 by the monad.
27 ## Tracing the effect of safe-div on a larger computation
29 So let's see how this works in terms of a specific computation.
31 <pre>
32 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
34  ___________
35  |         |
36 _|__    ___|___
37 |  |    |     |
38 +  1  __|___  4
39       |    |
40       *  __|___
41          |    |
42         _|__  2
43         |  |
44         /  6
45 </pre>
47 This computation should reduce to 13.  But given a specific reduction
48 strategy, we can watch the order in which the computation proceeds.
49 Following on the lambda evaluator developed during the previous
50 homework, let's adopt the following reduction strategy:
52     In order to reduce (head arg), do the following in order:
53     1. Reduce head to h'
54     2. Reduce arg to a'.
55     3. If (h' a') is a redex, reduce it.
57 There are many details left unspecified here, but this will be enough
58 for today.  The order in which the computation unfolds will be
60     1. Reduce head (+ 1) to itself
61     2. Reduce arg ((* ((/ 6) 2)) 3)
62          1. Reduce head (* ((/ 6) 2))
63               1. Reduce head *
64               2. Reduce arg ((/ 6) 2)
65                    1. Reduce head (/ 6) to itself
66                    2. Reduce arg 2 to itself
67                    3. Reduce ((/ 6) 2) to 3
68               3. Reduce (* 3) to itself
69          2. Reduce arg 4 to itself
70          3. Reduce ((* 3) 4) to 12
71      3. Reduce ((+ 1) 12) to 13
73 This reduction pattern follows the structure of the original
74 expression exactly, at each node moving first to the left branch,
75 processing the left branch, then moving to the right branch, and
76 finally processing the results of the two subcomputation.  (This is
77 called depth-first postorder traversal of the tree.)
79 It will be helpful to see how the types change as we make adjustments.
81     type num = int
82     type contents = Num of num   | Op of (num -> num -> num)
83     type tree = Leaf of contents | Branch of tree * tree
85 Never mind that these types will allow us to construct silly
86 arithmetric trees such as `+ *` or `2 3`.  Note that during the
87 reduction sequence, the result of reduction was in every case a
88 well-formed subtree.  So the process of reduction could be animated by
89 replacing subtrees with the result of reduction on that subtree, till
90 the entire tree is replaced by a single integer (namely, 13).
92 Now we replace the number 2 with 0:
94 <pre>
95 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
97  ___________
98  |         |
99 _|__    ___|___
100 |  |    |     |
101 +  1  __|___  4
102       |    |
103       *  __|___
104          |    |
105         _|__  0
106         |  |
107         /  6
108 </pre>
110 When we reduce, we get quite a ways into the computation before things
111 go south:
113     1. Reduce head (+ 1) to itself
114     2. Reduce arg ((* ((/ 6) 0)) 3)
115          1. Reduce head (* ((/ 6) 0))
116               1. Reduce head *
117               2. Reduce arg ((/ 6) 0)
118                    1. Reduce head (/ 6) to itself
119                    2. Reduce arg 0 to itself
120                    3. Reduce ((/ 6) 0) to ACKKKK
122 This is where we replace `/` with `safe-div`.  This means changing the
123 type of the arithmetic operators from `int -> int -> int` to
124 `int -> int -> int option`; and since we now have to anticipate the
125 possibility that any argument might involve division by zero inside of
126 it, here is the net result for our types:
128     type num = int option
129     type contents = Num of num   | Op of (num -> num -> num)
130     type tree = Leaf of contents | Branch of tree * tree
132 The only difference is that instead of defining our numbers to be
133 simple integers, they are now int options; and so Op is an operator
134 over int options.
136 At this point, we bring in the monadic machinery.  In particular, here
137 is the ⇧ and the map2 function from the notes on safe division:
139     ⇧ (a: 'a) = Just a;;
141     map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
142       match u with
143       | None -> None
144       | Some x ->
145           (match v with
146           | None -> None
147           | Some y -> Some (g x y));;
149 Then we lift the entire computation into the monad by applying ⇧ to
150 the integers, and by applying `map1` to the operators:
152 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
154      ___________________
155      |                 |
156   ___|____         ____|_____
157   |      |         |        |
158 map2 +  ⇧1    _____|_____  ⇧4
159               |         |
160             map2 *  ____|____
161                     |       |
162                  ___|____  ⇧0
163                  |      |
164                map2 /  ⇧6
166 With these adjustments, the faulty computation now completes smoothly:
168     1. Reduce head ((map2 +)  -->
170 The Reader Monad
171 ================
173 The goal for this part is to introduce the Reader Monad, and present
174 two linguistics applications: binding and intensionality.  Along the
175 way, we'll continue to think through issues related to order, and a
176 related notion of flow of information.
178 At this point, we've seen monads in general, and three examples of
179 monads: the identity monad (invisible boxes), the Maybe monad (option
180 types), and the List monad.
182 We've also seen an application of the Maybe monad to safe division.
183 The starting point was to allow the division function to return an int
184 option instead of an int.  If we divide 6 by 2, we get the answer Just
185 3.  But if we divide 6 by 0, we get the answer Nothing.
187 The next step was to adjust the other arithmetic functions to know how
188 to handle receiving Nothing instead of a (boxed) integer.  This meant
189 changing the type of their input from ints to int options.  But we
190 didn't need to do this piecemeal; rather, we could "lift" the ordinary
191 arithmetic operations into the monad using the various tools provided
192 by the monad.
194 So let's see how this works in terms of a specific computation.
196 <pre>
197 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
199  ___________
200  |         |
201 _|__    ___|___
202 |  |    |     |
203 +  1  __|___  4
204       |    |
205       *  __|___
206          |    |
207         _|__  2
208         |  |
209         /  6
210 </pre>
212 This computation should reduce to 13.  But given a specific reduction
213 strategy, we can watch the order in which the computation proceeds.
214 Following on the lambda evaluator developed during the previous
215 homework, let's adopt the following reduction strategy:
217     In order to reduce (head arg), do the following in order:
218     1. Reduce head to h'
219     2. Reduce arg to a'.
220     3. If (h' a') is a redex, reduce it.
222 There are many details left unspecified here, but this will be enough
223 for today.  The order in which the computation unfolds will be
225     1. Reduce head (+ 1) to itself
226     2. Reduce arg ((* (/ 6 2)) 3)
227          1. Reduce head (* ((/ 6) 2))
228               1. Reduce head *
229               2. Reduce arg ((/ 6) 2)
230                    1. Reduce head (/ 6) to itself
231                    2. Reduce arg 2 to itself
232                    3. Reduce ((/ 6) 2) to 3
233               3. Reduce (* 3) to itself
234          2. Reduce arg 4 to itself
235          3. Reduce ((* 3) 4) to 12
236      3. Reduce ((+ 1) 12) to 13
238 This reduction pattern follows the structure of the original
239 expression exactly, at each node moving first to the left branch,
240 processing the left branch, then moving to the right branch, and
241 finally processing the results of the two subcomputation.  (This is
242 called depth-first postorder traversal of the tree.)
244 It will be helpful to see how the types change as we make adjustments.
246     type num = int
247     type contents = Num of num   | Op of (num -> num -> num)
248     type tree = Leaf of contents | Branch of tree * tree
250 Never mind that these types will allow us to construct silly
251 arithmetric trees such as `+ *` or `2 3`.  Note that during the
252 reduction sequence, the result of reduction was in every case a
253 well-formed subtree.  So the process of reduction could be animated by
254 replacing subtrees with the result of reduction on that subtree, till
255 the entire tree is replaced by a single integer (namely, 13).
257 Now we replace the number 2 with 0:
259 <pre>
260 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
262  ___________
263  |         |
264 _|__    ___|___
265 |  |    |     |
266 +  1  __|___  4
267       |    |
268       *  __|___
269          |    |
270         _|__  0
271         |  |
272         /  6
273 </pre>
275 When we reduce, we get quite a ways into the computation before things
276 go south:
278     1. Reduce head (+ 1) to itself
279     2. Reduce arg ((* (/ 6 0)) 3)
280          1. Reduce head (* ((/ 6) 0))
281               1. Reduce head *
282               2. Reduce arg ((/ 6) 0)
283                    1. Reduce head (/ 6) to itself
284                    2. Reduce arg 0 to itself
285                    3. Reduce ((/ 6) 0) to ACKKKK
287 This is where we replace `/` with `safe-div`.  This means changing the
288 type of the arithmetic operators from `int -> int -> int` to
289 `int -> int -> int option`; and since we now have to anticipate the
290 possibility that any argument might involve division by zero inside of
291 it, here is the net result for our types:
293     type num = int option
294     type contents = Num of num   | Op of (num -> num -> num)
295     type tree = Leaf of contents | Branch of tree * tree
297 The only difference is that instead of defining our numbers to be
298 simple integers, they are now int options; and so Op is an operator
299 over int options.
301 At this point, we bring in the monadic machinery.  In particular, here
302 is the ⇧ and the map2 function from the notes on safe division:
304     ⇧ (a: 'a) = Just a;;
306     map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
307       match u with
308       | None -> None
309       | Some x ->
310           (match v with
311           | None -> None
312           | Some y -> Some (g x y));;
314 Then we lift the entire computation into the monad by applying ⇧ to
315 the integers, and by applying `map1` to the operators:
317 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
319      ___________________
320      |                 |
321   ___|____         ____|_____
322   |      |         |        |
323 map2 +  ⇧1    _____|_____  ⇧4
324               |         |
325             map2 *  ____|____
326                     |       |
327                  ___|____  ⇧0
328                  |      |
329                map2 /  ⇧6
331 With these adjustments, the faulty computation now completes smoothly:
333     1. Reduce head ((map2 +) ⇧1)
334     2. Reduce arg (((map2 *) (((map2 /) ⇧6) ⇧2)) ⇧3)
335          1. Reduce head ((map2 *) (((map2 /) ⇧6) ⇧2))
336               1. Reduce head *
337               2. Reduce arg (((map2 /) ⇧6) ⇧0)
338                    1. Reduce head ((map2 /) ⇧6)
339                    2. Reduce arg ⇧0
340                    3. Reduce (((map2 /) ⇧6) ⇧0) to Nothing
341               3. Reduce ((map2 *) Nothing) to Nothing
342          2. Reduce arg ⇧4
343          3. Reduce (((map2 *) Nothing) ⇧4) to Nothing
344      3. Reduce (((map2 +) ⇧1) Nothing) to Nothing
346 As soon as we try to divide by 0, safe-div returns Nothing.
347 Thanks to the details of map2, the fact that Nothing has been returned
348 by one of the arguments of a map2-ed operator guarantees that the
349 map2-ed operator will pass on the Nothing as its result.  So the
350 result of each enclosing computation will be Nothing, up to the root
351 of the tree.
353 It is unfortunate that we need to continue the computation after
354 encountering our first Nothing.  We know immediately at the result of
355 the entire computation will be Nothing, yet we continue to compute
356 subresults and combinations.  It would be more efficient to simply
357 jump to the top as soon as Nothing is encoutered.  Let's call that
358 strategy Abort.  We'll arrive at an Abort operator later in the semester.
360 So at this point, we can see how the Maybe/option monad provides
361 plumbing that allows subcomputations to send information from one part
362 of the computation to another.  In this case, the safe-div function
363 can send the information that division by zero has been attempted
364 throughout the rest of the computation.  If you think of the plumbing
365 as threaded through the tree in depth-first, postorder traversal, then
366 safe-div drops Nothing into the plumbing half way through the
367 computation, and that Nothing travels through the rest of the plumbing
368 till it comes out of the result faucet at the top of the tree.
370 ## Information flowing in the other direction: top to bottom
372 In the save-div example, a subcomputation created a message that
373 propagated upwards to the larger computation:
375 <pre>
376                  message: Division by zero occurred!
377                       ^
378  ___________          |
379  |         |          |
380 _|__    ___|___       |
381 |  |    |     |       |
382 +  1  __|___  4       |
383       |    |          |
384       *  __|___  -----|
385          |    |
386         _|__  0
387         |  |
388         /  6
389 </pre>
391 We might want to reverse the direction of information flow, making
392 information available at the top of the computation available to the
393 subcomputations:
395 <pre>
396                     [λx]
397  ___________          |
398  |         |          |
399 _|__    ___|___       |
400 |  |    |     |       |
401 +  1  __|___  4       |
402       |    |          |
403       *  __|___       |
404          |    |       |
405         _|__  x  <----|
406         |  |
407         /  6
408 </pre>
410 We've seen exactly this sort of configuration before: it's exactly
411 what we have when a lambda binds a variable that occurs in a deeply
412 embedded position.  Whatever the value of the argument that the lambda
413 form combines with, that is what will be substituted in for free
414 occurrences of that variable within the body of the lambda.
416 So our next step is to add a (primitive) version of binding to our
417 computation.  Rather than anticipating any number of binding
418 operators, we'll allow for just one binding dependency for now.
420 This example is independent of the safe-div example, so we'll return
421 to a situation in which the Maybe monad hasn't been added.  So the
422 types are the ones where numbers are just integers, not int options.
423 (In a couple of weeks, we'll start combining monads into a single
424 system; if you're impatient, you might think about how to do that now.)
426     type num = int
428 And the computation will be without the map2 or the ⇧ from the option
429 monad.
431 As you might guess, the technique we'll use to arrive at binding will
432 be to use the Reader monad, defined here in terms of m-identity and bind:
434     α --> int -> α
435     ⇧a = \x.a
436     u >>= f = \x.f(ux)x
437     map2 u v = \x.ux(vx)
439 A boxed type in this monad will be a function from an integer to an
440 object in the original type.  The unit function ⇧ lifts a value `a` to
441 a function that expects to receive an integer, but throws away the
442 integer and returns `a` instead (most values in the computation don't
443 depend on the input integer).
445 The bind function in this monad takes a monadic object `u`, a function
446 `f` lifting non-monadic objects into the monad, and returns a function
447 that expects an integer `x`.  It feeds `x` to `u`, which delivers a
448 result in the orginal type, which is fed in turn to `f`.  `f` returns
449 a monadic object, which upon being fed an integer, returns an object
450 of the orginal type.
452 The map2 function corresponding to this bind operation is given
453 above.  It should look familiar---we'll be commenting on this
454 familiarity in a moment.
456 Lifing the computation into the monad, we have the following adjusted
457 types:
459 type num = int -> int
461 That is, `num` is once again replaced with the type of a boxed int.
462 When we were dealing with the Maybe monad, a boxed int had type `int
463 option`.  In this monad, a boxed int has type `int -> int`.
465 <pre>
466 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
468      __________________
469      |                |
470   ___|____        ____|_____
471   |      |        |        |
472 map2 +  ⇧1    ____|_____  ⇧4
473               |        |
474             map2 *  ___|____
475                     |      |
476                  ___|____  x
477                  |      |
478                map2 /  ⇧6
479 </pre>
481 It remains only to decide how the variable `x` will access the value input
482 at the top of the tree.  Since the input value is supposed to be the
483 value put in place of the variable `x`.  Like every leaf in the tree
484 in argument position, the code we want in order to represent the
485 variable will have the type of a boxed int, namely, `int -> int`.  So
486 we have the following:
488     x (i:int):int = i
490 That is, variables in this system denote the indentity function!
492 The result of evaluating this tree will be a boxed integer: a function
493 from any integer `x` to `(+ 1 (* (/ 6 x)) 4)`.
495 Take a look at the definition of the reader monad again.  The
496 midentity takes some object `a` and returns `\x.a`.  In other words,
497 `⇧a = Ka`, so `⇧ = K`.  Likewise, `map2` for this monad is the `S`
498 combinator.  We've seen this before as a strategy for translating a
499 lambda abstract into a set of combinators.  Here is a part of the
500 general scheme for translating a lambda abstract into Combinatory
501 Logic.  The translation function `[.]` translates a lambda term into a
502 term in Combinatory Logic:
504     [(MN)] = ([M] [N])
505     [\a.a] = I
506     [\a.M] = K[M]       (assuming a not free in M)
507     [\a.(MN)] = S[\a.M][\a.N]
509 The reason we can make do with this subset of the full function is
510 that we're making the simplifying assumption that there is at most a
511 single lambda involved.  So here you see the I (the translation of the
512 bound variable), the K and the S.
515 ## Jacobson's Variable Free Semantics as a Reader Monad
517 We've designed the discussion so far to make the following claim as
518 easy to show as possible: Jacobson's Variable Free Semantics
519 (e.g., Jacobson 1999, [Towards a
520 Variable-Free
521 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
522 is a reader monad.
524 More specifically, it will turn out that Jacobson's geach combinator
525 *g* is exactly our `lift` operator, and her binding combinator *z* is
526 exactly our `bind` (though with the arguments reversed)!
528 Jacobson's system contains two main combinators, *g* and *z*.  She
529 calls *g* the Geach rule, and *z* performs binding.  Here is a typical
530 computation.  This implementation is based closely on email from Simon
531 Charlow, with beta reduction as performed by the on-line evaluator:
533 <pre>
534 ; Analysis of "Everyone_i thinks he_i left"
535 let g = \f g x. f (g x) in
536 let z = \f g x. f (g x) x in
537 let he = \x. x in
538 let everyone = \P. FORALL x (P x) in
540 everyone (z thinks (g left he))
542 ~~>  FORALL x (thinks (left x) x)
543 </pre>
545 Several things to notice: First, pronouns once again denote identity functions.
546 As Jeremy Kuhn has pointed out, this is related to the fact that in
547 the mapping from the lambda calculus into combinatory logic that we
548 discussed earlier in the course, bound variables translated to I, the
549 identity combinator (see additional comments below).  We'll return to
550 the idea of pronouns as identity functions in later discussions.
552 Second, *g* plays the role of transmitting a binding dependency for an
553 embedded constituent to a containing constituent.
555 Third, one of the peculiar aspects of Jacobson's system is that
556 binding is accomplished not by applying *z* to the element that will
557 (in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
558 rather by applying *z* instead to the predicate that will take
559 *everyone* as an argument, here, *thinks*.
561 The basic recipe in Jacobson's system, then, is that you transmit the
562 dependence of a pronoun upwards through the tree using *g* until just
563 before you are about to combine with the binder, when you finish off
564 with *z*.  (There are examples with longer chains of *g*'s below.)
566 Jacobson's *g* combinator is exactly our `lift` operator: it takes a
567 functor and lifts it into the monad.
568 Furthermore, Jacobson's *z* combinator, which is what she uses to
569 create binding links, is essentially identical to our reader-monad
570 `bind`!
572 <pre>
573 everyone (z thinks (g left he))
575 ~~> forall w (thinks (left w) w)
577 everyone (z thinks (g (t bill) (g said (g left he))))
579 ~~> forall w (thinks (said (left w) bill) w)
580 </pre>
582 (The `t` combinator is given by `t x = \xy.yx`; it handles situations
583 in which English word order places the argument (in this case, a
584 grammatical subject) before the predicate.)
586 So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
587 is exactly `bind` with the arguments reversed.  It appears that
588 Jacobson's variable-free semantics is essentially a Reader monad.
590 ## The Reader monad for intensionality
592 Now we'll look at using monads to do intensional function application.
593 This is just another application of the Reader monad, not a new monad.
594 In Shan (2001) [Monads for natural
595 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
596 making expressions sensitive to the world of evaluation is conceptually
597 the same thing as making use of the Reader monad.
598 This technique was beautifully re-invented
599 by Ben-Avi and Winter (2007) in their paper [A modular
600 approach to
601 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
602 though without explicitly using monads.
604 All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
605 To run it, download the file, start OCaml, and say
607         # #use "intensionality-monad.ml";;
609 Note the extra `#` attached to the directive `use`.
611 First, the familiar linguistic problem:
613        Bill left.
614            Cam left.
615            Ann believes [Bill left].
616            Ann believes [Cam left].
618 We want an analysis on which the first three sentences can be true at
619 the same time that the last sentence is false.  If sentences denoted
620 simple truth values or booleans, we have a problem: if the sentences
621 *Bill left* and *Cam left* are both true, they denote the same object,
622 and Ann's beliefs can't distinguish between them.
624 The traditional solution to the problem sketched above is to allow
625 sentences to denote a function from worlds to truth values, what
626 Montague called an intension.  So if `s` is the type of possible
627 worlds, we have the following situation:
630 <pre>
631 Extensional types              Intensional types       Examples
632 -------------------------------------------------------------------
634 S         t                    s->t                    John left
635 DP        e                    s->e                    John
636 VP        e->t                 (s->e)->s->t            left
637 Vt        e->e->t              (s->e)->(s->e)->s->t    saw
638 Vs        t->e->t              (s->t)->(s->e)->s->t    thought
639 </pre>
641 This system is modeled on the way Montague arranged his grammar.
642 There are significant simplifications compared to Montague: for
643 instance, determiner phrases are thought of here as corresponding to
644 individuals rather than to generalized quantifiers.
646 The main difference between the intensional types and the extensional
647 types is that in the intensional types, the arguments are functions
648 from worlds to extensions: intransitive verb phrases like "left" now
649 take so-called "individual concepts" as arguments (type s->e) rather than plain
650 individuals (type e), and attitude verbs like "think" now take
651 propositions (type s->t) rather than truth values (type t).
652 In addition, the result of each predicate is an intension.
653 This expresses the fact that the set of people who left in one world
654 may be different than the set of people who left in a different world.
656 Normally, the dependence of the extension of a predicate to the world
657 of evaluation is hidden inside of an evaluation coordinate, or built
658 into the the lexical meaning function, but we've made it explicit here
659 in the way that the intensionality monad makes most natural.
661 The intensional types are more complicated than the extensional
662 types.  Wouldn't it be nice to make the complicated types available
663 for those expressions like attitude verbs that need to worry about
664 intensions, and keep the rest of the grammar as extensional as
665 possible?  This desire is parallel to our earlier desire to limit the
666 concern about division by zero to the division function, and let the
667 other functions, like addition or multiplication, ignore
668 division-by-zero problems as much as possible.
670 So here's what we do:
672 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:
674         type s = int;;
675         type e = char;;
676         type t = bool;;
678         let ann = 'a';;
679         let bill = 'b';;
680         let cam = 'c';;
682         let left1 (x:e) = true;;
683         let saw1 (x:e) (y:e) = y < x;;
685         left1 ann;; (* true *)
686         saw1 bill ann;; (* true *)
687         saw1 ann bill;; (* false *)
689 So here's our extensional system: everyone left, including Ann;
690 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann.  (Note that the word
691 order we're using is VOS, verb-object-subject.)
693 Now we add intensions.  Because different people leave in different
694 worlds, the meaning of *leave* must depend on the world in which it is
695 being evaluated:
697     let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
698     left ann 1;; (* true: Ann left in world 1 *)
699     left cam 2;; (* false: Cam didn't leave in world 2 *)
701 This new definition says that everyone always left, except that
702 in world 2, Cam didn't leave.
704 Note that although this general *left* is sensitive to world of
705 evaluation, it does not have the fully intensionalized type given in
706 the chart above, which was `(s->e)->s->t`.  This is because
707 *left* does not exploit the additional resolving power provided by
708 making the subject an individual concept.  In semantics jargon, we say
709 that *leave* is extensional with respect to its first argument.
711 Therefore we will adopt the general strategy of defining predicates
712 in a way that they take arguments of the lowest type that will allow
713 us to make all the distinctions the predicate requires.  When it comes
714 time to combine this predicate with monadic arguments, we'll have to
715 make use of various lifting predicates.
717 Likewise, although *see* depends on the world of evaluation, it is
718 extensional in both of its syntactic arguments:
720     let saw x y w = (w < 2) && (y < x);;
721     saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
722     saw bill ann 2;; (* false: no one saw anyone in world 2 *)
724 This (again, partially) intensionalized version of *see* coincides
725 with the `saw1` function we defined above for world 1; in world 2, no
726 one saw anyone.
728 Just to keep things straight, let's review the facts:
730 <pre>
731      World 1: Everyone left.
732               Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
733      World 2: Ann left, Bill left, Cam didn't leave.
734               No one saw anyone.
735 </pre>
737 Now we are ready for the intensionality monad:
739 <pre>
740 type 'a intension = s -> 'a;;
741 let unit x = fun (w:s) -> x;;
742 (* as before, bind can be written more compactly, but having
743    it spelled out like this will be useful down the road *)
744 let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
745 </pre>
747 Then the individual concept `unit ann` is a rigid designator: a
748 constant function from worlds to individuals that returns `'a'` no
749 matter which world is used as an argument.  This is a typical kind of
750 thing for a monad unit to do.
752 Then combining a predicate like *left* which is extensional in its
753 subject argument with an intensional subject like `unit ann` is simply bind
754 in action:
756     bind (unit ann) left 1;; (* true: Ann left in world 1 *)
757     bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
759 As usual, bind takes a monad box containing Ann, extracts Ann, and
760 feeds her to the extensional *left*.  In linguistic terms, we take the
761 individual concept `unit ann`, apply it to the world of evaluation in
762 order to get hold of an individual (`'a'`), then feed that individual
763 to the extensional predicate *left*.
765 We can arrange for a transitive verb that is extensional in both of
766 its arguments to take intensional arguments:
768     let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
770 This is almost the same `lift2` predicate we defined in order to allow
771 addition in our division monad example.  The difference is that this
772 variant operates on verb meanings that take extensional arguments but
773 returns an intensional result.  Thus the original `lift2` predicate
774 has `unit (f x y)` where we have just `f x y` here.
776 The use of `bind` here to combine *left* with an individual concept,
777 and the use of `lift2'` to combine *see* with two intensional
778 arguments closely parallels the two of Montague's meaning postulates
779 (in PTQ) that express the relationship between extensional verbs and
780 their uses in intensional contexts.
782 <pre>
783 lift2' saw (unit bill) (unit ann) 1;;  (* true *)
784 lift2' saw (unit bill) (unit ann) 2;;  (* false *)
785 </pre>
787 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
789 Finally, we can define our intensional verb *thinks*.  *Think* is
790 intensional with respect to its sentential complement, though still extensional
791 with respect to its subject.  (As Montague noticed, almost all verbs
792 in English are extensional with respect to their subject; a possible
793 exception is "appear".)
795     let thinks (p:s->t) (x:e) (w:s) =
796       match (x, p 2) with ('a', false) -> false | _ -> p w;;
798 Ann disbelieves any proposition that is false in world 2.  Apparently,
799 she firmly believes we're in world 2.  Everyone else believes a
800 proposition iff that proposition is true in the world of evaluation.
802     bind (unit ann) (thinks (bind (unit bill) left)) 1;;
804 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
806     bind (unit ann) (thinks (bind (unit cam) left)) 1;;
808 But in world 1, Ann doesn't believe that Cam left (even though he
809 did leave in world 1: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
810 what is happening in world 2, where Cam doesn't leave.
812 *Small project*: add intersective ("red") and non-intersective
813  adjectives ("good") to the fragment.  The intersective adjectives
814  will be extensional with respect to the nominal they combine with
815  (using bind), and the non-intersective adjectives will take
816  intensional arguments.