Document Open Access Logo

An Effectful Object Calculus

Authors Francesco Dagnino , Paola Giannini , Elena Zucca

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.8.pdf
  • Filesize: 1.01 MB
  • 30 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Theory of computation → Type structures
Keywords
  • Object calculi
  • handlers
  • type-and-effect systems

Metrics

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

Abstract

We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative of the last generation of OO languages, and the effectful extension is manageable enough for ordinary programmers; notably, constructs to raise effects are just special methods. We equip the calculus with an expressive type-and-effect system, which, again by relying on standard features such as inheritance and generic types, allows a simple form of effect polymorphism. The soundness of the type-and-effect system is expressed and proved by a recently introduced technique, where the semantics is formalized by a one-step reduction relation from language expressions into monadic ones, so that it is enough to prove progress and subject reduction properties on this relation.

Cite As Get BibTex

Francesco Dagnino, Paola Giannini, and Elena Zucca. An Effectful Object Calculus. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 8:1-8:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.8

Author Details

Francesco Dagnino
  • DIBRIS, Università di Genova, Italy
Paola Giannini
  • DiSSTE, Università del Piemonte Orientale, Italy
Elena Zucca
  • DIBRIS, Università di Genova, Italy

Funding

This work was partially funded by the MUR project "T-LADIES" (PRIN 2020TL3X8X) and has the financial support of the Università del Piemonte Orientale.

References

  1. Martín Abadi and Luca Cardelli. A theory of primitive objects: Untyped and first-order systems. Information and Computation, 125(2):78-102, 1996. URL: https://doi.org/10.1006/INCO.1996.0024.
  2. Danel Ahman and Andrej Bauer. Runners in action. In Peter Müller, editor, Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, volume 12075 of Lecture Notes in Computer Science, pages 29-55. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_2.
  3. Davide Ancona, Giovanni Lagorio, and Elena Zucca. A core calculus for Java exceptions. In Linda M. Northrop and John M. Vlissides, editors, ØOPSLA2001, pages 16-30. ACM Press, 2001. URL: https://doi.org/10.1145/504282.504284.
  4. Andrej Bauer and Matija Pretnar. Eff. URL: https://www.eff-lang.org/.
  5. Andrej Bauer and Matija Pretnar. An effect system for algebraic effects and handlers. Logical Methods in Computer Science, 10(4), 2014. URL: https://doi.org/10.2168/LMCS-10(4:9)2014.
  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. URL: https://doi.org/10.1016/J.JLAMP.2014.02.001.
  7. Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Abstracting algebraic effects. Proceedings of the ACM on Programming Languages, 3(POPL):6:1-6:28, 2019. URL: https://doi.org/10.1145/3290319.
  8. Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. Effects as capabilities: effect handlers and lightweight effect polymorphism. Proceedings of the ACM on Programming Languages, 4(OOPSLA):126:1-126:30, 2020. URL: https://doi.org/10.1145/3428194.
  9. Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in scala. Journal of Functional Programming, 30:e8, 2020. URL: https://doi.org/10.1017/S0956796820000027.
  10. Francesco Dagnino and Francesco Gavazzo. A fibrational tale of operational logical relations: Pure, effectful and differential. Logical Methods in Computer Science, 20(2), 2024. URL: https://doi.org/10.46298/LMCS-20(2:1)2024.
  11. Francesco Dagnino, Paola Giannini, and Elena Zucca. An effectful object calculus (extended version). CoRR, 2025. URL: https://doi.org/10.48550/arXiv.2504.15936.
  12. Francesco Dagnino, Paola Giannini, and Elena Zucca. Monadic type-and-effect soundness. In Jonathan Aldrich and Alexandra Silva, editors, 39th European Conference on Object-Oriented Programming, ECOOP 2025, volume 333 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2025.1.
  13. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proceedings of the ACM on Programming Languages, 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498692.
  14. David Darais, Nicholas Labich, Phuc C. Nguyen, and David Van Horn. Abstracting definitional interpreters (functional pearl). Proceedings of the ACM on Programming Languages, 1(ICFP):12:1-12:25, 2017. URL: https://doi.org/10.1145/3110256.
  15. Isaac Oscar Gariano, James Noble, and Marco Servetto. Calle: an effect system for method calls. In Hidehiko Masuhara and Tomas Petricek, editors, Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2019, pages 32-45. ACM, 2019. URL: https://doi.org/10.1145/3359591.3359731.
  16. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 452-461. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209149.
  17. Francesco Gavazzo and Claudia Faggian. A relational theory of monadic rewriting systems, part I. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470633.
  18. Francesco Gavazzo, Riccardo Treglia, and Gabriele Vanoni. Monadic intersection types, relationally. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, volume 14576 of Lecture Notes in Computer Science, pages 22-51. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_2.
  19. Daniel Hillerström and Sam Lindley. Shallow effect handlers. In Sukyoung Ryu, editor, Proceedings of the 16th Asian Symposium on Programming Languages and Systems, APLAS 2018, volume 11275 of Lecture Notes in Computer Science, pages 415-435. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02768-1_22.
  20. Daniel Hillerström, Sam Lindley, Robert Atkey, and K. C. Sivaramakrishnan. Continuation passing style for effect handlers. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, volume 84 of LIPIcs, pages 18:1-18:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.FSCD.2017.18.
  21. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ØOPSLA1999, pages 132-146. ACM Press, 1999. URL: https://doi.org/10.1145/320384.320395.
  22. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  23. Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational metatheory for algebraic effects. In Proceedings of the 25th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2010, pages 209-218. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.29.
  24. Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pages 145-158. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500590.
  25. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Suresh Jagannathan and Peter Sewell, editors, Proceedings of the 41st ACM/SIGPLAN Symposium on Principles of Programming Languages, POPL 2014, pages 633-646. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535846.
  26. Daan Leijen. Type directed compilation of row-typed algebraic effects. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM/SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 486-499. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009872.
  27. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Information and Computation, 185(2):182-210, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00088-9.
  28. Sheng Liang, Paul Hudak, and Mark P. Jones. Monad transformers and modular interpreters. In Ron K. Cytron and Peter Lee, editors, Proceedings of the 22nd ACM/SIGPLAN Symposium on Principles of Programming Languages, POPL 1995, pages 333-343. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199528.
  29. Sam Lindley, Conor McBride, and Craig McLaughlin. Do be do be do. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM/SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 500-514. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009897.
  30. Daniel Marino and Todd D. Millstein. A generic type-and-effect system. In Andrew Kennedy and Amal Ahmed, editors, TLDI'09: Types in Languages Design and Implementatio, pages 39-50. ACM Press, 2009. URL: https://doi.org/10.1145/1481861.1481868.
  31. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the 4th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 1989, pages 14-23. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39155.
  32. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  33. Flemming Nielson and Hanne Riis Nielson. Type and effect systems. In Ernst-Rüdiger Olderog and Bernhard Steffen, editors, Correct System Design, Recent Insight and Advances, volume 1710 of Lecture Notes in Computer Science, pages 114-136. Springer, 1999. URL: https://doi.org/10.1007/3-540-48092-7_6.
  34. Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, 4th International Conference, FoSSaCS 2001, volume 2030 of Lecture Notes in Computer Science, pages 1-24. Springer, 2001. URL: https://doi.org/10.1007/3-540-45315-6_1.
  35. Gordon D. Plotkin and John Power. Notions of computation determine monads. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FoSSaCS 2002, volume 2303 of Lecture Notes in Computer Science, pages 342-356. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_24.
  36. Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69-94, 2003. URL: https://doi.org/10.1023/A:1023064908962.
  37. Gordon D. Plotkin and John Power. Tensors of comodels and models for operational semantics. In Andrej Bauer and Michael W. Mislove, editors, The 24th Conference on Mathematical Foundations of Programming Semantics, MFPS 2008, volume 218 of Electronic Notes in Theoretical Computer Science, pages 295-311. Elsevier, 2008. URL: https://doi.org/10.1016/J.ENTCS.2008.10.018.
  38. Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Giuseppe Castagna, editor, Programming Languages and Systems - 18th European Symposium on Programming, ESOP 2009, volume 5502 of Lecture Notes in Computer Science, volume 5502 of Lecture Notes in Computer Science, pages 80-94. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_7.
  39. 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.
  40. A. John Power and Olha Shkaravska. From comodels to coalgebras: State and arrays. In Jirí Adámek and Stefan Milius, editors, Proceedings of the Workshop on Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of Electronic Notes in Theoretical Computer Science, pages 297-314. Elsevier, 2004. URL: https://doi.org/10.1016/J.ENTCS.2004.02.041.
  41. Matija Pretnar. An introduction to algebraic effects and handlers. Invited tutorial paper. In Dan R. Ghica, editor, The 31st Conference on Mathematical Foundations of Programming Semantics, MFPS 2015, volume 319 of Electronic Notes in Theoretical Computer Science, pages 19-35. Elsevier, 2015. URL: https://doi.org/10.1016/J.ENTCS.2015.12.003.
  42. Emily Riehl. Category theory in context. Courier Dover Publications, 2017. Google Scholar
  43. Marco Servetto and Elena Zucca. λ-based object-oriented programming (pearl). In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, volume 194 of LIPIcs, pages 21:1-21:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.ECOOP.2021.21.
  44. Alex Simpson and Niels F. W. Voorneveld. Behavioural equivalence via modalities for algebraic effects. ACM Transactions on Programming Languages and Systems, 42(1):4:1-4:45, 2020. URL: https://doi.org/10.1145/3363518.
  45. Tarmo Uustalu. Stateful runners of effectful computations. In Dan R. Ghica, editor, The 31st Conference on Mathematical Foundations of Programming Semantics, MFPS 2015, volume 319 of Electronic Notes in Theoretical Computer Science, pages 403-421. Elsevier, 2015. URL: https://doi.org/10.1016/J.ENTCS.2015.12.024.
  46. Philip Wadler. Monads for functional programming. In Johan Jeuring and Erik Meijer, editors, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, May 24-30, 1995, Tutorial Text, volume 925 of Lecture Notes in Computer Science, pages 24-52. Springer, 1995. URL: https://doi.org/10.1007/3-540-59451-5_2.
  47. Philip Wadler. The marriage of effects and monads. In Matthias Felleisen, Paul Hudak, and Christian Queinnec, editors, 3rd ACM SIGPLAN International Conference on Functional Programming, ICFP 1998, pages 63-74. ACM, 1998. URL: https://doi.org/10.1145/289423.289429.
  48. Philip Wadler and Peter Thiemann. The marriage of effects and monads. ACM Transactions on Computational Logic, 4(1):1-32, 2003. URL: https://doi.org/10.1145/601775.601776.
  49. Yanlin Wang, Haoyuan Zhang, Bruno C. d. S. Oliveira, and Marco Servetto. Classless Java. In Bernd Fischer and Ina Schaefer, editors, Generative Programming: Concepts and Experiences, GPCE 2016, pages 14-24. ACM Press, 2016. URL: https://doi.org/10.1145/2993236.2993238.
  50. Nick Webster, Marco Servetto, and Michael Homer. The Fearless journey [Draft]. CoRR, abs/2405.06233, 2014. URL: https://doi.org/10.48550/arXiv.2405.06233.
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