call/cc
abort
playing the role of nil
and shift
the role of cons
amb
in OCamlPrompt
s as local exceptionsshift
as a green fork
shift
vs fork(2)
call/cc
The tutorial on delimited continuations was given together with Kenichi Asai (Ochanomizu University, Japan) in the evening before the Continuation Workshop 2011.
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
tail-call or 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 shift
and 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.
CW2011 Tutorial Session. September 23, 2011
<http://logic.cs.tsukuba.ac.jp/cw2011/tutorial.html>
<http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/>
Tutorial notes for OchaCaml and Haskell
<http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-e.pdf>
Haskell-tutorial.pdf [86K]
ContExample.hs [4K]
A sample shift/reset code in Haskell, in
the Cont
monad -- the monad for delimited control
ContTutorial.hs [9K]
The complete code for the Haskell portion of the tutorial
ACM SIGPLAN Continuation Workshop 2011 (co-located with ICFP 2011)
Tokyo, Japan. Saturday, September 24, 2011.
<http://logic.cs.tsukuba.ac.jp/cw2011/>
This tutorial-like Haskell code illustrates the application of delimited control for non-deterministic search. We apply different search strategies to the same non-deterministic program without re-writing it. A non-deterministic computation is reified into a lazy search tree, which can then be examined in different ways. We write non-deterministic search strategies as standard depth-first, breadth-first, etc., tree traversals.
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]
Using the Cont
monad from the standard monad transformer library
and its operations shift
and reset
, we
implement two primitives: non-deterministically choosing a value
from a finite list, and reifying a computation into a SearchTree
:
choose :: [a] -> Cont (SearchTree w) a reify :: Cont (SearchTree a) a -> SearchTree aOther non-deterministic operations --
failure
, mplus
(to join two computations), choose'
(to choose
from a potentially infinite list) -- are all written in terms of
choose
.
The running example non-deterministically computes all Pythagorean triples, naively:
ex = do x <- choose' [1..] y <- choose' [1..] z <- choose' [1..] if x*x + y*y == z*z then return (x,y,z) else failureWe show the first five found triples:
test3d = take 5 . dfs . reify $ ex -- diverges!! test3b = take 5 . bfs . reify $ ex -- [(3,4,5),(4,3,5),(6,8,10),(8,6,10),(5,12,13)] test3i = take 5 . iter_deepening . reify $ ex -- [(3,4,5),(4,3,5),(6,8,10),(8,6,10),(5,12,13)]Depth-first search expectedly diverges. Breadth-first and iterative deepening are both complete strategies and both find the answer if it exists. Expectedly iterative deepening takes much less memory than breadth-first search.
Searches.hs [9K]
The complete Haskell code with comments and tests. The comments
tell why the search tree is defined as it is, with a thunk.
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
This technical report shows that the delimited continuation
operators shift
, control
, shift0
,
etc. are macro-expressible in terms of each other. The report thus
confirms the result first established by Chung-chieh Shan in ``Shift
to Control'' (Scheme Workshop, 2004). The report uses a more uniform
technique that lets us skip an arbitrary number of prompt
s. The report formally proves that control
implemented via shift
indeed has its standard reduction
semantics. It is a common knowledge that first-class continuations are
quite tricky -- and delimited continuations are trickier
still. Therefore, a formal proof is a necessity.
The report shows the simplest known Scheme implementations of
control
, shift0
and control0
(similar to cupto
). The method in the
report lets us design 700 more delimited control operators, which
compose stack fragments in arbitrary ways.
Technical Report TR611, Department of Computer Science, Indiana
University, 2005
<http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR611>
delim-cont.scm [10K]
Scheme code with the simplest implementation of control
,shift0
, control0
and other
delimited continuation operators in terms of shift
/reset
. The code includes a large set of test cases.
``Lambda the Ultimate'' discussion thread, esp. on the meaning of
delimited contexts
<http://lambda-the-ultimate.org/node/view/606>
impromptu-shift-tr.scm [61K]
The master SXML file of the report
[The Abstract of the paper]
The salient feature of delimited-control operators is their
ability to modify answer types during computation. The feature,
answer-type modification (ATM for short), allows one to express
various interesting programs such as typed printf compactly and
nicely, while it makes it difficult to embed these operators in
standard functional languages. In this paper, we present a typed
translation of delimited-control operators shift and reset with ATM
into a familiar language with multi-prompt shift and reset without
ATM, which lets us use ATM in standard languages without modifying the
type system. Our translation generalizes Kiselyov's direct-style
implementation of typed printf, which uses two prompts to emulate the
modification of answer types, and passes them during computation. We
prove that our translation preserves typing. As the naive
prompt-passing style translation generates and passes many prompts
even for pure terms, we show an optimized translation that generate
prompts only when needed, which is also type-preserving. Finally, we
give an implementation in the tagless-final style which respects
typing by construction.
Joint work with Ikuo Kobori and Yukiyoshi Kameyama.
We present a simple CGI framework for web programming with nested transactions. The framework uses the unmodified OCaml system and an arbitrary, unmodified web server (e.g., Apache). The library makes writing web applications (CGI scripts) as straightforward as writing interactive console applications using read and printf. We write the scripts in the natural question-answer, storytelling style, with the full use of lexical scope, exceptions, mutable data and other imperative features (if necessary). The scripts can even be compiled and run as interactive console applications. With a different implementation of basic primitives for reading and writing, the console programs become CGI scripts.
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.
Fest2008-talk.pdf [204K]
Fest2008-talk-notes.pdf [244K]
The demonstration of the library at the Continuation Fest 2008
The extended version of the talk, Clicking on Delimited Continuations, has been given at FLOLAC in July 2008. The extended version
includes a detailed introduction to delimited continuations.
caml-web.tar.gz [16K]
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.
We present Church-style call-by-name lambda-calculus with delimited control operators shift/reset and first-class contexts. In addition to the regular lambda-abstractions -- permitting substitutions of general, even effectful terms -- the calculus also supports strict lambda-abstractions. The latter can only be applied to values. The demand for values exerted by reset and strict functions determines the evaluation order. The calculus most closely corresponds to the familiar call-by-value shift/reset calculi and embeds the latter with the help of strict functions.
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.
cbn-xi-calc.elf [19K]
Twelf code that implements the dynamic semantics (the eval*
relation) and the type
inference (the teval
relation). The teval
relation 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.
gengo-side-effects-cbn.pdf [161K]
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 shift
.
Simply typed lambda-calculus has strong normalization property:
the sequence of reductions of any term terminates. If we add delimited
control operators with typed prompts (e.g., 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 loop
is essentially
fun () -> Omega
: its inferred type is unit -> 'a
, and 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,
the type of delta
, 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.
Carl A. Gunter, Didier R'emy and Jon G. Riecke: A Generalization of Exceptions and Control in ML-Like Languages. Proc. Functional Programming Languages and Computer Architecture Conf., June 26-28, 1995, pp. 12-23.
The paper that introduced cupto
, the first
delimited control operator with an explicitly typed prompt.
Delimited Dynamic Binding
Reformulation of the above in terms of shift and simply typed
lambda-calculus.
Simply typed lambda-calculus with dynamic binding is not strongly normalizing
A differently-formulated proof: representing general recursive types
[The Abstract of the paper]
We propose type systems that abstractly interpret
small-step rather than big-step operational semantics. We treat an
expression or evaluation context as a structure in a linear logic with
hypothetical reasoning. Evaluation order is not only regulated by
familiar focusing rules in the operational semantics, but also
expressed by structural rules in the type system, so the types track
control flow more closely. Binding and evaluation contexts are
related, but the latter are linear.
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.
Type checking as small-step abstract evaluation
Detailed discussion of the two main slogans of the paper:
delim-control-logic.pdf [250K]
The extended (with Appendices) version of the paper published
in Proc. of Int. Conf. on Typed Lambda Calculi and Applications, Paris,
June 26-28, 2007 -- LNCS volume 4583.
Chung-chieh Shan. Slides of the TLCA 2007 Presentation, Jun 26, 2007.
<http://www.cs.rutgers.edu/~ccshan/binding/talk.pdf>
small-step-typechecking.tar.gz [10K]
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.
In the recent paper `Typed Dynamic Control Operators for Delimited Continuations' Kameyama and Yonezawa exhibited a divergent term in their polymorphically typed calculus for prompt/control. Hence the latter calculus, in contrast to Asai and Kameyama's polymorphically typed shift/reset calculus, is not strongly normalizing. Unlike the untyped case, typed control is not macro-expressible in terms of shift. Kameyama and Yonezawa conjectured that the (typed) fixpoint operator is expressible in their calculus too. The conjecture is correct: Here is the derivation of the fixpoint combinator, using the notation of their paper. The combinator is not fully polymorphically typed however: the result type must be populated.
Let 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
expression
#( 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 eta-expansion: Suppose
f
is of the type
(a->b) -> (a->b)
. Let d
be any value of the
type a->b
: this is the witness that the return type is populated.
We build the termFX = #( 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) we notice that k d = control k.(f (\x . #(k d; k d) x)) so we get f (\x . FX x)Thus we obtain
FX x = f (\x . FX x) x
, which means
FX
is the call-by-value fixpoint of f
.
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
be a->a
, which is obviously populated, by the identity
function.
open Delimcc let control p f = take_subcont p (fun sk () -> push_prompt p (fun () -> (f (fun c -> push_subcont sk (fun () -> c))))) let fix f = let p = new_prompt () in let d = fun x -> x in let delta u = control p (fun k -> f (fun x -> push_prompt p (fun () -> (k d; k d)) x)) in push_prompt p (fun () -> (delta d; delta d));; (* val fix : (('a -> 'a) -> 'a -> 'a) -> 'a -> 'a = <fun> *) let fact self n = if n <= 1 then 1 else n * self (pred n);; fix fact 5;; (* 120 *)
Yukiyoshi Kameyama and Takuo Yonezawa:
Typed Dynamic Control Operators for Delimited Continuations (draft Oct. 21, 2007).
<http://logic.cs.tsukuba.ac.jp/~kam/research.html>
Kenichi Asai and Yukiyoshi Kameyama:
Polymorphic Delimited Continuations
Proc. Fifth Asian Symposium on Programming Languages and Systems (APLAS
2007), LNCS
<http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf>
A general recursive type is usually defined (see
Kameyama and Yonezawa) as \mu X. F[X]
where X
may appear negatively (i.e., contravariantly) in F[X]
. If X
appears 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 (* an abstract type *) 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 x
from the untyped lambda-calculus to the
typed one.
ML supports one implementation of RecType
, using
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.
Call-by-need, or lazy, evaluation is call-by-name evaluation with the memoization of the result. A lazy expression is not evaluated until its result is needed. At that point, the expression is evaluated and the result is memoized. Thus a lazy expression is evaluated at most once. Lazy expressions may nest: a lazy expression may include other lazy expressions.
We implement lazy evaluation without any mutation or other destructive operations -- essentially in call-by-value lambda-calculus with shift and reset.
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML