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