+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 (a : e) = fun (p : e -> t) -> p a
+
+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:
+
+ type 'a continuation = ('a -> 'b) -> 'b
+ c_unit (a : 'a) = fun (p : 'a -> 'b) -> p a
+ c_bind (u : ('a -> 'b) -> 'b) (f : 'a -> ('c -> 'd) -> 'd) : ('c -> 'd) -> 'd =
+ fun (k : 'a -> 'b) -> u (fun (a : 'a) -> f a k)
+
+How similar is it to the List monad? Let's examine the type
+constructor and the terms from the list monad derived above: