First-class continuations are an abstraction that evolved from various
nonstandard control structures such as Landin's J-operator~\cite{landin65},
Reynold's {\tt escape}~\cite{reynolds72}, label variables in
Gedanken~\cite{reynolds70} and PAL~\cite{evans68}, and from the semantic
analyses of general control structures, including jumps~\cite{strachey+74}.
Scheme~\cite{sussman+75} originally introduced a binding construct {\tt (catch
k body)} that captured its own expression continuation and bound it to the
variable {\tt k}, with the expression {\tt body} as the scope of the binding.
The continuation represents the ``rest of the computation,'' and behaves as a
function that takes the value of the expression as its argument and yields the
final result of the evaluation of the remainder of the program.  In a typical
implementation the final result is passed to the interactive top-level, which
prints the result, and continues by evaluating the next expression.

Around 1982 the special-form {\tt catch} was replaced by {\tt
call-with-current-continuation} or {\tt call/cc} for
short~\cite{clinger+85}.  The act of capturing the current
continuation did not require a special variable binding form, but
could be performed by a primitive operator whose argument was a
function that would be applied to the captured continuation. Therefore,
{\tt (catch x body)} becomes {\tt (call/cc (lambda (x) body))} in
Scheme.  This is an example of the well-known technique of replacing
a special variable binding form with an operation acting on a
function, so that variable binding is handled solely by lambda
abstraction.

In an untyped language there is not much to choose between the functional and
binding forms of continuation-capturing construct.  However, in the context of
an ML-like type system, the two differ substantially.  To understand the
distinction, it is helpful to consider the interaction between typing and the
invocation of a captured continuation.  There are two main points.  First,
continuations arise in a program only by capturing the evaluation context of
some expression: there are no expression forms denoting continuations.  Therefore
a continuation expects values of the type of the expression whose evaluation
context the continuation represents.  Second, the invocation of a captured
continuation discards the current evaluation context, passing a value to the
captured, instead of the current, continuation.  Although the passed value
must be consistent with the argument type of the continuation, the result type
is unconstrained since invocations of continuations do not return to the
evaluation context.  (For similar reasons the exception-raising construct of
Standard ML has arbitrary result type.)

For example, if {\tt k} is bound to a continuation expecting an integer value,
we may invoke {\tt k} in several incompatible type contexts, as
in the following expression\footnote{We (temporarily) use ordinary function
application notation to indicate invocation of a continuation.}
\begin{code}
 1 + callcc(fn k =>
               hd(if b
	          then [ (k 3) + 1 ]
	          else 5 :: (k 4)))
\end{code}
Here {\tt k} is invoked in two contexts, one expecting an integer, the other
expecting an integer list.  Since continuation invocations never return, it
makes sense to regard this as a well-typed expression (of type
\verb+int+).

The incorporation of continuation primitives in ML involves making two
related decisions, namely the continuation-capturing construct and the
continuation-invoking construct.  Since ML is a typed language, continuations
should be values of some type, say {\tt $\tau$ cont}, the type of
continuations expecting values of type $\tau$.  The continuation-capturing
constructs may then be given typing rules as follows.  The functional form,
written \verb|callcc| in keeping with the ML lexical conventions, may be
assigned any type of the form
\[
(\tau\ {\tt cont}\rightarrow\tau)\rightarrow\tau
\]
since the body may either invoke the passed continuation, or else return
normally.  Written polymorphically, the type of \verb|callcc| is then
\[
\forall\alpha.(\alpha\ {\tt cont} \rightarrow \alpha)\rightarrow \alpha.
\]
The variable-binding form, written {\tt letcc $k$ in $e$}, has the following
typing rule:
\[
\infrule{A,k{:}\tau\ {\tt cont} \vdash e:\tau}{A\vdash {\tt letcc}\ k\ {\tt in}\
e : \tau}{}
\]
where $A$ is a type assignment giving types to the set of free variables of
$e$.

The choice of functional or binding form of continuation-capturing construct
depends on the definition of the type {\tt $\tau$ cont}.  We consider two
possibilities: regard a continuation as a function that is invoked by
application, or regard a continuation as a new form of value that is invoked
by a special primitive.  In the first case the type {\tt $\tau$ cont} is
rendered as a functional type, whereas in the second it is introduced as a new
primitive type.  We consider each in turn.

If continuations are to be regarded as functions, some provision must be made
for ensuring that the result type is allowed to vary according to context.
This suggests the following polymorphic typing:
\[
{\tt callcc} : \forall \alpha . \forall \beta . ((\alpha \rightarrow \beta)
\rightarrow \alpha) \rightarrow \alpha
\]
But since {\tt k} is lambda-bound in the expression {\tt callcc(fn k => ...)}
this does not give us the freedom to instantiate the polymorphic type variable
{$\beta$} independently at each applied occurrence of {\tt k} within the body
of the abstraction.  Instead we are forced to choose a {\em single} type for
$\beta$ suitable for all applications of {\tt k}, ruling out examples such as the
one considered above.

There are two ways to proceed.  One involves moving the
quantifier over {$\beta$} inward (which could be formally justified by the
observation that {$\beta$} occurs in a positive position in the type
expression), yielding the typing
\[
{\tt callcc} : \forall \alpha . (( \alpha \rightarrow \forall \beta.\beta) \rightarrow \alpha) \rightarrow \alpha,
\]
then replacing the type \(\forall \beta . \beta\), which is not the type
of any defined value, by a new primitive type {\tt void}, resulting in the
typing
\[
{\tt callcc} : \forall \alpha . (( \alpha \rightarrow {\tt void}) \rightarrow \alpha) \rightarrow \alpha.
\]
The type {\tt $\tau$ cont} is then defined to be the type $\tau\rightarrow{\tt
void}$.  To match the type of a continuation invocation (\ie, {\tt void}) with
its context we could either view {\tt void} as a subtype of all types and use a
subsumption rule, which introduces many of the complexities of subtyping into
the type system, or we can simply introduce a polymorphic coercion function
\[
{\tt ignore} : \forall \alpha . {\tt void} \rightarrow \alpha
\]
and surround applications of continuations with a call to {\tt ignore}, as in
\begin{code}
if b then [ ignore(k 3) + 1 ]
     else 5 :: ignore(k 4)
\end{code}
(where {\tt k} is an {\tt int cont}).

As an alternative to {\tt ignore} we can exploit the polymorphic type
system of ML, using {\tt letcc} instead of {\tt callcc}.  The idea is to take
type $\tau\ {\tt cont}$ to stand for the polymorphic type $\forall
\alpha.\tau\rightarrow\alpha$, leading to the following typing rule for
{\tt letcc}:
\[
\infrule{A,k:\forall\alpha.\tau\rightarrow\alpha\vdash e : \tau}{A\vdash {\tt
letcc}\ k\ {\tt in}\ e : \tau}{}
\]
Since $k$ is assigned a polymorphic type, the result type, $\alpha$,
may be chosen freely on a case-by-case basis for each applied
occurrence of $k$.  This rule is consistent with the ML type system in
that {\tt let}-like constructs admit assignment of polymorphic types
to the bound identifier. This method cannot be adapted to {\tt callcc}.
The required type has the form 
$(\forall \alpha.\tau\rightarrow \alpha)\rightarrow\tau$ which lies
outside of the scope of the ML type system.  It is here
that the two constructs differ in an ML-like setting.

Another way of typing continuations, and the one currently adopted
in Standard ML of New Jersey~\cite{appel91}, is to abandon the view that
continuations are functions in the ordinary sense and to consider {\tt $\tau$
cont} as a primitive type with an operation {\tt throw} for invoking a
continuation.  The type of {\tt throw} is given by
\[
{\tt throw} : \forall \alpha . \forall \beta . (\alpha {\tt\ cont}) \rightarrow
(\alpha  \rightarrow \beta),
\]
and hence {\tt throw} is essentially a coercion that turns a continuation into
a function, introducing a separate instance of the type parameter
{$\beta$} at each invocation of the continuation.   Our example becomes
\begin{code}
if b then [ (throw k 3) + 1 ]
     else 5 :: (throw k 4)
\end{code}
where the first and second occurrences of throw receive the types
\(
{\tt int\ cont}\rightarrow{\tt int}\rightarrow{\tt int}
\)
and
\(
{\tt int\ cont}\rightarrow{\tt int}\rightarrow{\tt int\ list},
\)
respectively.

