previous   next   up   top

Undelimited continuations are co-values rather than functions

 


 

Undelimited continuations are not functions

When one part of a program is being evaluated, producing the result, the rest of the program lies ready to consume it. For example, in the program print 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.

References
Pierre-Louis Curien and Hugo Herbelin: The duality of computation. ICFP 2000
< http://pauillac.inria.fr/~herbelin/publis/icfp-CuHer00-duality+errata.pdf >

 

Vast difference between delimited and undelimited continuations

Whereas an undelimited continuation is the meaning of the whole context, a delimited continuation is the meaning of context's prefix, mapping a context to a wider one. Despite sounding pretty much alike, undelimited and delimited continuations are qualitatively different. Since a delimited continuation is a mapping between contexts, it may truly be a function, which returns and can be composed. Undelimited continuations are not true functions. Undelimited and delimited continuations also differ in expressiveness, and this difference has been proven. First-class delimited continuations can express any expressible computational effect, including exceptions and mutable state. To be precise, any effect that can be emulated by transforming the whole program (into the state-passing--style, into an 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.

References
Andrzej Filinski: Representing Monads. POPL 1994.
< http://www.diku.dk/~andrzej/papers/RM-abstract.html >

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 >

 

Monads for undelimited continuations

The proper implementation of undelimited continuations is surprisingly tricky. In particular, the 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.

Version
The current version is February 2011.
References
CPSs.hs [7K]
Complete Haskell code for the four implementations of the monad of undelimited continuations. The code includes several examples.

 

Recursion from Iteration

Let us call, as Filinski did, the looping computation iteration and identify the least fix-point combinator with recursion:
     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 k
stating 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 proposition
     forall f x k. exists h y. fix f x k = loop h y k
stating that fix is expressible via loop in the continuation monad. Skolemizing, we obtain
     fix f x k = loop (h f x k) (y f x k) k
We 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 k1
for 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) k
can 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.

Version
The current version is (original) February 2003; (monadic) February 2011.
References
Andrzej Filinski: Recursion from Iteration
Lisp and Symbolic Computation, vol. 7, no.1, pp. 11-38 (January 1994)
< http://www.diku.dk/hjemmesider/ansatte/andrzej/papers/RfI.ps.gz >

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.

 

Self-application as the fixpoint of call/cc

Truly call/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.

Here 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.

References
Normal-order direct-style beta-evaluator with syntax-rules, and the repeated applications of call/cc

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



Last updated October 24, 2014

This site's top page is http://okmij.org/ftp/

oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML