+Montague's conception of determiner phrases as generalized quantifiers
+is a limited form of continuation-passing. (See, e.g., chapter 4 of
+Barker and Shan 2014.) Start by assuming that ordinary DPs such as
+proper names denote objects of type `e`. Then verb phrases denote
+functions from individuals to truth values, i.e., functions of type `e
+-> t`.
+
+The meaning of extraordinary DPs such as *every woman* or *no dog*
+can't be expressed as a simple individual. As Montague argued, it
+works much better to view them as predicates on verb phrase meanings,
+i.e., as having type `(e->t)->t`. Then *no woman left* is true just
+in case the property of leaving is true of no woman:
+
+ no woman: \k.not \exists x . (woman x) & kx
+ left: \x.left x
+ (no woman) (left) = not \exists x . woman x & left x
+
+Montague also proposed that all determiner phrases should have the
+same type. After all, we can coordinate proper names with
+quantificational DPs, as in *John and no dog left*. Then generalized
+quantifier corresponding to the proper name *John* is the quantifier
+`\k.kj`.
+
+At this point, we have a type for our Kliesli arrow and a value for
+our mid. Given some result type (such as `t` in the Montague application),
+
+ α ==> (α -> ρ) -> ρ
+ ⇧a = \k.ka
+
+It remains only to find a suitable value for bind. Montague didn't
+provide one, but it's easy to find:
+
+ bind :: Mα -> (α -> Mβ) -> Mβ
+
+given variables of the following types
+
+ u :: Mα == (α -> ρ) -> ρ
+ f :: α -> Mβ
+ k :: β -> ρ
+ x :: α
+
+We have
+
+ bind u f = \k.u(\x.fxk)
+
+Let's carefully make sure that this types out:
+
+ bind u f = \k. u (\x . f x k)
+ -------- --
+ α -> Mβ α
+ ------------ ------
+ Mβ β -> ρ
+ -- --------------------
+ α ρ
+ ------------- ------------------------
+ (α -> ρ) -> ρ α -> ρ
+ ---------------------------------
+ ρ
+ -----------------------
+ (β -> ρ) -> ρ
+
+Yep!
+
+Is there any other way of building a bind operator? Well, the
+challenge is getting hold of the "a" that is buried inside of `u`.
+In the Reader monad, we could get at the a inside of the box by
+applying the box to an environment. In the State monad, we could get
+at the a by applying to box to a state and deconstructing the
+resulting pair. In the continuation case, the only way to do it is to
+apply the boxed a (i.e., u) to a function that takes an a as an
+argument. That means that f must be invoked inside the scope of the
+functional argument to u. So we've deduced the structure
+
+ ... u (\x. ... f x ...) ...
+
+At this point, in order to provide u with an argument of the
+appropriate type, the argument must not only take objects of type
+α as an argument, it must return a result of type ρ. That means that
+we must apply fx to an object of type β -> ρ. We can hypothesize such
+an object, as long as we eliminate that hypothesis later (by binding
+it), and we have the complete bind operation.
+
+The way in which the value of type α that is needed in order to unlock
+the function f is hidden inside of u is directly analogous to the
+concept of "data hiding" in object-oriented programming. See Pierce's
+discussion of how to extend system F with existential type
+quantification by encoding the existential using continuations.
+
+So the Kliesli type pretty much determines the bind operation.
+
+## What continuations are doing
+
+Ok, we have a continuation monad. We derived it from first
+principles, and we have seen that it behaves at least in some respects
+as we expect a continuation monad to behave (in that it allows us to
+give a good implementation of the task).