It is easy to define the {\tt cont} and {\tt throw} primitives in
terms of {\tt void} and {\tt ignore}:
\begin{code}
type $\alpha$ cont = $\alpha$ -> void
fun throw k x = ignore(k x).
\end{code}
Defining {\tt void} and {\tt ignore} in terms of {\tt cont} and {\tt
throw} is a bit trickier, but it can be done:
\begin{code}
abstype void = VOID
with
  fun ignore (x:void) : 'a =
      let fun loop() = loop()
      in loop()
      end
  val callcc =
      fn f => callcc(fn k =>
              f((throw k) : 'a -> void))
end
\end{code}
So, in principle, there is not much to distinguish the two approaches.
In practice, it is useful to be able to easily distinguish the
invocation of a continuation from the application of a function.
This is why {\tt cont} and {\tt throw} are the chosen primitives in
Standard ML of New Jersey.

It would seem, then, that there are essentially two alternatives for
representing continuations in ML: as polymorphic functions, using \verb|letcc|
as the capturing construct, and values of a new primitive type, using
\verb|throw| to invoke them.  Although the two are equivalent for the purely
functional fragment of ML, the approach based on a primitive type of
continuations is better-behaved in the context of the full Standard ML
language than is the polymorphic approach.  The problem is that
current schemes for introducing references (assignable cells) in ML
preclude the possibility of storing objects of polymorphic type.  For
instance, if the identity function is stored into a cell, then a
single instance of its polymorphic type must be chosen for all
subsequent retrievals: its polymorphic character is lost.  (See
Tofte's thesis~\cite{tofte88} for further discussion of this point.)
Thus if a continuation was represented as a function of polymorphic
result type, then the result type, which is irrelevant since no result
is actually returned, would have to be fixed when the continuation is
{\em stored}, rather than when it is {\em invoked}.  This would
significantly limit the utility of stored continuations because all
invocations would have to be in the same type context.  The approach based
on a primitive type of continuations does not suffer from this
limitation, and is therefore to be preferred for Standard ML.

We are thus led to the following simple signature for supporting first-class
continuations in Standard ML:
\begin{code}
type \mbox{$\alpha$} cont
val callcc : \mbox{$(\alpha{\tt cont}\to\alpha)\to\alpha$}
val throw : \mbox{$\alpha{\tt cont}\to\alpha\to\beta$}
\end{code}
(We could just as well have taken {\tt letcc} as primitive, but since there is
no advantage in doing so, it is simpler to introduce {\tt callcc} as a new
constant of polymorphic type.)

Some examples will suggest how first-class continuations are used in
practice. The simplest and earliest use of continuations was to
provide an escape, as in the following function that returns the
product of a list of integers.
If a zero is found the answer is returned via a continuation and
no multiplications are performed.
\begin{code}
fun prod l =
    callcc(fn exit =>
      let fun loop [] = 1
	    | loop(0::t) = throw exit 0
	    | loop(h::t) = h * loop t
      in loop l
      end)
\end{code}

Another common application is to implement coroutines.  Here
an interesting typing issue arises.  A common technique is to resume a
coroutine by passing the continuation of the current coroutine as the
argument to the continuation representing the resumed coroutine.
If {\tt state} is the type representing the state of a coroutine,
this leads naively to the circular identification
\[
{\tt state} = {\tt state\ cont}
\]
We cannot solve this identity directly, but we can use a datatype
declaration to define the type {\tt state} recursively.  This is illustrated
by the following example of a pair of coroutines, one producing and
the other consuming a sequence of integers.
\begin{code}
datatype state = S of state cont

fun resume(S k: state) : state =
    callcc(fn k': state cont =>
              throw k (S k'))

val buffer = ref 0

fun produce(n: int, cons: state) =
    (buffer := n; produce(n+1, resume(cons)))

fun consume(prod: state) =
    (print(!buffer); consume(resume prod))

fun pinit (n: int) : state =
    callcc(fn k : state cont =>
              produce(n,S k))

fun prun () = consume(pinit(0))
\end{code}
Coroutines can be generalized to lightweight processes or threads.
Continuations have been used as the basis for the implementations of several
process facilities for Standard ML of New Jersey,
some of which use preemptive
scheduling~\cite{reppy89,cooper90,ramsey90,sufrin89}.

The following example uses stored continuations to implement a simple
backtracking scheme.
\begin{code}
let
 val stack : unit cont list ref = ref []
 fun pushstate(k : unit cont) =
     stack := k :: !stack
 fun popstate() = stack := tl(!stack)
 fun backtrack() : 'a =
     case !stack
       of [] => raise Error
        | k :: r => (stack := r; throw k ())
 fun alt(a:unit -> unit,b:unit -> unit) =
     callcc(fn exit =>
 	(callcc(fn k => (pushstate k;
 			 a();
 			 popstate();
 			 throw exit ()));
         b()))
in \ldots {\em backtracking application} \ldots
end
\end{code}
Calls of {\tt alt} can be nested (i.e. inside of the actions {\tt a}
and {\tt b}), and {\tt backtrack} can be called in any type context.

Another use of continuations is to provide a clean, typed interface
for asynchronous signal handling~\cite{reppy90}.  In Standard ML of New Jersey
the type of a signal handler is {\tt (int * unit cont) -> unit cont},
where the argument is a pair consisting of a count of pending signals of the
kind being handled and a continuation representing the state of the interrupted
process.  The continuation returned by the signal handler is typically
used to resume the interrupted process after signals have been unmasked,
but it can also provide an alternative continuation, for instance one
that aborts the computation and returns to top-level.  The signal handling module
provides functions to set handlers for each signal and to mask all
signals.

%Introducing continuations into an interactive system such as Standard
%ML of New Jersey requires special care. Because it is possible to grab
%the continuation of a particular interaction the notion of a
%top-level expression returning more than once must be well defined. In a
%language like Scheme, where interaction is typically implemented as a
%side-effecting read-eval-print loop, returning a new value for a
%previous interaction causes no harm: continuations do not undo
%side-effects. In ML, on the other hand, interaction is thought of as
%incrementally opening a new scope for each top-level declaration.
%Without continuations there is no way to ever leave this scope. 
%However, with continuations it is possible to return to a previous
%interaction and lose all subsequent bindings. While this
%implementation is possible it inflicts a high cost on those who do not
%use continuations. Most implementations of ML do use side-effects to
%alter the growing top-level environment.
%
%Another possibility (the one chosen by Standard ML of New Jersey) is
%to exclude the top-level from all continuations.  This is similar to
%adding a prompt~\cite{felleisen+88} at each top-level declaration.
%This enforces a kind of master/slave coroutine relation between the
%top-level loop and the object level evaluation that it invokes. Not
%only does this allow efficient implementation of top-level bindings it
%also helps minimize the accessible context when exporting an
%executable image generated by a function (using the {\tt exportFn}
%function of Standard ML of New Jersey).  It also properly assigns
%responsibility for printing results and performing top-level bindings
%to the top level, not to the object-level computation.

There is a subtle issue concerning the behavior of continuations in an
interactive system.  Unless the context of a continuation is carefully
defined and controlled one can subvert the type system.  The following
sequence of top-level declarations illustrates the problem.
\begin{code}
val c = ref NONE : int cont option ref;
val n:int = callcc(fn k => (c := SOME k; 2));
val b:bool =
    let val SOME k' = !c in throw k' 3 end;
\end{code}
We are dealing with expression continuations that merely deliver a
value; the binding of that value in the top-level environment and the
printing of a report for the user are the responsibility of the
interactive top-level.\footnote{The interface between the interactive
system and the object level evaluation is similar to a {\em
prompt}~\cite{felleisen+88}.} So the evaluation context represented by
the continuation {\tt k} stored in {\tt c} is limited to the right
hand side of the declaration of {\tt n}, of type {\tt int}.  When this
continuation is fetched and invoked in the right hand side of the
declaration of {\tt b}, that expression returns the value 3, which the
top-level would erroneously interpret as a boolean value.  To prevent
this anomaly we must enforce a strict association between a continuation and its
top-level context that determines the type of the answer returned.
The continuation should ``expire'' when this
context changes and if it is invoked after it has expired
this should be detected and should generate an error message.

In Standard ML of New Jersey, expiration of continuations is enforced
by timestamping continuations.  Each time a top-level evaluation is
begun a new stamp {\em v} is generated and pushed onto a stack.  The
initial continuation used for that evaluation will finish by popping
the stack and comparing the top value with {\em v}, and if they differ
it will signal an error.  A stack of stamps is used because
``top-level'' evaluations may be nested when files are loaded with the
{\em use} function.

Another interesting issue is the relation between continuations and
exception handling.  In the dynamic semantics of Standard ML, an
expression can produce either a normal value or an exception packet
indicating that an exception has been raised but not handled during
the evaluation of the expression.  Therefore the dynamic context of an
expression, {\em i.e.} its continuation, must be able to deal with
either sort of result.  In effect, one could think of the dynamic
context of an expression in ML as a pair of continuations, one for the
``normal'' value return, the other giving the exception handling
context.  This suggests possible new primitives that would provide
access to the exception handling part of a continuation, either by
invoking a continuation with an exception packet instead of a normal
value, or by extracting the ``exception handler'' part of a
continuation as a separate object.  One reason why such primitives should
not be provided is that in conjunction with asynchronous signal handling
they introduce the possibility of asynchronous exceptions.  The
existence of asynchronous exceptions makes it impossible to statically
verify that a particular expression cannot raise a particular
exception, precluding some compiler optimizations.
