Now we'll look at using monads to do intensional function application. This is just another application of the Reader monad, not a new monad. In Shan (2001) [Monads for natural language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that making expressions sensitive to the world of evaluation is conceptually the same thing as making use of the Reader monad. This technique was beautifully re-invented by Ben-Avi and Winter (2007) in their paper [A modular approach to intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf), though without explicitly using monads. All of the code in the discussion below can be found here: [[intensionality-monad.ml]]. To run it, download the file, start OCaml, and say # #use "intensionality-monad.ml";; Note the extra `#` attached to the directive `use`. First, the familiar linguistic problem: Bill left. Cam left. Ann believes [Bill left]. Ann believes [Cam left]. We want an analysis on which the first three sentences can be true at the same time that the last sentence is false. If sentences denoted simple truth values or booleans, we have a problem: if the sentences *Bill left* and *Cam left* are both true, they denote the same object, and Ann's beliefs can't distinguish between them. The traditional solution to the problem sketched above is to allow sentences to denote a function from worlds to truth values, what Montague called an intension. So if `s` is the type of possible worlds, we have the following situation:
Extensional types              Intensional types       Examples
-------------------------------------------------------------------

S         t                    s->t                    John left
DP        e                    s->e                    John
VP        e->t                 (s->e)->s->t            left
Vt        e->e->t              (s->e)->(s->e)->s->t    saw
Vs        t->e->t              (s->t)->(s->e)->s->t    thought
This system is modeled on the way Montague arranged his grammar. There are significant simplifications: for instance, determiner phrases are thought of as corresponding to individuals rather than to generalized quantifiers. The main difference between the intensional types and the extensional types is that in the intensional types, the arguments are functions from worlds to extensions: intransitive verb phrases like "left" now take so-called "individual concepts" as arguments (type s->e) rather than plain individuals (type e), and attitude verbs like "think" now take propositions (type s->t) rather than truth values (type t). In addition, the result of each predicate is an intension. This expresses the fact that the set of people who left in one world may be different than the set of people who left in a different world. (Normally, the dependence of the extension of a predicate to the world of evaluation is hidden inside of an evaluation coordinate, or built into the the lexical meaning function, but we've made it explicit here in the way that the intensionality monad makes most natural.) The intensional types are more complicated than the extensional types. Wouldn't it be nice to make the complicated types available for those expressions like attitude verbs that need to worry about intensions, and keep the rest of the grammar as extensional as possible? This desire is parallel to our earlier desire to limit the concern about division by zero to the division function, and let the other functions, like addition or multiplication, ignore division-by-zero problems as much as possible. So here's what we do: 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: type s = int;; type e = char;; type t = bool;; let ann = 'a';; let bill = 'b';; let cam = 'c';; let left1 (x:e) = true;; let saw1 (x:e) (y:e) = y < x;; left1 ann;; (* true *) saw1 bill ann;; (* true *) saw1 ann bill;; (* false *) So here's our extensional system: everyone left, including Ann; and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word order we're using is VOS, verb-object-subject.) Now we add intensions. Because different people leave in different worlds, the meaning of *leave* must depend on the world in which it is being evaluated: let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;; left ann 1;; (* true: Ann left in world 1 *) left cam 2;; (* false: Cam didn't leave in world 2 *) This new definition says that everyone always left, except that in world 2, Cam didn't leave. Note that although this general *left* is sensitive to world of evaluation, it does not have the fully intensionalized type given in the chart above, which was `(s->e)->s->t`. This is because *left* does not exploit the additional resolving power provided by making the subject an individual concept. In semantics jargon, we say that *leave* is extensional with respect to its first argument. Therefore we will adopt the general strategy of defining predicates in a way that they take arguments of the lowest type that will allow us to make all the distinctions the predicate requires. When it comes time to combine this predicate with monadic arguments, we'll have to make use of various lifting predicates. Likewise, although *see* depends on the world of evaluation, it is extensional in both of its syntactic arguments: let saw x y w = (w < 2) && (y < x);; saw bill ann 1;; (* true: Ann saw Bill in world 1 *) saw bill ann 2;; (* false: no one saw anyone in world 2 *) This (again, partially) intensionalized version of *see* coincides with the `saw1` function we defined above for world 1; in world 2, no one saw anyone. Just to keep things straight, let's review the facts:
     World 1: Everyone left.
              Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.              
     World 2: Ann left, Bill left, Cam didn't leave.
              No one saw anyone.
Now we are ready for the intensionality monad:
type 'a intension = s -> 'a;;
let unit x = fun (w:s) -> x;;
(* as before, bind can be written more compactly, but having
   it spelled out like this will be useful down the road *)
let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
Then the individual concept `unit ann` is a rigid designator: a constant function from worlds to individuals that returns `'a'` no matter which world is used as an argument. This is a typical kind of thing for a monad unit to do. Then combining a predicate like *left* which is extensional in its subject argument with an intensional subject like `unit ann` is simply bind in action: bind (unit ann) left 1;; (* true: Ann left in world 1 *) bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *) As usual, bind takes a monad box containing Ann, extracts Ann, and feeds her to the extensional *left*. In linguistic terms, we take the individual concept `unit ann`, apply it to the world of evaluation in order to get hold of an individual (`'a'`), then feed that individual to the extensional predicate *left*. We can arrange for a transitive verb that is extensional in both of its arguments to take intensional arguments: let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));; This is almost the same `lift2` predicate we defined in order to allow addition in our division monad example. The difference is that this variant operates on verb meanings that take extensional arguments but returns an intensional result. Thus the original `lift2` predicate has `unit (f x y)` where we have just `f x y` here. The use of `bind` here to combine *left* with an individual concept, and the use of `lift2'` to combine *see* with two intensional arguments closely parallels the two of Montague's meaning postulates (in PTQ) that express the relationship between extensional verbs and their uses in intensional contexts.
lift2' saw (unit bill) (unit ann) 1;;  (* true *)
lift2' saw (unit bill) (unit ann) 2;;  (* false *)
Ann did see bill in world 1, but Ann didn't see Bill in world 2. Finally, we can define our intensional verb *thinks*. *Think* is intensional with respect to its sentential complement, though still extensional with respect to its subject. (As Montague noticed, almost all verbs in English are extensional with respect to their subject; a possible exception is "appear".) let thinks (p:s->t) (x:e) (w:s) = match (x, p 2) with ('a', false) -> false | _ -> p w;; Ann disbelieves any proposition that is false in world 2. Apparently, she firmly believes we're in world 2. Everyone else believes a proposition iff that proposition is true in the world of evaluation. bind (unit ann) (thinks (bind (unit bill) left)) 1;; So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave). bind (unit ann) (thinks (bind (unit cam) left)) 1;; But in world 1, Ann doesn't believe that Cam left (even though he did leave in world 1: `bind (unit cam) left 1 == true`). Ann's thoughts are hung up on what is happening in world 2, where Cam doesn't leave. *Small project*: add intersective ("red") and non-intersective adjectives ("good") to the fragment. The intersective adjectives will be extensional with respect to the nominal they combine with (using bind), and the non-intersective adjectives will take intensional arguments.