Document Open Access Logo

A Functional Abstraction of Typed Invocation Contexts

Authors Youyou Cong , Chiaki Ishio, Kaho Honda, Kenichi Asai

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2021.12.pdf
  • Filesize: 0.84 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Functional constructs
  • Theory of computation → Control primitives
  • Theory of computation → Type structures
Keywords
  • delimited continuations
  • control operators
  • control and prompt
  • CPS translation
  • type system

Metrics

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

Abstract

In their paper "A Functional Abstraction of Typed Contexts", Danvy and Filinski show how to derive a type system of the shift and reset operators from a CPS translation. In this paper, we show how this method scales to Felleisen’s control and prompt operators. Compared to shift and reset, control and prompt exhibit a more dynamic behavior, in that they can manipulate a trail of contexts surrounding the invocation of captured continuations. Our key observation is that, by adopting a functional representation of trails in the CPS translation, we can derive a type system that allows fine-grain reasoning of programs involving manipulation of invocation contexts.

Cite As Get BibTex

Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai. A Functional Abstraction of Typed Invocation Contexts. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.12

Author Details

Youyou Cong
  • Tokyo Institute of Technology, Japan
Chiaki Ishio
  • Ochanomizu University, Tokyo,Japan
Kaho Honda
  • Ochanomizu University, Tokyo, Japan
Kenichi Asai
  • Ochanomizu University, Tokyo, Japan

Funding

  • Cong, Youyou: supported in part by JSPS KAKENHI under Grant No. 19K24339.
  • Asai, Kenichi: supported in part by JSPS KAKENHI under Grant No. JP18H03218.

Acknowledgements

We sincerely thank the reviewers for their constructive feedback.

Supplementary Materials

