The three approches are:
-* Rethinking the list monad;
-* Montague's PTQ treatment of DPs as generalized quantifiers; and
-* Refunctionalizing zippers (Shan: zippers are defunctionalized continuations);
+[[!toc]]
Rethinking the list monad
-------------------------
then we can deduce the unit and the bind:
- runit x:'a -> 'a reader = fun (e:env) -> x
+ r_unit x:'a -> 'a reader = fun (e:env) -> x
Since the type of an `'a reader` is `fun e:env -> 'a` (by definition),
-the type of the `runit` function is `'a -> e:env -> 'a`, which is a
+the type of the `r_unit` function is `'a -> e:env -> 'a`, which is a
specific case of the type of the *K* combinator. So it makes sense
that *K* is the unit for the reader monad.
We have to open up the `u` box and get out the `'a` object in order to
feed it to `f`. Since `u` is a function from environments to
-objects of type `'a`, we'll have
+objects of type `'a`, the way we open a box in this monad is
+by applying it to an environment:
.... f (u e) ...
This subexpression types to `'b reader`, which is good. The only
-problem is that we don't have an `e`, so we have to abstract over that
-variable:
+problem is that we invented an environment `e` that we didn't already have ,
+so we have to abstract over that variable to balance the books:
fun e -> f (u e) ...
This types to `env -> 'b reader`, but we want to end up with `env ->
-'b`. The easiest way to turn a 'b reader into a 'b is to apply it to
+'b`. Once again, the easiest way to turn a `'b reader` into a `'b` is to apply it to
an environment. So we end up as follows:
r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) = f (u e) e
And we're done.
+[This bind is a simplified version of the careful `let a = u e in ...`
+constructions we provided in earlier lectures. We use the simplified
+versions here in order to emphasize similarities of structure across
+monads; the official bind is still the one with the plethora of `let`'s.]
+
The **State Monad** is similar. We somehow intuit that we want to use
the following type constructor:
But where is the reasoning that led us to this unit and bind?
And what is the type `['a]`? Magic.
-So let's take a *completely useless digressing* and see if we can
+So let's make a completely useless digression and see if we can
gain some insight into the details of the List monad. Let's choose
type constructor that we can peer into, using some of the technology
we built up so laboriously during the first half of the course. I'm
and a `z` that will turn our hand-crafted lists into standard Ocaml
lists, so that they will print out.
+<pre>
# let cons h t = h :: t;; (* Ocaml is stupid about :: *)
# l'_bind (fun f z -> f 1 (f 2 z))
(fun i -> fun f z -> f i (f (i+1) z)) cons [];;
- : int list = [1; 2; 2; 3]
+</pre>
Ta da!
elements of the course, has *no relevance whatsoever* to the topic of
continuations.
+Montague's PTQ treatment of DPs as generalized quantifiers
+----------------------------------------------------------
+
+We've hinted that Montague's treatment of DPs as generalized
+quantifiers embodies the spirit of continuations (see de Groote 2001,
+Barker 2002 for lengthy discussion). Let's see why.
+
+First, we'll need a type constructor. As you probably know,
+Montague replaced individual-denoting determiner phrases (with type `e`)
+with generalized quantifiers (with [extensional] type `(e -> t) -> t`.
+In particular, the denotation of a proper name like *John*, which
+might originally denote a object `j` of type `e`, came to denote a
+generalized quantifier `fun pred -> pred j` of type `(e -> t) -> t`.
+Let's write a general function that will map individuals into their
+corresponding generalized quantifier:
+
+ gqize (x:e) = fun (p:e->t) -> p x
+
+This function wraps up an individual in a fancy box. That is to say,
+we are in the presence of a monad. The type constructor, the unit and
+the bind follow naturally. We've done this enough times that I won't
+belabor the construction of the bind function, the derivation is
+similar to the List monad just given:
+
+ type 'a continuation = ('a -> 'b) -> 'b
+ c_unit (x:'a) = fun (p:'a -> 'b) -> p x
+ c_bind (u:('a -> 'b) -> 'b) (f: 'a -> ('c -> 'd) -> 'd): ('c -> 'd) -> 'd =
+ fun (k:'a -> 'b) -> u (fun (x:'a) -> f x k)
+
+How similar is it to the List monad? Let's examine the type
+constructor and the terms from the list monad derived above:
+
+ type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
+ l'_unit x = fun f -> f x
+ l'_bind u f = fun k -> u (fun x -> f x k)
+
+(I performed a sneaky but valid eta reduction in the unit term.)
+
+The unit and the bind for the Montague continuation monad and the
+homemade List monad are the same terms! In other words, the behavior
+of the List monad and the behavior of the continuations monad are
+parallel in a deep sense. To emphasize the parallel, we can
+instantiate the type of the list' monad using the Ocaml list type:
+
+ type 'a c_list = ('a -> 'a list) -> 'a list
+ let c_list_unit x = fun f -> f x;;
+ let c_list_bind u f = fun k -> u (fun x -> f x k);;
+
+Have we really discovered that lists are secretly continuations?
+Or have we merely found a way of simulating lists using list
+continuations? Both perspectives are valid, and we can use our
+intuitions about the list monad to understand continuations, and vice
+versa. The connections will be expecially relevant when we consider
+indefinites and Hamblin semantics on the linguistic side, and
+non-determinism on the list monad side.
+
+Refunctionalizing zippers
+-------------------------
+