Document Open Access Logo

A Reflection on Continuation-Composing Style

Authors Dariusz Biernacki , Mateusz Pyzik , Filip Sieczkowski

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.18.pdf
  • Filesize: 468 kB
  • 17 pages

Document Identifiers

Author Details

Dariusz Biernacki
  • Institute of Computer Science, University of Wrocław, Poland
Mateusz Pyzik
  • Institute of Computer Science, University Wrocław, Poland
Filip Sieczkowski
  • Institute of Computer Science, University Wrocław, Poland

Acknowledgements

We thank the anonymous reviewers and participants of NWPT'19 as well as the anonymous reviewers of FSCD 2020 for helpful comments on the presentation of this work.

Cite AsGet BibTex

Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski. A Reflection on Continuation-Composing Style. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.18

Abstract

We present a study of the continuation-composing style (CCS) that describes the image of the CPS translation of Danvy and Filinski’s shift and reset delimited-control operators. In CCS continuations are composable rather than abortive as in the traditional CPS, and, therefore, the structure of terms is considerably more complex. We show that the CPS translation from Moggi’s computational lambda calculus extended with shift and reset has a right inverse and that the two translations form a reflection i.e., a Galois connection in which the target is isomorphic to a subset of the source (the orders are given by the reduction relations). Furthermore, we use this result to show that Plotkin’s call-by-value lambda calculus extended with shift and reset is isomorphic to the image of the CPS translation. This result, in particular, provides a first direct-style transformation for delimited continuations that is an inverse of the CPS transformation up to syntactic identity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Control primitives
  • Theory of computation → Lambda calculus
Keywords
  • delimited control
  • continuation-passing style
  • reflection
  • call-by-value lambda calculus
  • computational lambda calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, 1992. Google Scholar
  2. Olivier Danvy. Back to direct style. Sci. Comput. Program., 22(3):183-195, 1994. URL: https://doi.org/10.1016/0167-6423(94)00003-4.
  3. Olivier Danvy and Andrzej Filinski. Abstracting control. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP 1990, Nice, France, 27-29 June 1990, pages 151-160. ACM, 1990. URL: https://doi.org/10.1145/91556.91622.
  4. Olivier Danvy and Julia L. Lawall. Back to direct style II: first-class continuations. In Proceedings of the Conference on Lisp and Functional Programming, LFP 1992, San Francisco, California, USA, 22-24 June 1992, pages 299-310. ACM, 1992. URL: https://doi.org/10.1145/141471.141564.
  5. Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD-machine, and the λ-calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986, pages 193-222. North-Holland, 1987. Google Scholar
  6. Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235-271, 1992. URL: https://doi.org/10.1016/0304-3975(92)90014-7.
  7. Andrzej Filinski. Representing monads. In Hans-Juergen Boehm, Bernard Lang, and Daniel M. Yellin, editors, Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, pages 446-457. ACM Press, 1994. URL: https://doi.org/10.1145/174675.178047.
  8. Michael J. Fischer. Lambda-calculus schemata. Lisp and Symbolic Computation, 6(3-4):259-288, 1993. Google Scholar
  9. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. PACMPL, 1(ICFP):13:1-13:29, 2017. URL: https://doi.org/10.1145/3110257.
  10. Annius Groenink. Literal movement grammars. In Steven P. Abney and Erhard W. Hinrichs, editors, EACL 1995, 7th Conference of the European Chapter of the Association for Computational Linguistics, March 27-31, 1995, University College Dublin, Belfield, Dublin, Ireland, pages 90-97. The Association for Computer Linguistics, 1995. URL: https://www.aclweb.org/anthology/E95-1013/.
  11. John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Hans-Juergen Boehm, Bernard Lang, and Daniel M. Yellin, editors, Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, pages 458-471. ACM Press, 1994. URL: https://doi.org/10.1145/174675.178053.
  12. Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Olin Shivers, editor, Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming (ICFP'03), SIGPLAN Notices, Vol. 38, No. 9, pages 177-188, Uppsala, Sweden, August 2003. ACM Press. Google Scholar
  13. Marek Materzok. Axiomatizing subtyped delimited continuations. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 521-539. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.521.
  14. Marek Materzok and Dariusz Biernacki. Subtyping delimited continuations. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 81-93. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034786.
  15. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 14-23. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39155.
  16. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  17. John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363-397, 1998. URL: https://doi.org/10.1023/A:1010027404223.
  18. John C. Reynolds. Theories of programming languages. Cambridge University Press, 1998. Google Scholar
  19. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3-4):289-360, 1993. Google Scholar
  20. Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Trans. Program. Lang. Syst., 19(6):916-941, 1997. URL: https://doi.org/10.1145/267959.269968.
  21. David A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc., 1986. Google Scholar
  22. Chung-chieh Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation, 20(4):371-401, 2007. URL: https://doi.org/10.1007/s10990-007-9010-4.
  23. Guy L. Steele Jr. Rabbit: A compiler for Scheme. Master’s thesis, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978. Technical report AI-TR-474. Google Scholar
  24. Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Higher-Order and Symbolic Computation, 13(1/2):135-152, 2000. URL: https://doi.org/10.1023/A:1010026413531.
  25. Philip Wadler. The essence of functional programming. In Ravi Sethi, editor, Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992, pages 1-14. ACM Press, 1992. URL: https://doi.org/10.1145/143165.143169.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact