[[!toc]]
# Continuations
Last week we saw how to turn a list zipper into a continuation-based
list processor. The function computed something we called "the task",
which was a simplified langauge involving control operators.
abSdS ~~> ababdS ~~> ababdababd
The task is to process the list from left to right, and at each "S",
double the list so far. Here, "S" is a kind of control operator, and
captures the entire previous computation. We also considered a
variant in which '#' delimited the portion of the list to be copied:
ab#deSfg ~~> abededfg
In this variant, "S" and "#" correspond to `shift` and `reset`, which
provide access to delimited continuations.
The expository logic of starting with this simplified task is the
notion that as lists are to trees, so is this task to full-blown
continuations. So to the extent that, say, list zippers are easier to
grasp than tree zippers, the task is easier to grasp than full
continuations.
We then presented CPS transforms, and demonstrated how they provide
an order-independent analysis of order of evaluation.
In order to continue to explore continuations, we will proceed in the
followin fashion.
## The continuation monad
Let's take a look at some of our favorite monads from the point of
view of types. Here, `==>` is the Kleisli arrow.
Reader monad: types: Mα ==> β -> α
⇧: \ae.a : α -> Mα
compose: \fghe.f(ghe)e : (Q->MR)->(P->MQ)->(P->MR)
gloss: copy environment and distribute it to f and g
State monad: types: α ==> β -> (α x β)
⇧: \ae.(a,e) : α -> Mα
compose: \fghe.let (x,s) = ghe in fxs
thread the state through g, then through f
List monad: types: α ==> [α]
⇧: \a.[a] : α -> Mα
compose: \fgh.concat(map f (gh))
gloss: compose f and g pointwise
Maybe monad: types: α ==> Nothing | Just α
⇧: \a. Just a
compose: \fgh.
case gh of Nothing -> Nothing
| Just x -> case fx of Nothing -> Nothing
| Just y -> Just y
gloss: strong Kline
Now we need a type for a continuation. A continuized term is one that
expects its continuation as an argument. The continuation of a term
is a function from the normal value of that term to a result. So if
the term has type continuized term has type α, the continuized version
has type (α -> ρ) -> ρ:
Continuation monad: types: Mα => (α -> ρ) -> ρ
⇧: \ak.ka
compose: \fghk.f(\f'.g h (\g'.f(g'h)
gloss: first give the continuation to f, then build
a continuation out of the result to give to
The first thing we should do is demonstrate that this monad is
suitable for accomplishing the task.
We lift the computation `("a" ++ ("b" ++ ("c" ++ "d")))` into
the monad as follows:
t1 = (map1 ((++) "a") (map1 ((++) "b") (map1 ((++) "c") (mid "d"))))
Here, `(++) "a"` is a function of type [Char] -> [Char] that prepends
the string "a", so `map1 ((++) "a")` takes a string continuation k and
returns a new string continuation that takes a string s returns "a" ++ k(s).
So `t1 (\k->k) == "abcd"`.
We can now define a shift operator to perform the work of "S":
shift u k = u(\s.k(ks))
Shift takes two arguments: a string continuation u of type (String -> String) -> String,
and a string continuation k of type String -> String. Since u is the
result returned by the argument to shift, it represents the tail of
the list after the shift operator. Then k is the continuation of the
expression headed by `shift`. So in order to execute the task, shift
needs to invoke k twice.
Note that the shift operator constructs a new continuation by
composing its second argument with itself (i.e., the new doubled
continuation is \s.k(ks)). Once it has constructed this
new continuation, it delivers it as an argument to the remaining part
of the computation!
(map1 ((++) "a") (map1 ((++) "b") (shift (mid "d")))) (\k->k) == "ababd"
Let's just make sure that we have the left-to-right evaluation we were
hoping for by evaluating "abSdeSf":
t6 = map1 ((++) "a")
(map1 ((++) "b")
(shift
(map1 ((++) "d")
(map1 ((++) "e")
(shift (mid "f"))))))
t6 (\k->k) == "ababdeababdef"
As expected.
In order to add a reset operator #, we can have
# u k = k(u(\k.k))
ab#deSf ~~> abdedef
Note that the lifting of the original unmonadized computation treated
prepending "a" as a one-place operation. If we decompose this
operation into a two-place operation of appending combined with a
string "a", an interesting thing happens.
map2 f u v k = u(\u' -> v (\v' -> k(f u' v')))
shift k = k (k "")
t2 = map2 (++) (mid "a")
(map2 (++) (mid "b")
(map2 (++) shift
(map2 (++) (mid "d")
(mid []))))
t2 (\k->k) == "ababdd"
First, we need map2 instead of map1. Second, the type of the shift
operator will be a string continuation, rather than a function from
string continuations to string continuations.
But here's the interesting part: from the point of view of the shift
operator, the continuation that it will be fed will be the entire rest
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,
continuations allow functions to see into the future!
What do you expect will be the result of executing "aScSe" under the
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.
## Viewing Montague's PTQ as CPS
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
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.
## Delimited versus undelimited continuations
## Natural language requries delimited continuations