shift vs fork(2)
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.
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
Our running example is a rather typical Beamer slide with overlays:
\begin{frame}{My Slide}
This is my talk
It has several points
\begin{itemize}
\item First, me have to mention this
\only<2,3,4>{\item Then it comes to that}
\only<3>{\item We have to stress that}
\only<4>{\item Or, to put it better,}
\end{itemize}
\note<1>{To expand on 1}
\note<2,3,4>{Note on 2}
\note<4>{Note on 4}
\note<3,4>{Note on 3}
\end{frame}
Here, \only<numbers>{content} means that content appears only on
overlays listed in numbers (\note<X>{Y} is essentially the
shorthand for \only<X>{\note{Y}}). The slide, hence, has four
overlays (because 4 is the largest overlay number mentioned). On the
first one, the itemized list has the single, top, item (with the
first note attached, displayed or not depending on Beamer
settings). The item and the text above it remain through the end.
The second overlay brings the second list item (and the
associated note), which also persist. The next overlay adds
the third item, replaced in the last overlay. To be sure, Beamer has
other overlay operators -- which can either be implemented in terms of
\only or analogously. Therefore, we
restrict ourselves to \only.
We describe two implementations of \only: without and with delimited
control, and contrast them. Beamer is written in TeX, which is not the
best language to present algorithms in (or to program in general). We
use OCaml instead. OCaml (at least up to version 4.14) has a
general-purpose delimited control facility (the delimcc library),
used in the second implementation.
Beamer takes the above slide TeX code and creates several pdf pages of
output, one page per overlay. In our OCaml implementation we
concentrate on overlay expansion, skipping typesetting and pdf
rendering. That is, we take a frame with overlay operators and expand
it into a list of `rendered' frames, without overlay operators. A frame
is represented in OCaml in perhaps the most naive way, as the frame data
structure:
type frame = Frame of string * content list
and content =
| Lit of string
| List of content list
| Note of content
| Empty
let frame t c = Frame(t,c)
The frame content is made of literal strings, itemizations and notes -- just
enough for our running example. One can easily render it in
markdown, html, or any other format.
For overlays, we assume the most minimal interface:
module type framer = sig
val make_overlays : (unit -> frame) -> frame list
val only : int list -> content -> content
end
The function make_overlays takes a frame
expression (represented as a thunk) that may include only --
and returns the list of completed frames, one per overlay. The function
only that may appear in an overlay expression displays its content
only on the listed overlays. Here is how the sample Beamer slide is
represented in OCaml -- in what amounts to a simple embedded DSL for
slides with overlays.
module Ex(S:framer) = struct
open S
let r = make_overlays @@ fun () ->
frame "My Slide" [
Lit "This is my talk";
Lit "It has several points";
List [
Lit "First, we have to mention this";
only [2;3;4] @@ Lit "Then it comes to that";
only [3] @@ Lit "We have to stress that";
only [4] @@ Lit "Or, to put it better,";
];
only [1] @@ Note (Lit "To expand on 1");
only [2;3;4] @@ Note (Lit "Note on 2");
only [4] @@ Note (Lit "Note on 4");
only [3;4] @@ Note (Lit "Note on 3");
]
end
Clearly, writing slides in OCaml is quite less convenient than in TeX
(the inconvenience could be alleviated to some extent by smart
constructors with optional arguments, or, better, using the ppx
pre-processor).
We explicitly parameterized the code by the implementation of the
framer interface: we will have two.
The first implementation of framer is how overlay expansion is
likely to be implemented in Beamer. The idea is simple: keep re-executing the
frame expression, in different dynamic environments: with the
different current overlay number. The operator
\only<numbers>{content} (or, note [numbers] content, in OCaml)
omits its content unless the the current overlay number is listed in
numbers.
module FramerState : framer = struct
let curr_frame = ref 0
let max_frames = ref 0
let make_overlays th =
curr_frame := 1;
max_frames := 1;
let rec loop f =
if !curr_frame >= !max_frames then [f] else
(incr curr_frame; f :: loop (th ()))
in loop (th ())
let only ixs c =
let mx = List.fold_left max 1 ixs in
if !max_frames < mx then max_frames := mx;
if List.mem !curr_frame ixs then c else Empty
end
FramerState literally implements the idea: it is an
executable specification. Its only complication is that the number
of overlays is not known beforehand but has to be determined during
expansion: it is the largest overlay number mentioned in only.
The drawbacks, the global mutable state, are also clear. Consider what
happens if make_overlays is invoked recursively, within the frame
content: It can happen by mistake; it is also legitimate, to format a
`miniframe'. Although the mutable state can be hidden with some
elaboration, it is inevitable: It is the communication channel between
make_overlays and only.
The biggest drawback of FramerState is, admittedly, aesthetic: it
just feels wrong to re-render everything from scratch, over and over
again. On our sample slide, the first itemized item and the text above
it stay put. Surely this part could be rendered once and for all and then
shared, across all output pages? Likewise, the second item in the itemized
list occurs on overlays 2,3, and 4. Wouldn't it be nice to render
up to this list once, and then share in the output?
It is this line of thought that leads to delimited control. Consider the frame expression from our running example, repeated below:
frame "My Slide" [
Lit "This is my talk";
Lit "It has several points";
List [
Lit "First, we have to mention this";
only [2;3;4] @@ Lit "Then it comes to that";
only [3] @@ Lit "We have to stress that";
...
]
In left-to-right evaluation, we first evaluate
Lit "This is my talk", then
Lit "It has several points", then enter the List expression and
evaluate its first item. The evaluation builds content data
structures on heap, linking them and referencing
from the stack. Now we come to the first only. The common part of
the overlays ends here: some overlays continue with
Lit "Then it comes to that";, some without. Either way, the stack up
to that point is shared. The delimited control is exactly the
mechanism to resume from a choice point, sharing the results obtained
before it.
module FramerCont : framer = struct
open Delimcc
type req = Done of frame
| OnlyAt of int list * content * (content -> req)
let p = new_prompt ()
let only ixs c = shift0 p (fun k -> OnlyAt (ixs,c,k))
...
As in FramerState, the operations make_overlays and only
communicate: this time, using control rather than mutable
state. (Incidentally, that mutable state can be emulated with
delimited control has been noted early on.) The communication is
one-sided and simple: only reports its arguments to the receiver
(a.k.a, handler: part of make_overlays) and lets it do all the work.
Crucially, only captures the part of the stack at the point of its evaluation,
as the continuation k. When the continuation is invoked, the
evaluation of the frame expression continues, from the saved
point. The continuation can be invoked several times: all these
resumptions start with the same, shared stack.
The function make_overlays tries to continue the evaluation on
only numbers content twice: once for overlays that are listed in
numbers (and hence include content), and once that are not listed.
The continuation of only may include another only: another choice
point. Not all the choices are possible however, since a continuation
of only imposes constraints on the overlay numbers. The function
make_overlays tracks the constraints: see the source code for details.
All in all, FramerCont builds overlays maintaining sharing and
avoiding needless re-evaluations.
We should stress that the continuation k of only is invoked
(reinstated) twice times: so-called multi-shot delimited
control. Since version 5, OCaml offers delimited control in the form
of algebraic effects -- which, however, are `one-shot': a captured
continuation may be reinstated only once (often, almost
immediately). This is indeed the most common use of delimited
control. Multi-shot delimited control is indispensable for
representing non-determinism (see Hansei probabilistic programming
library) -- and not for anything else, commonly thought. It is
somewhat surprising (for me as well) to see another use for multi-shot
delimited control.
PDF itself has overlays, or transitions -- although few viewers, aside from Acrobat, seem to implement it. If one is to write a PDF viewer supporting transitions, perhaps this article could be of reference. Perhaps one might even want to use delimited control...
Hansei: Embedded probabilistic programming in OCaml
This embedded probabilistic programming language crucially relies on
(multi-shot) delimited control.
David Wingate, Andreas Stuhlmüller and Noah D. Goodman:
Lightweight Implementations of Probabilistic Programming
Languages Via Transformational Compilation. AISTATS 2011,
Revision 3. February 8, 2014
The paper proposed an implementation technique for probabilistic
programming languages based on repeated re-evaluation. The technique requires
no delimited control or other advanced features and can be used with
many existing systems: the paper itself demonstrates a stochastic
Matlab. Many other probabilistic languages use
the technique.
Embedded probabilistic domain-specific language Hakaru10
It uses the repeated evaluation but with memoization and tracking
dependencies; therefore only the necessary parts are re-evaluated.
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-test
induct 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 is
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
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.
delim-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
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.
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.
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.
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.
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.
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 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.
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 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 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.
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>
\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.