+To bad this digression, though it ties together various
+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 we won't
+belabor the construction of the bind function, the derivation is
+similar to the List monad just given:
+
+<pre>
+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)
+</pre>
+
+How similar is it to the List monad? Let's examine the type
+constructor and the terms from the list monad derived above: