ABSTRACT
The last few years have seen a renewed interest in continuations for expressing advanced control structures in programming languages, and new models such as Abstract Continuations have been proposed to capture these dimensions. This article investigates an alternative formulation, exploiting the latent expressive power of the standard continuation-passing style (CPS) instead of introducing yet other new concepts. We build on a single foundation: abstracting control as a hierarchy of continuations, each one modeling a specific language feature as acting on nested evaluation contexts.
We show how iterating the continuation-passing conversion allows us to specify a wide range of control behavior. For example, two conversions yield an abstraction of Prolog-style backtracking. A number of other constructs can likewise be expressed in this framework; each is defined independently of the others, but all are arranged in a hierarchy making any interactions between them explicit.
This approach preserves all the traditional results about CPS, e.g., its evaluation order independence. Accordingly, our semantics is directly implementable in a call-by-value language such as Scheme or ML. Furthermore, because the control operators denote simple, typable lambda-terms in CPS, they themselves can be statically typed. Contrary to intuition, the iterated CPS transformation does not yield huge results: except where explicitly needed, all continuations beyond the first one disappear due to the extensionality principle (η-reduction).
Besides presenting a new motivation for control operators, this paper also describes an improved conversion into applicative-order CPS. The conversion operates in one pass by performing all administrative reductions at translation time; interestingly, it can be expressed very concisely using the new control operators. The paper also presents some examples of nondeterministic programming in direct style.
- Aho, Hopcroft, & Ullman 74.Alfred V. Aho, 3ohn E. Hopcroft, Jeffrey D. Ullman: The Design and Analffsis of Computer Algorithms, Addison-Wesley (1974) Google ScholarDigital Library
- Appel & Jim 89.Andrew W. Appel, Trevor Jim: Continuation. Passing, Closure-Passing Style, proceedings of the Sixteenth Annual ACM SIGACT-SIG PLAN Symposium on Principles of Programming Languages pp 293-302, Austin, Texas (January 1989) Google ScholarDigital Library
- Barendregt 85.Hendrick P. Barendregt: The Lambda Calculus, Rs Syntax and Semantics, revised edition, Studies in Logic and the Foundations of Mathematics, Vol. 103, North-Holland (1985)Google Scholar
- Danvy & Malmkjær 88.Olivier Danvy, Haroline Malmkjaer: Intensions and Extensions in a Reflective Tower, proceedings of the 1988 ACM Conference on Lisp and Functional Programming pp 327-341, Snowbird, Utah (July 1988) Google ScholarDigital Library
- Danvy & Filinski 89.Olivier Danvy, Andrzej Fillnski: A Functional Abstraction of Typed Contexts, DIKU Rapport 89/12, DIKU, University of Copenhagen, Copenhagen, Denmark (August 1989)Google Scholar
- Danvy 89.Olivier Danvy: Programming with Tighter Control, pp 10-29 of the BIGRE journal, No 65 on Putting Scheme to Work, Andr~ Pic, Michel Briand, and Jean B~zivin (eds.), Brest, France (July 1989)Google Scholar
- Felleisen et al 87.Matthiaz Felleisen, Daniel P. Friedman, Bruce Dubs, John Merrill: Beyond Continuations, Technical Report No 216, Computer Science Department, Indiana University, Bloomington, Indiana (February 1987)Google Scholar
- Felleisen 88.Matthias Felleisen: The Theory and Prac. tice of First-Glass Prompts, proceedings of the Firteenth Annual ACM SiGACT-SIGPLAN Symposium on Principles of Programming Languages pp 180-190, San Diego, California (January 1988) Google ScholarDigital Library
- Felleisen et al 88.Matthiaz Felleisen, Mitchell Wand, Daniel P. Friedman, Bruce F. Dubs: Abstract Contin. uations: A Mathematical Semantics for Handling Full Functional Jumps, proceedings of the 1988 ACM Conference on Lisp and Functional Programming pp 52-62, Snowbird, Utah (July 1988) Google ScholarDigital Library
- Filinski 89.Andrzej Filinski' Declarative Continuations' An Investigation o! Duality in Programming Language Semantics, proceedings of the Summer Conference on Category Theory and Computer Science, Lecture Notes in Computer Science No 389 pp 224-249, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, & A. Poign~ (eds.), Springer-Verlag, Manchester, UK (September 1989) Google ScholarDigital Library
- Fischer 72.Michael J. Fischer: Lambda Calculus Schemata, proceedings of the ACM conference Proving assertions about programs pp 104-109, SiGPLAN Notices, Vol. 7, No 1 and SIGACT News, No 14 (January 1972) Google ScholarDigital Library
- Friedman, Haynes, & Kohlbecker 84.Daniel P. Friedman, Christopher T. Haynes, Eugene Kohlbecker: Programruing with Continuations, NATO ASI Series, Vol. F8, Program Transformation and Programming Environments pp 263-274, P. Pepper (ed.), Springer-Verlag Berlin Heidelberg (1984)Google Scholar
- Haynes & Friedman 87.Christopher T. Haynes, Daniel P. Friedman: Embedding Continuations in Procedural Ohj~cts, TOPLAS, Vol. 9, No 4 pp 582-598 (October 1987) Preliminary version: Constraining Control, proceedings of the 12th ACM Symposium on Principles of Programruing Languages pp 245-254 (January 1985) Google ScholarDigital Library
- Johnson 87.Gregory F. Johnson: GL - A Denotational Testbed with Continuations and Partial Continuations as First-Class Objects, proceedings of the SIGPLAN'87 Symposium on Interpreters and Interpretive Tech~ niques pp 154-176, Saint-Paul, Minnesota (June 1987) Google ScholarDigital Library
- Johnson & Duggan 88.Gregory F. Johnson, Dominic Duggan: Stores and Partial Continuations as First-Class Objects in a Language and its Environment, proceedings of the Fifteenth Annum ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages pp 158-168, San Diego, California (January 1988) Google ScholarDigital Library
- Malmkjær 89.Karoline Malmkjaer: On some Semantic As. pects of the Reflective Tower, proceedings of the 4th Conference on Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science No ??, Michael Main, Austin Melton, Michael Mislove, and David Schmidt (eds.), Springer-Verlag, New Orleans, Louisiana (April 1989) Google ScholarDigital Library
- Mazurkiewicz 71.Antoni W. Mazurkiewicz: Proving Algorithms by Tail Functions, Information and Control Vol. 18 pp 220-226 (1971)Google ScholarCross Ref
- Mellish & Hardy 84.Chris Mellish, Steve Hardy: Integrating Prolog in the POPLOG Environment, in Implementations of PROLOG, John A. Campbell (ed.) pp 147- 162, Ellis Horwood (1984)Google Scholar
- Miller 87.James S. Miller: MultiScheme: A Parallel Pro. cessing System Based on MIT Scheme, PhD thesis, MIT/LGS/TR-402 (September 1987)Google Scholar
- Milne & Strachey 76.Robert E. Milne, Christopher Stra~ chey: A Theory of Programming Language Semantics, Chapman and Hall, London, and John Wiley, New York (1976) Google ScholarDigital Library
- Moggi 89.Eugenic Moggi' Computational Lambda-calculus and Monads, proceedings of 4th Conference on Logic in Computer Science pp 14-23, IEEE (1989). Google ScholarDigital Library
- Morris 72.James H. Morris Jr.: A Bonus from van Wijngaarden's Device, Communications of the ACM Vol. 15, No 8, p 773 (August 1972) Google ScholarDigital Library
- Plotkin 75.Gordon Plotkin: Call-by-Name, Gall-b~t-Value, and the A.calculus, Theoretical Computer Science, Vol. I pp 125-159 (1975)Google ScholarCross Ref
- Rees & Clinger 86.Jonathan Rees, William Clinger (eds.): SIGPLAN Notices, Vol. 21, No 12 pp 37-79 (December 1986) Google ScholarDigital Library
- Reynolds 72.John Reynolds: Definitional Interpreters for Higher-Order Programming Languages, proceedings 25th AGM National Conference pp 717-740, New York (1972) Google ScholarDigital Library
- Reynolds 74.John Reynolds: On the Relation between Direct and Continuation Semantics, 2nd Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science No 14 pp 141-156, Springer- Verlag, Jacques Loeckx (ed.), Saarbrflcken, West Getmany (July 1974) Google Scholar
- Sethi & Tang 80.Ravi Sethi, Adrian Tang: Constructing Call-by. Value Continuation Semantics, Journal of the ACM, Vol. 27, No 3 pp 580-597 (July 1980) Google ScholarDigital Library
- Sitaram & Felleisen 90.Dorai Sitaram, Matthias Felleisen: Control Delimiters and their Hierarchies, to appear in Lisp and Symbolic Computation, Rice University, Houston, Texas (June 1989) Google ScholarDigital Library
- Smith 82.Brian C. Smith: Reflection and Semantics in a Procedural Language, PhD thesis, MIT/LCS/TR-272, MIT, Cambridge, Massachusetts (January 1982)Google Scholar
- Steele & Sussman 76.Guy L. Steele Jr., Gerald J. Sussman: Lambda, the Ultimate Imperative, MIT-AIL, AI Memo No 353, Cambridge, Massachusetts (March 1976) Google ScholarDigital Library
- Steele 78.Guy L. Steele Jr.: RABBIT: A Compiler/or SCHEME, MIT-AIL, AI-TR-474, Cambridge, Massachusetts (May 1978) Google ScholarDigital Library
- Stoy 81.Joseph E. Stoy: The Congruence of Two Program. ruing Language Definitions, Theoretical Computer Science, Vol. 13 pp 151-174 (1981)Google ScholarCross Ref
- Strachey & Wadsworth 74.Christopher Strachey, Christopher P. Wadsworth: Continuations: A Mathematical Semantics for Handling Full Jumps, Technical Monograph PRG-11, Oxford University Computing Laboratory, Programming Research Group, Oxford, England (1974)Google Scholar
- van Wijngaarden 66.Adriaan van Wijngaarden: Recursive Definition of Syntax and Semantics, in Formal Lan. guage Description Languages for Computer Programruing pp 13-24, T. B. Steel Jr. (ed.), North-Holland (1966)Google Scholar
- Wand & Friedman 88.Mitchell Wand, Daniel P. Friedman: The MIlsterll of the Tower Revealed: A Non. Reflective Description of the Reflective Tower, Volume 1, Issue 1 of/Lisp and Symbolic Computation (May 1988)Google Scholar
Index Terms
- Abstracting control
Recommendations
Typing, representing, and abstracting control: functional pearl
TyDe 2018: Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven DevelopmentA well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a ...
Abstracting definitional interpreters (functional pearl)
In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide a ...
Abstracting abstract control
DLS '14The strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as closures, continuations, various forms of reflection, and a lack of static ...
Comments