--- /dev/null
+[[!toc]]
+
+Monads
+------
+
+Start by (re)reading the discussion of monads in the lecture notes for
+week 6 [Towards Monads](http://lambda.jimpryor.net//week6/#index4h2).
+In those notes, we saw a way to separate thining about error
+conditions (such as trying to divide by zero) from thinking about
+normal arithmetic computations. We did this by making use of the
+Option monad: in each place where we had something of type `int`, we
+put instead something of type `int option`, which is a sum type
+consisting either of just an integer, or else some special value which
+we could interpret as signaling that something had gone wrong.
+
+The goal was to make normal computing as convenient as possible: when
+we're adding or multiplying, we don't have to worry about generating
+any new errors, so we do want to think about the difference between
+ints and int options. We tried to accomplish this by defining a
+`bind` operator, which enabled us to peel away the option husk to get
+at the delicious integer inside. There was also a homework problem
+which made this even more convenient by mapping any bindary operation
+on plain integers into a lifted operation that understands how to deal
+with int options in a sensible way.
+
+[Linguitics note: Dividing by zero is supposed to feel like a kind of
+presupposition failure. If we wanted to adapt this approach to
+building a simple account of presupposition projection, we would have
+to do several things. First, we would have to make use of the
+polymorphism of the `option` type. In the arithmetic example, we only
+made use of int options, but when we're composing natural language
+expression meanings, we'll need to use types like `N int`, `Det Int`,
+`VP int`, and so on. But that works automatically, because we can use
+any type for the `'a` in `'a option`. Ultimately, we'd want to have a
+theory of accommodation, and a theory of the situations in which
+material within the sentence can satisfy presuppositions for other
+material that otherwise would trigger a presupposition violation; but,
+not surprisingly, these refinements will require some more
+sophisticated techniques than the super-simple option monad.]
+
+So what examctly is a monad? As usual, we're not going to be pedantic
+about it, but for our purposes, we can consider a monad to be a system
+that provides at least the following three elements:
+
+* A way to build a complex type from some basic type. In the division
+ example, the polymorphism of the `'a option` type provides a way of
+ building an option out of any other type of object. People often
+ use a container metaphor: if `x` has type `int option`, then `x` is
+ a box that (may) contain an integer.
+
+ type 'a option = None | Some of 'a;;
+
+* A way to turn an ordinary value into a monadic value. In Ocaml, we
+ did this for any integer n by mapping an arbitrary integer `n` to
+ the option `Some n`. To be official, we can define a function
+ called unit:
+
+ let unit x = Some x;;
+ val unit : 'a -> 'a option = <fun>
+
+ So `unit` is a way to put something inside of a box.
+
+* A bind operation (note the type):
+
+ let bind m f = match m with None -> None | Some n -> f n;;
+ val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>
+
+ `bind` takes two arguments (a monadic object and a function from
+ ordinary objects to monadic objects), and returns a monadic
+ object.
+
+ Intuitively, the interpretation of what `bind` does is like this:
+ the first argument computes a monadic object m, which will
+ evaluate to a box containing some ordinary value, call it `x`.
+ Then the second argument uses `x` to compute a new monadic
+ value. Conceptually, then, we have
+
+ let bind m f = (let x = unwrap m in f x);;
+
+ The guts of the definition of the `bind` operation amount to
+ specifying how to unwrap the monadic object `m`. In the bind
+ opertor for the option monad, we unwraped the option monad by
+ matching the monadic object `m` with `Some n`--whenever `m`
+ happend to be a box containing an integer `n`, this allowed us to
+ get our hands on that `n` and feed it to `f`.
+
+So the "Option monad" consists of the polymorphic option type, the
+unit function, and the bind function.
+
+A note on notation: some people use the infix operator `>==` to stand
+for `bind`. I really hate that symbol. Following Wadler, I prefer to
+infix five-pointed star, or on a keyboard, `*`.
+
+
+The Monad laws
+--------------
+
+Just like good robots, monads must obey three laws designed to prevent
+them from hurting the people that use them or themselves.
+
+* Left identity: unit is a left identity for the bind operation.
+ That is, for all `f:'a -> 'a M`, where `'a M` is a monadic
+ object, we have `(unit x) * f == f x`. For instance, `unit` is a
+ function of type `'a -> 'a option`, so we have
+
+<pre>
+# let ( * ) m f = match m with None -> None | Some n -> f n;;
+val ( * ) : 'a option -> ('a -> 'b option) -> 'b option = <fun>
+# let unit x = Some x;;
+val unit : 'a -> 'a option = <fun>
+# unit 2 * unit;;
+- : int option = Some 2
+</pre>
+
+ The parentheses is the magic for telling Ocaml that the
+ function to be defined (in this case, the name of the function
+ is `*`, pronounced "bind") is an infix operator, so we write
+ `m * f` or `( * ) m f` instead of `* m f`.
+
+* Associativity: bind obeys a kind of associativity, like this:
+
+ (m * f) * g == m * (fun x -> f x * g)
+
+ If you don't understand why the lambda form is necessary, you need
+ to look again at the type of bind. This is important.
+
+ For an illustration of associativity in the option monad:
+
+<pre>
+Some 3 * unit * unit;;
+- : int option = Some 3
+Some 3 * (fun x -> unit x * unit);;
+- : int option = Some 3
+</pre>
+
+ Of course, associativity must hold for arbitrary functions of
+ type `'a -> M 'a`, where `M` is the monad type. It's easy to
+ convince yourself that the bind operation for the option monad
+ obeys associativity by dividing the inputs into cases: if `m`
+ matches `None`, both computations will result in `None`; if
+ `m` matches `Some n`, and `f n` evalutes to `None`, then both
+ computations will again result in `None`; and if the value of
+ `f n` matches `Some r`, then both computations will evaluate
+ to `g r`.
+
+* Right identity: unit is a right identity for bind. That is,
+ `m * unit == m` for all monad objects `m`. For instance,
+
+<pre>
+# Some 3 * unit;;
+- : int option = Some 3
+</pre>
+
+Now, if you studied algebra, you'll remember that a *monoid* is an
+associative operation with a left and right identity. For instance,
+the natural numbers along with multiplication form a monoid with 1
+serving as the left and right identity. That is, temporarily using
+`*` to mean arithmetic multiplication, `1 * n == n == n * 1` for all
+`n`, and `(a * b) * c == a * (b * c)` for all `a`, `b`, and `c`. As
+presented here, a monad is not exactly a monoid, because (unlike the
+arguments of a monoid operation) the two arguments of the bind are of
+different types. But if we generalize bind so that both arguments are
+of type `'a -> M 'a`, then we get plain identity laws and
+associativity laws, and the monad laws are exactly like the monoid
+laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>).
+
+
+Monad outlook
+-------------
+
+We're going to be using monads for a number of different things in the
+weeks to come. The first main application will be the State monad,
+which will enable us to model mutation: variables whose values appear
+to change as the computation progresses. Later, we will study the
+Continuation monad.
+
+The intensionality monad
+------------------------
+
+In the meantime, we'll see a linguistic application for monads:
+intensional function application. 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 a *reader monad* (which
+we'll see again soon). 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"`.
+
+Here's the idea: since people can have different attitudes towards
+different propositions that happen to have the same truth value, we
+can't have sentences denoting simple truth values. Then if John
+believed that the earth was round, it would force him to believe
+Fermat's last theorem holds, since both propositions are equally true.
+The traditional solution 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 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
+</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.) 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 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.
+
+<pre>
+type 'a intension = s -> 'a;;
+let unit x (w:s) = x;;
+
+let ann = unit 'a';;
+let bill = unit 'b';;
+let cam = unit 'c';;
+</pre>
+
+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:
+
+<pre>
+# let bind m f (w:s) = f (m w) w;;
+val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b = <fun>
+# bind (unit 'a') unit 1;;
+- : char = 'a'
+</pre>
+
+We'll assume that this and the other laws always hold.
+
+We now build up some extensional meanings:
+
+ let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
+
+This function says that everyone always left, except for Cam in world
+2 (i.e., `left 2 'c' == false`).
+
+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:
+
+<pre>
+let extapp fn arg w = fn w (arg w);;
+
+extapp left ann 1;;
+# - : bool = true
+
+extapp left cam 2;;
+# - : bool = false
+</pre>
+
+`extapp` stands for "extensional function application".
+So Ann left in world 1, but Cam didn't leave in world 2.
+
+A transitive predicate:
+
+ let saw w x y = (w < 2) && (y < x);;
+ extapp (extapp saw bill) ann 1;; (* true *)
+ extapp (extapp saw bill) ann 2;; (* false *)
+
+In world 1, Ann saw Bill and Cam, and Bill saw Cam. No one saw anyone
+in world two.
+
+Good. Now for intensions:
+
+ let intapp fn arg w = fn w arg;;
+
+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.
+
+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:
+
+<pre>
+let lift pred w arg = bind arg (fun x w -> pred w x) w;;
+
+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 *)
+</pre>
+
+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.)
+
+Likewise for extensional transitive predicates like "saw":
+
+<pre>
+let lift2 pred w arg1 arg2 =
+ bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;;
+intapp (intapp (lift2 saw) bill) ann 1;; (* true: Ann saw Bill in world 1 *)
+intapp (intapp (lift2 saw) bill) ann 2;; (* false: No one saw anyone in world 2 *)
+</pre>
+
+Crucially, an intensional predicate does not use `bind` to consume its
+arguments. Attitude verbs like "thought" are intensional with respect
+to their sentential complement, but extensional with respect to their
+subject (as Montague noticed, almost all verbs in English are
+extensional with respect to their subject; a possible exception is "appear"):
+
+<pre>
+let think (w:s) (p:s->t) (x:e) =
+ match (x, p 2) with ('a', false) -> false | _ -> p w;;
+</pre>
+
+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.
+
+<pre>
+intapp (lift (intapp think
+ (intapp (lift left)
+ (unit 'b'))))
+ (unit 'a')
+1;; (* true *)
+</pre>
+
+So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
+
+The `lift` is there because "think Bill left" is extensional wrt its
+subject. The important bit is that "think" takes the intension of
+"Bill left" as its first argument.
+
+<pre>
+intapp (lift (intapp think
+ (intapp (lift left)
+ (unit 'c'))))
+ (unit 'a')
+1;; (* false *)
+</pre>
+
+But even in world 1, Ann doesn't believe that Cam left (even though he
+did: `intapp (lift left) cam 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.
+
+Finally, note that within an intensional grammar, extensional funtion
+application is essentially just bind:
+
+<pre>
+# let swap f x y = f y x;;
+# bind cam (swap left) 2;;
+- : bool = false
+</pre>