```-Extensional types                 Intensional types       Examples
+Extensional types              Intensional types       Examples
-------------------------------------------------------------------

-S         s->t                    s->t                    John left
-DP        s->e                    s->e                    John
-VP        s->e->t                 s->(s->e)->t            left
-Vt        s->e->e->t              s->(s->e)->(s->e)->t    saw
-Vs        s->t->e->t              s->(s->t)->(s->e)->t    thought
+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
```
```+let ann = 'a';;
+let bill = 'b';;
+let cam = 'c';;

-We'll assume that this and the other laws always hold.
+let left1 (x:e) = true;;
+let saw1 (x:e) (y:e) = y < x;;

-We now build up some extensional meanings:
+left1 ann;;
+saw1 bill ann;; (* true *)
+saw1 ann bill;; (* false *)
+```
- let left w x = match (w,x) with (2,'c') -> false | _ -> true;; +So here's our extensional system: everyone left, including Ann; +and Ann saw Bill, but Bill didn't see Ann. (Note that Ocaml word +order is VOS, verb-object-subject.) -This function says that everyone always left, except for Cam in world -2 (i.e., `left 2 'c' == false`). +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: -Then the way to evaluate an extensional sentence is to determine the -extension of the verb phrase, and then apply that extension to the -extension of the subject: + let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;; - let extapp fn arg w = fn w (arg w);; +This new definition says that everyone always left, except that +in world 2, Cam didn't leave. - extapp left ann 1;; - # - : bool = true + 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 *) - extapp left cam 2;; - # - : bool = false +Along similar lines, this general version of *see* coincides with the +`saw1` function we defined above for world 1; in world 2, no one saw anyone. -`extapp` stands for "extensional function application". -So Ann left in world 1, but Cam didn't leave in world 2. +Just to keep things straight, let's get the facts of the world set: -A transitive predicate: +
```+     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.
+```
- let saw w x y = (w < 2) && (y < x);; - extapp (extapp saw bill) ann 1;; (* true *) - extapp (extapp saw bill) ann 2;; (* false *) +Now we are ready for the intensionality monad: -In world 1, Ann saw Bill and Cam, and Bill saw Cam. No one saw anyone -in world two. +
```+type 'a intension = s -> 'a;;
+let unit x (w:s) = x;;
+let bind m f (w:s) = f (m w) w;;
+```
-Good. Now for intensions: +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. - let intapp fn arg w = fn w arg;; +Then combining a prediction like *left* which is extensional in its +subject argument with a monadic subject like `unit ann` is simply bind +in action: -The only difference between intensional application and extensional -application is that we don't feed the evaluation world to the argument. -(See Montague's rules of (intensional) functional application, T4 -- T10.) -In other words, instead of taking an extension as an argument, -Montague's predicates take a full-blown intension. + bind (unit ann) left 1;; (* true: Ann left in world 1 *) + bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *) -But for so-called extensional predicates like "left" and "saw", -the extra power is not used. We'd like to define intensional versions -of these predicates that depend only on their extensional essence. -Just as we used bind to define a version of addition that interacted -with the option monad, we now use bind to intensionalize an -extensional verb: +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*. - let lift pred w arg = bind arg (fun x w -> pred w x) w;; +We can arrange for an extensional transitive verb to take intensional +arguments: - intapp (lift left) ann 1;; (* true: Ann still left in world 1 *) - intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *) + let lift f u v = bind u (fun x -> bind v (fun y -> f x y));; -Because `bind` unwraps the intensionality of the argument, when the -lifted "left" receives an individual concept (e.g., `unit 'a'`) as -argument, it's the extension of the individual concept (i.e., `'a'`) -that gets fed to the basic extensional version of "left". (For those -of you who know Montague's PTQ, this use of bind captures Montague's -third meaning postulate.) +This is the exact same lift predicate we defined in order to allow +addition in our division monad example. -Likewise for extensional transitive predicates like "saw": +
```+lift saw (unit bill) (unit ann) 1;;  (* true *)
+lift saw (unit bill) (unit ann) 2;;  (* false *)
+```