call/cc*F* operators:
from control0 to shift
tail of a functional streamshift vs fork(2)
abort playing the role of nil and shift the role of consamb in OCamlPrompts as local exceptionscall/ccThe following article shows that call/cc and the
fix-point combinator Y are two sides of the same
coin. The article makes the claims formal and proves them as a
theorem. Two examples in the article demonstrate that first-class
continuations can be really tricky, and so being formal helps. The way
of proving the theorem is notable too: we extensively rely on
syntax-rules macros. Indeed, one macro does a
continuation-passing-style (CPS) transform, and another simple macro
-- which is actually a lambda-calculator -- normalizes the result of
the transform.
Theorem: Expressions
((call/cc ... (call/cc call/cc)) p)((call/cc ... (call/cc (call/cc id))) p)((lambda (x) (x x)) p)where p is a value, are observationally equivalent in CBV.
Here (call/cc ...) signify zero or more
applications of call/cc, and id is the
identity function (lambda (x) x).
The article also discusses self-applications of delimited continuation operators.
In this article, continuations, fixpoints, CPS, higher-order syntax, syntax-rule macros and lambda-calculators all come together.
Normal-order direct-style beta-evaluator with syntax-rules, and the repeated applications of call/cc
Self-application as the fixpoint of call/cc [plain text file]
The first version of that article was posted on a USENET
newsgroup comp.lang.scheme on Thu, 18 Sep 2003 23:39:02 -0700
Normalization as a yacc-style parsing
The algorithm for the normal-order lambda-calculator, which is
implemented in the article as a syntax-rule.
From enumerators to cursors: turning the left fold inside out
Another, practical illustration of the close relationship
between first-class continuations and fixpoints.
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 prompts. 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
*F* operators:
from control0 to shiftWe present for the first time the generic
and direct implementation of all four Friedman-Felleisen delimited control
operators: from -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. All four
combinations of the two flags correspond to four delimited control
operators. Each flag is present in the code exactly once, in a
trivial context. 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 forth-coming paper ``A Monadic Framework for Delimited Continuations'' by R. Kent Dybvig, Simon Peyton Jones and Amr Sabry.
delim-control-n.scm [7K]
The complete R5RS Scheme implementation along with regression
tests for all four delimited control operators
We present the OCaml library delimcc of delimited control operators
with multiple typed prompts. The code implements the superset of the interface
proposed by Dybvig, Sabry, and Peyton-Jones and supports
`static' (shift/reset) and
`dynamic' (prompt/control, shift0, control0) delimited continuation operators
with multiple, arbitrarily typed prompts. The test file testd0.ml is a good example of using shift/reset in OCaml programs.
The delimcc library is a pure library and makes no changes to the OCaml system -- neither to the compiler nor to the bytecode VM. Therefore the library is perfectly compatible with any OCaml program and any (compiled) OCaml library. The delimcc library has no effect on the code that does not capture delimited continuations.
The delimcc library is a native implementation: it
directly implements delimited continuations and deals only
with a fragment of the control stack rather than the whole stack. The
stack or its fragments are never inspected. The implementation is
efficient: only the necessary prefix of the stack is copied. The
implementation is fully integrated with OCaml 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
implementation does no patching to the OCaml system and is a regular
library. If one compiles the top-level (see `make top'), one can use
the delimited continuation operators in interactive OCaml sessions.
For comparison we show another implementation, which requires
the monadic style of writing code. That implementation however is in
pure OCaml and works both for byte-code--interpreted as well as
ocamlopt-compiled programs. That implementation is, too, strongly
typed and needs no bizarre 'a cont types and no
loopholes.
The new version of the delimcc library supports serialization
of captured continuations. The new version
implements abort as a primitive, which makes it
essentially as efficient as raise. The library
offers shift, shift0 and control for convenience, and
a useful debugging primitive show_val, to display the
structure of any OCaml value.
caml-shift.tar.gz [59K]
The delimcc distribution: library code, sample code,
and validation tests
cc-monad.ml [8K]
Complete code of the alternative,
monadic-style implementation, and the validation tests.
Version 1.1, Oct 27, 2005
R. Kent Dybvig, Simon Peyton Jones, and Amr Sabry:
A Monadic Framework for Delimited Continuations.
Indiana University Technical Report TR615
<http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR615>
Persistent twice-delimited continuations
Explanation of the feature to serialize captured delimited
continuations
We demonstrate the R5RS Scheme version of the delimcc library
of multi-prompt delimited control in OCaml. The library implements
the whole range of delimited control operators,
from cupto to multi-prompt versions
of control, shift0
and shift -- providing the superset of the
interface proposed by Dybvig, Sabry, and Peyton-Jones.
The Scheme implementation of delimcc attests to the generality of the scAPI-based approach to implementing delimited control. The presented code is a straightforward translation of the delimcc OCaml 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, corresponds only to the needed prefix of the
full continuation, even if call/cc copies the whole
stack. In other words, we obtain a so-called JAR
hack (see shift-reset.scm in Scheme48 distribution) automatically.
delimcc.scm [10K]
The complete implementation
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 small performance benchmark, due to Gasbichler and Sperber
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.
It is well-known that in the presence of effects, the
evaluation order matters. For example, let get_int be
an (effectful) computation that reads a number from a file. Then the
expression (get_int - get_int) evaluated left-to-right
and right-to-left gives opposite results. The requirements on the
evaluation order imposed by the correct sequencing of effects are not,
however, as rigid as they may appear. Left-to-right evaluation order
does mean that the left-most get_int must be evaluated
first. It does not have to be evaluated all-the-way. The evaluator is
not required to read data from the disk and convert them to the
integer before it even considers the other get_int of our
expression. Evaluating the left-most get_int may just as
well return a promise of an integer. The
other get_int returns a promise too. It is when the
numbers are required, by the subtraction operation, that the evaluator
will execute the outstanding promises, reading the two numbers from
the file. The evaluator keeps track which promise was made first, so
to assign read numbers to their correct promises.
The above scenario seems contrived for the regular local disk i/o. The delayed input makes more sense when the file in question is a communication pipe to a remote process. Delaying and bundling input requests becomes especially beneficial when communicating with a user through a web browser. The difference is then between asking for the two numbers on two separate web forms, or on one form. The bundling of questions reduces the traffic between the server and the browser and the resources for storing web continuations.
The article below presents a uniform mechanism for flexible and automatic bundling of questions into forms. The library takes care of parsing multiple responses, matching them with the questions and validating the replies. The library also takes care of reporting invalid replies back to the user and asking for the resubmission of the corrected answer.
Our mechanism relies on call-by-need: the library delays asking
questions until their answers are demanded. When a question really
needs to be answered, the library collects all outstanding questions,
makes a web form and sends it to the client as the response of the
server computation so far. When the form is submitted and the
computation resumes, the library parses all the replies and stores
them for future answer demands. Since our particular implementation
language (OCaml) is strict, call-by-need is not automatic: The
programmer does have to write Lazy.force explicitly. The
type system ensures that the programmer does not forget the forcing,
thus making the data dependencies apparent. OCaml type checker will
tell the programmer the points where a value is demanded. The
programmer should insert Lazy.force there -- or at some
earlier point, if the programmer so chooses. If the programmer forces
the answer after asking each question, we get back the sequential
behavior of asking questions one-by-one.
Form-ing web continuations, or asking several questions at once.
The complete article
<http://conway.rutgers.edu/~ccshan/wiki/blog/posts/MultipleQ/>
ask-by-need.ml [13K]
Extensively commented OCaml code
Native delimited continuations in (byte-code) OCaml Library required to run the code
Persistent delimited continuations for CGI programming with nested transactions A complementary approach
We describe the implementations of Asai and Kameyama's calculus of polymorphic delimited continuations with effect typing, answer-type modification and polymorphism. The calculus has greatly desirable properties of strong soundness (well-typed terms don't give any run-time exceptions), principal types, type inference, preservation of types and equality through CPS translation, confluence, and strong normalization for the subcalculus without fix.
The particularly elegant application of the calculus is 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. Given control operators supporting both
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 generalized monad typeclass in the recent version of Coq and so implemented the calculus along with the type-safe sprintf in Coq.
Kenichi Asai and Yukiyoshi Kameyama:
Polymorphic Delimited Continuations. APLAS 2007.
<http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf>
Genuine shift/reset in Haskell98 [plain text file]
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 [4K]
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.''
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.
Zipper is a construction that lets us replace an item deep in a complex data structure, e.g., a tree or a term, without any mutation. The result will share as much of its components with the old structure as possible. The old data structure is still available, and so the changes can be instantly rolled back. Zipper lets us handle a tree or any other enumerable data structure as if it were a stream. Zipper is essentially an `update' and yet pure functional cursor into a data structure. Zipper can be viewed as a delimited continuation reified as a data structure.
Our treatment of zipper is quite different from that of Huet (JFP, 1997) and Hinze and Jeuring (JFP 2001). Our zipper is polymorphic over the data structure to traverse, and the zipper creation procedure is generic and does not depend on the data structure at all. Different data structures or different realizations of the same abstract data structure can use the same zipper and the same zipper creation and manipulation functions. Our zipper type depends only on the interface (but not the implementation!) of a traversal function. Our zipper is a derivative of a traversal function rather than that of a data structure itself.
We can traverse the same term with several ``concurrent'' zippers: Delimited continuations let us view a single-threaded program as cooperatively multi-threading one. We support various isolation modes of concurrent traversals: from ``uncommitted read'' to ``repeatable read'' to ``serializable'' -- we even support sub-transactions. We can use either the push mode -- one cursor broadcasts its updates to the others -- or the pull mode. A cursor may decide to broadcast the accumulated updates at arbitrary checkpoints of its own choosing. A cursor may examine updates made by the other cursor and perhaps disregard some of them -- or apply in a different order, after its own updates. We are using terms zipper, cursor and transaction somewhat interchangeably: a zipper is a cursor which is by default isolated from the others and whose updates are instantly reversible.
Zipper1.lhs [12K]
Introduction to generic zippers as delimited continuations.
The code was originally posted as Zipper as a delimited continuation on Haskell mailing list on Wed, 27 Apr 2005 16:17:04 -0700 (PDT)
Zipper2.lhs [22K]
This part discusses the relationship between zippers
and (database) transactions of various isolation modes. We show the
updating enumerator and the corresponding zipper that maximally
preserve sharing and can walk terms with directed loops. We
demonstrate that a zipper can convert a (sequential) map to a fold.
The code was originally posted as Two-hole zippers and transactions of various isolation modes on Haskell mailing list on Tue, 10 May 2005 23:11:06 -0700 (PDT)
ZFS.tar.gz [12K]
That archive includes, among other things, the delimited
continuation framework by R. Kent Dybvig, Simon Peyton-Jones and Amr
Sabry. The Haskell implementations of Zipper rely on that
framework.
zipper data structure
<http://www.nist.gov/dads/HTML/zipper.html>
Ralf Hinze and Johan Jeuring. Weaving a Web
Journal of Functional Programming 11(6), pages 681 - 689,
2001. Technical report ICS Utrecht University, UU-CS-2001-33.
<http://citeseer.ist.psu.edu/hinze01web.html>
Joint processing of two immutable SXML documents with update cursors
We present a file server/OS where threading and exceptions are all realized via delimited continuations. We use zipper to navigate within any term. If the term in question is a finite map whose keys are strings and values are either strings or other finite maps, the zipper-based file system looks almost the same as the Unix file system. Unlike the latter, however, we offer: transactional semantics; undo of any file and directory operation; snapshots; statically guaranteed the strongest, repeatable read, isolation mode for clients; pervasive copy-on-write for files and directories; built-in traversal facility; and just the right behavior for cyclic directory references.
We can easily change our file server to support NFS or 9P or
other distributed file system protocol. We can traverse richer terms than
mere finite maps with string keys. In particular, we can use
lambda-terms as our file system: one can cd into a lambda-term in
bash.
The implementation of ZFS has no unsafe operations, no GHC let alone Unix threads, and no concurrency problems. Our threads cannot even do IO and cannot mutate any global state --- and the type system sees to it. We thus demonstrate how delimited continuations let us statically isolate effects even if the whole program eventually runs in an IO monad.
zfs-talk.pdf [103K]
Expanded talk with the demo. It was originally presented as an
extra demo at the Haskell Workshop 2005
ZFS.tar.gz [12K]
The complete source code, with comments. It was tested with GHC 6.4
on FreeBSD and Linux
[The Abstract of the paper]
Delimited continuations are the meanings of delimited
evaluation contexts in programming languages. We show they offer a
uniform view of many scenarios that arise in systems programming, such
as a request for a system service, an event handler for input/output,
a snapshot of a process, a file system being read and updated, and a
Web page. Explicitly recognizing these uses of delimited
continuations helps us design a system of concurrent, isolated
transactions where desirable features such as snapshots, undo,
copy-on-write, reconciliation, and interposition fall out by default.
It also lets us take advantage of efficient implementation techniques
from programming-language research. The Zipper File System
prototypes these ideas.
Joint work with Chung-chieh Shan.
Olivier Danvy has very kindly pointed out that continuations in operating systems delimited at process, job, etc. boundaries were first mentioned back in 1974 in the seminal work by Christopher Strachey and Christopher P. Wadsworth `Continuations: A mathematical semantics for handling full jumps.' Technical Monograph PRG-11, Programming Research Group, Oxford University Computing Laboratory, 1974. Reprinted in Higher-Order and Symbolic Computation, 2000, 13(1-2):135-152. Here is footnote 1 from their paper:
The reader may ask if it is any more justifiable to take a single program in isolation than it is to take a single command. The answer, of course, is that it is not, and that in the same way as command continuations are needed to explain jumps inside programs, further hierarchical levels of continuations, such as process continuations, job continuations and operating system continuations, will be needed to give the semantics of the operating system. The outer-most level (or possibly levels) are not inside the machine at all and are implemented by operator intervention. We do not discuss the use of continuations in the semantics of operating systems any further in this paper as to do so would require a fuller understanding of the differences between operating systems and programs that is yet at our disposal. It would also make the paper much too long...
context-OS.pdf [134K]
Proc. CONTEXT2007: 6th International and Interdisciplinary Conference
on Modeling and Using Context. Roskilde, Denmark, August 20-24, 2007. Lecture
Notes in Artificial Intelligence 4635, pp. 291-302.
<http://www.cs.rutgers.edu/~ccshan/zipper/poster.ps>
Poster presented at CONTEXT 2007, Roskilde U., Denmark,
August 22, 2007.
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
Native delimited continuations in (byte-code) OCaml
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)
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. The question becomes if there is an
implementation using delimited continuations. We show that cupto and
the corresponding shift with the typed prompt implement RecType. This conclusion is a different formulation of the proof
that simply typed lambda-calculus with a typed-prompt 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.
tail of a functional streamGiven the following functional stream or its monadic version:
newtype FStream a = SFK (forall ans. SK a ans -> FK ans -> ans)
type FK ans = () -> ans -- failure continuation
type SK a ans = a -> FK ans -> ans -- success continuation
newtype MFStream m a = MSFK (forall ans. MSK m a ans -> MFK m ans -> m ans)
type MFK m ans = m ans -- failure continuation
type MSK m a ans = a -> MFK m ans -> m ans -- success continuation
the question is obtaining several first elements of
that stream. In general, the problem is to split a non-empty
functional stream into the head element and the rest, which can be
split again, etc. That rest stream must be of the type MFStream m a, of course.
This is a far more difficult problem than it may appear. One
may think that we merely need to convert the functional stream to a
regular, nil/lazy-cons stream, for
example:
mfstream_to_stream:: (Monad m) => MFStream m a -> m (Stream a)
mfstream_to_stream mfstream = unMSFK mfstream sk fk
where fk = return Nil
sk a fk' = fk' >>= (\rest -> return (Cons a (\ () -> rest)))
However, if the monad m is strict (i.e., the bind
operator >>= forces its first argument -- as it is the
case for the IO monad, for example), then we must fully
convert the functional stream to the regular stream before we can
examine the first few elements. If the source functional stream is
infinite, mfstream_to_stream diverges.
The code below explains the problem and shows a general
solution. It underlies the LogicT monad transformer, and
the implementation of pruning operations in the Scheme-based logical
programming system Kanren.
car-fstream.lhs [6K]
Literate Haskell code with examples and explanation.
How to zip folds: A complete library of fold transformers (streams)
Corrado Boehm and Alessandro Berarducci: Automatic Synthesis of Typed
Lambda-Programs on Term Algebras. Theoretical Computer Science, 1985, v.39,
pp. 135-154
This article seems to be the first to describe the idea of representing
recursive data structures using a higher-rank rather than recursive type.
<http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00138.html>
is a further discussion. These references were pointed out by
Chung-chieh Shan.
KANREN: A declarative logic programming system
<http://kanren.sourceforge.net>
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML