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 option`s, 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
+expression meanings, we'll need to use types like `N option`, `Det option`,
+`VP option`, 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
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 it 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;;`
+* A complex type that's built around some more basic type. Usually
+ it will be polymorphic, and so can apply to different basic types.
+ In our 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 it to
+ the option `Some n`. In the general case, this operation is
+ known as `unit` or `return.` Both of those names are terrible. This
+ operation is only very loosely connected to the `unit` type we were
+ discussing earlier (whose value is written `()`). It's also only
+ very loosely connected to the "return" keyword in many other
+ programming languages like C. But these are the names that the literature
+ uses.
+
+ The unit/return operation is a way of lifting an ordinary object into
+ the monadic box you've defined, in the simplest way possible. You can think
+ of the singleton function as an example: it takes an ordinary object
+ and returns a set containing that object. In the example we've been
+ considering:
+
+ let unit x = Some x;;
+ val unit : 'a -> 'a option = <fun>
+
+ So `unit` is a way to put something inside of a monadic box. It's crucial
+ to the usefulness of monads that there will be monadic boxes that
+ aren't the result of that operation. In the option/maybe monad, for
+ instance, there's also the empty box `None`. In another (whimsical)
+ example, you might have, in addition to boxes merely containing integers,
+ special boxes that contain integers and also sing a song when they're opened.
+
+ The unit/return operation will always be the simplest, conceptually
+ most straightforward way to lift an ordinary value into a monadic value
+ of the monadic type in question.
+
+* Thirdly, an operation that's often called `bind`. This is another
+ unfortunate name: this operation is only very loosely connected to
+ what linguists usually mean by "binding." In our option/maybe monad, the
+ bind operation is:
+
+ let bind m f = match m with None -> None | Some n -> f n;;
+ val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>
+
+ Note the type. `bind` takes two arguments: first, a monadic "box"
+ (in this case, an 'a option); and second, a function from
+ ordinary objects to monadic boxes. `bind` then returns a monadic
+ value: in this case, a 'b option (you can start with, e.g., int options
+ and end with bool options).
+
+ Intuitively, the interpretation of what `bind` does is like this:
+ the first argument is a monadic value m, which
+ evaluates to a box that (maybe) contains 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 = unbox m in f x);;
+
+ The guts of the definition of the `bind` operation amount to
+ specifying how to unbox the monadic value `m`. In the bind
+ opertor for the option monad, we unboxed the option monad by
+ matching the monadic value `m` with `Some n`---whenever `m`
+ happened to be a box containing an integer `n`, this allowed us to
+ get our hands on that `n` and feed it to `f`.
+
+ If the monadic box didn't contain any ordinary value, then
+ we just pass through the empty box unaltered.
+
+ In a more complicated case, like our whimsical "singing box" example
+ from before, if the monadic value happened to be a singing box
+ containing an integer `n`, then the `bind` operation would probably
+ be defined so as to make sure that the result of `f n` was also
+ a singing box. If `f` also inserted a song, you'd have to decide
+ whether both songs would be carried through, or only one of them.
+
+ There is no single `bind` function that dictates how this must go.
+ For each new monadic type, this has to be worked out in an
+ useful way.
+
+So the "option/maybe monad" consists of the polymorphic option type, the
+unit/return function, and the bind function. With the option monad, we can
+think of the "safe division" operation
- `val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>`
+<pre>
+# let divide' num den = if den = 0 then None else Some (num/den);;
+val divide' : int -> int -> int option = <fun>
+</pre>
- `bind` takes two arguments (a monadic object and a function from
- ordinary objects to monadic objects), and returns a monadic
- object.
+as basically a function from two integers to an integer, except with
+this little bit of option plumbing on the side.
- 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
+A note on notation: Haskell uses the infix operator `>>=` to stand
+for `bind`. Chris really hates that symbol. Following Wadler, he prefers to
+use an infix five-pointed star, or on a keyboard, `*`. Jim on the other hand
+thinks `>>=` is what the literature uses and students won't be able to
+avoid it. Moreover, although ⋆ is OK (though not a convention that's been picked up), overloading the multiplication symbol invites its own confusion
+and Jim feels very uneasy about that. If not `>>=` then we should use
+some other unfamiliar infix symbol (but `>>=` already is such...)
- `let bind m f = (let x = unwrap m in f x);;`
+In any case, the course leaders will work this out somehow. In the meantime,
+as you read around, wherever you see `m >>= f`, that means `bind m f`. Also,
+if you ever see this notation:
- 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`.
+ do
+ x <- m
+ f x
-So the "option monad" consists of the polymorphic option type, the
-unit function, and the bind function. With the option monad, we can
-think of the "safe division" operation
+That's a Haskell shorthand for `m >>= (\x -> f x)`, that is, `bind m f`.
+Similarly:
-<pre>
-# let divide num den = if den = 0 then None else Some (num/den);;
-val divide : int -> int -> int option = <fun>
-</pre>
+ do
+ x <- m
+ y <- n
+ f x y
-as basically a function from two integers to an integer, except with
-this little bit of option frill, or option plumbing, on the side.
+is shorthand for `m >>= (\x -> n >>= (\y -> f x y))`, that is, `bind m (fun x
+-> bind n (fun y -> f x y))`. Those who did last week's homework may recognize
+this.
-A note on notation: Haskell uses 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, `*`.
+(Note that the above "do" notation comes from Haskell. We're mentioning it here
+because you're likely to see it when reading about monads. It won't work in
+OCaml. In fact, the `<-` symbol already means something different in OCaml,
+having to do with mutable record fields. We'll be discussing mutation someday
+soon.)
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
+* **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;;
- : int option = None
</pre>
-The parentheses is the magic for telling Ocaml that the
+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:
+* **Associativity: bind obeys a kind of associativity**. Like this:
- `(m * f) * g == m * (fun x -> f x * g)`
+ (m * f) * g == m * (fun x -> f x * g)
- If you don't understand why the lambda form is necessary (the "fun
- x" part), you need to look again at the type of bind.
+ If you don't understand why the lambda form is necessary (the "fun
+ x" part), you need to look again at the type of bind.
- Some examples of associativity in the option monad:
+ Some examples of associativity in the option monad:
<pre>
# Some 3 * unit * unit;;
</pre>
Of course, associativity must hold for arbitrary functions of
-type `'a -> M 'a`, where `M` is the monad type. It's easy to
+type `'a -> 'a m`, 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
`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,
+* **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;;
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
+of type `'a -> 'a m`, 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>, near the bottom).
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
+To run it, download the file, start OCaml, and say
- # #use "intensionality-monad.ml";;
+ # #use "intensionality-monad.ml";;
Note the extra `#` attached to the directive `use`.
So here's what we do:
-In Ocaml, we'll use integers to model possible worlds:
+In OCaml, we'll use integers to model possible worlds:
- type s = int;;
- type e = char;;
- type t = bool;;
+ 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.
+OCaml booleans will serve for truth values.
<pre>
type 'a intension = s -> 'a;;
We now build up some extensional meanings:
- let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
+ 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`).
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 *)
+ 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;;
+ 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.