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.
+