some rewrites, not finished
[lambda.git] / topics / week8_reader_monad.mdwn
1 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
2
3
4 [[!toc levels=2]]
5
6 The goal for these notes is to introduce the Reader Monad, and present
7 two linguistic applications: binding and intensionality. Along the
8 way, we'll continue to think through issues related to order, and a
9 related notion of flow of information.
10
11 At this point, we've seen monads in general, and three examples of
12 monads: the Identity monad (invisible boxes), the Option/Maybe monad (option
13 types), and the List monad.
14
15 We've also seen an application of the Option/Maybe monad to safe division.
16 The starting point was to allow the division function to return an `int
17 option` instead of an `int`. If we divide `6` by `2`, we get the answer `Some
18 3`. But if we divide `6` by `0`, we get the answer `None`.
19
20 The next step was to adjust the other arithmetic functions to teach
21 them what to do if they received `None` instead of a boxed integer.
22 This meant changing the type of their input from `int`s to `int option`s.
23 But we didn't need to do this piecemeal; rather, we "lift"ed the
24 ordinary arithmetic operations into the monad using the various tools
25 provided by the monad.
26
27 We'll go over this lifting operation in detail in the next section.
28
29 ## Tracing the effect of `safe_div` on a larger computation
30
31 So let's see how this works in terms of a specific computation.
32
33 <!--
34 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
35 -->
36 <pre>
37 (+ 1 (* (/ 6 2) 4)) in tree format:
38
39  ___________
40  |         |
41 _|__    ___|___
42 |  |    |     |
43 +  1  __|___  4
44       |    |
45       *  __|___
46          |    |
47         _|__  2
48         |  |
49         /  6
50 </pre>
51
52 No matter what order we evaluate it in, this computation
53 should eventually reduce to `13`. Given a specific reduction strategy,
54 we can watch the order in which the computation proceeds. Following
55 on the evaluator developed during the previous homework, let's
56 adopt the following reduction strategy:
57
58 > In order to reduce an expression of the form (head arg), do the following in order:
59
60 > 1. Reduce `head` to `head'`
61 > 2. Reduce `arg` to `arg'`.
62 > 3. If `(head' arg')` is a redex, reduce it.
63
64 There are many details left unspecified here, but this will be enough
65 for today. The order in which the computation unfolds will be
66
67 > 1.  Reduce head `(+ 1)` to itself
68 > 2.  Reduce arg `((* ((/ 6) 2)) 4)`
69 >     1.  Reduce head `(* ((/ 6) 2))`
70 >         1.  Reduce head `*` to itself
71 >         2.  Reduce arg `((/ 6) 2)`
72 >             1.  Reduce head `(/ 6)` to itself
73 >             2.  Reduce arg `2` to itself
74 >             3.  Reduce `((/ 6) 2)` to `3`
75 >         3.  Reduce `(* 3)` to itself
76 >     2.  Reduce arg `4` to itself
77 >     3.  Reduce `((* 3) 4)` to `12`
78 > 3.  Reduce `((+ 1) 12)` to `13`
79
80 This reduction pattern follows the structure of the original
81 expression exactly, at each node moving first to the left branch,
82 processing the left branch, then moving to the right branch, and
83 finally processing the results of the two subcomputation. (This is
84 called a depth-first postorder traversal of the tree.)
85
86 [diagram with arrows traversing the tree]
87
88 It will be helpful to see how the types change as we make adjustments.
89
90     type num = int
91     type contents = Num of num   | Op2 of (num -> num -> num)
92     type tree = Leaf of contents | Branch of tree * tree
93
94 Never mind that these types will allow us to construct silly
95 arithmetric trees such as `+ *` or `2 3`. Note that during the
96 reduction sequence, the result of reduction was in every case a
97 well-formed subtree. So the process of reduction could be animated by
98 replacing subtrees with the result of reduction on that subtree, until
99 the entire tree is replaced by a single integer (namely, `13`).
100
101 Now we replace the number `2` with `0`:
102
103 <!--
104 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
105 -->
106 <pre>
107  ___________
108  |         |
109 _|__    ___|___
110 |  |    |     |
111 +  1  __|___  4
112       |    |
113       *  __|___
114          |    |
115         _|__  0
116         |  |
117         /  6
118 </pre>
119
120 When we reduce, we get quite a ways into the computation before things
121 break down:
122
123 > 1.  Reduce head `(+ 1)` to itself
124 > 2.  Reduce arg `((* ((/ 6) 0)) 4)`
125 >     1.  Reduce head `(* ((/ 6) 0))`
126 >         1.  Reduce head `*` to itself
127 >         2.  Reduce arg `((/ 6) 0)`
128 >             1.  Reduce head `(/ 6)` to itself
129 >             2.  Reduce arg `0` to itself
130 >             3.  Reduce `((/ 6) 0)` to ACKKKK
131
132 This is where we replace `/` with `safe_div`. `safe_div` returns not an `int`, but an `int option`.  If the division goes
133 through, the result is `Some n`, where `n` is the integer result.
134 But if the division attempts to divide by zero, the result is `None`.
135
136 We could try changing the type of the arithmetic operators from `int
137 -> int -> int` to `int -> int -> int option`; but since we now have to
138 anticipate the possibility that *any* argument might involve division by
139 zero inside of it, it would be better to prepare for the possibility
140 that any subcomputation might return `None` here. So our operators should have
141 the type `int option -> int option -> int option`. Let's bring that about
142 by just changing the type `num` from `int` to `int option`, leaving everying else the same:
143
144     type num = int option
145     type contents = Num of num   | Op2 of (num -> num -> num)
146     type tree = Leaf of contents | Branch of tree * tree
147
148 The only difference is that instead of defining our numbers to be
149 simple integers, they are now `int option`s; and so `Op` is an operator
150 over `int option`s.
151
152 At this point, we bring in the monadic machinery. In particular, here
153 is the `⇧` and the `map2` function from the notes on safe division:
154
155     ⇧ (x : 'a) = Some x
156
157     map2 (f : 'a -> 'b -> 'c) (xx : 'a option) (yy : 'b option) =
158       match xx with
159       | None -> None
160       | Some x ->
161           (match yy with
162           | None -> None
163           | Some y -> Some (f x y))
164
165 Then we lift the entire computation into the monad by applying `⇧` to
166 the integers, and by applying `map2` to the operators. Only, we will replace `/` with `safe_div`, defined as follows:
167
168     safe_div (xx : 'a option) (yy : 'b option) =
169       match xx with
170       | None -> None
171       | Some x ->
172           (match yy with
173           | None -> None
174           | Some 0 -> None
175           | Some y -> Some ((/) x y))
176
177 <!--
178 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
179 -->
180 <pre>
181      ___________________
182      |                 |
183   ___|____         ____|_____
184   |      |         |        |
185 map2 +  ⇧1    _____|_____  ⇧4
186               |         |
187             map2 *  ____|____
188                     |       |
189                  ___|____  ⇧0
190                  |      |
191              safe_div  ⇧6
192 </pre>
193
194 With these adjustments, the faulty computation now completes smoothly:
195
196 > 1.  Reduce head `((map2 +) ⇧1)`
197 > 2.  Reduce arg `(((map2 *) ((safe_div ⇧6) ⇧0)) ⇧4)`
198 >     1.  Reduce head `((map2 *) ((safe_div ⇧6) ⇧0))`
199 >         1.  Reduce head `(map2 *)`
200 >         2.  Reduce arg `((safe_div ⇧6) ⇧0)`
201 >             1.  Reduce head `(safe_div ⇧6)`
202 >             2.  Reduce arg `⇧0`
203 >             3.  Reduce `((safe_div ⇧6) ⇧0)` to `None`
204 >         3.  Reduce `((map2 *) None)`
205 >     2.  Reduce arg `⇧4`
206 >     3.  Reduce `(((map2 *) None) ⇧4)` to `None`
207 > 3.  Reduce `(((map2 +) ⇧1) None)` to `None`
208
209 As soon as we try to divide by `0`, `safe_div` returns `None`.
210 Thanks to the details of `map2`, the fact that `None` has been returned
211 by one of the arguments of a `map2`-ed operator guarantees that the
212 `map2`-ed operator will pass on the `None` as its result. So the
213 result of each enclosing computation will be `None`, up to the root
214 of the tree.
215
216 It is unfortunate that we need to continue the computation after
217 encountering our first `None`. We know immediately at the result of
218 the entire computation will be `None`, yet we continue to compute
219 subresults and combinations. It would be more efficient to simply
220 jump to the top as soon as `None` is encoutered. Let's call that
221 strategy Abort. We'll arrive at an `Abort` operator later in the semester.
222
223 So at this point, we can see how the Option/Maybe monad provides
224 plumbing that allows subcomputations to send information from one part
225 of the computation to another. In this case, the `safe_div` function
226 can send the information that division by zero has been attempted
227 upwards to the rest of the computation. If you think of the plumbing
228 as threaded through the tree in depth-first, postorder traversal, then
229 `safe_div` drops `None` into the plumbing half way through the
230 computation, and that `None` travels through the rest of the plumbing
231 till it comes out of the result faucet at the top of the tree.
232
233
234 ## Information flowing in the other direction: top to bottom
235
236 We can think of this application as facilitating information flow.
237 In the `safe_div` example, a subcomputation created a message that
238 propagated upwards to the larger computation:
239
240 <pre>
241                  message: Division by zero occurred!
242                       ^
243  ___________          |
244  |         |          |
245 _|__    ___|___       |
246 |  |    |     |       |
247 +  1  __|___  4       |
248       |    |          |
249       *  __|___  -----|
250          |    |
251         _|__  0
252         |  |
253         /  6
254 </pre>
255
256 (The message was implemented by `None`.)
257
258 We might want to reverse the direction of information flow, making 
259 information available at the top of the computation available to the
260 subcomputations: 
261
262 <pre>
263                     [λn]  
264  ___________          |
265  |         |          |
266 _|__    ___|___       |
267 |  |    |     |       |
268 +  1  __|___  4       |
269       |    |          |
270       *  __|___       |
271          |    |       |
272         _|__  n  <----|
273         |  |
274         /  6
275 </pre>
276
277 We've seen exactly this sort of configuration before: it's exactly
278 what we have when a lambda binds a variable that occurs in a deeply
279 embedded position. Whatever the value of the argument that the lambda
280 form combines with, that is what will be substituted in for free
281 occurrences of that variable within the body of the lambda.
282
283
284 ## Binding
285
286 So our next step is to add a (primitive) version of binding to our
287 computation. We'll allow for just one binding dependency for now, and
288 then generalize later.
289
290 Binding is independent of the safe division, so we'll return to a
291 situation in which the Option/Maybe monad hasn't been added. One of the nice
292 properties of programming with monads is that it is possible to add or
293 subtract layers according to the needs of the moment. Since we need
294 simplicity, we'll set the Option/Maybe monad aside for now.
295
296 So we'll go back to the point where the num type is simple `int`, not
297 `int option`s.
298
299     type num = int
300
301 And we won't be using the `map2` or `⇧` from the Option/Maybe monad anymore.
302
303 As you might guess, the technique we'll use to arrive at binding will
304 be to use the Reader monad, defined here in terms of `mid`/`⇧` and `mbind`/`>>=`:
305
306 <pre>
307 type <u>α</u> = int -> α
308 ⇧x = \n. x
309 xx >>= k = \n. k (xx n) n
310 map  f xx = \n. f (xx n)
311 ff ¢ xx = \n. (ff n) (xx n)
312 map2 f xx yy = map f xx ¢ yy = \n. f (xx n) (yy n)
313 </pre>
314
315 A boxed type in this monad will be a function from an integer to an
316 value in the original type. The `mid`/`⇧` function lifts a value `x` to
317 a function that expects to receive an integer, but throws away the
318 integer and returns `x` instead (most values in the computation don't
319 depend on the input integer).
320
321 The `mbind`/`>>=` function in this monad takes a monadic value `xx`, a function
322 `k` taking non-monadic values into the monad, and returns a function
323 that expects an integer `n`. It feeds `n` to `xx`, which delivers a
324 result in the orginal type, which is fed in turn to `k`. `k` returns
325 a monadic value, which upon being fed an integer, also delivers a result
326 in the orginal type.
327
328 The `map`, `¢`, and `map2` functions corresponding to this `mbind` are given
329 above. They may look familiar --- we'll comment on this in a moment.
330
331 Lifing the computation into the monad, we have the following adjusted
332 types:
333
334     type num = int -> int
335
336 That is, `num` is once again replaced with the type of a boxed `int`.
337 When we were dealing with the Option/Maybe monad, a boxed `int` had type `int
338 option`. In this monad, a boxed int has type `int -> int`.
339
340 <!--
341 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
342 -->
343 <pre>
344      __________________
345      |                |
346   ___|____        ____|_____
347   |      |        |        |
348 map2 +  ⇧1    ____|_____  ⇧4
349               |        |
350             map2 *  ___|____
351                     |      |
352                  ___|____  x
353                  |      |
354                map2 /  ⇧6
355 </pre>
356
357 It remains only to decide how the variable `n` will access the input value supplied
358 at the top of the tree. The input value is supposed to be the
359 value that gets used for the variable `n`. Like every leaf in the tree
360 in argument position, the code we want in order to represent the
361 variable will have the type of a boxed `int`, namely, `int -> int`. So
362 we have the following:
363
364     var_n = fun (n : int) -> n
365
366 That is, variables in this system denote the identity function!
367
368 The result of evaluating this tree will be a boxed integer: a function
369 from any integer `n` to `(+ 1 (* (/ 6 n)) 4)`.
370
371 Take a look at the definition of the Reader monad again. The
372 `mid` takes some object `x` and returns `\n. x`. In other words,
373 `⇧x = Kx`, for our familiar combinator **K**, so `⇧ = K`. Likewise, the `map` operation
374 is just function composition, and the `mapply`/`¢` operation is our friend the **S** combinator. `map2 f xx yy` for the Reader monad is `(f ○ xx) ¢ yy` or `S (f ○ xx) yy`.
375
376 We've seen this before as a strategy for translating a binding
377 construct into a set of combinators. To remind you, here is a part of
378 the general scheme for translating a lambda abstract into Combinatory
379 Logic. The translation function `[.]` translates a lambda term into a
380 term in Combinatory Logic:
381
382     [(MN)] = ([M] [N])
383     [\a.a] = I
384     [\a.M] = K[M]       (assuming a not free in M)
385     [\a.(MN)] = S[\a.M][\a.N]
386
387 The reason we can make do with this subset of the full translation
388 scheme is that we're making the simplifying assumption that there is
389 at most a single lambda involved. So once again we have the identity
390 function **I** as the translation of the bound variable, **K** as the function
391 governing expressions that don't contain an instance of the bound
392 variable, **S** as an operation that manages `¢`, that is, the applicative combination of complex expressions.
393
394
395 ## Jacobson's Variable Free Semantics as a Reader Monad
396
397 We've designed the presentation above to make it as easy as possible
398 to show that Jacobson's Variable Free Semantics (e.g., Jacobson 1999,
399 [Towards a Variable-Free
400 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
401 implements a Reader monad.
402
403 More specifically, it will turn out that Jacobson's geach combinator
404 *g* is exactly our `map` operator, and her binding combinator *z* is
405 exactly our `mbind` (though with the arguments reversed).
406
407 Jacobson's system contains two main combinators, *g* and *z*. She
408 calls *g* the Geach rule, and *z* performs binding. Here is a typical
409 computation. This implementation is based closely on email from Simon
410 Charlow, with beta reduction as performed by the on-line evaluator:
411
412 <pre>
413 ; Jacobson's analysis of "Everyone_i thinks he_i left"
414 let g = \f xx. \n. f (xx n) in ; or `f ○ xx`
415 let z = \k xx. \n. k (xx n) n in ; or `S (flip k) xx`, or `Reader.(>>=) xx k`
416 let he = \n. n in
417 let everyone = \P. FORALL i (P i) in
418
419 everyone (z thinks (g left he))
420
421 ~~>  FORALL i (thinks (left i) i)
422 </pre>
423
424 Two things to notice: First, pronouns once again denote identity
425 functions, just as we saw in the reader monad in the previous section.
426
427 Second, *g* plays the role of transmitting a binding dependency for an
428 embedded constituent to a containing constituent.
429
430 The basic recipe in Jacobson's system is that you transmit the
431 dependence of a pronoun upwards through the tree using *g* until just
432 before you are about to combine with the binder, when you finish off
433 with *z*. Here is an example with a longer chain of *g*'s:
434
435 <pre>
436 ; "Everyone_i thinks that Bill said he_i left"
437
438 everyone (z thinks (g (T bill) (g said (g left he))))
439 ; or `everyone (thinks =<< T bill ○ said ○ left ○ I)`
440
441 ~~> FORALL i (thinks (said (left i) bill) i)
442 </pre>
443
444 If you compare Jacobson's values for *g* and *z* to the functions in
445 the reader monad given above, you'll see that Jacobson's *g*
446 combinator is exactly our `map` operator. Furthermore, Jacobson's *z*
447 combinator is identical to our Reader `>>=`, except with the order of the
448 arguments reversed (i.e., `(z k xx) == (xx >>= k)`).
449
450 (The `T` combinator in the derivations above is given by `T x <~~> \f. f x`;
451 it handles situations in which English word order reverses
452 the usual function/argument order. `T` is what Curry and Steedman call this
453 combinator. Jacobson calls it "lift", but it shouldn't be confused with the
454 `mid` and `map` operations that lift values into the Reader monad we're focusing
455 on here. It does lift values into a *different* monad, that we'll consider in
456 a few weeks.)
457
458 In other words, 
459 Jacobson's variable-free semantics is essentially a Reader monad.
460
461 One of the peculiar aspects of Jacobson's system is that binding is
462 accomplished not by applying *z* to the element that will (in some
463 pre-theoretic sense) bind the pronoun, here, *everyone*, but rather by
464 applying *z* instead to the predicate that will take *everyone* as an
465 argument, here, *thinks*.
466
467
468 ## The Reader monad for intensionality
469
470 Now we'll look at using the Reader monad to do intensional function application.
471
472 In Shan (2001) [Monads for natural
473 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
474 making expressions sensitive to the world of evaluation is conceptually
475 the same thing as making use of the Reader monad.
476 This technique was beautifully re-invented
477 by Ben-Avi and Winter (2007) in their paper [A modular
478 approach to
479 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
480 though without explicitly using monads.
481
482 All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
483 To run it, download the file, start OCaml, and say 
484
485         # #use "intensionality-monad.ml";;
486
487 Note the extra `#` attached to the directive `use`.
488
489 First, the familiar linguistic problem:
490
491     Bill left.  
492     Cam left.
493     Ann believes that Bill left.
494     Ann believes that Cam left.
495
496 We want an analysis on which the first three sentences can be true at
497 the same time that the last sentence is false. If sentences denoted
498 simple truth values or booleans, we have a problem: if the sentences
499 *Bill left* and *Cam left* are both true, they denote the same object,
500 and Ann's beliefs can't distinguish between them.
501
502 The traditional solution to the problem sketched above is to allow
503 sentences to denote a function from worlds to truth values, what
504 Montague called an intension. So if `s` is the type of possible
505 worlds, we have the following situation:
506
507
508 <pre>
509 Extensional types              Intensional types       Examples
510 -------------------------------------------------------------------
511
512 S         t                    s->t                    John left
513 DP        e                    s->e                    John
514 VP        e->t                 (s->e)->s->t            left
515 Vt        e->e->t              (s->e)->(s->e)->s->t    saw
516 Vs        t->e->t              (s->t)->(s->e)->s->t    thought
517 </pre>
518
519 This system is modeled on the way Montague arranged his grammar.
520 There are significant simplifications compared to Montague: for
521 instance, determiner phrases are thought of here as corresponding to
522 individuals rather than to generalized quantifiers.
523
524 The main difference between the intensional types and the extensional
525 types is that in the intensional types, the arguments are functions
526 from worlds to extensions: intransitive verb phrases like *left* now
527 take so-called "individual concepts" as arguments (type `s->e`) rather than plain
528 individuals (type `e`), and attitude verbs like *think* now take
529 propositions (type `s->t`) rather than truth values (type `t`).
530 In addition, the result of each predicate is an intension.
531 This expresses the fact that the set of people who left in one world
532 may be different than the set of people who left in a different world.
533
534 Normally, the dependence of the extension of a predicate to the world
535 of evaluation is hidden inside of an evaluation coordinate, or built
536 into the the lexical meaning function, but we've made it explicit here
537 in the way that the intensionality monad makes most natural.
538
539 The intensional types are more complicated than the extensional
540 types. Wouldn't it be nice to make the complicated types available
541 for expressions like attitude verbs that need to worry about
542 intensions, and keep the rest of the grammar as extensional as
543 possible? This desire is parallel to our earlier desire to limit the
544 concern about division by zero to the division function, and let the
545 other functions, like addition or multiplication, ignore
546 division-by-zero problems as much as possible.
547
548 So here's what we do:
549
550 In OCaml, we'll use integers to model possible worlds. `char`s (characters in the computational sense, i.e., letters like `'a'` and `'b'`, not Kaplanian characters) will model individuals, and OCaml `bool`s will serve for truth values:
551
552         type s = int
553         type e = char
554         type t = bool
555
556         let ann = 'a'
557         let bill = 'b'
558         let cam = 'c'
559
560         let left1 (x : e) = true 
561         let saw1 (y : e) (x : e) = x < y 
562
563         left1 ann (* true *)
564         saw1 bill ann (* true *)
565         saw1 ann bill (* false *)
566
567 So here's our extensional system: everyone left, including Ann;
568 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
569 order we're using is VOS, verb-object-subject.)
570
571 Now we add intensions. Because different people leave in different
572 worlds, the meaning of *leave* must depend on the world in which it is
573 being evaluated:
574
575     let left (x : e) (w : s) = match (x, w) with ('c', 2) -> false | _ -> true
576     left ann 1 (* true: Ann left in world 1 *)
577     left cam 2 (* false: Cam didn't leave in world 2 *) 
578
579 This new definition says that everyone always left, except that 
580 in world 2, Cam didn't leave.
581
582 Note that although this general *left* is sensitive to world of
583 evaluation, it does not have the fully intensionalized type given in
584 the chart above, which was `(s->e)->s->t`. This is because
585 *left* does not exploit the additional resolving power provided by
586 making the subject an individual concept. In semantics jargon, we say
587 that *leave* is extensional with respect to its first argument.
588
589 We will adopt the general strategy of defining predicates
590 in a way that they take arguments of the lowest type that will allow
591 us to make all the distinctions the predicate requires. When it comes
592 time to combine this predicate with monadic arguments, we'll have to
593 make use of various lifting predicates.
594
595 Likewise, although *see* depends on the world of evaluation, it is
596 extensional in both of its syntactic arguments:
597
598     let saw (y : e) (x : e) (w : s) = (w < 2) && (x < y)
599     saw bill ann 1 (* true: Ann saw Bill in world 1 *)
600     saw bill ann 2 (* false: no one saw anyone in world 2 *)
601
602 This (again, partially) intensionalized version of *see* coincides
603 with the `saw1` function we defined above for world 1; in world 2, no
604 one saw anyone.
605
606 Just to keep things straight, let's review the facts:
607
608 <pre>
609      World 1: Everyone left.
610               Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.              
611      World 2: Ann left, Bill left, Cam didn't leave.
612               No one saw anyone.
613 </pre>
614
615 Now we are ready for the intensionality monad:
616
617 <pre>
618 type 'a intension = s -> 'a
619 let mid x = fun (w : s) -> x
620 let (>>=) xx k = fun (w : s) -> let x = xx w in let yy = k x in yy w
621                  (* or just `fun w -> k (xx w) w` *)
622 </pre>
623
624 Then the individual concept `mid ann` is a rigid designator: a
625 constant function from worlds to individuals that returns `'a'` no
626 matter which world is used as an argument. This is a typical kind of
627 thing for a monadic `mid` to do.
628
629 Then combining a predicate like *left* which is extensional in its
630 subject argument with an intensional subject like `mid ann` is simply `mbind`
631 in action:
632
633     (mid ann >>= left) 1  (* true: Ann left in world 1 *)
634     (mid cam >>= left) 2  (* false: Cam didn't leave in world 2 *)
635
636 As usual, `>>=` takes a monadic box containing Ann, extracts Ann, and
637 feeds her to the function *left*. In linguistic terms, we take the
638 individual concept `mid ann`, apply it to the world of evaluation in
639 order to get hold of an individual (`'a'`), then feed that individual
640 to the predicate *left*.
641
642 We can arrange for a transitive verb that is extensional in both of
643 its arguments to take intensional arguments:
644
645 <pre>
646 let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> <span class=ul>f x y</span>))
647 </pre>
648
649 This is almost the same `map2` predicate we defined in order to allow
650 addition in our division monad example. The *difference* is that this
651 variant operates on verb meanings that take extensional arguments but
652 returns an intensional result. Thus the original `map2` predicate
653 has `mid (f x y)` where we have just <code><span class=ul>f x y</span></code> here.
654
655 The use of `>>=` here to combine *left* with an individual concept,
656 and the use of `map2'` to combine *see* with two intensional
657 arguments closely parallels the two of Montague's meaning postulates
658 (in PTQ) that express the relationship between extensional verbs and
659 their uses in intensional contexts.
660
661 <pre>
662 map2' saw (mid bill) (mid ann) 1  (* true *)
663 map2' saw (mid bill) (mid ann) 2  (* false *)
664 </pre>
665
666 Ann did see Bill in world 1, but Ann didn't see Bill in world 2.
667
668 Finally, we can define our intensional verb *thinks*. *Think* is
669 intensional with respect to its sentential complement (it takes complements of type `s -> t`), though still extensional
670 with respect to its subject (type `e`). (As Montague noticed, almost all verbs
671 in English are extensional with respect to their subject; a possible
672 exception is *appear*.)
673
674     let thinks (p : s->t) (x : e) (w : s) = 
675       match (x, p 2) with ('a', false) -> false | _ -> p w
676
677 In every world, Ann fails to believe any proposition that is false in world 2.
678 Apparently, she stably thinks we may be in world 2. Otherwise, everyone
679 believes a proposition iff that proposition is true in the world of evaluation.
680
681     (mid ann >>= thinks (mid bill >>= left)) 1  (* true *)
682
683 So in world 1, Ann thinks that Bill left (because in worlds 1 and 2, Bill did leave).
684
685 But although Cam left in world 1:
686
687     (mid cam >>= left) 1  (* true *)
688
689 he didn't leave in world 2, so Ann doesn't in world 1 believe that Cam left:
690
691     (mid ann >>= thinks (mid cam >>= left)) 1  (* false *)
692
693
694 **Small project**: add intersective (*red*) and non-intersective
695  adjectives (*good*) to the fragment. The intersective adjectives
696  will be extensional with respect to the nominal they combine with
697  (using `mbind`), and the non-intersective adjectives will take
698  intensional arguments.
699
700 **Connections with variable binding**: the rigid individual concepts generated by `mid ann` and the like correspond to the numerical constants, that don't interact with the environment in any way, in the variable binding examples we considered earlier on the page. If we had any non-contingent predicates that were wholly insensitive to intensional effects, they would be modeled using `map2` and would correspond to the operations like `map2 (+)` in the earlier examples. As it is, our predicates *lift* and *saw*, though only sensitive to the *extension* of their arguments, nonetheless *are* sensitive to the world of evaluation for their `bool` output. So these are somewhat akin, at the predicate level, to expressions like `var_n`, at the singular term level, in the variable bindings examples. Our predicate *thinks* shows yet a further kind of interaction with the intensional structures we introduced: namely, its output can depend upon evaluating its complement relative to other possible worlds. We didn't discuss analogues of this in the variable binding case, but they exist: namely, they are expressions like `let x = 2 in ...` and `forall x ...`, that have the effect of supplying their arguments with an environment or assignment function that is shifted from the one they are themselves being evaluated with.
701
702 notes: cascade, general env