- Introduction to programming with shift and reset
**Implementations of delimited control in OCaml, Haskell and Scheme**- A substructural type system for delimited continuations
- Streams and Iteratees
- How to remove a dynamic prompt: static and dynamic delimited continuation operators are equally expressible
- An argument against call/cc
- Generators: yield = exceptions + non-determinism
- Generic Zipper: the context of a traversal
- Delimited continuations in operating systems
- Delimited control and breadth-first, depth-first, and iterative deepening search
- Eff directly in OCaml
- Dynamic binding and delimited control effects
- Answer-Type Modification without tears: Prompt-passing style translation for typed delimited-control operators
- Recursion from Iteration: an exercise in program derivation
- A Time-Travel Story
- LogicT: Fair and expressive backtracking monad transformers
- Purely Functional Lazy Non-deterministic Programming
- The essence of shell pipelining, or: CPS can be convenient to use
- Undelimited continuations are not functions
- Mechanized proofs of type soundness of delimited control
- Persistent delimited continuations for CGI programming with nested transactions
- How to zip folds: A complete library of lists represented as two continuations
- Simply typed lambda-calculus with a typed-prompt delimited control is not strongly normalizing
- Executable direct denotational semantics of multiprompt delimited control
- General recursive types via delimited continuations
- Non-deterministic choice (amb) in OCaml
- Fixpoint combinator from typed prompt/control
- Embedded probabilistic programming in OCaml
- Normalizing loop bodies by evaluation, an application of multi-prompt delimited continuations
- Prompts as local exceptions
- Resumable exceptions in ML
- Let-insertion without pain or fear or guilt
- Staging with Delimited Control
- Typed Staged Future: Semi-implicit batched remote code execution as staging
- Delimited continuations do dynamic-wind
- Polyvariadic functions and keyword arguments: pattern-matching on the type of the context
- shift as a green fork
- Probabilistic programming in POSIX C and OCaml:
`shift`

vs`fork(2)`

- Differentiating Parsers
- Call-by-name typed shift/reset calculus
- Continuation Hierarchy and Quantifier Scope: flexible continuation hierarchy
- Self-application as the fixpoint of call/cc
- Total stream processors and their applications to all infinite streams
- Why a program in CPS specializes better
- Stack as the variable binding environment
- Delimited continuations in natural language semantics

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

**Version**- The current version is September 27, 2011
**References**- 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 controlContTutorial.hs [9K]

The complete code for the Haskell portion of the tutorial

- 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]

(Actually we use several versions of breadth-first search, optimized to a different extent.)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 a

Other 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 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 x

The solution is the familiar generate-and-testinduct io = reify $ do exp <- an_exp if all (\ (i,o) -> eval exp i == o) io then return exp else failure

where`an_exp`

generates a sample function representation, and the if-expression tests if evaluating it on given inputs gives the desired outputs. The generator of`Exp`

expressions isan_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. **Version**- The current version is February, 2022
**References**- Searches.hs [14K]

The complete Haskell code with many comments, explanations 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 memoizationsJoachim 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

- This technical report shows that the delimited continuation operators
`shift`

,`control`

,`shift0`

, etc. are*all*macro-expressible in terms of each other. Furthermore, the operators`shift`

,`control`

,`control0`

,`shift0`

are 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`shift`

indeed has its standard reduction semantics.The report presents 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, to split and compose stack fragments as one thinks fit. **References**- impromptu-shift-tr.pdf [136K]

<http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR611>

Technical Report TR611, Department of Computer Science, Indiana University, 2005delim-cont.scm [10K]

Scheme code with the simplest implementation of`control`

,`shift0`

,`control0`

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

**Version**- The current version is June 2016
**References**- Electronic Proceedings in Theoretical Computer Science EPTCS 212 (Post-Proceedings of the Workshop on Continuations 2015) June 20, 2016, pp. 36-52 doi:10.4204/EPTCS.212.3

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

**Version**- The current version is 1.7, April 2008
**References**- 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'', was presented 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.

- Simply typed lambda-calculus has strong normalization property:
any 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`

; 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

`delta`

's type`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.

**Version**- The current version is September 30, 2006
**References**- 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 promptDelimited Dynamic Binding

The reformulation in terms of shift and simply typed lambda-calculusSimply 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 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.

**Version**- The current version is 1.1, June 2007
**References**- Type checking as small-step abstract evaluation

Detailed discussion of the two main slogans of the paper:- Types are abstract expressions (Cousot)
- The colon is a turnstile (Lambek)

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 (TLCA), Paris, June 26-28, 2007 -- LNCS volume 4583.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.

- We present a 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.

**References**- 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`

.

- 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)

noticing that`k d`

is`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`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. **Version**- The current version is 1.1, Oct 24, 2007
**References**- Yukiyoshi Kameyama and Takuo Yonezawa:
Typed Dynamic Control Operators for Delimited Continuations.
FLOPS 2008.
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 (* abstract *) val wrap : (t->int->int) -> t val unwrap : t -> (t->int->int) end

provided 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. **Version**- The current version is 1.1, Oct 30, 2007; 1.2, Oct 2011
**References**- delimcc-rectype.ml [2K]

Complete commented OCaml code