The concept of continuations arises naturally in programming: a
conditional branch selects a continuation from the two possible
futures; raising an exception discards a part of the continuation; a
goto continues with the continuation. Although
continuations are implicitly manipulated in every language,
manipulating them explicitly as first-class objects is rarely used
because of the perceived difficulty.
This tutorial aims to give a gentle introduction to
continuations and a taste of programming with first-class delimited
continuations using the control operators
reset. Assuming no prior knowledge on continuations,
the tutorial helps participants write simple co-routines and
non-deterministic searches. The tutorial should make it easier to
understand and appreciate the talks at CW 2011.
We assume basic familiarity with functional programming languages, such as OCaml, Standard ML, Scheme, and Haskell. No prior knowledge of continuations is needed. Participants are encouraged to bring their laptops and program along.
Tutorial notes for OchaCaml and Haskell
A sample shift/reset code in Haskell, in the
Cont monad -- the monad for delimited control
The complete code for the Haskell portion of the tutorial
The search tree is the ordinary tree data type, with branches constructed on demand. The tree is potentially infinite, as is the case in the example below.
data SearchTree a = Leaf a | Node [() -> SearchTree a]We implement three tree traversals, which collect the values from leaf nodes into a list:
dfs, bfs, iter_deepening :: SearchTree a -> [a](Actually we use several versions of breadth-first search, optimized to a different extent.)
Cont monad from the standard monad transformer library
and its operations
implement two primitives: non-deterministically choosing a value
from a finite list, and reifying a computation into a
choose :: [a] -> Cont (SearchTree w) a reify :: Cont (SearchTree a) a -> SearchTree aOther non-deterministic operations --
mplus(to join two computations),
choose'(to choose from a potentially infinite list) -- are all written in terms of
The running example is a simple version of a real
inductive-programming problem: given a sequence of input-output pairs
[(Int,Int)], find an
Int->Int function with that input-output behavior. The
functions to search among are represented by the data structure:
data Exp = K Int -- constant function | X -- identity | Exp :+ Exp -- \x -> f x + g x | Exp :* Exp -- \x -> f x * g xThe solution is the familiar generate-and-test
induct io = reify $ do exp <- an_exp if all (\ (i,o) -> eval exp i == o) io then return exp else failurewhere
an_expgenerates a sample function representation, and the if-expression tests if evaluating it on given inputs gives the desired outputs. The generator of
an_exp = (fmap K $ choose numbers) `mplus` (return X) `mplus` (liftM2 (:+) an_exp an_exp) `mplus` (liftM2 (:*) an_exp an_exp) where numbers = [-2..2]Depth-first search cannot be used for this problem since the search tree is infinite. Breadth-first and iterative deepening are both complete strategies and both find the answer if it exists. For example, for the sequence
[(0,1), (1,1), (2,3)]of input-output pairs, we find
K 1 :+ (X :* (K (-1) :+ X))(which corresponds to the function
1 + x*(x-1)), which indeed has the given behavior. Benchmarking on a slightly bigger problem
[(0,1), (1,1), (2,3), (-1,3)]shows that the optimized breadth-first search takes 303MB whereas iterative deepening takes 64MB of memory (and roughly the same time). Although toy, this inductive programming problem is not simple. For input-output pairs
[(0,1), (1,3), (-1,3), (2,15)], breadth-first search quickly allocates 8GB and is killed by the kernel. Iterative deepening allocates at much slower pace, but still reaches 8GB and dies as well.
Embedded probabilistic programming
The paper explains the reification of non-deterministic programs as lazy search trees. We use the same technique here, only in Haskell rather than OCaml, and without probabilities.
Preventing memoization in (AI) search problems
The explanation of the trick to prevent unwelcome implicit memoizations
Joachim Breitner: dup -- Explicit un-sharing in Haskell
July 2012. <https://arxiv.org/abs/1207.2017>
An extensive discussion of unwanted memoization and ways to prevent it
shift0, etc. are all macro-expressible in terms of each other. Furthermore, the operators
shift0are the members of a single parameterized family, and the standard CPS is sufficient to express their denotational semantics.
The report formally proves that
control implemented via
indeed has its standard reduction semantics.
The report presents the simplest known Scheme implementations of
control0 (similar to
cupto). The method
in the report lets us design 700 more delimited control operators,
to split and compose stack fragments as one thinks fit.
Scheme code with the simplest implementation of
control0 in terms of
The code includes a large set of test cases.
``Lambda the Ultimate'' discussion thread, esp. on the meaning of
The master SXML file of the report
Writing LaTeX/PDF mathematical papers with SXML
Joint work with Ikuo Kobori and Yukiyoshi Kameyama.
Our library depends on the delimcc library of persistent delimited continuations. The captured delimited continuations can be stored on disk, to be later loaded and resumed in a different process. Alternatively, serialized captured continuations can be inserted as an encoded string into a hidden field of the response web form. The use of continuations lets us avoid iterations, relying instead on the `Back button.' Delimited continuations naturally support `thread-local' scope and are quite compact to serialize. The library works with the unmodified OCaml system as it is.
Delimited continuations help us implement nested transactions. The simple blog application demonstrates that a user may repeatedly go back-and-forth between editing and previewing their blog post, perhaps in several windows. The finished post can be submitted only once.
The source code for the library of delimited-continuation--based CGI programming with form validation and nested transactions. The library includes the complete code for the Continuation Fest demos.
cupto), the strong normalization property no longer holds. A single typed prompt already leads to non-termination. The following example has been designed by Chung-chieh Shan, from the example of non-termination of simply typed lambda-calculus with dynamic binding. It uses the OCaml delimited control library. The function
fun () -> Omega: its inferred type is
unit -> 'a; consequently, the evaluation of
loop ()loops forever.
let loop () = let p = new_prompt () in let delta () = shift p (fun f v -> f v v) () in push_prompt p (fun () -> let r = delta () in fun v -> r) delta
Chung-chieh Shan also offered the explanation: the answer
type being an arrow type hides a recursive type. In other words,
unit -> 'a hides the answer
type and the fact the function is impure.
Olivier Danvy has kindly pointed out the similar non-terminating example that he and Andrzej Filinski designed in 1998 using their version of shift implemented in SML/NJ. Their example too relied on the answer type being an arrow type.
cupto, the first delimited control operator with an explicitly typed prompt
Delimited Dynamic Binding
The reformulation in terms of shift and simply typed lambda-calculus
Simply typed lambda-calculus with dynamic binding is not strongly normalizing
General recursive types via delimited continuations
A differently-formulated proof: representing general recursive types
We use these ideas to build a type system for delimited continuations. It lets control operators change the answer type or act beyond the nearest dynamically-enclosing delimiter, yet needs no extra fields in judgments and arrow types to record answer types. The typing derivation of a direct-style program desugars it into continuation-passing style.
Joint work with Chung-chieh Shan.
The extended (with Appendices) version of the paper published in Proc. of Int. Conf. on Typed Lambda Calculi and Applications (TLCA), Paris, June 26-28, 2007 -- LNCS volume 4583.
Commented Twelf code accompanying the paper
The code implements type checking -- of simply-typed lambda-calculus for warm-up, and of the main lambda-xi0 calculus -- and contains numerous tests and sample derivations.
The calculus is typed, assigning types both to terms and to contexts. Types abstractly interpret operational semantics, and thus concisely describe all the effects that could occur in the evaluation of a term. Pure types are given to the terms whose evaluation incurs no effect, i.e., includes no shift-transitions, in any context and in any environment binding terms' free variables, if any. A term whose evaluation may include shift-transitions has an effectful type, which describes the eventual answer-type of the term along with the delimited context required for the evaluation of the term. Control operators may change the answer type of their context.
eval*relation) and the type inference (the
tevalrelation is deterministic and terminating, thus constructively proving that the type system for our Church-style calculus is decidable. The code includes a large number of examples of evaluating terms and determining their types.
Call-by-name linguistic side effects
ESSLLI 2008 Workshop on Symmetric calculi and Ludics for the semantic interpretation. 4-7 August, 2008. Hamburg, Germany.
Compilation by evaluation as syntax-semantics interface
Linguistics turns out to offer the first interesting application of the typed call-by-name shift/reset. The paper develops the calculus in several steps, presenting the syntax and the dynamic semantics of the final calculus in Figure 3 and the type system in Figures 4 and 5. The paper details several sample reductions and type reconstructions, and discusses the related work.
A substructural type system for delimited continuations
That TLCA 2007 paper introduced the abstract interpretation technique for reconstructing the effect type of a term in a calculus of delimited control. The technique progressively reduces a term to its abstract form, i.e., the type. The TCLA paper used a call-by-value calculus with a so-called dynamic control operator,
shift0. Here we apply the technique to the call-by-name
calculus with the static control operator
f be a pure function of the type
a -> a and
d be a value of the type
a (in the paper,
d is written as a black
dot). As in the paper, we write
# for prompt. The
#( control k.(f #(k d; k d)) ; control k.(f #(k d; k d)) )appears to be well-typed. It reduces to
#(f #(k d; k d)) where k u = u; control k.(f #(k d; k d)) then #(f #(f #(k d; k d))) eventually to #(f #(f #(f ..... )))
Since we are in a call-by-value language, the above result is not
terribly useful, but it is a good start. We only need an
f is of the type
(a->b) -> (a->b). Let
d be any value of the
a->b: this is the witness that the return type is populated.
We build the term
FX = #( control k.(f (\x . #(k d; k d) x)) ; control k.(f (\x . #(k d; k d) x)) )that is well-typed and expands as
#(f (\x . #(k d; k d) x) ) where k u = u; control k.(f (\x . #(k d; k d) x)) and then f (\x . #(k d; k d) x)noticing that
control k.(f (\x . #(k d; k d) x))we get
f (\x . FX x)
Thus we obtain that
FX x is equal to
f (\x . FX x) x, which means
FX is the call-by-value fixpoint of
Without access to the implementation of Kameyama and
Yonezawa's calculus, we can test this expression using the
cupto-derived control. The latter is implemented in OCaml. We cannot
test the typing of our fix, since the type system of cupto is too
coarse. We can test the dynamic behavior however. To avoid passing the
witness that the result type is populated, we set the result type to
a->a, which is obviously populated, by the identity
Kenichi Asai and Yukiyoshi Kameyama:
Polymorphic Delimited Continuations
Proc. Fifth Asian Symposium on Programming Languages and Systems (APLAS 2007), LNCS
\mu X. F[X]where
Xmay appear negatively (i.e., contravariantly) in
Xappears only positively (as in the type of integer lists,
\mu X. (1 + Int * X))), the resulting type is often called inductive.
A general recursive type, e.g.,
\mu X. X->Int->Int
can be characterized by the following signature:
module type RecType = sig type t (* abstract *) val wrap : (t->int->int) -> t val unwrap : t -> (t->int->int) endprovided that
(unwrap . wrap)is the identity. If we have an implementation of this signature, we can transcribe a term such as
\x. x xfrom the untyped lambda-calculus to the typed one.
ML supports one implementation of
iso-recursive (data)types. However, there is another implementation,
using ML exceptions. Since exceptions are a particular case of
delimited control, we obtain another proof that simply
typed lambda-calculus with a cupto-like delimited
control is not strongly normalizing.
We implement lazy evaluation without any mutation or other destructive operations -- essentially in a call-by-value lambda-calculus with shift and reset.