call/cc
call/ccprint 1 + 2*3, the context print [] is the consumer of the
result of the addition, and print 1 + [] is the consumer for
the result of the multiplication. Whereas value is the meaning
of an expression, (undelimited) continuation is the meaning of a context.
Ever-present and implicit, continuations become explicit
when the program is converted to the
continuation-passing style (CPS) or when they are captured by a control
operator such as call/cc. Explicit continuations are often
represented as functions, which can be applied. One must keep
in mind however that an undelimited continuation is not a genuine
function. It does not return, and hence cannot be meaningfully composed.
We alert to the misconception of explicit, or first-class,
undelimited continuations as ordinary functions. The confusion is
wide-spread, for example, in the description and the code for the
Cont monad in Haskell's monad transformer libraries.
We argue for a better call/cc interface, to hopefully reduce
the bewilderment commonly associated with that control operator. We
describe the proper undelimited continuation monad, pointing out that
Haskell's Cont is actually the monad for delimited
continuations. Delimited and undelimited continuations are vastly
different. Delimited continuations are isomorphic to functions, they
do return the result and can be composed. We emphasize the great
help of types in understanding continuations and avoiding their surprises.
Scheme's call/cc might be responsible for mistaking first-class
undelimited continuations as functions: the captured undelimited
continuation k in (call/cc (lambda (k) ...)) indeed looks like
a function and can be applied to a value. It is not a genuine function
however. The expression (k (k 1)), albeit well-formed, is meaningless.
It makes as much sense to compose captured undelimited continuations
as to compose abort or exit `functions.' The call/cc interface
in SML is quite more helpful:
type 'a cont
val callcc: ('a cont -> 'a) -> 'a
val throw: 'a cont -> 'a -> 'b
A captured continuation is represented as the value of an abstract type
'a cont. Since it is not a function, we need an operator, throw, to
pass the continuation a value to consume and so let it `continue.' The
type of throw is similar to the type of the exception-raising raise,
indicating that neither `function' returns.
The untyped CPS transform might also make undelimited continuations
appear as functions. After all, they are represented as
functions -- in the metalanguage. One must clearly distinguish the
metalanguage, in which the CPS code is written, from the object
language, of which the CPS transform is taken.
Types make the distinction clear. An object-language expression
of the type Int has the CPS transform of the metalanguage
type (Int->w)->w, where w is the `answer-type'. An object-language
function, say, Int->Bool, is represented in CPS as the metalanguage
value of the type (Bool->w) -> (Int->w). An object-level continuation
receiving the value Int has the metalanguage type Int->w.
The object-language continuation is represented as the metalanguage
function, whose type sets it apart from representations of
object-language functions.
Distinguishing undelimited continuations and functions not only reduces
confusion but also gives a deep insight into the duality of
computation. A continuation is a co-value. Whereas a term, a producer,
has the type t, the context of the term -- the consumer, or the co-term --
can be given the type NOT t, isomorphic to t -> Falsum.
The answer-type Falsum has no constructors: Informally, it describes
the result of a crashed computer. The type of the
undelimited continuation t -> Falsum
clarifies that although the continuation may look like a function,
it never returns because there is no way to create a Falsum value.
In other words, the `result' of an undelimited continuation may never be
used by the program itself; it is `beyond the grave'.
Therefore, the value of the type t -> Falsum witnesses the
impossibility to produce a value of the type t. The type
t -> Falsum represents the proposition that is the negation
of that of t.
Either-returning style, etc.) can be
expressed with first-class delimited continuations without
the global transformation, see Filinski's ``Representing
Monads.'' In contrast, first-class undelimited continuations cannot
express raising and catching of exceptions. Furthermore, first-class
undelimited continuations, even when aided by exceptions, cannot
express mutable state. The limited expressiveness of undelimited
continuations has been proven by Hayo Thielecke, see the reference and
the abstract below.
One sometimes hears a misleading statement that ``it is
possible to implement Scheme's set! in terms of Scheme's call/cc
and letrec.'' The statement mis-represents
Alan Bawden's observation that according to Scheme standards and common
practice, letrec is implemented in terms of set!; that hidden set!
can be `pried open' with call/cc. Of course letrec can be
implemented without set!, for example, via the fix-point combinator.
The inability of call/cc to express mutable state becomes clear
then. Section 4.4 of Friedman and Sabry's
``Recursion is a Computational Effect'' has the detailed explanation.
One may wonder what is the use of first-class undelimited
continuations then. That is a good question. Many applications that
use call/cc also contain mutable cells holding continuations,
betraying the well-known Filinski's emulation of delimited control via
call/cc and a mutable cell. Undelimited continuations by themselves
are hardly practically useful. The best non-trivial application of
bare call/cc is along the lines of Nick Benton's ``Undoing Dynamic
Typing.'' The paper mentions at the end that in practice `undoing'
should be done within transaction boundaries. The latter calls for
delimited continuations. Given that first-class delimited
continuations -- often emulated via call/cc together with set! --
are strictly more expressive than undelimited ones, and most often used
in practice, one would think that call/cc should have been replaced
by a delimited control operator.
Hayo Thielecke: Contrasting Exceptions and Continuations. 2001
< http://www.cs.bham.ac.uk/~hxt/research/exncontjournal.pdf >
Abstract: ``Exceptions and first-class continuations are the most
powerful forms of control in programming languages. While both are a
form of non-local jumping, there is a fundamental difference between
them. We formalize this difference by proving a contextual equivalence
that holds in the presence of exceptions, but not continuations; and
conversely, we prove an equivalence that holds in the presence of
continuations, but not exceptions. By the same technique, we show that
exceptions and continuations together do not give rise to state, and
that exceptions and state do not give rise to continuations.''
Daniel P. Friedman and Amr Sabry: Recursion is a Computational Effect.
Tech. Rep. TR546, Computer Science Department, Indiana University, December 2000.
< http://www.cs.indiana.edu/~sabry/papers/recursion-monads-tr.pdf >
Nick Benton: Undoing Dynamic Typing. FLOPS 2008.
< http://research.microsoft.com/~nick/newtrans.pdf >
Cont monad in Haskell's
monad transformer library has a couple of imperfections.
Our ideal monad for undelimited continuations: (i) spells out
in syntax and types of its operations that undelimited continuations
are not to be treated as functions; (ii) statically prevents
building or executing computations that break the undelimited continuation
abstraction and depend on the answer-type. We eventually develop
two implementations satisfying both requirements; the second one
is almost the same as Cont but with a crucial distinction of the
higher-rank type for runCont.
The Cont monad in the popular Haskell monad transformer library
does not satisfy the requirements. The captured continuation has the
type of a monadic function. The Cont documentation (through the
current version 2.0.1.0) confirms that view, saying ``Computations are
built up from sequences of nested continuations, terminated by a
final continuation (often id) which produces the final result.
Since continuations are functions which represent the future of
a computation...'' We have already argued that
undelimited continuations are not functions and that one should
forget about the ``final result.'' It behoves for a typed language
to statically enforce the forgetting. Incidentally, in the presence
of first-class undelimited continuations, computations can no longer be
viewed as ``sequences of nested continuations.'' As Peter Landin
said, ``You can enter a room once, and yet leave it twice.''
Our code will show a simple example.
Recall that monad is a technique of embedding an impure, object language,
into a pure functional (meta)language. For an object language
with control effects, the well-known embedding technique is
continuation-passing style (CPS) --
which is what all our monads implement. In CPS, an object
language expression of the base object type a is represented
as a Haskell value of the type (a -> w) -> w where w
is a so-called `answer-type', to be discussed shortly.
An object-language a->b function is represented as Haskell's
a -> ((b->w) -> w) function. An object-language co-value of
the type a, that is, the continuation consuming a value
is represented in Haskell
as the value of the type a->w. We stress
that although the representation of an object language
continuation is a Haskell function, it differs, in type, from
the representation of any object language function. CPS operations
for building primitive computations, extending them, capturing an
undelimited continuation and invoking it have the following form:
return x = \k -> k x
m >>= f = \k -> m (\v -> f v k)
callCC f = \k -> f k k
throw k x = \_ -> k x
All our monads share the above code, modulo newtype-induced
conversions. The monads differ in their treatment of the answer-type w.
An object-language computation cannot know what w is; to it, w
is arbitrary. This fact gives us the first implementation, with the following
types for monadic values and continuations:
newtype CPS1 a = CPS1{unCPS1:: forall w. (a -> w) -> w}
type K1 a = forall w. a -> w
Alas, we cannot write callCC: callCC1 :: (K1 a -> CPS1 a) -> CPS1 a
callCC1 f = CPS1 $ \k -> unCPS1 (f k) k
The type-checker keeps complaining that
the code for callCC identifies w quantified in the type of CPS1
with w quantified in the type of K1. The type-checker has the point.
The answer-type is the type of the value of the crashed computer; the program
cannot make any use of that value, or care of that type. Ostensibly that
is what the types CPS1 and K1 say, that the answer-type
is arbitrary. It cannot be totally arbitrary however: the continuation
captured by callCC leads to the same crashed computer value as the
computation whose continuation has been captured. The code for callCC1
says that the answer-type
of the captured K1 must be the same as that of CPS1. The signature of
callCC1 has no way to express that constraint.A different way to introduce a type whose values cannot be used is to define an algebraic data type with no constructors -- an empty type (disregarding bottom). Monadic values and continuations get the following types:
data Falsum -- no constructors
newtype CPS2 a = CPS2{unCPS2:: (a -> Falsum) -> Falsum}
type K2 a = a -> Falsum
with indeed the same answer-type, Falsum.
Even the program knows that, but it cannot get its values since none exist.
The type-checker now accepts the definitions of all four operations; we can
write any computation with undelimited control effects. Alas, we cannot
execute these computations. To execute a CPS2 a computation,
we need the initial continuation a -> Falsum.
We cannot construct values of that type: Falsum really has no constructors.
The initial continuation (whose invocation leads to the crashed computer,
eventually) should be supplied by the operating or the run-time system.
GHC RTS does supply it.Cheating is always an option. We can run the computation and obtain its result through a side-channel. Since the side-channel is an effect, we need another monad:
newtype CPS3 m a = CPS3{unCPS3:: (a -> m Falsum) -> m Falsum}
type K3 m a = a -> m Falsum
The following code of the run operation instantiates m
to ST s, using a mutable cell to stash away the result of the computation.
The code exhibits lots of partiality, which is inherent, betraying the
essential cheating. Instead of ST s, we could have used the Error
monad Either a. runCPS3 :: (forall m. CPS3 m a) -> a
runCPS3 m = runST (do
res <- newSTRef (error "Continuation has escaped!")
unCPS3 m (\v -> writeSTRef res v >> return undefined)
readSTRef res)
We stress the higher-rank type of runCPS3: we introduced the monad
m only for the sake of runCPS3. The rest of the monadic computation
should stay away from it. The quantification over m keeps the program
away from using m in any way whatsoever.
The implementation CPS3 looks suspiciously like Cont in the
monad transformer library MTL, with the side-channel monad m playing
the role of the answer-type w. Neither should be looked at
by computations. We obtain the final implementation
newtype Cont w a = Cont{unCont:: (a -> w) -> w}
type K w a = a -> w
callCC :: (K w a -> Cont w a) -> Cont w a
callCC f = Cont $ \k -> unCont (f k) k
throw :: K w a -> a -> Cont w b
throw k x = Cont $ \ k_ignored -> k x
runCont :: (forall w. Cont w a) -> a
runCont m = unCont m id
The first difference from the monad-transformer library is the type
of the captured continuation, K w a, corresponding to no object
function. Therefore, we need a special operation to invoke the
continuation: throw. Our implementation thus emphasizes in syntax
and in types the difference between undelimited continuations and
functions. The second, main difference is the higher-rank type of
runCont, ensuring that computations really not have looked at the
answer-type. The answer-type is fixed all throughout, yet a
computation cannot know what it is. Therefore, we may chose w as we
wish -- and we do, after the program has been constructed. The
higher-rank type of runCont hence prevents the program from using
runCont internally to run parts of its computation. No such
restriction exists for MTL's runCont, telling us that the latter is
the monad for delimited continuations.
loop :: Monad m => (a -> m a) -> (a -> m b)
loop g = \x -> g x >>= loop g
fix :: Monad m => ((a -> m b) -> (a -> m b)) -> (a -> m b)
fix f = \x -> f (fix f) x
We wrote the monadic version of loop so that we can get out of it
(e.g., by throwing an exception). According to its type the above fix is the applicative fix-point combinator (like the one
typically used in strict languages), to be distinguished from the very
different, lazy mfix of Haskell. It is trivial to write loop in
terms of fix. Can we do the other way around?Intuitively, that should be possible: after all, any recursive program, however general, is going to be executed on a CPU, which runs in a simple tail-recursive loop. The details are very tricky and the final result is all but intuitive or comprehensible. One wonders how it could ever work. Andrzej Filinski was the first to systematically derive recursion from iteration, in the paper presented at the Continuation Workshop 1992. The journal version developed the example further, making it an excellent illustration for the duality of computation. We show an alternative, shorter derivation -- in Haskell rather than ML, relying on monads and demonstrating forward and backward equational reasoning. The example also shows off the Haskell library of proper undelimited continuations developed above. We solve the problem by equationally deriving a constructive proof of the proposition
forall f x k. exists h y. fix f x k = loop h y kstating that
fix is expressible via loop in the continuation
monad.
Let's first explore our intuition. If we take for a moment g . f to mean
the monadic composition \x -> f x >>= g then after unrolling the definitions
we find that
loop1 g = ... g . g . g . g
fix1 f = f $ f $ f $ f ...
which is the first hint of their duality. The CPU analogy gives us the
second hint: to run a recursive program on bare metal we need to
explicitly deal with the stack, saving and restoring return addresses.
The stack with the saved return addresses is one realization of
undelimited continuations.
As a warm-up, let us look at simple examples of using our fix and loop. To show off fix, we define the factorial with open recursion
in an arbitrary monad:
fact2 :: Monad m => (Int -> m Int) -> (Int -> m Int)
fact2 self n = if n == 0 then return 1 else liftM (n *) (self (n-1))
fact2r = fix fact2 5 >>= print
We tie the knot and run it in the IO monad, printing the result.
Iteration, that is, loop, is easily expressed in terms of the more general
recursion:
loop' g = fix (\s x -> g x >>= s)The proof is simple equational reasoning:
loop' g
= fix (\s x -> g x >>= s) {- definition of loop' -}
= (\s x -> g x >>= s) (fix (\s x -> g x >>= s)) {- definition of fix -}
= (\s x -> g x >>= s) (loop' g) {- definition of loop' -}
= \x -> g x >>= (loop' g) {- beta-reduction -}
= loop g {- definition of loop -}
We now search for an expression of fix in terms of loop. We will be using a monad of undelimited continuations:
newtype CPS3 m a = CPS3{unCPS3:: (a -> m Falsum) -> m Falsum}
For clarity, we will drop CPS3 and unCPS3 conversions,
which operationally the identity anyway. The monad operations take the
following form then: return x = \k -> k x
m >>= f = \k -> m (\v -> f v k)
callCC f = \k -> f k k
throw k x = \_ -> k x
We solve the problem by equationally deriving a constructive proof
of the propositionforall f x k. exists h y. fix f x k = loop h y kstating that
fix is expressible via loop in the continuation monad.
Skolemizing, we obtainfix f x k = loop (h f x k) (y f x k) kWe need to find such functions
h and y that the equality above
holds for the arbitrary f, x, and k.
Unrolling fix and loop and inlining the definition of (>>=) from
the above, gives further equalities
f (fix f) x k = (h f x k) (y f x k) (\v -> loop (h f x k) v k)
f (\x1 k1 -> loop (h f x1 k1) (y f x1 k1) k1) x k
= (h f x k) (y f x k) (\v -> loop (h f x k) v k)
We have to match (\x1 k1 -> loop ...) on the left-hand-side
with (\v -> loop (h f x k) v k) on the right-hand-side.
The first function receives two independent pieces of data,
so the second should too. Thus v must be a pair, (x,k);
the invoking function h will uncurry. The hint
that loop's argument, the `state' to be repeatedly
transformed by the loop function, must be a pair (x,k)
comes also from the low-level point of view.
Recall that x is the argument of the recursive
function, and k is its continuation, the stack with the
return address on it. Together, (x,k) is the stack frame:
the argument plus the return address. A processor running in a loop
is indeed a frame transformer.
Letting v be a pair gives us
f (\x1 k1 -> loop (h f x1 k1) (y f x1 k1) k1) x k
= (h f x k) (y f x k) (\(x1,k1) -> loop (h f x k) (x1,k1) k)
To match the two loop expressions in parentheses, we have to define y f x k = (x,k)
h f x k = h' f
that is, h should not depend of x and k arguments; h' is
to be determined. Substituting these definitions, we obtain f (\x1 k1 -> loop (h' f) (x1,k1) k1) x k
= (h' f) (x,k) (\ (x1,k1) -> loop (h' f) (x1,k1) k)
We need an auxiliary lemma:loop g x k = loop g x k1for any
g, x, k, k1. In other words, loop never invokes
its continuation and therefore can be given any: loop loops and
never returns. We can easily prove the lemma by co-induction.
Applying the lemma gives f (\x1 k1 -> loop (h' f) (x1,k1) k1) x k
= (h' f) (x,k) (\ (x1,k1) -> loop (h' f) (x1,k1) k1)
which can be read (after flipping) as the definition for the
sought h':h' f (x,k) k2 = f (\x1 k1 -> k2 (x1,k1)) x k
We are done. We would like to polish the result: during the derivation,
we broke the monadic abstraction, replacing bind and return
of the CPS monad with their concrete expressions. We want to get
the abstraction back, re-introducing (>>=) and return.
They won't be enough, as we can see by comparing the pattern
of using k in these operations with the pattern in h'.
Our h' not just passes the received continuation around or immediately
invokes it. It also stores continuations in
data structures (pairs). Our resulting expression:
fix f x k = loop (h' f) (x,k) kcan be re-written, using the definition of
callCC from above, as fix :: ((a -> CPS3 m b) -> (a -> CPS3 m b)) -> (a -> CPS3 m b)
fix f x = callCC (\k -> loop (h' f) (x,k))
The definition of h' can be likewise transformed in these steps: h' f (x,k) k2 = f (\x1 k1 -> k2 (x1,k1)) x k
h' f (x,k) k2 = f (\x1 -> callCC (\k1 -> throw k2 (x1,k1))) x (\v -> k v)
giving us the final result: h' :: ((a -> CPS3 m w) -> (b -> CPS3 m w))
-> ((b, K3 m w) -> CPS3 m (a, K3 m w))
h' f (x,k) = callCC (\k2 ->
f (\x1 -> callCC (\k1 -> throw k2 (x1,k1))) x >>= (\v -> throw k v))
The result is achieved by equational reasoning and is correct by construction.
It has indeed worked the first time.
The type of h' makes classical logical sense, expressing the proposition
(f1 -> f2) = (NOT f1 -> NOTNOTNOT f2)keeping in mind that
K3 m w is logically NOT w, reading CPS3 m
as double-negation, and using K3 m (b -> CPS3 m w)
~ NOT (b -> NOTNOT w)
= NOT (NOT b OR (NOTNOT w)) = b AND (NOT w)
~ (b,K m w)
What is left to prove is the fix-point thus obtained being the least one, or the related property of universality. See Filinski's paper for details.
The original version of this article was written in early 2003, in
Scheme, after the independent re-discovery of recursion via iteration.
Unlike Filinski's, our derivation was directly in terms of call/cc
rather than the C operator.
The main hint probably came from the CPU point of view. The original
version too relied on equational reasoning. The present version
uses Haskell, which permits equational reasoning on the code itself.
We no longer have to translate Math into code; Math is code. The monadic style
also gives a shorter derivation.
IterRec.hs [3K]
Complete Haskell code for all the fragments mentioned in the article. The code contains several more examples, of nested and higher-order fix-points, mentioned in Filinski's paper.
Self-application as the fixpoint of call/cc
In Scheme, we can obtain general recursion from call/cc alone, without any loop. Types are again revealing, that the application of call/cc to the identity has the recursive type.
Many faces of the fixed-point combinator
The web page points to several ways of defining the fix-point combinator in OCaml and Haskell without value recursion or iteration.
call/cccall/cc and the fix-point combinator Y are two sides of the
same coin. The following article makes the claims formal and proves
them. Two examples in the article demonstrate that first-class
continuations can be really tricky, and so being formal helps. For
proofs we rely on syntax-rules macros: one macro does a
continuation-passing-style (CPS) transform, and another simple macro
-- which is actually a lambda-calculator -- normalizes the result of
the transform.Theorem: The following expressions are observationally equivalent in call-by-value untyped lambda-calculus.
((call/cc ... (call/cc call/cc)) p)((call/cc ... (call/cc (call/cc id))) p)((lambda (x) (x x)) p)p is a value; (call/cc ...) signify zero or more
applications of call/cc, and id is the identity function. The
article also discusses self-applications of delimited continuation
operators.In this article, continuations, fixpoints, CPS, higher-order syntax, syntax-rule macros and lambda-calculators all come together.
callcc-fixpoint.txt [16K]
Self-application as the fixpoint of call/cc
The first version of the article, posted on the newsgroup comp.lang.scheme on Thu, 18 Sep 2003 23:39:02 -0700
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML