Document Open Access Logo

Typed Equivalence of Effect Handlers and Delimited Control

Authors Maciej Piróg , Piotr Polesiuk , Filip Sieczkowski

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.30.pdf
  • Filesize: 488 kB
  • 16 pages

Document Identifiers

Author Details

Maciej Piróg
  • University of Wrocław, Poland
Piotr Polesiuk
  • University of Wrocław, Poland
Filip Sieczkowski
  • University of Wrocław, Poland

Funding

  • Piróg, Maciej: National Science Centre, Poland, POLONEZ 3 grant "Algebraic Effects and Continuations" no. 2016/23/P/ST6/02217. This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 665778.
  • Polesiuk, Piotr: National Science Centre, Poland, grant no. 2014/15/B/ST6/00619.
  • Sieczkowski, Filip: National Science Centre, Poland, grant no. 2016/23/D/ST6/01387.

Acknowledgements

We would like to thank the anonymous reviewers of this paper for providing insightful comments and questions, particularly regarding presentation, as well as Dariusz Biernacki and Sam Lindley for helpful discussions of the technical content of the paper.

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.30

Abstract

It is folklore that effect handlers and delimited control operators are closely related: recently, this relationship has been proved in an untyped setting for deep handlers and the shift_0 delimited control operator. We positively resolve the conjecture that in an appropriately polymorphic type system this relationship can be extended to the level of types, by identifying the necessary forms of polymorphism, thus extending the definability result to the typed context. In the process, we identify a novel and potentially interesting type system feature for delimited control operators. Moreover, we extend these results to substantiate the folklore connection between shallow handlers and control_0 flavour of delimited control, both in an untyped and typed settings.

Subject Classification

ACM Subject Classification
  • Theory of computation → Control primitives
  • Theory of computation → Operational semantics
  • Software and its engineering → Polymorphism
Keywords
  • type-and-effect systems
  • algebraic effects
  • delimited control
  • macro expressibility

Metrics

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

Supplementary Materials

References

  1. Kenichi Asai. On typing delimited continuations: three new solutions to the printf problem. Higher-Order and Symbolic Computation, 22(3):275-291, 2009. URL: http://dx.doi.org/10.1007/s10990-009-9049-5.
  2. Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Handle with care: relational interpretation of algebraic effects and handlers. PACMPL, 2(POPL):8:1-8:30, 2018. URL: http://dx.doi.org/10.1145/3158096.
  3. Olivier Danvy. An analytical approach to programs as data objects. DSc thesis, Department of Computer Science, Aarhus University, 11, 2006. Google Scholar
  4. Olivier Danvy and Andrzej Filinski. Abstracting Control. In LISP and Functional Programming, pages 151-160, 1990. URL: http://dx.doi.org/10.1145/91556.91622.
  5. Matthias Felleisen. The Theory and Practice of First-Class Prompts. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, pages 180-190, 1988. URL: http://dx.doi.org/10.1145/73560.73576.
  6. Matthias Felleisen. On the Expressive Power of Programming Languages. Sci. Comput. Program., 17(1-3):35-75, 1991. URL: http://dx.doi.org/10.1016/0167-6423(91)90036-W.
  7. Matthias Felleisen and Daniel P. Friedman. A Reduction Semantics for Imperative Higher-Order Languages. In PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel Languages, Eindhoven, The Netherlands, June 15-19, 1987, Proceedings, pages 206-223, 1987. URL: http://dx.doi.org/10.1007/3-540-17945-3_12.
  8. 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: http://dx.doi.org/10.1145/3110257.
  9. Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, New York, NY, USA, 2nd edition, 2016. Google Scholar
  10. Daniel Hillerström and Sam Lindley. Shallow Effect Handlers. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, pages 415-435, 2018. URL: http://dx.doi.org/10.1007/978-3-030-02768-1_22.
  11. Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 145-158, 2013. URL: http://dx.doi.org/10.1145/2500365.2500590.
  12. Ikuo Kobori, Yukiyoshi Kameyama, and Oleg Kiselyov. Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators. In Proceedings of the Workshop on Continuations, WoC 2016, London, UK, April 12th 2015., pages 36-52, 2015. URL: http://dx.doi.org/10.4204/EPTCS.212.3.
  13. Daan Leijen. Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 486-499, 2017. URL: http://dl.acm.org/citation.cfm?id=3009872.
  14. Sam Lindley and James Cheney. Row-based effect types for database integration. In Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012, pages 91-102, 2012. URL: http://dx.doi.org/10.1145/2103786.2103798.
  15. John M. Lucassen and David K. Gifford. Polymorphic Effect Systems. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, pages 47-57, 1988. URL: http://dx.doi.org/10.1145/73560.73564.
  16. Marek Materzok and Dariusz Biernacki. A Dynamic Interpretation of the CPS Hierarchy. In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, pages 296-311, 2012. URL: http://dx.doi.org/10.1007/978-3-642-35182-2_21.
  17. 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, 1989. URL: http://dx.doi.org/10.1109/LICS.1989.39155.
  18. Gordon D. Plotkin and Matija Pretnar. Handling Algebraic Effects. Logical Methods in Computer Science, 9(4), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(4:23)2013.
  19. Chung-chieh Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation, 20(4):371-401, 2007. URL: http://dx.doi.org/10.1007/s10990-007-9010-4.
  20. Jean-Pierre Talpin and Pierre Jouvelot. The Type and Effect Discipline. Inf. Comput., 111(2):245-296, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1046.
  21. Philip Wadler. Comprehending Monads. In LISP and Functional Programming, pages 61-78, 1990. URL: http://dx.doi.org/10.1145/91556.91592.
  22. Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Inf. Comput., 115(1):38-94, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1093.
  23. Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003, pages 224-235, 2003. URL: http://dx.doi.org/10.1145/640128.604150.
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 About DROPS Imprint Privacy Contact