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 <pre>
155 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
157      ___________________
158      |                 |
159   ___|____         ____|_____
160   |      |         |        |
161 map2 +  ⇧1    _____|_____  ⇧4
162               |         |
163             map2 *  ____|____
164                     |       |
165                  ___|____  ⇧0
166                  |      |
167                map2 /  ⇧6
168 </pre>
170 With these adjustments, the faulty computation now completes smoothly:
172     1. Reduce head ((map2 +)  -->
174 %%%
175 <pre>
176 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
178  ___________
179  |         |
180 _|__    ___|___
181 |  |    |     |
182 +  1  __|___  4
183       |    |
184       *  __|___
185          |    |
186         _|__  2
187         |  |
188         /  6
189 </pre>
191 This computation should reduce to 13.  But given a specific reduction
192 strategy, we can watch the order in which the computation proceeds.
193 Following on the lambda evaluator developed during the previous
194 homework, let's adopt the following reduction strategy:
196     In order to reduce (head arg), do the following in order:
197     1. Reduce head to h'
198     2. Reduce arg to a'.
199     3. If (h' a') is a redex, reduce it.
201 There are many details left unspecified here, but this will be enough
202 for today.  The order in which the computation unfolds will be
204     1. Reduce head (+ 1) to itself
205     2. Reduce arg ((* (/ 6 2)) 3)
206          1. Reduce head (* ((/ 6) 2))
208               2. Reduce arg ((/ 6) 2)
209                    1. Reduce head (/ 6) to itself
210                    2. Reduce arg 2 to itself
211                    3. Reduce ((/ 6) 2) to 3
212               3. Reduce (* 3) to itself
213          2. Reduce arg 4 to itself
214          3. Reduce ((* 3) 4) to 12
215      3. Reduce ((+ 1) 12) to 13
217 This reduction pattern follows the structure of the original
218 expression exactly, at each node moving first to the left branch,
219 processing the left branch, then moving to the right branch, and
220 finally processing the results of the two subcomputation.  (This is
221 called depth-first postorder traversal of the tree.)
223 It will be helpful to see how the types change as we make adjustments.
225     type num = int
226     type contents = Num of num   | Op of (num -> num -> num)
227     type tree = Leaf of contents | Branch of tree * tree
229 Never mind that these types will allow us to construct silly
230 arithmetric trees such as `+ *` or `2 3`.  Note that during the
231 reduction sequence, the result of reduction was in every case a
232 well-formed subtree.  So the process of reduction could be animated by
233 replacing subtrees with the result of reduction on that subtree, till
234 the entire tree is replaced by a single integer (namely, 13).
236 Now we replace the number 2 with 0:
238 <pre>
239 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
241  ___________
242  |         |
243 _|__    ___|___
244 |  |    |     |
245 +  1  __|___  4
246       |    |
247       *  __|___
248          |    |
249         _|__  0
250         |  |
251         /  6
252 </pre>
254 When we reduce, we get quite a ways into the computation before things
255 go south:
257     1. Reduce head (+ 1) to itself
258     2. Reduce arg ((* (/ 6 0)) 3)
259          1. Reduce head (* ((/ 6) 0))
261               2. Reduce arg ((/ 6) 0)
262                    1. Reduce head (/ 6) to itself
263                    2. Reduce arg 0 to itself
264                    3. Reduce ((/ 6) 0) to ACKKKK
266 This is where we replace `/` with `safe-div`.  This means changing the
267 type of the arithmetic operators from `int -> int -> int` to
268 `int -> int -> int option`; and since we now have to anticipate the
269 possibility that any argument might involve division by zero inside of
270 it, here is the net result for our types:
272     type num = int option
273     type contents = Num of num   | Op of (num -> num -> num)
274     type tree = Leaf of contents | Branch of tree * tree
276 The only difference is that instead of defining our numbers to be
277 simple integers, they are now int options; and so Op is an operator
278 over int options.
280 At this point, we bring in the monadic machinery.  In particular, here
281 is the ⇧ and the map2 function from the notes on safe division:
283     ⇧ (a: 'a) = Just a;;
285     map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
286       match u with
287       | None -> None
288       | Some x ->
289           (match v with
290           | None -> None
291           | Some y -> Some (g x y));;
293 Then we lift the entire computation into the monad by applying ⇧ to
294 the integers, and by applying `map1` to the operators:
296 <pre>
297 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
299      ___________________
300      |                 |
301   ___|____         ____|_____
302   |      |         |        |
303 map2 +  ⇧1    _____|_____  ⇧4
304               |         |
305             map2 *  ____|____
306                     |       |
307                  ___|____  ⇧0
308                  |      |
309                map2 /  ⇧6
310 </pre>
312 With these adjustments, the faulty computation now completes smoothly:
314     1. Reduce head ((map2 +) ⇧1)
315     2. Reduce arg (((map2 *) (((map2 /) ⇧6) ⇧2)) ⇧3)
316          1. Reduce head ((map2 *) (((map2 /) ⇧6) ⇧2))
318               2. Reduce arg (((map2 /) ⇧6) ⇧0)
319                    1. Reduce head ((map2 /) ⇧6)
320                    2. Reduce arg ⇧0
321                    3. Reduce (((map2 /) ⇧6) ⇧0) to Nothing
322               3. Reduce ((map2 *) Nothing) to Nothing
323          2. Reduce arg ⇧4
324          3. Reduce (((map2 *) Nothing) ⇧4) to Nothing
325      3. Reduce (((map2 +) ⇧1) Nothing) to Nothing
327 As soon as we try to divide by 0, safe-div returns Nothing.
328 Thanks to the details of map2, the fact that Nothing has been returned
329 by one of the arguments of a map2-ed operator guarantees that the
330 map2-ed operator will pass on the Nothing as its result.  So the
331 result of each enclosing computation will be Nothing, up to the root
332 of the tree.
334 It is unfortunate that we need to continue the computation after
335 encountering our first Nothing.  We know immediately at the result of
336 the entire computation will be Nothing, yet we continue to compute
337 subresults and combinations.  It would be more efficient to simply
338 jump to the top as soon as Nothing is encoutered.  Let's call that
339 strategy Abort.  We'll arrive at an Abort operator later in the semester.
341 So at this point, we can see how the Maybe/option monad provides
342 plumbing that allows subcomputations to send information from one part
343 of the computation to another.  In this case, the safe-div function
344 can send the information that division by zero has been attempted
345 throughout the rest of the computation.  If you think of the plumbing
346 as threaded through the tree in depth-first, postorder traversal, then
347 safe-div drops Nothing into the plumbing half way through the
348 computation, and that Nothing travels through the rest of the plumbing
349 till it comes out of the result faucet at the top of the tree.
351 ## Information flowing in the other direction: top to bottom
353 In the save-div example, a subcomputation created a message that
354 propagated upwards to the larger computation:
356 <pre>
357                  message: Division by zero occurred!
358                       ^
359  ___________          |
360  |         |          |
361 _|__    ___|___       |
362 |  |    |     |       |
363 +  1  __|___  4       |
364       |    |          |
365       *  __|___  -----|
366          |    |
367         _|__  0
368         |  |
369         /  6
370 </pre>
372 We might want to reverse the direction of information flow, making
373 information available at the top of the computation available to the
374 subcomputations:
376 <pre>
377                     [λx]
378  ___________          |
379  |         |          |
380 _|__    ___|___       |
381 |  |    |     |       |
382 +  1  __|___  4       |
383       |    |          |
384       *  __|___       |
385          |    |       |
386         _|__  x  <----|
387         |  |
388         /  6
389 </pre>
391 We've seen exactly this sort of configuration before: it's exactly
392 what we have when a lambda binds a variable that occurs in a deeply
393 embedded position.  Whatever the value of the argument that the lambda
394 form combines with, that is what will be substituted in for free
395 occurrences of that variable within the body of the lambda.
397 So our next step is to add a (primitive) version of binding to our
398 computation.  Rather than anticipating any number of binding
399 operators, we'll allow for just one binding dependency for now.
401 This example is independent of the safe-div example, so we'll return
402 to a situation in which the Maybe monad hasn't been added.  So the
403 types are the ones where numbers are just integers, not int options.
404 (In a couple of weeks, we'll start combining monads into a single
405 system; if you're impatient, you might think about how to do that now.)
407     type num = int
409 And the computation will be without the map2 or the ⇧ from the option
412 As you might guess, the technique we'll use to arrive at binding will
413 be to use the Reader monad, defined here in terms of m-identity and bind:
415     α --> int -> α
416     ⇧a = \x.a
417     u >>= f = \x.f(ux)x
418     map2 u v = \x.ux(vx)
420 A boxed type in this monad will be a function from an integer to an
421 object in the original type.  The unit function ⇧ lifts a value `a` to
422 a function that expects to receive an integer, but throws away the
423 integer and returns `a` instead (most values in the computation don't
424 depend on the input integer).
426 The bind function in this monad takes a monadic object `u`, a function
427 `f` lifting non-monadic objects into the monad, and returns a function
428 that expects an integer `x`.  It feeds `x` to `u`, which delivers a
429 result in the orginal type, which is fed in turn to `f`.  `f` returns
430 a monadic object, which upon being fed an integer, returns an object
431 of the orginal type.
433 The map2 function corresponding to this bind operation is given
434 above.  It should look familiar---we'll be commenting on this
435 familiarity in a moment.
437 Lifing the computation into the monad, we have the following adjusted
438 types:
440 type num = int -> int
442 That is, `num` is once again replaced with the type of a boxed int.
443 When we were dealing with the Maybe monad, a boxed int had type `int
444 option`.  In this monad, a boxed int has type `int -> int`.
446 <pre>
447 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
449      __________________
450      |                |
451   ___|____        ____|_____
452   |      |        |        |
453 map2 +  ⇧1    ____|_____  ⇧4
454               |        |
455             map2 *  ___|____
456                     |      |
457                  ___|____  x
458                  |      |
459                map2 /  ⇧6
460 </pre>
462 It remains only to decide how the variable `x` will access the value input
463 at the top of the tree.  Since the input value is supposed to be the
464 value put in place of the variable `x`.  Like every leaf in the tree
465 in argument position, the code we want in order to represent the
466 variable will have the type of a boxed int, namely, `int -> int`.  So
467 we have the following:
469     x (i:int):int = i
471 That is, variables in this system denote the indentity function!
473 The result of evaluating this tree will be a boxed integer: a function
474 from any integer `x` to `(+ 1 (* (/ 6 x)) 4)`.
476 Take a look at the definition of the reader monad again.  The
477 midentity takes some object `a` and returns `\x.a`.  In other words,
478 `⇧a = Ka`, so `⇧ = K`.  Likewise, `map2` for this monad is the `S`
479 combinator.  We've seen this before as a strategy for translating a
480 lambda abstract into a set of combinators.  Here is a part of the
481 general scheme for translating a lambda abstract into Combinatory
482 Logic.  The translation function `[.]` translates a lambda term into a
483 term in Combinatory Logic:
485     [(MN)] = ([M] [N])
486     [\a.a] = I
487     [\a.M] = K[M]       (assuming a not free in M)
488     [\a.(MN)] = S[\a.M][\a.N]
490 The reason we can make do with this subset of the full function is
491 that we're making the simplifying assumption that there is at most a
492 single lambda involved.  So here you see the I (the translation of the
493 bound variable), the K and the S.
498 We've designed the discussion so far to make the following claim as
499 easy to show as possible: Jacobson's Variable Free Semantics
500 (e.g., Jacobson 1999, [Towards a
501 Variable-Free
505 More specifically, it will turn out that Jacobson's geach combinator
506 *g* is exactly our `lift` operator, and her binding combinator *z* is
507 exactly our `bind` (though with the arguments reversed)!
509 Jacobson's system contains two main combinators, *g* and *z*.  She
510 calls *g* the Geach rule, and *z* performs binding.  Here is a typical
511 computation.  This implementation is based closely on email from Simon
512 Charlow, with beta reduction as performed by the on-line evaluator:
514 <pre>
515 ; Analysis of "Everyone_i thinks he_i left"
516 let g = \f g x. f (g x) in
517 let z = \f g x. f (g x) x in
518 let he = \x. x in
519 let everyone = \P. FORALL x (P x) in
521 everyone (z thinks (g left he))
523 ~~>  FORALL x (thinks (left x) x)
524 </pre>
526 Several things to notice: First, pronouns once again denote identity functions.
527 As Jeremy Kuhn has pointed out, this is related to the fact that in
528 the mapping from the lambda calculus into combinatory logic that we
529 discussed earlier in the course, bound variables translated to I, the
531 the idea of pronouns as identity functions in later discussions.
533 Second, *g* plays the role of transmitting a binding dependency for an
534 embedded constituent to a containing constituent.
536 Third, one of the peculiar aspects of Jacobson's system is that
537 binding is accomplished not by applying *z* to the element that will
538 (in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
539 rather by applying *z* instead to the predicate that will take
540 *everyone* as an argument, here, *thinks*.
542 The basic recipe in Jacobson's system, then, is that you transmit the
543 dependence of a pronoun upwards through the tree using *g* until just
544 before you are about to combine with the binder, when you finish off
545 with *z*.  (There are examples with longer chains of *g*'s below.)
547 Jacobson's *g* combinator is exactly our `lift` operator: it takes a
548 functor and lifts it into the monad.
549 Furthermore, Jacobson's *z* combinator, which is what she uses to
551 `bind`!
553 <pre>
554 everyone (z thinks (g left he))
556 ~~> forall w (thinks (left w) w)
558 everyone (z thinks (g (t bill) (g said (g left he))))
560 ~~> forall w (thinks (said (left w) bill) w)
561 </pre>
563 (The `t` combinator is given by `t x = \xy.yx`; it handles situations
564 in which English word order places the argument (in this case, a
565 grammatical subject) before the predicate.)
567 So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
568 is exactly `bind` with the arguments reversed.  It appears that
573 Now we'll look at using monads to do intensional function application.
575 In Shan (2001) [Monads for natural
576 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
577 making expressions sensitive to the world of evaluation is conceptually
579 This technique was beautifully re-invented
580 by Ben-Avi and Winter (2007) in their paper [A modular
581 approach to
582 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
583 though without explicitly using monads.
585 All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
590 Note the extra `#` attached to the directive `use`.
592 First, the familiar linguistic problem:
594        Bill left.
595            Cam left.
596            Ann believes [Bill left].
597            Ann believes [Cam left].
599 We want an analysis on which the first three sentences can be true at
600 the same time that the last sentence is false.  If sentences denoted
601 simple truth values or booleans, we have a problem: if the sentences
602 *Bill left* and *Cam left* are both true, they denote the same object,
603 and Ann's beliefs can't distinguish between them.
605 The traditional solution to the problem sketched above is to allow
606 sentences to denote a function from worlds to truth values, what
607 Montague called an intension.  So if `s` is the type of possible
608 worlds, we have the following situation:
611 <pre>
612 Extensional types              Intensional types       Examples
613 -------------------------------------------------------------------
615 S         t                    s->t                    John left
616 DP        e                    s->e                    John
617 VP        e->t                 (s->e)->s->t            left
618 Vt        e->e->t              (s->e)->(s->e)->s->t    saw
619 Vs        t->e->t              (s->t)->(s->e)->s->t    thought
620 </pre>
622 This system is modeled on the way Montague arranged his grammar.
623 There are significant simplifications compared to Montague: for
624 instance, determiner phrases are thought of here as corresponding to
625 individuals rather than to generalized quantifiers.
627 The main difference between the intensional types and the extensional
628 types is that in the intensional types, the arguments are functions
629 from worlds to extensions: intransitive verb phrases like "left" now
630 take so-called "individual concepts" as arguments (type s->e) rather than plain
631 individuals (type e), and attitude verbs like "think" now take
632 propositions (type s->t) rather than truth values (type t).
633 In addition, the result of each predicate is an intension.
634 This expresses the fact that the set of people who left in one world
635 may be different than the set of people who left in a different world.
637 Normally, the dependence of the extension of a predicate to the world
638 of evaluation is hidden inside of an evaluation coordinate, or built
639 into the the lexical meaning function, but we've made it explicit here
640 in the way that the intensionality monad makes most natural.
642 The intensional types are more complicated than the extensional
643 types.  Wouldn't it be nice to make the complicated types available
644 for those expressions like attitude verbs that need to worry about
645 intensions, and keep the rest of the grammar as extensional as
646 possible?  This desire is parallel to our earlier desire to limit the
647 concern about division by zero to the division function, and let the
648 other functions, like addition or multiplication, ignore
649 division-by-zero problems as much as possible.
651 So here's what we do:
653 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:
655         type s = int;;
656         type e = char;;
657         type t = bool;;
659         let ann = 'a';;
660         let bill = 'b';;
661         let cam = 'c';;
663         let left1 (x:e) = true;;
664         let saw1 (x:e) (y:e) = y < x;;
666         left1 ann;; (* true *)
667         saw1 bill ann;; (* true *)
668         saw1 ann bill;; (* false *)
670 So here's our extensional system: everyone left, including Ann;
671 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann.  (Note that the word
672 order we're using is VOS, verb-object-subject.)
674 Now we add intensions.  Because different people leave in different
675 worlds, the meaning of *leave* must depend on the world in which it is
676 being evaluated:
678     let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
679     left ann 1;; (* true: Ann left in world 1 *)
680     left cam 2;; (* false: Cam didn't leave in world 2 *)
682 This new definition says that everyone always left, except that
683 in world 2, Cam didn't leave.
685 Note that although this general *left* is sensitive to world of
686 evaluation, it does not have the fully intensionalized type given in
687 the chart above, which was `(s->e)->s->t`.  This is because
688 *left* does not exploit the additional resolving power provided by
689 making the subject an individual concept.  In semantics jargon, we say
690 that *leave* is extensional with respect to its first argument.
692 Therefore we will adopt the general strategy of defining predicates
693 in a way that they take arguments of the lowest type that will allow
694 us to make all the distinctions the predicate requires.  When it comes
695 time to combine this predicate with monadic arguments, we'll have to
696 make use of various lifting predicates.
698 Likewise, although *see* depends on the world of evaluation, it is
699 extensional in both of its syntactic arguments:
701     let saw x y w = (w < 2) && (y < x);;
702     saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
703     saw bill ann 2;; (* false: no one saw anyone in world 2 *)
705 This (again, partially) intensionalized version of *see* coincides
706 with the `saw1` function we defined above for world 1; in world 2, no
707 one saw anyone.
709 Just to keep things straight, let's review the facts:
711 <pre>
712      World 1: Everyone left.
713               Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
714      World 2: Ann left, Bill left, Cam didn't leave.
715               No one saw anyone.
716 </pre>
720 <pre>
721 type 'a intension = s -> 'a;;
722 let unit x = fun (w:s) -> x;;
723 (* as before, bind can be written more compactly, but having
724    it spelled out like this will be useful down the road *)
725 let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
726 </pre>
728 Then the individual concept `unit ann` is a rigid designator: a
729 constant function from worlds to individuals that returns `'a'` no
730 matter which world is used as an argument.  This is a typical kind of
731 thing for a monad unit to do.
733 Then combining a predicate like *left* which is extensional in its
734 subject argument with an intensional subject like `unit ann` is simply bind
735 in action:
737     bind (unit ann) left 1;; (* true: Ann left in world 1 *)
738     bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
740 As usual, bind takes a monad box containing Ann, extracts Ann, and
741 feeds her to the extensional *left*.  In linguistic terms, we take the
742 individual concept `unit ann`, apply it to the world of evaluation in
743 order to get hold of an individual (`'a'`), then feed that individual
744 to the extensional predicate *left*.
746 We can arrange for a transitive verb that is extensional in both of
747 its arguments to take intensional arguments:
749     let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
751 This is almost the same `lift2` predicate we defined in order to allow
752 addition in our division monad example.  The difference is that this
753 variant operates on verb meanings that take extensional arguments but
754 returns an intensional result.  Thus the original `lift2` predicate
755 has `unit (f x y)` where we have just `f x y` here.
757 The use of `bind` here to combine *left* with an individual concept,
758 and the use of `lift2'` to combine *see* with two intensional
759 arguments closely parallels the two of Montague's meaning postulates
760 (in PTQ) that express the relationship between extensional verbs and
761 their uses in intensional contexts.
763 <pre>
764 lift2' saw (unit bill) (unit ann) 1;;  (* true *)
765 lift2' saw (unit bill) (unit ann) 2;;  (* false *)
766 </pre>
768 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
770 Finally, we can define our intensional verb *thinks*.  *Think* is
771 intensional with respect to its sentential complement, though still extensional
772 with respect to its subject.  (As Montague noticed, almost all verbs
773 in English are extensional with respect to their subject; a possible
774 exception is "appear".)
776     let thinks (p:s->t) (x:e) (w:s) =
777       match (x, p 2) with ('a', false) -> false | _ -> p w;;
779 Ann disbelieves any proposition that is false in world 2.  Apparently,
780 she firmly believes we're in world 2.  Everyone else believes a
781 proposition iff that proposition is true in the world of evaluation.
783     bind (unit ann) (thinks (bind (unit bill) left)) 1;;
785 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
787     bind (unit ann) (thinks (bind (unit cam) left)) 1;;
789 But in world 1, Ann doesn't believe that Cam left (even though he
790 did leave in world 1: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
791 what is happening in world 2, where Cam doesn't leave.
793 *Small project*: add intersective ("red") and non-intersective