References

  1. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, PPDP '03, pages 8-19, New York, NY, USA, 2003. ACM. URL: https://doi.org/10.1145/888251.888254.
  2. Kenichi Asai, Youyou Cong, and Chiaki Ishio. A functional abstraction of typed trails. Short paper presented at the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2021), 2021. Google Scholar
  3. Kenichi Asai and Yukiyoshi Kameyama. Polymorphic delimited continuations. In Proceedings of the 5th Asian Conference on Programming Languages and Systems, APLAS'07, pages 239-254, Berlin, Heidelberg, 2007. Springer-Verlag. Google Scholar
  4. Kenichi Asai and Chihiro Uehara. Selective CPS transformation for shift and reset. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM '18, pages 40-52, New York, NY, USA, December 2017. ACM. URL: https://doi.org/10.1145/3162069.
  5. Andrej Bauer and Matija Pretnar. An effect system for algebraic effects and handlers. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science, pages 1-16, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  6. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming, 84(1):108-123, 2015. Google Scholar
  7. Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1, 2005. Google Scholar
  8. Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A dynamic continuation-passing style for dynamic delimited continuations. BRICS Report Series, 13(15), 2006. Google Scholar
  9. Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A dynamic continuation-passing style for dynamic delimited continuations. ACM Trans. Program. Lang. Syst., 38(1), 2015. URL: https://doi.org/10.1145/2794078.
  10. Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the static and dynamic extents of delimited continuations. Science of Computer Programming, 60(3):274-297, 2006. Google Scholar
  11. Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski. A reflection on continuation-composing style. In Proceedings of 5th International Conference on Formal Structures for Computation and Deduction, FSCD '20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2020. Google Scholar
  12. Thierry Coquand. Pattern matching with dependent types. In Proceedings of the Third Workshop on Logical Frameworks, 1992. Google Scholar
  13. Olivier Danvy. Type-directed partial evaluation. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '96, pages 242-257. ACM, 1996. Google Scholar
  14. Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. BRICS 89/12, 1989. Google Scholar
  15. Olivier Danvy and Andrzej Filinski. Abstracting control. In Proceedings of the 1990 ACM conference on LISP and functional programming, pages 151-160. ACM, 1990. Google Scholar
  16. R. Kent Dyvbig, Simon Peyton Jones, and Amr Sabry. A monadic framework for delimited continuations. J. Funct. Program., 17(6):687-730, November 2007. URL: https://doi.org/10.1017/S0956796807006259.
  17. Matthias Felleisen. On the expressive power of programming languages. In Selected Papers from the Symposium on 3rd European Symposium on Programming, ESOP '90, pages 35-75, New York, NY, USA, 1991. Elsevier North-Holland, Inc. Google Scholar
  18. Mattias Felleisen. The theory and practice of first-class prompts. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '88, pages 180-190, New York, NY, USA, 1988. ACM. URL: https://doi.org/10.1145/73560.73576.
  19. Andrzej Filinski. Representing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '94, pages 446-457, New York, NY, USA, 1994. ACM. URL: https://doi.org/10.1145/174675.178047.
  20. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang., 1(ICFP):13:1-13:29, August 2017. URL: https://doi.org/10.1145/3110257.
  21. Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, FPCA '95, pages 12-23, New York, NY, USA, 1995. ACM. URL: https://doi.org/10.1145/224164.224173.
  22. Daniel Hillerström and Sam Lindley. Shallow effect handlers. In Asian Symposium on Programming Languages and Systems, APLAS '18, pages 415-435. Springer, 2018. Google Scholar
  23. Daniel Hillerström, Sam Lindley, and Robert Atkey. Effect handlers via generalised continuations. Journal of Functional Programming, 30, 2020. URL: https://doi.org/10.1017/S0956796820000040.
  24. Daniel Hillerström, Sam Lindley, Robert Atkey, and KC Sivaramakrishnan. Continuation passing style for effect handlers. In Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction, FSCD '17, pages 18:1-18:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  25. Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming, ICFP '03, pages 177-188. ACM, 2003. Google Scholar
  26. Yukiyoshi Kameyama and Takuo Yonezawa. Typed dynamic control operators for delimited continuations. In International Symposium on Functional and Logic Programming, FLOPS '08, pages 239-254. Springer, 2008. Google Scholar
  27. Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13, pages 145-158, New York, NY, USA, 2013. ACM. URL: https://doi.org/10.1145/2500365.2500590.
  28. Oleg Kiselyov and K. C. Sivaramakrishnan. Eff directly in ocaml. In ML Workshop, 2016. Google Scholar
  29. Daan Leijen. Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 486-499, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009872.
  30. Moe Masuko and Kenichi Asai. Caml Light+ shift/reset= Caml Shift. In Theory and Practice of Delimited Continuations, TPDC '11, pages 33-46, 2011. Google Scholar
  31. Marek Materzok. Axiomatizing subtyped delimited continuations. In Computer Science Logic 2013, CSL 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  32. Marek Materzok and Dariusz Biernacki. Subtyping delimited continuations. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 81-93, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/2034773.2034786.
  33. Robin Milner. A theory of type polymorphism in programming. Journal of computer and system sciences, 17(3):348-375, 1978. Google Scholar
  34. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  35. Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Typed equivalence of effect handlers and delimited control. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  36. Gordon Plotkin and Matija Pretnar. Handlers of algebraic effects. In European Symposium on Programming, ESOP '09, pages 80-94. Springer, 2009. Google Scholar
  37. Tiark Rompf, Ingo Maier, and Martin Odersky. Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP '09, pages 317-328, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1596550.1596596.
  38. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and symbolic computation, 6(3):289-360, 1993. Google Scholar
  39. Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM transactions on programming languages and systems (TOPLAS), 19(6):916-941, 1997. Google Scholar
  40. Chung-chieh Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation, 20(4):371-401, 2007. Google Scholar
  41. Fei Wang, Daniel Zheng, James Decker, Xilun Wu, Grégory M Essertel, and Tiark Rompf. Demystifying differentiable programming: Shift/reset the penultimate backpropagator. Proceedings of the ACM on Programming Languages, 3(ICFP):1-31, 2019. Google Scholar
  42. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and computation, 115(1):38-94, 1994. Google Scholar
  43. Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen. Effect handlers, evidently. Proceedings of the ACM on Programming Languages, 4(ICFP):1-29, 2020. URL: https://doi.org/10.1145/3408981.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact