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 Option/Maybe monad (option
15 types), and the List monad.
17 We've also seen an application of the Option/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 `Some
20 3`. But if we divide `6` by `0`, we get the answer `None`.
22 The next step was to adjust the other arithmetic functions to teach
23 them what to do if they received `None` instead of a boxed integer.
24 This meant changing the type of their input from `int`s to `int option`s.
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 what order we evaluate it in, 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:
61 > 1. Reduce head to h'
62 > 2. Reduce arg to a'.
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)) 4)
70 > 1. Reduce head (* ((/ 6) 2))
71 > 1. Reduce head * to itself
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)) 4)
126 > 1. Reduce head (* ((/ 6) 0))
127 > 1. Reduce head * to itself
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`. `safe_div` returns not an `int`, but an `int option`. If the division goes
134 through, the result is `Some n`, where `n` is the integer result.
135 But if the division attempts to divide by zero, the result is `None`.
137 We could try changing the type of the arithmetic operators from `int
138 -> int -> int` at least to `int -> int -> int option`; but since we now have to
139 anticipate the possibility that *any* argument might involve division by
140 zero inside of it, it would be better to prepare for the possibility
141 that any subcomputation might return `None` here. So our operators should have
142 the type `int option -> int option -> int option`. Let's bring that about
143 by just changing the type `num` from `int` to `int option`, leaving everying else the same:
145 type num = int option
146 type contents = Num of num | Op2 of (num -> num -> num)
147 type tree = Leaf of contents | Branch of tree * tree
149 The only difference is that instead of defining our numbers to be
150 simple integers, they are now `int option`s; and so `Op` is an operator
153 At this point, we bring in the monadic machinery. In particular, here
154 is the `⇧` and the `map2` function from the notes on safe division:
158 map2 (g : 'a -> 'b -> 'c) (xx : 'a option) (yy : 'b option) =
164 | Some y -> Some (g x y));;
166 Then we lift the entire computation into the monad by applying `⇧` to
167 the integers, and by applying `map2` to the operators. Only, we will replace `/` with `safe_div`, defined as follows:
169 safe_div (xx : 'a option) (yy : 'b option) =
176 | Some y -> Some ((/) x y));;
179 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
186 map2 + ⇧1 _____|_____ ⇧4
195 With these adjustments, the faulty computation now completes smoothly:
197 > 1. Reduce head ((map2 +) ⇧1)
198 > 2. Reduce arg (((map2 *) ((safe_div ⇧6) ⇧0)) ⇧4)
199 > 1. Reduce head ((map2 *) ((safe_div ⇧6) ⇧0))
200 > 1. Reduce head (map2 *)
201 > 2. Reduce arg ((safe_div ⇧6) ⇧0)
202 > 1. Reduce head (safe_div ⇧6)
204 > 3. Reduce ((safe_div ⇧6) ⇧0) to None
205 > 3. Reduce ((map2 *) None)
207 > 3. Reduce (((map2 *) None) ⇧4) to None
208 > 3. Reduce (((map2 +) ⇧1) None) to None
210 As soon as we try to divide by 0, `safe_div` returns `None`.
211 Thanks to the details of `map2`, the fact that `None` has been returned
212 by one of the arguments of a `map2`-ed operator guarantees that the
213 `map2`-ed operator will pass on the `None` as its result. So the
214 result of each enclosing computation will be `None`, up to the root
217 It is unfortunate that we need to continue the computation after
218 encountering our first `None`. We know immediately at the result of
219 the entire computation will be `None`, yet we continue to compute
220 subresults and combinations. It would be more efficient to simply
221 jump to the top as soon as `None` is encoutered. Let's call that
222 strategy Abort. We'll arrive at an `Abort` operator later in the semester.
224 So at this point, we can see how the Option/Maybe monad provides
225 plumbing that allows subcomputations to send information from one part
226 of the computation to another. In this case, the `safe_div` function
227 can send the information that division by zero has been attempted
228 throughout the rest of the computation. If you think of the plumbing
229 as threaded through the tree in depth-first, postorder traversal, then
230 `safe_div` drops `None` into the plumbing half way through the
231 computation, and that `None` travels through the rest of the plumbing
232 till it comes out of the result faucet at the top of the tree.
235 ## Information flowing in the other direction: top to bottom
237 We can think of this application as facilitating information flow.
238 In the save-div example, a subcomputation created a message that
239 propagated upwards to the larger computation:
242 message: Division by zero occurred!
257 (The message was implemented by `None`.)
259 We might want to reverse the direction of information flow, making
260 information available at the top of the computation available to the
278 We've seen exactly this sort of configuration before: it's exactly
279 what we have when a lambda binds a variable that occurs in a deeply
280 embedded position. Whatever the value of the argument that the lambda
281 form combines with, that is what will be substituted in for free
282 occurrences of that variable within the body of the lambda.
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.
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.
296 So we'll go back to the point where the num type is simple `int`, not
301 And we won't be using the `map2` or `⇧` from the Option/Maybe monad anymore.
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`/`>>=`:
307 type <u>α</u> = int -> α
309 xx >>= k = \n. k (xx n) n
310 map f xx = \n. f (xx n)
311 map2 f xx yy = \n. f (xx n) (yy n)
314 A boxed type in this monad will be a function from an integer to an
315 value in the original type. The `mid`/`⇧` function lifts a value `x` to
316 a function that expects to receive an integer, but throws away the
317 integer and returns `x` instead (most values in the computation don't
318 depend on the input integer).
320 The `mbind`/`>>=` function in this monad takes a monadic value `xx`, a function
321 `k` lifting non-monadic objects into the monad, and returns a function
322 that expects an integer `n`. It feeds `n` to `xx`, which delivers a
323 result in the orginal type, which is fed in turn to `k`. `k` returns
324 a monadic value, which upon being fed an integer, also delivers a value
327 The `map2` function corresponding to this bind operation is given
328 above. It may look familiar --- we'll be commenting on this
329 familiarity in a moment.
331 Lifing the computation into the monad, we have the following adjusted
334 type num = int -> int
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`.
341 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
348 map2 + ⇧1 ____|_____ ⇧4
357 It remains only to decide how the variable `x` 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 `x`. 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:
364 varx = fun (n : int) -> n
366 That is, variables in this system denote the identity function!
368 The result of evaluating this tree will be a boxed integer: a function
369 from any integer `n` to `(+ 1 (* (/ 6 n)) 4)`.
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 reason the `map2` function looked familiar is that it seems to involve the `S` combinator. In fact, the `mapply`/`¢` operator for the Reader monad is exactly `\ff xx n -> (ff n) (xx n)`, or the **S** combinator. `map2 f xx yy` for the Reader monad is `(f ○ xx) ¢ yy`, where `○` is function composition, which implements `map` for the Reader monad. So in other words, `map2 f xx yy` is `S (f ○ xx) yy`.
375 We've seen this before as a strategy for translating a binding
376 construct into a set of combinators. To remind you, here is a part of
377 the general scheme for translating a lambda abstract into Combinatory
378 Logic. The translation function `[.]` translates a lambda term into a
379 term in Combinatory Logic:
383 [\a.M] = K[M] (assuming a not free in M)
384 [\a.(MN)] = S[\a.M][\a.N]
386 The reason we can make do with this subset of the full translation
387 scheme is that we're making the simplifying assumption that there is
388 at most a single lambda involved. So once again we have the identity
389 function **I** as the translation of the bound variable, **K** as the function
390 governing expressions that don't contain an instance of the bound
391 variable, **S** as an operation that manages the applicative combination of complex
395 ## Jacobson's Variable Free Semantics as a Reader Monad
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.
403 More specifically, it will turn out that Jacobson's geach combinator
404 *g* is exactly our `lift` operator, and her binding combinator *z* is
405 exactly our `bind` (though with the arguments reversed).
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:
413 ; Jacobson's analysis of "Everyone_i thinks he_i left"
414 let g = \f u. \x. f (u x) in
415 let z = \f u. \x. f (u x) x in
417 let everyone = \P. FORALL x (P x) in
419 everyone (z thinks (g left he))
421 ~~> FORALL x (thinks (left x) x)
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.
427 Second, *g* plays the role of transmitting a binding dependency for an
428 embedded constituent to a containing constituent.
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:
436 everyone (z thinks (g (t bill) (g said (g left he))))
438 ~~> FORALL x (thinks (said (left x) bill) x)
441 If you compare Jacobson's values for *g* and *z* to the functions in
442 the reader monad given above, you'll see that Jacobson's *g*
443 combinator is exactly our `map` operator. Furthermore, Jacobson's *z*
444 combinator is identital to `>>=`, except with the order of the
445 arguments reversed (i.e., `(z f u) == (u >>= f)`).
447 (The `t` combinator in the derivations above is given by `t x =
448 \xy.yx`; it handles situations in which English word order reverses
449 the usual function/argument order.)
452 Jacobson's variable-free semantics is essentially a Reader monad.
454 One of the peculiar aspects of Jacobson's system is that binding is
455 accomplished not by applying *z* to the element that will (in some
456 pre-theoretic sense) bind the pronoun, here, *everyone*, but rather by
457 applying *z* instead to the predicate that will take *everyone* as an
458 argument, here, *thinks*.
461 ## The Reader monad for intensionality
463 [This section has not been revised since 2010, so there may be a few
464 places where it doesn't follow the convetions we've adopted this time;
465 nevertheless, it should be followable.]
467 Now we'll look at using the Reader monad to do intensional function application.
469 In Shan (2001) [Monads for natural
470 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
471 making expressions sensitive to the world of evaluation is conceptually
472 the same thing as making use of the Reader monad.
473 This technique was beautifully re-invented
474 by Ben-Avi and Winter (2007) in their paper [A modular
476 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
477 though without explicitly using monads.
479 All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
480 To run it, download the file, start OCaml, and say
482 # #use "intensionality-monad.ml";;
484 Note the extra `#` attached to the directive `use`.
486 First, the familiar linguistic problem:
490 Ann believes [Bill left].
491 Ann believes [Cam left].
493 We want an analysis on which the first three sentences can be true at
494 the same time that the last sentence is false. If sentences denoted
495 simple truth values or booleans, we have a problem: if the sentences
496 *Bill left* and *Cam left* are both true, they denote the same object,
497 and Ann's beliefs can't distinguish between them.
499 The traditional solution to the problem sketched above is to allow
500 sentences to denote a function from worlds to truth values, what
501 Montague called an intension. So if `s` is the type of possible
502 worlds, we have the following situation:
506 Extensional types Intensional types Examples
507 -------------------------------------------------------------------
511 VP e->t (s->e)->s->t left
512 Vt e->e->t (s->e)->(s->e)->s->t saw
513 Vs t->e->t (s->t)->(s->e)->s->t thought
516 This system is modeled on the way Montague arranged his grammar.
517 There are significant simplifications compared to Montague: for
518 instance, determiner phrases are thought of here as corresponding to
519 individuals rather than to generalized quantifiers.
521 The main difference between the intensional types and the extensional
522 types is that in the intensional types, the arguments are functions
523 from worlds to extensions: intransitive verb phrases like "left" now
524 take so-called "individual concepts" as arguments (type s->e) rather than plain
525 individuals (type e), and attitude verbs like "think" now take
526 propositions (type s->t) rather than truth values (type t).
527 In addition, the result of each predicate is an intension.
528 This expresses the fact that the set of people who left in one world
529 may be different than the set of people who left in a different world.
531 Normally, the dependence of the extension of a predicate to the world
532 of evaluation is hidden inside of an evaluation coordinate, or built
533 into the the lexical meaning function, but we've made it explicit here
534 in the way that the intensionality monad makes most natural.
536 The intensional types are more complicated than the extensional
537 types. Wouldn't it be nice to make the complicated types available
538 for those expressions like attitude verbs that need to worry about
539 intensions, and keep the rest of the grammar as extensional as
540 possible? This desire is parallel to our earlier desire to limit the
541 concern about division by zero to the division function, and let the
542 other functions, like addition or multiplication, ignore
543 division-by-zero problems as much as possible.
545 So here's what we do:
547 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:
557 let left1 (x:e) = true;;
558 let saw1 (x:e) (y:e) = y < x;;
560 left1 ann;; (* true *)
561 saw1 bill ann;; (* true *)
562 saw1 ann bill;; (* false *)
564 So here's our extensional system: everyone left, including Ann;
565 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
566 order we're using is VOS, verb-object-subject.)
568 Now we add intensions. Because different people leave in different
569 worlds, the meaning of *leave* must depend on the world in which it is
572 let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
573 left ann 1;; (* true: Ann left in world 1 *)
574 left cam 2;; (* false: Cam didn't leave in world 2 *)
576 This new definition says that everyone always left, except that
577 in world 2, Cam didn't leave.
579 Note that although this general *left* is sensitive to world of
580 evaluation, it does not have the fully intensionalized type given in
581 the chart above, which was `(s->e)->s->t`. This is because
582 *left* does not exploit the additional resolving power provided by
583 making the subject an individual concept. In semantics jargon, we say
584 that *leave* is extensional with respect to its first argument.
586 Therefore we will adopt the general strategy of defining predicates
587 in a way that they take arguments of the lowest type that will allow
588 us to make all the distinctions the predicate requires. When it comes
589 time to combine this predicate with monadic arguments, we'll have to
590 make use of various lifting predicates.
592 Likewise, although *see* depends on the world of evaluation, it is
593 extensional in both of its syntactic arguments:
595 let saw x y w = (w < 2) && (y < x);;
596 saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
597 saw bill ann 2;; (* false: no one saw anyone in world 2 *)
599 This (again, partially) intensionalized version of *see* coincides
600 with the `saw1` function we defined above for world 1; in world 2, no
603 Just to keep things straight, let's review the facts:
606 World 1: Everyone left.
607 Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
608 World 2: Ann left, Bill left, Cam didn't leave.
612 Now we are ready for the intensionality monad:
615 type 'a intension = s -> 'a;;
616 let unit x = fun (w:s) -> x;;
617 (* as before, bind can be written more compactly, but having
618 it spelled out like this will be useful down the road *)
619 let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
622 Then the individual concept `unit ann` is a rigid designator: a
623 constant function from worlds to individuals that returns `'a'` no
624 matter which world is used as an argument. This is a typical kind of
625 thing for a monad unit to do.
627 Then combining a predicate like *left* which is extensional in its
628 subject argument with an intensional subject like `unit ann` is simply bind
631 bind (unit ann) left 1;; (* true: Ann left in world 1 *)
632 bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
634 As usual, bind takes a monad box containing Ann, extracts Ann, and
635 feeds her to the extensional *left*. In linguistic terms, we take the
636 individual concept `unit ann`, apply it to the world of evaluation in
637 order to get hold of an individual (`'a'`), then feed that individual
638 to the extensional predicate *left*.
640 We can arrange for a transitive verb that is extensional in both of
641 its arguments to take intensional arguments:
643 let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
645 This is almost the same `lift2` predicate we defined in order to allow
646 addition in our division monad example. The difference is that this
647 variant operates on verb meanings that take extensional arguments but
648 returns an intensional result. Thus the original `lift2` predicate
649 has `unit (f x y)` where we have just `f x y` here.
651 The use of `bind` here to combine *left* with an individual concept,
652 and the use of `lift2'` to combine *see* with two intensional
653 arguments closely parallels the two of Montague's meaning postulates
654 (in PTQ) that express the relationship between extensional verbs and
655 their uses in intensional contexts.
658 lift2' saw (unit bill) (unit ann) 1;; (* true *)
659 lift2' saw (unit bill) (unit ann) 2;; (* false *)
662 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
664 Finally, we can define our intensional verb *thinks*. *Think* is
665 intensional with respect to its sentential complement, though still extensional
666 with respect to its subject. (As Montague noticed, almost all verbs
667 in English are extensional with respect to their subject; a possible
668 exception is "appear".)
670 let thinks (p:s->t) (x:e) (w:s) =
671 match (x, p 2) with ('a', false) -> false | _ -> p w;;
673 Ann disbelieves any proposition that is false in world 2. Apparently,
674 she firmly believes we're in world 2. Everyone else believes a
675 proposition iff that proposition is true in the world of evaluation.
677 bind (unit ann) (thinks (bind (unit bill) left)) 1;;
679 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
681 bind (unit ann) (thinks (bind (unit cam) left)) 1;;
683 But in world 1, Ann doesn't believe that Cam left (even though he
684 did leave in world 1: `bind (unit cam) left 1 == true`). Ann's thoughts are hung up on
685 what is happening in world 2, where Cam doesn't leave.
687 *Small project*: add intersective ("red") and non-intersective
688 adjectives ("good") to the fragment. The intersective adjectives
689 will be extensional with respect to the nominal they combine with
690 (using bind), and the non-intersective adjectives will take
691 intensional arguments.
693 notes: cascade, general env