We present the library as an implementation of an abstract machine derived by elaborating the definitional machine. The abstract view lets us distill a minimalistic API, scAPI, sufficient for implementing multi-prompt delimited control. We argue that a language system that supports exception and stack-overflow handling supports scAPI. With byte- and native-code OCaml systems as two examples, our library illustrates how to use scAPI to implement multi-prompt delimited control in a typed language. The approach is general and has been used to add multi-prompt delimited control to other existing language systems.
caml-shift-talk.pdf [182K]
Slides of the talk at FLOPS10, April 21, 2010
shift as a green fork(2)
The example used in the talk to introduce the delimcc library
shift/reset, control/prompt, shift0, control0
delimited continuation operators with multiple, arbitrarily typed
prompts. The library has been fruitfully used since 2006, for
implementing (delimited) dynamic binding, probabilistic programming,
CGI programming with nested transactions, efficient and comprehensible
direct-style code generators, normalization of MapReduce-loop bodies
by evaluation, and automatic bundling of RPC requests. This web site
details these and other examples of using delimcc.
The delimcc library was the first direct implementation of
delimited control in a typed, mainstream, mature language. It
captures only the needed prefix of the current continuation, requires
no code transformations, and integrates with native-language
exceptions. Exception handlers may be captured in delimited
continuations (and re-instated when the captured continuation is
installed); exceptions remove the prompts along the way. The
implementation has no typing problems, no bizarre 'a cont types, and
no use for magic.
The delimcc library is a pure library and makes no changes to the OCaml system -- neither to the compiler nor to the run-time system. Therefore the library is perfectly compatible with any OCaml program and any (compiled) OCaml library. The delimcc library has no performance or other effect on the code that does not capture delimited continuations.
The native- and byte-code versions of the library implement the
identical interface, described in delimcc.mli.
The two versions share the very same OCaml code. Only the C code files,
implementing scAPI, vary between byte- and native-code. Using the native-code
delimcc is identical to the byte-code version; the sole
change is invoking the ocamlopt compiler to build the project.
The byte-code version of the delimcc library supports serialization
of captured continuations. The library defines a convenient debugging
primitive show_val to outline the structure of any OCaml value.
The very operation of capturing and reinstalling a delimited continuation will always be faster in byte-code than in the native code. A captured byte-code continuation is a uniform sequence of values and code pointers. In contrast, the corresponding captured native-code delimited continuation -- a portion of the C stack -- is not only bigger but also contains unboxed values. We have to refer to frame tables to figure out which stack slots contain heap pointers. Manipulating the stack required extra care and effort to please GC. Since the captured native-code continuation contains the mixture of boxed and unboxed values, it is not an ordinary OCaml value, requiring a custom GC scanning function. Custom-scanned data types can be emulated without any changes to OCaml, thanks to GC hooks. Alas, the emulation does not seem to be efficient.
The library has been tested with OCaml 3.08-3.12.0, 4.00.1, 4.04, 4.06, 4.07, 4.11.1 and 4.14.1 on i386 and amd64 Linux and FreeBSD platforms (using GCC 5.3, 7.2, 8.2, 11.2 and clang 5.0.1 to compile the C code). Since the OCaml byte-code is portable, the byte-code delimcc should work on any supported architecture. The native-code part can probably be used on other architectures whose stack grows downwards. The library contains no custom assembly code and is written to be a portable client of the OCaml run-time.
The library is distributed under the MIT license.
testd0.ml
contains many simple examples of using delimited control.R. Kent Dybvig, Simon Peyton Jones, and Amr Sabry:
A Monadic Framework for Delimited Continuations
J. Functional Programming, v17, N6, pp. 687--730, 2007
Delimited Control in OCaml, Abstractly and Concretely
The explanation of the implementation techniques
Persistent twice-delimited continuations
The explanation of the serialization of captured delimited continuations
cc-monad.ml [8K]
For historical interest: the original, indirect,
monadic-style implementation. Oct 27, 2005.
The executable semantics takes form of an embedded DSL for delimited control. Therefore, the code has to be written in a particular stylized way, shown below. After all, the semantics was developed for theory sake and hence is minimalistic: the fewer and simpler are the operations, the simpler and shorter the proofs.
For an example we take the famous Danvy-Filinski test of delimited control, written in Scheme as
(+ 10 (reset (+ 2 (shift k (+ 100 (k (k 3)))))))
; --> 117
(it also works with shift0). In the executable denotational
semantics, the example takes the following form:
module ExDF(D:Delimcc) = struct
open D (* D is the interface of the delimcc DSL *)
(* First, a bit of syntax sugar: D is a very bare-bone DSL.
It also distinguishes expressions and values, in types
*)
(* A macro to apply a computation: in contrast, ($$) applies a value *)
let ($$>) v e = let_ e (fun x -> v $$ x)
(* Add an expression to an integer value *)
let (++%) v e = let_ (add $$ v) (fun fv -> let_ e (fun ev -> fv $$ ev))
(* The example itself *)
let ans =
let_ (newpr ()) @@ fun p0 ->
int 10 ++%
pushpr p0 (int 2 ++% sh0 p0 (fun sk -> int 100 ++% (sk $$> (sk $$ int 3))))
end
To run the example, we supply an implementation of the
Delimcc interface, which provides denotations of Delimcc
operations in terms of OCaml functions and data types:
let module M = ExDF(RDelimcc) in M.ansThe denotation of
M.ans is computed as an OCaml integer 117, as
expected.
In contrast, here is how the example looks with the delimcc library:
let test5 =
let p0 = new_prompt () in
10 + push_prompt p0 @@ fun () ->
2 + shift0 p0 (fun sk -> 100 + sk (sk 3))
The delimcc library can be used with the existing OCaml code as it is,
without any need to embed or stylize anything. Control operations
deliver OCaml values directly, with no wrappers; hence the ordinary
OCaml addition can be used to add to the result of shift0.
Also for contrast, here is the same example in Haskell, using the
CCExc implementation described elsewhere on the page:
test5 = runIdentity . runCC $
incr 10 . pushPrompt ps $
incr 2 . shiftP ps $ \sk -> incr 100 $ sk =<< (sk 3)
where
incr :: Monad m => Int -> m Int -> m Int
incr n = ((return . (n +)) =<<)
All in all, the executable denotational semantics is not too difficult
to use in practice; in fact, it is no more bothersome than using
delimited control monads in Haskell.delimcc_semantics.ml [7K]
The executable denotational semantics, along with two tests (sample
code using it)
bench_nondet.ml [9K]
Gasbichler and Sperber's micro-benchmark of delimited control
(implementing the amb operator).
The executable denotational semantics turns out to be rather close to delimcc in
performance.
All three libraries provide monad transformers, with basic operations
to capture and reinstall delimited continuations: pushPrompt,
shift, shift0, control, takeSubCont/pushSubCont. All three
libraries support multiple, typed prompts. All three libraries are
quite distinct from the original implementation in Dybvig, Peyton
Jones, Sabry's paper. For instance, none of the new libraries use
unsafeCoerce. All three implementations are derived from the
specification of delimited control: from the reduction semantics or
from the definitional interpreter. The new libraries are faster.
The new libraries differ in: performance; ease of understanding;
constraints on the base monad or the prompt types; flavors of prompts
and support for global prompts. The libraries are named CCRef,
CCExc and CCCxe.
The library CCRef is the closest to the interface of Dybvig, Peyton Jones
and Sabry. It is derived from the definitional interpreter using the
implementation techniques described and justified in the FLOPS 2010
paper. The monad transformer CC implemented by CCRef
requires the base monad to support reference cells. In other words,
the base monad must be a member of the type class Mutable:
that is, it must be IO, ST, STM or their transformer. CCRef
adds to the original interface the frequently used
abortP as a primitive.
As one may guess from their names, the libraries CCExc and CCCxe
are closely related. CCCxe is derived as a CPS version of CCExc.
CCCxe is sometimes more efficient; it is always less perspicuous. Both
libraries provide the identical interface and are interchangeable. It
seems that CCExc is faster at delimited control but imposes more
overhead on the conventional code; CCCxe is dual. It pays to use CCCxe
in code with long stretches of determinism punctuated by fits and
restarts.
The library CCExc is the most direct implementation of the bubble-up
reduction semantics of multi-prompt delimited control.
The library stands out in not being based on the
continuation monad. Rather, the monad of CCExc is an extension of
the Error monad: a monad for restartable exceptions. The library
offers not one monad transformer but a family (CC p)
parameterized by the prompt flavor p.
The library defines several prompt flavors; the users are welcome
to define their own.
Prompt flavors are inherently like exception flavors (the FLOPS 2010
paper even calls prompts `exception types' or `exception envelopes').
Control.Exception defines singular global exceptions such as
BlockedOnDeadMVar. There are global exceptions like
ErrorCall parameterized by the error string. There are
closed global variants, such as ArithException,
with the fixed number of alternatives. There is also
SomeException, with any number of potential alternatives.
Users may define their own exception types, whose visibility may be
restricted to a module or a package. Finally, one may even generate
distinct expression types dynamically, although that is seldom needed.
The libraries CCExc and CCCxe support all these flavors. On one end is
the prompt flavor PS w. There is only one prompt of that flavor, ps,
which is globally defined and does not have to be passed
around. The monad transformer (CC (PS w)) then is the
monad transformer for regular, single-prompt delimited continuations,
for the answer-type w. The Danvy/Filinski test, which looks in Scheme as
(display (+ 10 (reset (+ 2 (shift k (+ 100 (k (k 3))))))))appears as follows in Haskell:
test5 = (print =<<) . runCC $
incr 10 . pushPrompt ps $
incr 2 . shiftP ps $ \sk -> incr 100 $ sk =<< (sk 3)
where
incr :: Monad m => Int -> m Int -> m Int
incr n = ((return . (n +)) =<<)
One should read the operator (=<<), the flipped bind,
as the ``call-by-value application'', akin to application in call-by-value
languages like Scheme. The application f =<< e
first evaluates the argument e, performing its effects.
The result is passed to f, which is evaluated in turn.
The application sk 3 is an optimized version of
sk =<< (return 3).
The appearance of print tells us that test5
is the IO computation. If we rather had the result of test5
as a pure value (an integer), we merely need to apply runIdentity
to the the runCC expression.
The sample code file Generator1.hs shows one example of
PS; the file SRReifT.hs of the LogicT library
is a larger example. The sample code file Generator2.hs
demonstrates why we may need several prompts, perhaps with different
types. CCExc offers several flavors of multiple prompts: closed
unions P2 and open unions PP,
PM and PD. The open unions are like
SomeException. The prompt flavor PD
carries an extra integer identifier to further distinguish prompts of the
same type. We may therefore dynamically generate an arbitrary number of
PD prompts, which was required in Dybvig, Peyton Jones and
Sabry's framework.
Historical note: the implementation CCRef is not really new:
its first version was written back in 2005. It
inspired the direct implementation of delimited control for OCaml,
which underwent several distillations and re-derivation based on
abstract machine and became the general method of implementing delimited
control. The current CCRef is the application of that general method
(in fact, most of the CCRef code is translated from OCaml) -- testifying
that abstract machines are abstract indeed, but helpful.
CC-delcont-alt, CC-delcont-ref, CC-delcont-exc and
CC-delcont-cxe packages on Hackage
contain all Haskell code belowCCExc.hs [9K]
CCCxe.hs [9K]
CCRef.hs [20K]
The implementations of the three libraries
Mutation.hs [<1K]
Basic interface for reference cell, used by CCRef
CC_Test.hs [7K]
Regression test suite, with many examples of different flavors of
prompts
Bench_nondet.hs [10K]
A micro-benchmark for estimating the overhead of exercising
delimited control. The benchmark does not help in measuring the
indirect overhead, imposed by the libraries on the code that
that uses no delimited control operators. Therefore, the benchmark is
not realistic.
Generator1.hs [3K]
Generator2.hs [7K]
More interesting sample code, implementing generators like those of Python.
The second file tells why one prompt is not enough.
CAG-talk.pdf [168K]
PDF page 57 defines the bubble-up (bottom-up) reduction semantics of
multi-prompt delimited control, which is implemented by CCExc
as written.
Executable direct denotational semantics of multiprompt delimited control
The CCExc library looks like an implementation of the executable
denotational semantics, using Haskell as the metalanguage
LogicT - backtracking monad transformer with fair
operations and pruning
The LogicT library has been ported to the new implementation of delimited
control, CCExc and CCCxe.
One of the sample applications, of a computer playing
5x5 tic-tac-toe against itself, was used as a macro-benchmark of the
new libraries. The end of the file TicTacToe.hs summarizes the results.
The new libraries are faster.
The particularly elegant application of the calculus is the typed
sprintf: sprintf format_expression arg1 arg2 ....
The type system ensures that the number and the types of format specifiers
in format_expression agree with the number and the types
of arg1, etc. With control operators supporting
the answer-type modification and polymorphism, sprintf
is expressible as a regular, simple function.
The Haskell98 implementation below is the first implementation of delimited continuations with answer-type modification, polymorphism, effect typing and type inference in a widely available language. Thanks to parameterized (generalized) monads the implementation is the straightforward translation of the rules of the calculus. Less than a month later Matthieu Sozeau has defined the generalized monad typeclass in Coq. Hence Coq gained the type-safe sprintf.
genuine-shift-reset.txt [6K]
Genuine shift/reset in Haskell98
Announcement of the Haskell implementation and the
explanation of the implementation in terms of parameterized
(generalized) monads. It has been posted on the Haskell mailing list
on Wed, 12 Dec 2007 02:23:52 -0800 (PST).
ShiftResetGenuine.hs [5K]
SRTest.hs [2K]
The complete source code and the test, including the type-safe sprintf
Type-safe Formatted IO
Many more implementations of type-safe sprintf and sscanf
Variable (type)state `monad'
Description of the parameterized (generalized) monads
Matthieu Sozeau: The Proved Program of The Month -
Type-safe printf via delimited continuations
<http://www.lri.fr/perso/~sozeau/repos/coq/misc/shiftreset/GenuineShiftReset.html>
``In this development we define the generalized monad typeclass and one
particular instance: the continuation monad with variable input and output
types. The latter lets us define shift and reset delimited control operators
with effect typing, answer-type modification, and polymorphism. As an
application of these operators, we build a type-safe sprintf.''
SRDSL.hs [4K]
Emulating direct-style
The two distinguished features of OchaCaml are the type system
for shift/reset with the answer-type
modification and polymorphism, and the direct style of its control
operators. The first feature permits the examples of delimited
control that are not possible with the Cont monad.
Direct-style lets us write expressions with nested applications,
typical of applicative programming. We attempt to emulate both
features in Haskell, so to write OchaCaml examples similarly to
the way they are written in OchaCaml.
We rely on RebindableSyntax to hide parameterized monad plumbing as
much as possible.
cupto to multi-prompt versions of control, shift0 and
shift -- providing the superset of the interface proposed by Dybvig,
Peyton Jones and Sabry.
The library relies on call/cc for capturing continuations. As any other
implementation of delimited control in terms of call/cc, including
the original Filinski's implementation of shift, the library must
be used with extreme care in the presence of other effects:
dynamic binding, exceptions, or independent uses of call/cc.
The Scheme implementation of delimcc attests to the generality
of the scAPI-based approach to implementing delimited control. The
presented code is the straightforward translation of the
CCRef Haskell code. Although the present code works on
any R5RS Scheme system, good performance should be expected only on
the systems that implement call/cc
efficiently, such as Chez Scheme, Scheme48, Gambit, Larceny.
By specializing the code to the single prompt and to the
shift operator, we obtain a new implementation of shift/reset
in R5RS Scheme. Even on systems that support call/cc
only inefficiently, this implementation has an advantage of not
leaking memory. The captured continuation, reified by shift,
is just the needed prefix of the full continuation,
even if call/cc copies the whole stack. In other words,
we automatically obtain the so-called JAR hack (see shift-reset.scm in Scheme48
distribution).
delimcc-tests.scm [6K]
The test suite
delimcc-simple.scm [7K]
Ordinary shift/reset in R5RS Scheme
This implementation is derived by specializing the multi-prompt
implementation to the single prompt and to the shift operator.
The code includes a few regression tests and two memory-leak tests.
bench-nondet.scm [3K]
A micro-benchmark, due to Gasbichler and Sperber
-F- (similar to cupto) to
+F- (aka control) to +F+ (aka shift).
This R5RS Scheme code is parameterized by two boolean flags: is-shift and
keep-delimiter-upon-effect.
The four combinations of the two flags correspond to the four
delimited control operators. We can change the flags at run-time and
so mutate shift into control at run-time. The regression test
code does exactly that, so it can test all four *F* operators.
The code relies on call/cc for capturing undelimited continuations,
and uses one global mutable cell. This turns out sufficient for
implementing not only shift/reset (Danvy/Filinski) but also for
control/prompt and the other F operators. In contrast to
Sitaram/Felleisen's implementation of control,
our code needs no equality on continuations. Our code is also far
simpler. Our implementation of all four F operators is
direct rather than an emulation, and hence has the best performance.
This implementation immediately leads to a CPS transform for
control/prompt, thus confirming the result by Chung-chieh Shan. That
transform turns almost identical to the one discussed in the
Dybvig, Peyton Jones and Sabry's paper.
Multi-prompt delimited control in R5RS Scheme
R. Kent Dybvig, Simon Peyton Jones, and Amr Sabry:
A Monadic Framework for Delimited Continuations
JFP, v17, N6, pp. 687--730, 2007
dynamic-wind. Fortunately, delimited control operators let
application programmers write dynamic-wind themselves; that function
is no longer a primitive, is no longer hard-to-explain, and no longer
has to be provided by the implementation. We show a sample
code, as a generalization of the familiar re-throwing of
exceptions.
The procedure dynamic-wind is one of the most complex Scheme
procedures. The mere size of its description in R5RS or the draft
R7RS, let alone time to understand it, is telling. And yet
the procedure is indispensable to prevent leaking of resources. Consider
the code that uses call/cc for a non-local exit from processing file
data:
(call/cc (lambda (exit)
(with-input-from-file "file-name" (lambda ()
(let ((x (read)))
(if (some-test x) (exit #f))
(process x))))))
The Scheme procedure with-input-from-file takes
care of opening the file, and closing it upon return. Alas, if the
non-local exit is taken the file will remain open.
The problems are more serious than the mere failure to close the file. Here is an example of a non-local transfer of control silently breaking the implementation of dynamic binding. Suppose we are writing a pretty-printer and introduce a dynamically bound parameter for the target line width. We implement this parameter using the efficient technique of so-called ``shallow binding''.
(define current-line-width 80)
(define (with-new-line-width new-lw thunk)
(let*
((old current-line-width)
(_ (set! current-line-width new-lw))
(r (thunk))
(_ (set! current-line-width old)))
r))
(define (task title)
(display title)
(display "Current line width: ") (display current-line-width) (newline))
(define (ex2 flag)
(task "Begin. ")
(call/cc (lambda (exit)
(with-new-line-width 120
(lambda ()
(task "Inner1. ")
(if flag (exit #f))
(task "Inner2. ")))))
(task "End. "))
The task "Inner" is executed in its own dynamic environment, when
current-line-width is bound to 120 from the default 80. Whereas the
transcript of running (ex2 #f) shows that current-line-width
is restored at the end, for (ex2 #t), current-line-width is still
120 at the end. The non-local transfer of control broke the implementation.
We must use dynamic-wind when re-binding the dynamic variable, so to
restore the old binding on normal or `abnormal' exit.
(define (with-new-line-width-dw new-lw thunk)
(let ((old #f))
(dynamic-wind
(lambda () ; before-thunk
(set! old current-line-width)
(set! current-line-width new-lw))
thunk ; real work
(lambda () ; after-thunk
(set! current-line-width old))
)))
The code also restores the new binding when the dynamic scope is re-entered
through the captured continuation -- see the example in the accompanying
code.
Obviously the same problems occur if we use delimited continuation
operators rather than call/cc for non-local transfer of
control. Delimited control also needs something like dynamic-wind.
Fortunately, delimited control lets us write dynamic-wind ourselves.
Instead of shift, we shall use a wholly equivalent
control operator yield. Many uses of shift are actually yield.
(Since shift can be written in terms of yield, and vice versa,
no expressivity is lost.)
(define (yield-record-tag) yield-record-tag)
(define (make-yield-record v k)
(list yield-record-tag v k))
(define-syntax try-yield
(syntax-rules ()
((try-yield exp (r on-r) (v k on-y))
(let ((exp-r exp))
(if (and (pair? exp-r) (eq? (car exp-r) yield-record-tag))
(let ((v (cadr exp-r)) (k (caddr exp-r))) on-y)
(let ((r exp-r)) on-r))))))
(define (yield v) (shift k (make-yield-record v k)))
Here is the implementation of dynamic-wind, with the standard
interface.
(define (dyn-wind-yield before-thunk thunk after-thunk)
(let loop ((th (lambda () (reset (thunk)))))
(before-thunk)
(let ((res (th)))
(after-thunk)
(try-yield res
(r r) ; return the result
(v k
(let ((reenter (yield v)))
(loop (lambda () (k reenter)))))
))))
It is the drop-in replacement for R5RS dynamic-wind. Really:
call/cc can also be written in terms of yield. The accompanying code
demonstrates how old examples of call/cc and dynamic-wind continue
to work when both are re-implemented in terms of yield.
The last example in the accompanying code shows a simple generator, or two coroutines, each with its own dynamic environment:
(define (ex7)
(task "Begin. ")
(for-loop (lambda () ; generator
(with-new-line-width-yl 120
(lambda ()
(task "Inner1. ")
(yield 1)
(task "Inner2. ")
(yield 2)
(task "Inner3. "))))
(lambda (v) ; loop body
(display "Yielded value: ") (display v) (newline)
(task "Loop body. ")))
(task "End. "))
We see from the transcript that switching coroutines also switches the binding
to current-line-width, in and out, several times.
We have demonstrated that delimited control operators, yield in particular,
let us implement `finally'-like constructs such as dynamic-wind.
The implementation is quite like the standard implementation of finally
in terms of exception-handling primitives, keeping in mind that
yield is akin to a (multiply) restartable exception.