Document Open Access Logo

A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers

Authors Dariusz Biernacki , Sergueï Lenglet , Piotr Polesiuk

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.7.pdf
  • Filesize: 0.54 MB
  • 22 pages

Document Identifiers

Author Details

Dariusz Biernacki
  • University of Wrocław, Poland
Sergueï Lenglet
  • Université de Lorraine, Nancy, France
Piotr Polesiuk
  • University of Wrocław, Poland

Acknowledgements

We would like to thank the anonymous reviewers for their helpful comments on the presentation of this work.

Cite As Get BibTex

Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.7

Abstract

We present a complete coinductive syntactic theory for an untyped calculus of algebraic operations and handlers, a relatively recent concept that augments a programming language with unprecedented flexibility to define, combine and interpret computational effects. Our theory takes the form of a normal-form bisimilarity and its soundness w.r.t. contextual equivalence hinges on using so-called context variables to test evaluation contexts comprising normal forms other than values. The theory is formulated in purely syntactic elementary terms and its completeness demonstrates the discriminating power of handlers. It crucially takes advantage of the clean separation of effect handling code from effect raising construct, a distinctive feature of algebraic effects, not present in other closely related control structures such as delimited-control operators.

Subject Classification

ACM Subject Classification
  • Theory of computation → Control primitives
Keywords
  • algebraic effect
  • handler
  • behavioral equivalence
  • bisimilarity

Metrics

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

References

  1. Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, The University of Texas Year of Programming Series, chapter 4, pages 65-116. Addison-Wesley, 1990. Google Scholar
  2. Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. Logical Methods in Computer Science, 13(3), 2017. Google Scholar
  3. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program., 84(1):108-123, 2015. URL: https://doi.org/10.1016/j.jlamp.2014.02.001.
  4. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Bisimulations for delimited-control operators. Logical Methods in Computer Science, 15(2), 2019. Google Scholar
  5. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. A complete normal-form bisimilarity for state. In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 98-114. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_6.
  6. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Diacritical companions. In Barbara König, editor, Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, volume 347 of Electronic Notes in Theoretical Computer Science, pages 25-43, London, England, 2019. Google Scholar
  7. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Proving soundness of extensional normal-form bisimilarities. Logical Methods in Computer Science, 15(1), 2019. Google Scholar
  8. 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. Google Scholar
  9. Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Abstracting algebraic effects. PACMPL, 3(POPL):6:1-6:28, 2019. URL: https://doi.org/10.1145/3290319.
  10. Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151-160, Nice, France, June 1990. ACM Press. Google Scholar
  11. Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and Peter Mager, editors, Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180-190, San Diego, California, January 1988. ACM Press. Google Scholar
  12. 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. Google Scholar
  13. Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational metatheory for algebraic effects. In Jean-Pierre Jouannaud, editor, Proceedings of the 25th IEEE Symposium on Logic in Computer Science (LICS 2010), pages 209-218, Edinburgh, UK, July 2010. IEEE Computer Society Press. Google Scholar
  14. Ugo Dal Lago and Francesco Gavazzo. Effectful normal form bisimulation. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 263-292, Prague, Czech Republic, April 2019. Springer. Google Scholar
  15. Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. Effectful applicative bisimilarity: Monads, relators, and Howe’s method. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12, Reykjavik, Iceland, June 2017. IEEE Computer Society. Google Scholar
  16. Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. Effectful applicative similarity for call-by-name lambda calculi. In Dario Della Monica, Aniello Murano, Sasha Rubin, and Luigi Sauro, editors, Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 IEEE International Workshop on Measurements and Networking (2017 IEEE M&N), volume 1949 of CEUR Workshop Proceedings, pages 87-98, Naples, Italy, September 2017. CEUR-WS.org. Google Scholar
  17. Søren B. Lassen. Eager normal form bisimulation. In Prakash Panangaden, editor, Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science, pages 345-354, Chicago, IL, June 2005. IEEE Computer Society Press. Google Scholar
  18. Jean-Marie Madiot. Higher-order languages: dualities and bisimulation enhancements. PhD thesis, Université de Lyon and Università di Bologna, 2015. Google Scholar
  19. Cristina Matache and Sam Staton. A sound and complete logic for algebraic effects. In Mikolaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 382-399, Prague, Czech Republic, April 2019. Springer. Google Scholar
  20. James H. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, Massachusets Institute of Technology, 1968. Google Scholar
  21. Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Typed equivalence of effect handlers and delimited control. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, volume 131 of LIPIcs, pages 30:1-30:16, Dortmund, Germany, June 2019. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. Google Scholar
  22. Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Logical Methods in Computer Science, 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:23)2013.
  23. Damien Pous. Coinduction all the way up. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 307-316, New York, NY, USA, July 2016. ACM. Google Scholar
  24. John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513-523, Paris, France, 1983. IFIP. Google Scholar
  25. Davide Sangiorgi. The lazy lambda calculus in a concurrency scenario. In Andre Scedrov, editor, LICS'92, pages 102-109, Santa Cruz, California, June 1992. IEEE Computer Society. Google Scholar
  26. Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, October 1998. Google Scholar
  27. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems, 33(1):1-69, January 2011. Google Scholar
  28. Chung-chieh Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation, 20(4):371-401, 2007. Google Scholar
  29. Alex Simpson and Niels F. W. Voorneveld. Behavioural equivalence via modalities for algebraic effects. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 300-326, Thessaloniki, Greece, April 2018. Springer. Google Scholar
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