of the computation. This includes not only what has come before, but
what will come after it as well. That means when the continuation is
doubled (self-composed), the result duplicates not only the prefix
-(ab ~~> abab), but also the suffix (d ~~> dd). In some sense, then,
+`(ab ~~> abab)`, but also the suffix `(d ~~> dd)`. In some sense, then,
continuations allow functions to see into the future!
What do you expect will be the result of executing "aScSe" under the
-second perspective?
+second perspective? The answer to this question is not determined by
+the informal specification of the task that we've been using, since
+under the new perspective, we're copying complete (bi-directional)
+contexts rather than just left contexts.
+
+It might be natural to assume that what execution does is choose an S,
+and double its context, temporarily treating all other shift operators
+as dumb letters, then choosing a remaining S to execute. If that was
+our interpreation of the task, then no string with more than one S
+would ever terminate, since the number S's after each reduction step
+would always be 2(n-1), where n is the number before reduction.
+
+But there is another equally natural way to answer the question.
+Assume the leftmost S is executed first. What will the value of its
+continuation k be? It will be a function that maps a string s to the
+result of computing `ascSe`, which will be `ascascee`. So `k(k "")`
+will be `k(acacee)`, which will result in `a(acacee)ca(acacee)cee`
+(the parentheses are added to show stages in the construction of the
+final result).
+
+So the continuation monad behaves in a way that we expect a
+continuation to behave. But where did the continuation monad come
+from? Let's consider some ways of deriving the continuation monad.
-This depends on which S is executed first. Assume the first S is
-executed first. What will the value of its continuation k be?
-It will be a function that maps a string s to the result of computing
-ascSe, which will be ascascee. So k(k "") will be k(acacee), which
-will result in a(acacee)ca(acacee)cee (the parenthesese are added to
-show stages in the construction of the final result).
+## Viewing Montague's PTQ as CPS
-Note that this is a different result than assuming that what execution
-does is choose an S, and double its context, treating all other shift
-operators as dumb letters, then choosing a remaining S to execute. If
-that was our interpreation of the task, then no string with more than
-one S would ever terminate (on the bi-directional continuation
-perspective).
+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).
+## How continuations can simulate other monads
-## Viewing Montague's PTQ as CPS
+Because the continuation monad allows the result type ρ to be any
+type, we can choose ρ in clever ways that allow us to simulate other
+monads.
+ Reader: ρ = env -> α
+ State: ρ = s -> (α, s)
+ Maybe: ρ = Just α | Nothing
+You see how this is going to go. Let's see an example by adding an
+abort operator to our task language, which represents what
+we want to have happen if we divide by zero, where what we want to do
+is return Nothing.
+
+ abort k = Nothing
+ mid a k = k a
+ map2 f u v k = u(\u' -> v (\v' -> k(f u' v')))
+ t13 = map2 (++) (mid "a")
+ (map2 (++) (mid "b")
+ (map2 (++) (mid "c")
+ (mid "d")))
+
+ t13 (\k->Just k) == Just "abcd"
+
+ t14 = map2 (++) (mid "a")
+ (map2 (++) abort
+ (map2 (++) (mid "c")
+ (mid "d")))
+
+
+ t14 (\k->Just k) == Nothing
+
+Super cool.
-## How continuations can simulate other monads
## Delimited versus undelimited continuations