1 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ¢ ⇧ -->
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 teach
23 them what to do if they received Nothing instead of a boxed integer.
24 This meant changing the type of their input from ints to int options.
25 But we didn't need to do this piecemeal; rather, we "lift"ed the
26 ordinary arithmetic operations into the monad using the various tools
27 provided by the monad.
29 We'll go over this lifting operation in detail in the next section.
31 ## Tracing the effect of safe-div on a larger computation
33 So let's see how this works in terms of a specific computation.
36 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
39 (+ 1 (* (/ 6 2) 4)) in tree format:
54 No matter which arithmetic operation we begin with, this computation
55 should eventually reduce to 13. Given a specific reduction strategy,
56 we can watch the order in which the computation proceeds. Following
57 on the lambda evaluator developed during the previous homework, let's
58 adopt the following reduction strategy:
60 In order to reduce an expression of the form (head arg), do the following in order:
63 3. If (h' a') is a redex, reduce it.
65 There are many details left unspecified here, but this will be enough
66 for today. The order in which the computation unfolds will be
68 1. Reduce head (+ 1) to itself
69 2. Reduce arg ((* ((/ 6) 2)) 3)
70 1. Reduce head (* ((/ 6) 2))
72 2. Reduce arg ((/ 6) 2)
73 1. Reduce head (/ 6) to itself
74 2. Reduce arg 2 to itself
75 3. Reduce ((/ 6) 2) to 3
76 3. Reduce (* 3) to itself
77 2. Reduce arg 4 to itself
78 3. Reduce ((* 3) 4) to 12
79 3. Reduce ((+ 1) 12) to 13
81 This reduction pattern follows the structure of the original
82 expression exactly, at each node moving first to the left branch,
83 processing the left branch, then moving to the right branch, and
84 finally processing the results of the two subcomputation. (This is
85 called depth-first postorder traversal of the tree.)
87 [diagram with arrows traversing the tree]
89 It will be helpful to see how the types change as we make adjustments.
92 type contents = Num of num | Op2 of (num -> num -> num)
93 type tree = Leaf of contents | Branch of tree * tree
95 Never mind that these types will allow us to construct silly
96 arithmetric trees such as `+ *` or `2 3`. Note that during the
97 reduction sequence, the result of reduction was in every case a
98 well-formed subtree. So the process of reduction could be animated by
99 replacing subtrees with the result of reduction on that subtree, till
100 the entire tree is replaced by a single integer (namely, 13).
102 Now we replace the number 2 with 0:
105 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
121 When we reduce, we get quite a ways into the computation before things
124 1. Reduce head (+ 1) to itself
125 2. Reduce arg ((* ((/ 6) 0)) 3)
126 1. Reduce head (* ((/ 6) 0))
128 2. Reduce arg ((/ 6) 0)
129 1. Reduce head (/ 6) to itself
130 2. Reduce arg 0 to itself
131 3. Reduce ((/ 6) 0) to ACKKKK
133 This is where we replace `/` with `safe-div`.
134 Safe-div returns not an int, but an int option. If the division goes
135 through, the result is Just n, where n is the integer result.
136 But if the division attempts to divide by zero, the result is Nothing.
138 We could try changing the type of the arithmetic operators from `int
139 -> int -> int` to `int -> int -> int option`; but since we now have to
140 anticipate the possibility that any argument might involve division by
141 zero inside of it, it would be better to prepare for the possibility
142 that any subcomputation might return here is the net result for our
143 types. The easy way to do that is to change (only) the type of num
144 from int to int option, leaving everying else the same:
146 type num = int option
147 type contents = Num of num | Op2 of (num -> num -> num)
148 type tree = Leaf of contents | Branch of tree * tree
150 The only difference is that instead of defining our numbers to be
151 simple integers, they are now int options; and so Op is an operator
154 At this point, we bring in the monadic machinery. In particular, here
155 is the ⇧ and the map2 function from the notes on safe division:
159 map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
165 | Some y -> Some (g x y));;
167 Then we lift the entire computation into the monad by applying ⇧ to
168 the integers, and by applying `map2` to the operators:
171 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
178 map2 + ⇧1 _____|_____ ⇧4
187 With these adjustments, the faulty computation now completes smoothly:
189 1. Reduce head ((map2 +) ⇧1)
190 2. Reduce arg (((map2 *) (((map2 /) ⇧6) ⇧2)) ⇧3)
191 1. Reduce head ((map2 *) (((map2 /) ⇧6) ⇧2))
193 2. Reduce arg (((map2 /) ⇧6) ⇧0)
194 1. Reduce head ((map2 /) ⇧6)
196 3. Reduce (((map2 /) ⇧6) ⇧0) to Nothing
197 3. Reduce ((map2 *) Nothing) to Nothing
199 3. Reduce (((map2 *) Nothing) ⇧4) to Nothing
200 3. Reduce (((map2 +) ⇧1) Nothing) to Nothing
202 As soon as we try to divide by 0, safe-div returns Nothing.
203 Thanks to the details of map2, the fact that Nothing has been returned
204 by one of the arguments of a map2-ed operator guarantees that the
205 map2-ed operator will pass on the Nothing as its result. So the
206 result of each enclosing computation will be Nothing, up to the root
209 It is unfortunate that we need to continue the computation after
210 encountering our first Nothing. We know immediately at the result of
211 the entire computation will be Nothing, yet we continue to compute
212 subresults and combinations. It would be more efficient to simply
213 jump to the top as soon as Nothing is encoutered. Let's call that
214 strategy Abort. We'll arrive at an Abort operator later in the semester.
216 So at this point, we can see how the Maybe/option monad provides
217 plumbing that allows subcomputations to send information from one part
218 of the computation to another. In this case, the safe-div function
219 can send the information that division by zero has been attempted
220 throughout the rest of the computation. If you think of the plumbing
221 as threaded through the tree in depth-first, postorder traversal, then
222 safe-div drops Nothing into the plumbing half way through the
223 computation, and that Nothing travels through the rest of the plumbing
224 till it comes out of the result faucet at the top of the tree.
226 ## Information flowing in the other direction: top to bottom
228 We can think of this application as facilitating information flow.
229 In the save-div example, a subcomputation created a message that
230 propagated upwards to the larger computation:
233 message: Division by zero occurred!
248 We might want to reverse the direction of information flow, making
249 information available at the top of the computation available to the
267 We've seen exactly this sort of configuration before: it's exactly
268 what we have when a lambda binds a variable that occurs in a deeply
269 embedded position. Whatever the value of the argument that the lambda
270 form combines with, that is what will be substituted in for free
271 occurrences of that variable within the body of the lambda.
275 So our next step is to add a (primitive) version of binding to our
276 computation. We'll allow for just one binding dependency for now, and
277 then generalize later.
279 Binding is independent of the safe division, so we'll return to a
280 situation in which the Maybe monad hasn't been added. One of the nice
281 properties of programming with monads is that it is possible to add or
282 subtract layers according to the needs of the moment. Since we need
283 simplicity, we'll set the Maybe monad aside for now.
285 So we'll go back to the point where the num type is simple int, not
290 And we'll start with the computation the map2 or the ⇧ from the option
293 As you might guess, the technique we'll use to arrive at binding will
294 be to use the Reader monad, defined here in terms of m-identity and bind:
296 α ==> int -> α (* The ==> is a Kleisli arrow *)
300 map2 f u v = \x.f(ux)(vx)
303 A boxed type in this monad will be a function from an integer to an
304 object in the original type. The unit function ⇧ lifts a value `a` to
305 a function that expects to receive an integer, but throws away the
306 integer and returns `a` instead (most values in the computation don't
307 depend on the input integer).
309 The bind function in this monad takes a monadic object `u`, a function
310 `f` lifting non-monadic objects into the monad, and returns a function
311 that expects an integer `x`. It feeds `x` to `u`, which delivers a
312 result in the orginal type, which is fed in turn to `f`. `f` returns
313 a monadic object, which upon being fed an integer, returns an object
316 The map2 function corresponding to this bind operation is given
317 above. It should look familiar---we'll be commenting on this
318 familiarity in a moment.
320 Lifing the computation into the monad, we have the following adjusted
323 type num = int -> int
325 That is, `num` is once again replaced with the type of a boxed int.
326 When we were dealing with the Maybe monad, a boxed int had type `int
327 option`. In this monad, a boxed int has type `int -> int`.
330 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
337 map2 + ⇧1 ____|_____ ⇧4
346 It remains only to decide how the variable `x` will access the value input
347 at the top of the tree. Since the input value is supposed to be the
348 value put in place of the variable `x`. Like every leaf in the tree
349 in argument position, the code we want in order to represent the
350 variable will have the type of a boxed int, namely, `int -> int`. So
351 we have the following:
353 x = (\fun (i:int) = i)
355 That is, variables in this system denote the indentity function!
357 The result of evaluating this tree will be a boxed integer: a function
358 from any integer `x` to `(+ 1 (* (/ 6 x)) 4)`.
360 Take a look at the definition of the reader monad again. The
361 midentity takes some object `a` and returns `\x.a`. In other words,
362 `⇧a = Ka`, so `⇧ = K`. Likewise, the reason the `map2` function
363 looked familiar is that it is essentially the `S` combinator.
365 We've seen this before as a strategy for translating a binding
366 construct into a set of combinators. To remind you, here is a part of
367 the general scheme for translating a lambda abstract into Combinatory
368 Logic. The translation function `[.]` translates a lambda term into a
369 term in Combinatory Logic:
373 [\a.M] = K[M] (assuming a not free in M)
374 [\a.(MN)] = S[\a.M][\a.N]
376 The reason we can make do with this subset of the full translation
377 scheme is that we're making the simplifying assumption that there is
378 at most a single lambda involved. So once again we have the identity
379 function I as the translation of the bound variable, K as the function
380 governing expressions that don't contain an instance of the bound
381 variable, S as the operation that manages the combination of complex
384 ## Jacobson's Variable Free Semantics as a Reader Monad
386 We've designed the presentation above to make it as easy as possible
387 to show that Jacobson's Variable Free Semantics (e.g., Jacobson 1999,
388 [Towards a Variable-Free
389 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
390 implements a reader monad.
392 More specifically, it will turn out that Jacobson's geach combinator
393 *g* is exactly our `lift` operator, and her binding combinator *z* is
394 exactly our `bind` (though with the arguments reversed).
396 Jacobson's system contains two main combinators, *g* and *z*. She
397 calls *g* the Geach rule, and *z* performs binding. Here is a typical
398 computation. This implementation is based closely on email from Simon
399 Charlow, with beta reduction as performed by the on-line evaluator:
402 ; Jacobson's analysis of "Everyone_i thinks he_i left"
403 let g = \f u. \x. f (u x) in
404 let z = \f u. \x. f (u x) x in
406 let everyone = \P. FORALL x (P x) in
408 everyone (z thinks (g left he))
410 ~~> FORALL x (thinks (left x) x)
413 Two things to notice: First, pronouns once again denote identity
414 functions, just as we saw in the reader monad in the previous section.
416 Second, *g* plays the role of transmitting a binding dependency for an
417 embedded constituent to a containing constituent.
419 The basic recipe in Jacobson's system is that you transmit the
420 dependence of a pronoun upwards through the tree using *g* until just
421 before you are about to combine with the binder, when you finish off
422 with *z*. Here is an example with a longer chain of *g*'s:
425 everyone (z thinks (g (t bill) (g said (g left he))))
427 ~~> FORALL x (thinks (said (left x) bill) x)
430 If you compare Jacobson's values for *g* and *z* to the functions in
431 the reader monad given above, you'll see that Jacobson's *g*
432 combinator is exactly our `map` operator. Furthermore, Jacobson's *z*
433 combinator is identital to `>>=`, except with the order of the
434 arguments reversed (i.e., `(z f u) == (u >>= f)`).
436 (The `t` combinator in the derivations above is given by `t x =
437 \xy.yx`; it handles situations in which English word order reverses
438 the usual function/argument order.)
441 Jacobson's variable-free semantics is essentially a Reader monad.
443 One of the peculiar aspects of Jacobson's system is that binding is
444 accomplished not by applying *z* to the element that will (in some
445 pre-theoretic sense) bind the pronoun, here, *everyone*, but rather by
446 applying *z* instead to the predicate that will take *everyone* as an
447 argument, here, *thinks*.
450 ## The Reader monad for intensionality
452 [This section has not been revised since 2010, so there may be a few
453 places where it doesn't follow the convetions we've adopted this time;
454 nevertheless, it should be followable.]
456 Now we'll look at using the Reader monad to do intensional function application.
458 In Shan (2001) [Monads for natural
459 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
460 making expressions sensitive to the world of evaluation is conceptually
461 the same thing as making use of the Reader monad.
462 This technique was beautifully re-invented
463 by Ben-Avi and Winter (2007) in their paper [A modular
465 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
466 though without explicitly using monads.
468 All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
469 To run it, download the file, start OCaml, and say
471 # #use "intensionality-monad.ml";;
473 Note the extra `#` attached to the directive `use`.
475 First, the familiar linguistic problem:
479 Ann believes [Bill left].
480 Ann believes [Cam left].
482 We want an analysis on which the first three sentences can be true at
483 the same time that the last sentence is false. If sentences denoted
484 simple truth values or booleans, we have a problem: if the sentences
485 *Bill left* and *Cam left* are both true, they denote the same object,
486 and Ann's beliefs can't distinguish between them.
488 The traditional solution to the problem sketched above is to allow
489 sentences to denote a function from worlds to truth values, what
490 Montague called an intension. So if `s` is the type of possible
491 worlds, we have the following situation:
495 Extensional types Intensional types Examples
496 -------------------------------------------------------------------
500 VP e->t (s->e)->s->t left
501 Vt e->e->t (s->e)->(s->e)->s->t saw
502 Vs t->e->t (s->t)->(s->e)->s->t thought
505 This system is modeled on the way Montague arranged his grammar.
506 There are significant simplifications compared to Montague: for
507 instance, determiner phrases are thought of here as corresponding to
508 individuals rather than to generalized quantifiers.
510 The main difference between the intensional types and the extensional
511 types is that in the intensional types, the arguments are functions
512 from worlds to extensions: intransitive verb phrases like "left" now
513 take so-called "individual concepts" as arguments (type s->e) rather than plain
514 individuals (type e), and attitude verbs like "think" now take
515 propositions (type s->t) rather than truth values (type t).
516 In addition, the result of each predicate is an intension.
517 This expresses the fact that the set of people who left in one world
518 may be different than the set of people who left in a different world.
520 Normally, the dependence of the extension of a predicate to the world
521 of evaluation is hidden inside of an evaluation coordinate, or built
522 into the the lexical meaning function, but we've made it explicit here
523 in the way that the intensionality monad makes most natural.
525 The intensional types are more complicated than the extensional
526 types. Wouldn't it be nice to make the complicated types available
527 for those expressions like attitude verbs that need to worry about
528 intensions, and keep the rest of the grammar as extensional as
529 possible? This desire is parallel to our earlier desire to limit the
530 concern about division by zero to the division function, and let the
531 other functions, like addition or multiplication, ignore
532 division-by-zero problems as much as possible.
534 So here's what we do:
536 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:
546 let left1 (x:e) = true;;
547 let saw1 (x:e) (y:e) = y < x;;
549 left1 ann;; (* true *)
550 saw1 bill ann;; (* true *)
551 saw1 ann bill;; (* false *)
553 So here's our extensional system: everyone left, including Ann;
554 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
555 order we're using is VOS, verb-object-subject.)
557 Now we add intensions. Because different people leave in different
558 worlds, the meaning of *leave* must depend on the world in which it is
561 let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
562 left ann 1;; (* true: Ann left in world 1 *)
563 left cam 2;; (* false: Cam didn't leave in world 2 *)
565 This new definition says that everyone always left, except that
566 in world 2, Cam didn't leave.
568 Note that although this general *left* is sensitive to world of
569 evaluation, it does not have the fully intensionalized type given in
570 the chart above, which was `(s->e)->s->t`. This is because
571 *left* does not exploit the additional resolving power provided by
572 making the subject an individual concept. In semantics jargon, we say
573 that *leave* is extensional with respect to its first argument.
575 Therefore we will adopt the general strategy of defining predicates
576 in a way that they take arguments of the lowest type that will allow
577 us to make all the distinctions the predicate requires. When it comes
578 time to combine this predicate with monadic arguments, we'll have to
579 make use of various lifting predicates.
581 Likewise, although *see* depends on the world of evaluation, it is
582 extensional in both of its syntactic arguments:
584 let saw x y w = (w < 2) && (y < x);;
585 saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
586 saw bill ann 2;; (* false: no one saw anyone in world 2 *)
588 This (again, partially) intensionalized version of *see* coincides
589 with the `saw1` function we defined above for world 1; in world 2, no
592 Just to keep things straight, let's review the facts:
595 World 1: Everyone left.
596 Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
597 World 2: Ann left, Bill left, Cam didn't leave.
601 Now we are ready for the intensionality monad:
604 type 'a intension = s -> 'a;;
605 let unit x = fun (w:s) -> x;;
606 (* as before, bind can be written more compactly, but having
607 it spelled out like this will be useful down the road *)
608 let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
611 Then the individual concept `unit ann` is a rigid designator: a
612 constant function from worlds to individuals that returns `'a'` no
613 matter which world is used as an argument. This is a typical kind of
614 thing for a monad unit to do.
616 Then combining a predicate like *left* which is extensional in its
617 subject argument with an intensional subject like `unit ann` is simply bind
620 bind (unit ann) left 1;; (* true: Ann left in world 1 *)
621 bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
623 As usual, bind takes a monad box containing Ann, extracts Ann, and
624 feeds her to the extensional *left*. In linguistic terms, we take the
625 individual concept `unit ann`, apply it to the world of evaluation in
626 order to get hold of an individual (`'a'`), then feed that individual
627 to the extensional predicate *left*.
629 We can arrange for a transitive verb that is extensional in both of
630 its arguments to take intensional arguments:
632 let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
634 This is almost the same `lift2` predicate we defined in order to allow
635 addition in our division monad example. The difference is that this
636 variant operates on verb meanings that take extensional arguments but
637 returns an intensional result. Thus the original `lift2` predicate
638 has `unit (f x y)` where we have just `f x y` here.
640 The use of `bind` here to combine *left* with an individual concept,
641 and the use of `lift2'` to combine *see* with two intensional
642 arguments closely parallels the two of Montague's meaning postulates
643 (in PTQ) that express the relationship between extensional verbs and
644 their uses in intensional contexts.
647 lift2' saw (unit bill) (unit ann) 1;; (* true *)
648 lift2' saw (unit bill) (unit ann) 2;; (* false *)
651 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
653 Finally, we can define our intensional verb *thinks*. *Think* is
654 intensional with respect to its sentential complement, though still extensional
655 with respect to its subject. (As Montague noticed, almost all verbs
656 in English are extensional with respect to their subject; a possible
657 exception is "appear".)
659 let thinks (p:s->t) (x:e) (w:s) =
660 match (x, p 2) with ('a', false) -> false | _ -> p w;;
662 Ann disbelieves any proposition that is false in world 2. Apparently,
663 she firmly believes we're in world 2. Everyone else believes a
664 proposition iff that proposition is true in the world of evaluation.
666 bind (unit ann) (thinks (bind (unit bill) left)) 1;;
668 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
670 bind (unit ann) (thinks (bind (unit cam) left)) 1;;
672 But in world 1, Ann doesn't believe that Cam left (even though he
673 did leave in world 1: `bind (unit cam) left 1 == true`). Ann's thoughts are hung up on
674 what is happening in world 2, where Cam doesn't leave.
676 *Small project*: add intersective ("red") and non-intersective
677 adjectives ("good") to the fragment. The intersective adjectives
678 will be extensional with respect to the nominal they combine with
679 (using bind), and the non-intersective adjectives will take
680 intensional arguments.
682 notes: cascade, general env