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 thoughtThis 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. If you're curious about the initial `s`'s in the extensional types, they're there because the behavior of these expressions depends on which world they're evaluated at. If you are in a situation in which you can hold the evaluation world constant, you can further simplify the extensional types. Usually, the dependence of the extension of an expression on the evaluation world is hidden in a superscript, or built into the lexical interpretation function. 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 intensional 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). The intenstional types are more complicated than the intensional types. Wouldn't it be nice to keep the complicated types to just those 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: type s = int;; type e = char;; type t = bool;; 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 'a intension = s -> 'a;; let unit x (w:s) = x;; let ann = unit 'a';; let bill = unit 'b';; let cam = unit 'c';; In our monad, the intension of an extensional type `'a` is `s -> 'a`, a function from worlds to extensions. Our unit will be the constant function (an instance of the K combinator) that returns the same individual at each world. Then `ann = unit 'a'` is a rigid designator: a constant function from worlds to individuals that returns `'a'` no matter which world is used as an argument. Let's test compliance with the left identity law: # let bind u f (w:s) = f (u w) w;; val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b =