f
as its only argument, (call/cc f)
within an expression is applied to the current ((call/cc f) e2)
is equivalent to applying f
to the current continuation of the expression. The current continuation is given by replacing (call/cc f)
by a variable c
bound by a lambda abstraction, so the current continuation is (lambda (c) (c e2))
. Applying the function f
to it gives the final result (f (lambda (c) (c e2)))
.
As a complementary example, in an expression (e1 (call/cc f))
, the continuation for the sub-expression (call/cc f)
is (lambda (c) (e1 c))
, so the whole expression is equivalent to (f (lambda (c) (e1 c)))
.
In other words it takes a "snapshot" of the current control context or control state of the program as an object and applies f
to it.
The continuation object is a first-class value and is represented as a function, with amb
operator for nondeterministic choice, Examples
As shown by the next example, call/cc can be used to emulate the function of the ISTOF X/code>, the code generalizes to ''any'' collection that can be traversed.
Call-with-current-continuation can also express other sophisticated primitives. For example, the next sample performs cooperative multitasking using continuations:
;; Cooperative multitasking using call-with-current-continuation
;; in 25 lines of scheme
;; The list of threads waiting to run. This is a list of one
;; argument non-returning functions (continuations, mostly)
;; A continuation is a non-returning function, just like (exit),
;; in that it never gives up control to whatever called it.
(define ready-list '())
;; A non-returning function. If there is any other thread
;; waiting to be run, it causes the next thread to run if there
;; is any left to run, otherwise it calls the original exit
;; which exits the whole environment.
(define exit
;; The original exit which we override.
(let ((exit exit))
;; The overriding function.
(lambda ()
(if (not (null? ready-list))
;; There is another thread waiting to be run.
;; So we run it.
(let ((cont (car ready-list)))
(set! ready-list (cdr ready-list))
;; Since the ready-list is only non-returning
;; functions, this will not return.
(cont #f))
;; Nothing left to run.
;; The original (exit) is a non returning function,
;; so this is a non-returning function.
(exit)))))
;; Takes a one argument function with a given
;; argument and forks it off. The forked function's new
;; thread will exit if/when the function ever exits.
(define (fork fn arg)
(set! ready-list
(append ready-list
;; This function added to the
;; ready-list is non-returning,
;; since exit is non returning.
(list
(lambda (x)
(fn arg)
(exit))))))
;; Gives up control for the next thread waiting to be run.
;; Although it will eventually return, it gives up control
;; and will only regain it when the continuation is called.
(define (yield)
(call-with-current-continuation
;; Capture the continuation representing THIS call to yield
(lambda (cont)
;; Stick it on the ready list
(set! ready-list
(append ready-list
(list cont)))
;; Get the next thread, and start it running.
(let ((cont (car ready-list)))
(set! ready-list (cdr ready-list))
;; Run it.
(cont #f)))))
In 1999, David Madore (inventor of the Unlambda
Unlambda is a minimal, "nearly pure" functional programming language invented by David Madore. It is based on combinatory logic, an expression system without the lambda operator or free variables. It relies mainly on two built-in functions (s ...
programming language) accidentally discovered a 12-character Unlambda term, making use of call/cc, that printed all natural numbers sequentially in unary representation: ``r`ci`.*`ci
. This program and the apparent mystery surrounding its effect have attracted some attention, and are commonly known as the ''yin-yang puzzle''. A Scheme translation, provided by Madore, is as follows:
(let* ((yin
((lambda (cc) (display #\@) cc) (call-with-current-continuation (lambda (c) c))))
(yang
((lambda (cc) (display #\*) cc) (call-with-current-continuation (lambda (c) c)))))
(yin yang))
Criticism
Oleg Kiselyov, author of a delimited continuation In programming languages, a delimited continuation, composable continuation or partial continuation, is a "slice" of a continuation frame that has been reified into a function. Unlike regular continuations, delimited continuations return a value, ...
implementation for OCaml
OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...
, and designer of an application programming interface
An application programming interface (API) is a connection between computers or between computer programs. It is a type of software Interface (computing), interface, offering a service to other pieces of software. A document or standard that des ...
(API) for delimited stack manipulation to implement control operators, advocates the use of delimited continuation In programming languages, a delimited continuation, composable continuation or partial continuation, is a "slice" of a continuation frame that has been reified into a function. Unlike regular continuations, delimited continuations return a value, ...
s instead of the full-stack continuations that call/cc manipulates: "Offering call/cc as a core control feature in terms of which all other control facilities should be implemented turns out a bad idea. Performance, memory and resource leaks, ease of implementation, ease of use, ease of reasoning all argue against call/cc."
Relation to non-constructive logic
The Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-p ...
between proofs and programs relates ''call/cc'' to Peirce's law
In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an Axiom#Mathematics, axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written ...
, which extends intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
to non-constructive, classical logic
Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this c ...
: ((α → β) → α) → α. Here, ((α → β) → α) is the type of the function ''f'', which can either return a value of type α directly or apply an argument to the continuation of type (α → β). Since the existing context is deleted when the continuation is applied, the type β is never used and may be taken to be ⊥, the empty type.
The principle of double negation elimination
In propositional logic, the double negation of a statement states that "it is not the case that the statement is not true". In classical logic, every statement is logically equivalent to its double negation, but this is not true in intuitionis ...
((α → ⊥) → ⊥) → α is comparable to a variant of call-cc which expects its argument ''f'' to always evaluate the current continuation without normally returning a value.
Embeddings of classical logic into intuitionistic logic are related to continuation passing style translation.
Languages implementing call/cc
* Scheme
* Racket
* Standard ML
Standard ML (SML) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Modular programming, modular, Functional programming, functional programming language with compile-time type checking and t ...
* Haskell
Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
in the continuation Monad
* Ruby
Ruby is a pinkish-red-to-blood-red-colored gemstone, a variety of the mineral corundum ( aluminium oxide). Ruby is one of the most popular traditional jewelry gems and is very durable. Other varieties of gem-quality corundum are called sapph ...
* Unlambda
Unlambda is a minimal, "nearly pure" functional programming language invented by David Madore. It is based on combinatory logic, an expression system without the lambda operator or free variables. It relies mainly on two built-in functions (s ...
* C++
* R
See also
* Goto
* Continuation-passing style
In functional programming, continuation-passing style (CPS) is a style of programming in which control is passed explicitly in the form of a continuation. This is contrasted with direct style, which is the usual style of programming. Gerald Jay S ...
* Fiber (computer science)
In computer science, a fiber is a particularly lightweight thread of execution.
Like threads, fibers share address space. However, fibers use cooperative multitasking while threads use preemptive multitasking. Threads often depend on the k ...
References
External links
A short introduction to call-with-current-continuation
* call-with-current-continuation
from Rob Warnock in Usenet's comp.lang.lisp
">ttps://groups.google.com/group/comp.lang.lisp/msg/4e1f782be5ba2841 Humorous explanation of call-with-current-continuation
from Rob Warnock in Usenet's comp.lang.lisp
br>Cooperative multitasking in Scheme using Call-CC