In programming languages, a delimited continuation, composable continuation or partial continuation, is a "slice" of a continuationframe that has been reified into a function. Unlike regular continuations, delimited continuations return a value, and thus may be reused and composed. Control delimiters, the basis of delimited continuations, were introduced by Matthias Felleisen in 1988[1] though early allusions to composable and delimited continuations can be found in Carolyn Talcott's Stanford 1984 dissertation, Felleisen et al.,[2] Felleisen's 1987 dissertation,[3] and algorithms for functional backtracking, e.g., for pattern matching, for parsing, in the Algebraic Logic Functional programming language, and in the functional implementations of Prolog where the failure continuation is often kept implicit and the reason of being for the success continuation is that it is composable.
Delimited continuations were first introduced by Felleisen in 1988[1] with an operator called , first introduced in a tech report in 1987,[2] along with a prompt construct . The operator was designed to be a generalization of control operators that had been described in the literature such as call/cc from Scheme, ISWIM's J operator, John C. Reynolds' escape operator, and others. Subsequently, many competing delimited control operators were invented by the programming languages research community such as prompt and control,[4]shift and reset,[5][6]cupto,[7]fcontrol, and others.
Examples
Various operators for delimited continuations have been proposed in the research literature.[8]
One independent proposal[5] is based on continuation-passing style (CPS) -- i.e., not on continuation frames—and offers two control operators, shift and reset, that give rise to static rather than to dynamic delimited continuations.[9] The reset operator sets the limit for the continuation while the shift operator captures or reifies the current continuation up to the innermost enclosing reset. For example, consider the following snippet in Scheme:
(*2(reset(+1(shiftk(k5)))))
The reset delimits the continuation that shift captures (named by k in this example). When this snippet is executed, the use of shift will bind k to the continuation (+ 1 []) where [] represents the part of the computation that is to be filled with a value. This continuation directly corresponds to the code that surrounds the shift up to the reset. Because the body of shift (i.e., (k 5)) immediately invokes the continuation, this code is equivalent to the following:
(*2(+15))
In general, these operators can encode more interesting behavior by, for example, returning the captured continuation k as a value or invoking k multiple times. The shift operator passes the captured continuation k to the code in its body, which can either invoke it, produce it as a result, or ignore it entirely. Whatever result that shift produces is provided to the innermost reset, discarding the continuation in between the reset and shift. However, if the continuation is invoked, then it effectively re-installs the continuation after returning to the reset. When the entire computation within reset is completed, the result is returned by the delimited continuation.[10] For example, in this Scheme code:
(reset(*2(shiftkCODE)))
whenever CODE invokes (k N), (* 2 N) is evaluated and returned.
This is equivalent to the following:
(let((k(lambda(x)(*2x))))CODE)
Furthermore, once the entire computation within shift is completed, the continuation is discarded, and execution restarts outside reset. Therefore,
(reset(*2(shiftk(k(k4)))))
invokes (k 4) first (which returns 8), and then (k 8) (which returns 16). At this point, the shift expression has terminated, and the rest of the reset expression is discarded. Therefore, the final result is 16.
Everything that happens outside the reset expression is hidden, i.e. not influenced by the control transfer. For example, this returns 17:
(+1(reset(*2(shiftk(k(k4))))))
Delimited continuations were first described independently by Felleisen et al.[2] and Johnson.[11] They have since been used in a large number of domains, particularly in defining new control operators; see Queinnec[12] for a survey.
Let's take a look at a more complicated example. Let null be the empty list:
(reset(begin(shiftk(cons1(k(void))));; (1)null))
The context captured by shift is (begin [*] null), where [*] is the hole where k's parameter will be injected. The first call of k inside shift evaluates to this context with (void) = #<void> replacing the hole, so the value of (k (void)) is (begin #<void> null) = null. The body of shift, namely (cons 1 null) = (1), becomes the overall value of the reset expression as the final result.
A worked-out illustration of the (shift k k) idiom: the generalized curry function
The generalized curry function is given an uncurried function f and its arity (say, 3), and it returns the value of (lambda (v1) (lambda (v2) (lambda (v3) (f v1 v2 v3)))). This example is due to Olivier Danvy and was worked out in the mid-1980s.[13]
Here is a unit-test function to illustrate what the generalized curry function is expected to do:
These unit tests verify whether currying the variadic function + into an n-ary curried function and applying the result to n arguments yields the same result as applying + to these n arguments, for n = 0, 1, 2, 3, and 4.
The following recursive function is accumulator-based and eventually reverses the accumulator before applying the given uncurried function. In each instance of the induction step, the function (lambda (v) ...) is explicitly applied to an argument in the curried application:
The following recursive function is continuation-based and involves no list reversal. Likewise, in each instance of the induction step, the function (lambda (v) ...) is explicitly applied to an argument in the curried application:
The following recursive function, curry_d, is the direct-style counterpart of curry_c and features the (shift k k) idiom, using Andrzej Filinski's implementation of shift and reset in terms of a global mutable cell and of call/cc.[14] In each instance of the induction step, the continuation abstraction is implicitly applied to an argument in the curried application:
The heart of the matter is the observational equivalence between (reset (... (shift k k) ...)) and (lambda (x) (reset (... x ...))) where x is fresh and the ellipses represent a pure context, i.e., one without control effects.
The definition of curry_d also illustrates static delimited continuations. This static extent needs to be explicitly encoded if one wants to use control and prompt:[15]
In mathematics and computer science, currying is the technique of translating a function that takes multiple arguments into a sequence of families of functions, each taking a single argument.
In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an expression until its value is needed and which also avoids repeated evaluations.
Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic of this article, is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. In 1936, Church found a formulation which was logically consistent, and documented it in 1940.
Scheme is a dialect of the Lisp family of programming languages. Scheme was created during the 1970s at the MIT Computer Science and Artificial Intelligence Laboratory and released by its developers, Guy L. Steele and Gerald Jay Sussman, via a series of memos now known as the Lambda Papers. It was the first dialect of Lisp to choose lexical scope and the first to require implementations to perform tail-call optimization, giving stronger support for functional programming and associated techniques such as recursive algorithms. It was also one of the first programming languages to support first-class continuations. It had a significant influence on the effort that led to the development of Common Lisp.
In programming languages, a closure, also lexical closure or function closure, is a technique for implementing lexically scoped name binding in a language with first-class functions. Operationally, a closure is a record storing a function together with an environment. The environment is a mapping associating each free variable of the function with the value or reference to which the name was bound when the closure was created. Unlike a plain function, a closure allows the function to access those captured variables through the closure's copies of their values or references, even when the function is invoked outside their scope.
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 and an apply operator. These alone make it Turing-complete, but there are also some input/output (I/O) functions to enable interacting with the user, some shortcut functions, and a lazy evaluation function. Variables are unsupported.
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.
In combinatory logic for computer science, a fixed-point combinator, is a higher-order function that returns some fixed point of its argument function, if one exists.
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.
In computer science, a continuation is an abstract representation of the control state of a computer program. A continuation implements (reifies) the program control state, i.e. the continuation is a data structure that represents the computational process at a given point in the process's execution; the created data structure can be accessed by the programming language, instead of being hidden in the runtime environment. Continuations are useful for encoding other control mechanisms in programming languages such as exceptions, generators, coroutines, and so on.
In computer science, a generator is a routine that can be used to control the iteration behaviour of a loop. All generators are also iterators. A generator is very similar to a function that returns an array, in that a generator has parameters, can be called, and generates a sequence of values. However, instead of building an array containing all the values and returning them all at once, a generator yields the values one at a time, which requires less memory and allows the caller to get started processing the first few values immediately. In short, a generator looks like a function but behaves like an iterator.
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 Sussman and Guy L. Steele, Jr. coined the phrase in AI Memo 349 (1975), which sets out the first version of the Scheme programming language. John C. Reynolds gives a detailed account of the numerous discoveries of continuations.
In the Scheme computer programming language, the procedure call-with-current-continuation, abbreviated call/cc, is used as a control flow operator. It has been adopted by several other programming languages.
The SKI combinator calculus is a combinatory logic system and a computational system. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language. It can be likened to a reduced version of the untyped lambda calculus. It was introduced by Moses Schönfinkel and Haskell Curry.
In computer science, function composition is an act or mechanism to combine simple functions to build more complicated ones. Like the usual composition of functions in mathematics, the result of each function is passed as the argument of the next, and the result of the last one is the result of the whole.
Daniel Paul Friedman is a professor of Computer Science at Indiana University in Bloomington, Indiana. His research focuses on programming languages, and he is a prominent author in the field.
In computer programming, an anonymous function is a function definition that is not bound to an identifier. Anonymous functions are often arguments being passed to higher-order functions or used for constructing the result of a higher-order function that needs to return a function. If the function is only used once, or a limited number of times, an anonymous function may be syntactically lighter than using a named function. Anonymous functions are ubiquitous in functional programming languages and other languages with first-class functions, where they fulfil the same role for the function type as literals do for other data types.
In mathematics and computer science, apply is a function that applies a function to arguments. It is central to programming languages derived from lambda calculus, such as LISP and Scheme, and also in functional languages. It has a role in the study of the denotational semantics of computer programs, because it is a continuous function on complete partial orders. Apply is also a continuous function in homotopy theory, and, indeed underpins the entire theory: it allows a homotopy deformation to be viewed as a continuous path in the space of functions. Likewise, valid mutations (refactorings) of computer programs can be seen as those that are "continuous" in the Scott topology.
A CEK Machine is an abstract machine invented by Matthias Felleisen and Daniel P. Friedman that implements left-to-right call by value. It is generally implemented as an interpreter for functional programming languages, but can also be used to implement simple imperative programming languages. A state in a CEK machine includes a control statement, environment and continuation. The control statement is the term being evaluated at that moment, the environment is (usually) a map from variable names to values, and the continuation stores another state, or a special halt case. It is a simplified form of another abstract machine called the SECD machine.
In computer science, refocusing is a program transformation used to implement a reduction semantics—i.e., a small-step operational semantics with an explicit representation of the reduction context—more efficiently. It is a step towards implementing a deterministic semantics as a deterministic abstract machine.
↑ Rémy, Didier; Gunter, Carl; Riecke, Jon G. (1995). "A generalization of exceptions and control in ML-like languages". Functional Programming Language and Computer Architecture.
↑ See for instance the operators offered by the racket/controlRacket library ; the following examples can run in Racket using (require racket/control)
↑ Gasbichler, Martin; Sperber, Michael (2002). International Conference on Functional Programming. CiteSeerX10.1.1.11.3425.
↑ Johnson, Gregory F. (June 1987). "GL: a denotational testbed with continuations and partial continuations". Proc. SIGPLAN '87 Symposium on Interpreters and Interpretive Techniques. pp.218–225.
↑ Queinnec, Christian (April 1994). "A library of high-level control operators". Lisp Pointers, ACM SIGPLAN Special Interest Publ. On Lisp. 6. École Polytechnique and INRIA-Rocquencourt: 11–26. CiteSeerX10.1.1.29.4790.
This page is based on this Wikipedia article Text is available under the CC BY-SA 4.0 license; additional terms may apply. Images, videos and audio are available under their respective licenses.
