86866db235e17782d11f4c8780519683a58352f5
1 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ¢ ⇧ -->
3 [[!toc levels=2]]
5 The Reader Monad
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
14 monads: the identity monad (invisible boxes), the Maybe monad (option
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
27 by the monad.
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))
65               1. Reduce head *
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))
118               1. Reduce head *
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 The Reader Monad
175 ================
177 The goal for this part is to introduce the Reader Monad, and present
178 two linguistics applications: binding and intensionality.  Along the
179 way, we'll continue to think through issues related to order, and a
180 related notion of flow of information.
182 At this point, we've seen monads in general, and three examples of
183 monads: the identity monad (invisible boxes), the Maybe monad (option
184 types), and the List monad.
186 We've also seen an application of the Maybe monad to safe division.
187 The starting point was to allow the division function to return an int
188 option instead of an int.  If we divide 6 by 2, we get the answer Just
189 3.  But if we divide 6 by 0, we get the answer Nothing.
191 The next step was to adjust the other arithmetic functions to know how
192 to handle receiving Nothing instead of a (boxed) integer.  This meant
193 changing the type of their input from ints to int options.  But we
194 didn't need to do this piecemeal; rather, we could "lift" the ordinary
195 arithmetic operations into the monad using the various tools provided
196 by the monad.
198 So let's see how this works in terms of a specific computation.
200 <pre>
201 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
203  ___________
204  |         |
205 _|__    ___|___
206 |  |    |     |
207 +  1  __|___  4
208       |    |
209       *  __|___
210          |    |
211         _|__  2
212         |  |
213         /  6
214 </pre>
216 This computation should reduce to 13.  But given a specific reduction
217 strategy, we can watch the order in which the computation proceeds.
218 Following on the lambda evaluator developed during the previous
219 homework, let's adopt the following reduction strategy:
221     In order to reduce (head arg), do the following in order:
222     1. Reduce head to h'
223     2. Reduce arg to a'.
224     3. If (h' a') is a redex, reduce it.
226 There are many details left unspecified here, but this will be enough
227 for today.  The order in which the computation unfolds will be
229     1. Reduce head (+ 1) to itself
230     2. Reduce arg ((* (/ 6 2)) 3)
231          1. Reduce head (* ((/ 6) 2))
232               1. Reduce head *
233               2. Reduce arg ((/ 6) 2)
234                    1. Reduce head (/ 6) to itself
235                    2. Reduce arg 2 to itself
236                    3. Reduce ((/ 6) 2) to 3
237               3. Reduce (* 3) to itself
238          2. Reduce arg 4 to itself
239          3. Reduce ((* 3) 4) to 12
240      3. Reduce ((+ 1) 12) to 13
242 This reduction pattern follows the structure of the original
243 expression exactly, at each node moving first to the left branch,
244 processing the left branch, then moving to the right branch, and
245 finally processing the results of the two subcomputation.  (This is
246 called depth-first postorder traversal of the tree.)
248 It will be helpful to see how the types change as we make adjustments.
250     type num = int
251     type contents = Num of num   | Op of (num -> num -> num)
252     type tree = Leaf of contents | Branch of tree * tree
254 Never mind that these types will allow us to construct silly
255 arithmetric trees such as `+ *` or `2 3`.  Note that during the
256 reduction sequence, the result of reduction was in every case a
257 well-formed subtree.  So the process of reduction could be animated by
258 replacing subtrees with the result of reduction on that subtree, till
259 the entire tree is replaced by a single integer (namely, 13).
261 Now we replace the number 2 with 0:
263 <pre>
264 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
266  ___________
267  |         |
268 _|__    ___|___
269 |  |    |     |
270 +  1  __|___  4
271       |    |
272       *  __|___
273          |    |
274         _|__  0
275         |  |
276         /  6
277 </pre>
279 When we reduce, we get quite a ways into the computation before things
280 go south:
282     1. Reduce head (+ 1) to itself
283     2. Reduce arg ((* (/ 6 0)) 3)
284          1. Reduce head (* ((/ 6) 0))
285               1. Reduce head *
286               2. Reduce arg ((/ 6) 0)
287                    1. Reduce head (/ 6) to itself
288                    2. Reduce arg 0 to itself
289                    3. Reduce ((/ 6) 0) to ACKKKK
291 This is where we replace `/` with `safe-div`.  This means changing the
292 type of the arithmetic operators from `int -> int -> int` to
293 `int -> int -> int option`; and since we now have to anticipate the
294 possibility that any argument might involve division by zero inside of
295 it, here is the net result for our types:
297     type num = int option
298     type contents = Num of num   | Op of (num -> num -> num)
299     type tree = Leaf of contents | Branch of tree * tree
301 The only difference is that instead of defining our numbers to be
302 simple integers, they are now int options; and so Op is an operator
303 over int options.
305 At this point, we bring in the monadic machinery.  In particular, here
306 is the ⇧ and the map2 function from the notes on safe division:
308     ⇧ (a: 'a) = Just a;;
310     map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
311       match u with
312       | None -> None
313       | Some x ->
314           (match v with
315           | None -> None
316           | Some y -> Some (g x y));;
318 Then we lift the entire computation into the monad by applying ⇧ to
319 the integers, and by applying `map1` to the operators:
321 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
323      ___________________
324      |                 |
325   ___|____         ____|_____
326   |      |         |        |
327 map2 +  ⇧1    _____|_____  ⇧4
328               |         |
329             map2 *  ____|____
330                     |       |
331                  ___|____  ⇧0
332                  |      |
333                map2 /  ⇧6
335 With these adjustments, the faulty computation now completes smoothly:
337     1. Reduce head ((map2 +) ⇧1)
338     2. Reduce arg (((map2 *) (((map2 /) ⇧6) ⇧2)) ⇧3)
339          1. Reduce head ((map2 *) (((map2 /) ⇧6) ⇧2))
340               1. Reduce head *
341               2. Reduce arg (((map2 /) ⇧6) ⇧0)
342                    1. Reduce head ((map2 /) ⇧6)
343                    2. Reduce arg ⇧0
344                    3. Reduce (((map2 /) ⇧6) ⇧0) to Nothing
345               3. Reduce ((map2 *) Nothing) to Nothing
346          2. Reduce arg ⇧4
347          3. Reduce (((map2 *) Nothing) ⇧4) to Nothing
348      3. Reduce (((map2 +) ⇧1) Nothing) to Nothing
350 As soon as we try to divide by 0, safe-div returns Nothing.
351 Thanks to the details of map2, the fact that Nothing has been returned
352 by one of the arguments of a map2-ed operator guarantees that the
353 map2-ed operator will pass on the Nothing as its result.  So the
354 result of each enclosing computation will be Nothing, up to the root
355 of the tree.
357 It is unfortunate that we need to continue the computation after
358 encountering our first Nothing.  We know immediately at the result of
359 the entire computation will be Nothing, yet we continue to compute
360 subresults and combinations.  It would be more efficient to simply
361 jump to the top as soon as Nothing is encoutered.  Let's call that
362 strategy Abort.  We'll arrive at an Abort operator later in the semester.
364 So at this point, we can see how the Maybe/option monad provides
365 plumbing that allows subcomputations to send information from one part
366 of the computation to another.  In this case, the safe-div function
367 can send the information that division by zero has been attempted
368 throughout the rest of the computation.  If you think of the plumbing
369 as threaded through the tree in depth-first, postorder traversal, then
370 safe-div drops Nothing into the plumbing half way through the
371 computation, and that Nothing travels through the rest of the plumbing
372 till it comes out of the result faucet at the top of the tree.
374 ## Information flowing in the other direction: top to bottom
376 In the save-div example, a subcomputation created a message that
377 propagated upwards to the larger computation:
379 <pre>
380                  message: Division by zero occurred!
381                       ^
382  ___________          |
383  |         |          |
384 _|__    ___|___       |
385 |  |    |     |       |
386 +  1  __|___  4       |
387       |    |          |
388       *  __|___  -----|
389          |    |
390         _|__  0
391         |  |
392         /  6
393 </pre>
395 We might want to reverse the direction of information flow, making
396 information available at the top of the computation available to the
397 subcomputations:
399 <pre>
400                     [λx]
401  ___________          |
402  |         |          |
403 _|__    ___|___       |
404 |  |    |     |       |
405 +  1  __|___  4       |
406       |    |          |
407       *  __|___       |
408          |    |       |
409         _|__  x  <----|
410         |  |
411         /  6
412 </pre>
414 We've seen exactly this sort of configuration before: it's exactly
415 what we have when a lambda binds a variable that occurs in a deeply
416 embedded position.  Whatever the value of the argument that the lambda
417 form combines with, that is what will be substituted in for free
418 occurrences of that variable within the body of the lambda.
420 So our next step is to add a (primitive) version of binding to our
421 computation.  Rather than anticipating any number of binding
422 operators, we'll allow for just one binding dependency for now.
424 This example is independent of the safe-div example, so we'll return
425 to a situation in which the Maybe monad hasn't been added.  So the
426 types are the ones where numbers are just integers, not int options.
427 (In a couple of weeks, we'll start combining monads into a single
428 system; if you're impatient, you might think about how to do that now.)
430     type num = int
432 And the computation will be without the map2 or the ⇧ from the option
433 monad.
435 As you might guess, the technique we'll use to arrive at binding will
436 be to use the Reader monad, defined here in terms of m-identity and bind:
438     α --> int -> α
439     ⇧a = \x.a
440     u >>= f = \x.f(ux)x
441     map2 u v = \x.ux(vx)
443 A boxed type in this monad will be a function from an integer to an
444 object in the original type.  The unit function ⇧ lifts a value `a` to
445 a function that expects to receive an integer, but throws away the
446 integer and returns `a` instead (most values in the computation don't
447 depend on the input integer).
449 The bind function in this monad takes a monadic object `u`, a function
450 `f` lifting non-monadic objects into the monad, and returns a function
451 that expects an integer `x`.  It feeds `x` to `u`, which delivers a
452 result in the orginal type, which is fed in turn to `f`.  `f` returns
453 a monadic object, which upon being fed an integer, returns an object
454 of the orginal type.
456 The map2 function corresponding to this bind operation is given
457 above.  It should look familiar---we'll be commenting on this
458 familiarity in a moment.
460 Lifing the computation into the monad, we have the following adjusted
461 types:
463 type num = int -> int
465 That is, `num` is once again replaced with the type of a boxed int.
466 When we were dealing with the Maybe monad, a boxed int had type `int
467 option`.  In this monad, a boxed int has type `int -> int`.
469 <pre>
470 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
472      __________________
473      |                |
474   ___|____        ____|_____
475   |      |        |        |
476 map2 +  ⇧1    ____|_____  ⇧4
477               |        |
478             map2 *  ___|____
479                     |      |
480                  ___|____  x
481                  |      |
482                map2 /  ⇧6
483 </pre>
485 It remains only to decide how the variable `x` will access the value input
486 at the top of the tree.  Since the input value is supposed to be the
487 value put in place of the variable `x`.  Like every leaf in the tree
488 in argument position, the code we want in order to represent the
489 variable will have the type of a boxed int, namely, `int -> int`.  So
490 we have the following:
492     x (i:int):int = i
494 That is, variables in this system denote the indentity function!
496 The result of evaluating this tree will be a boxed integer: a function
497 from any integer `x` to `(+ 1 (* (/ 6 x)) 4)`.
499 Take a look at the definition of the reader monad again.  The
500 midentity takes some object `a` and returns `\x.a`.  In other words,
501 `⇧a = Ka`, so `⇧ = K`.  Likewise, `map2` for this monad is the `S`
502 combinator.  We've seen this before as a strategy for translating a
503 lambda abstract into a set of combinators.  Here is a part of the
504 general scheme for translating a lambda abstract into Combinatory
505 Logic.  The translation function `[.]` translates a lambda term into a
506 term in Combinatory Logic:
508     [(MN)] = ([M] [N])
509     [\a.a] = I
510     [\a.M] = K[M]       (assuming a not free in M)
511     [\a.(MN)] = S[\a.M][\a.N]
513 The reason we can make do with this subset of the full function is
514 that we're making the simplifying assumption that there is at most a
515 single lambda involved.  So here you see the I (the translation of the
516 bound variable), the K and the S.
519 ## Jacobson's Variable Free Semantics as a Reader Monad
521 We've designed the discussion so far to make the following claim as
522 easy to show as possible: Jacobson's Variable Free Semantics
523 (e.g., Jacobson 1999, [Towards a
524 Variable-Free
525 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
526 is a reader monad.
528 More specifically, it will turn out that Jacobson's geach combinator
529 *g* is exactly our `lift` operator, and her binding combinator *z* is
530 exactly our `bind` (though with the arguments reversed)!
532 Jacobson's system contains two main combinators, *g* and *z*.  She
533 calls *g* the Geach rule, and *z* performs binding.  Here is a typical
534 computation.  This implementation is based closely on email from Simon
535 Charlow, with beta reduction as performed by the on-line evaluator:
537 <pre>
538 ; Analysis of "Everyone_i thinks he_i left"
539 let g = \f g x. f (g x) in
540 let z = \f g x. f (g x) x in
541 let he = \x. x in
542 let everyone = \P. FORALL x (P x) in
544 everyone (z thinks (g left he))
546 ~~>  FORALL x (thinks (left x) x)
547 </pre>
549 Several things to notice: First, pronouns once again denote identity functions.
550 As Jeremy Kuhn has pointed out, this is related to the fact that in
551 the mapping from the lambda calculus into combinatory logic that we
552 discussed earlier in the course, bound variables translated to I, the
553 identity combinator (see additional comments below).  We'll return to
554 the idea of pronouns as identity functions in later discussions.
556 Second, *g* plays the role of transmitting a binding dependency for an
557 embedded constituent to a containing constituent.
559 Third, one of the peculiar aspects of Jacobson's system is that
560 binding is accomplished not by applying *z* to the element that will
561 (in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
562 rather by applying *z* instead to the predicate that will take
563 *everyone* as an argument, here, *thinks*.
565 The basic recipe in Jacobson's system, then, is that you transmit the
566 dependence of a pronoun upwards through the tree using *g* until just
567 before you are about to combine with the binder, when you finish off
568 with *z*.  (There are examples with longer chains of *g*'s below.)
570 Jacobson's *g* combinator is exactly our `lift` operator: it takes a
571 functor and lifts it into the monad.
572 Furthermore, Jacobson's *z* combinator, which is what she uses to
573 create binding links, is essentially identical to our reader-monad
574 `bind`!
576 <pre>
577 everyone (z thinks (g left he))
579 ~~> forall w (thinks (left w) w)
581 everyone (z thinks (g (t bill) (g said (g left he))))
583 ~~> forall w (thinks (said (left w) bill) w)
584 </pre>
586 (The `t` combinator is given by `t x = \xy.yx`; it handles situations
587 in which English word order places the argument (in this case, a
588 grammatical subject) before the predicate.)
590 So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
591 is exactly `bind` with the arguments reversed.  It appears that
592 Jacobson's variable-free semantics is essentially a Reader monad.
594 ## The Reader monad for intensionality
596 Now we'll look at using monads to do intensional function application.
597 This is just another application of the Reader monad, not a new monad.
598 In Shan (2001) [Monads for natural
599 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
600 making expressions sensitive to the world of evaluation is conceptually
601 the same thing as making use of the Reader monad.
602 This technique was beautifully re-invented
603 by Ben-Avi and Winter (2007) in their paper [A modular
604 approach to
605 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
606 though without explicitly using monads.
608 All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
609 To run it, download the file, start OCaml, and say
611         # #use "intensionality-monad.ml";;
613 Note the extra `#` attached to the directive `use`.
615 First, the familiar linguistic problem:
617        Bill left.
618            Cam left.
619            Ann believes [Bill left].
620            Ann believes [Cam left].
622 We want an analysis on which the first three sentences can be true at
623 the same time that the last sentence is false.  If sentences denoted
624 simple truth values or booleans, we have a problem: if the sentences
625 *Bill left* and *Cam left* are both true, they denote the same object,
626 and Ann's beliefs can't distinguish between them.
628 The traditional solution to the problem sketched above is to allow
629 sentences to denote a function from worlds to truth values, what
630 Montague called an intension.  So if `s` is the type of possible
631 worlds, we have the following situation:
634 <pre>
635 Extensional types              Intensional types       Examples
636 -------------------------------------------------------------------
638 S         t                    s->t                    John left
639 DP        e                    s->e                    John
640 VP        e->t                 (s->e)->s->t            left
641 Vt        e->e->t              (s->e)->(s->e)->s->t    saw
642 Vs        t->e->t              (s->t)->(s->e)->s->t    thought
643 </pre>
645 This system is modeled on the way Montague arranged his grammar.
646 There are significant simplifications compared to Montague: for
647 instance, determiner phrases are thought of here as corresponding to
648 individuals rather than to generalized quantifiers.
650 The main difference between the intensional types and the extensional
651 types is that in the intensional types, the arguments are functions
652 from worlds to extensions: intransitive verb phrases like "left" now
653 take so-called "individual concepts" as arguments (type s->e) rather than plain
654 individuals (type e), and attitude verbs like "think" now take
655 propositions (type s->t) rather than truth values (type t).
656 In addition, the result of each predicate is an intension.
657 This expresses the fact that the set of people who left in one world
658 may be different than the set of people who left in a different world.
660 Normally, the dependence of the extension of a predicate to the world
661 of evaluation is hidden inside of an evaluation coordinate, or built
662 into the the lexical meaning function, but we've made it explicit here
663 in the way that the intensionality monad makes most natural.
665 The intensional types are more complicated than the extensional
666 types.  Wouldn't it be nice to make the complicated types available
667 for those expressions like attitude verbs that need to worry about
668 intensions, and keep the rest of the grammar as extensional as
669 possible?  This desire is parallel to our earlier desire to limit the
670 concern about division by zero to the division function, and let the
671 other functions, like addition or multiplication, ignore
672 division-by-zero problems as much as possible.
674 So here's what we do:
676 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:
678         type s = int;;
679         type e = char;;
680         type t = bool;;
682         let ann = 'a';;
683         let bill = 'b';;
684         let cam = 'c';;
686         let left1 (x:e) = true;;
687         let saw1 (x:e) (y:e) = y < x;;
689         left1 ann;; (* true *)
690         saw1 bill ann;; (* true *)
691         saw1 ann bill;; (* false *)
693 So here's our extensional system: everyone left, including Ann;
694 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann.  (Note that the word
695 order we're using is VOS, verb-object-subject.)
697 Now we add intensions.  Because different people leave in different
698 worlds, the meaning of *leave* must depend on the world in which it is
699 being evaluated:
701     let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
702     left ann 1;; (* true: Ann left in world 1 *)
703     left cam 2;; (* false: Cam didn't leave in world 2 *)
705 This new definition says that everyone always left, except that
706 in world 2, Cam didn't leave.
708 Note that although this general *left* is sensitive to world of
709 evaluation, it does not have the fully intensionalized type given in
710 the chart above, which was `(s->e)->s->t`.  This is because
711 *left* does not exploit the additional resolving power provided by
712 making the subject an individual concept.  In semantics jargon, we say
713 that *leave* is extensional with respect to its first argument.
715 Therefore we will adopt the general strategy of defining predicates
716 in a way that they take arguments of the lowest type that will allow
717 us to make all the distinctions the predicate requires.  When it comes
718 time to combine this predicate with monadic arguments, we'll have to
719 make use of various lifting predicates.
721 Likewise, although *see* depends on the world of evaluation, it is
722 extensional in both of its syntactic arguments:
724     let saw x y w = (w < 2) && (y < x);;
725     saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
726     saw bill ann 2;; (* false: no one saw anyone in world 2 *)
728 This (again, partially) intensionalized version of *see* coincides
729 with the `saw1` function we defined above for world 1; in world 2, no
730 one saw anyone.
732 Just to keep things straight, let's review the facts:
734 <pre>
735      World 1: Everyone left.
736               Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
737      World 2: Ann left, Bill left, Cam didn't leave.
738               No one saw anyone.
739 </pre>
741 Now we are ready for the intensionality monad:
743 <pre>
744 type 'a intension = s -> 'a;;
745 let unit x = fun (w:s) -> x;;
746 (* as before, bind can be written more compactly, but having
747    it spelled out like this will be useful down the road *)
748 let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
749 </pre>
751 Then the individual concept `unit ann` is a rigid designator: a
752 constant function from worlds to individuals that returns `'a'` no
753 matter which world is used as an argument.  This is a typical kind of
754 thing for a monad unit to do.
756 Then combining a predicate like *left* which is extensional in its
757 subject argument with an intensional subject like `unit ann` is simply bind
758 in action:
760     bind (unit ann) left 1;; (* true: Ann left in world 1 *)
761     bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
763 As usual, bind takes a monad box containing Ann, extracts Ann, and
764 feeds her to the extensional *left*.  In linguistic terms, we take the
765 individual concept `unit ann`, apply it to the world of evaluation in
766 order to get hold of an individual (`'a'`), then feed that individual
767 to the extensional predicate *left*.
769 We can arrange for a transitive verb that is extensional in both of
770 its arguments to take intensional arguments:
772     let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
774 This is almost the same `lift2` predicate we defined in order to allow
775 addition in our division monad example.  The difference is that this
776 variant operates on verb meanings that take extensional arguments but
777 returns an intensional result.  Thus the original `lift2` predicate
778 has `unit (f x y)` where we have just `f x y` here.
780 The use of `bind` here to combine *left* with an individual concept,
781 and the use of `lift2'` to combine *see* with two intensional
782 arguments closely parallels the two of Montague's meaning postulates
783 (in PTQ) that express the relationship between extensional verbs and
784 their uses in intensional contexts.
786 <pre>
787 lift2' saw (unit bill) (unit ann) 1;;  (* true *)
788 lift2' saw (unit bill) (unit ann) 2;;  (* false *)
789 </pre>
791 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
793 Finally, we can define our intensional verb *thinks*.  *Think* is
794 intensional with respect to its sentential complement, though still extensional
795 with respect to its subject.  (As Montague noticed, almost all verbs
796 in English are extensional with respect to their subject; a possible
797 exception is "appear".)
799     let thinks (p:s->t) (x:e) (w:s) =
800       match (x, p 2) with ('a', false) -> false | _ -> p w;;
802 Ann disbelieves any proposition that is false in world 2.  Apparently,
803 she firmly believes we're in world 2.  Everyone else believes a
804 proposition iff that proposition is true in the world of evaluation.
806     bind (unit ann) (thinks (bind (unit bill) left)) 1;;
808 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
810     bind (unit ann) (thinks (bind (unit cam) left)) 1;;
812 But in world 1, Ann doesn't believe that Cam left (even though he
813 did leave in world 1: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
814 what is happening in world 2, where Cam doesn't leave.
816 *Small project*: add intersective ("red") and non-intersective
817  adjectives ("good") to the fragment.  The intersective adjectives
818  will be extensional with respect to the nominal they combine with
819  (using bind), and the non-intersective adjectives will take
820  intensional arguments.