--- /dev/null
+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:
+
+
+<pre>
+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
+</pre>
+
+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:
+
+<pre>
+ 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.
+</pre>
+
+Now we are ready for the intensionality monad:
+
+<pre>
+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;;
+</pre>
+
+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.
+
+<pre>
+lift2' saw (unit bill) (unit ann) 1;; (* true *)
+lift2' saw (unit bill) (unit ann) 2;; (* false *)
+</pre>
+
+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.
+
+