Document Open Access Logo

Monadic Type-And-Effect Soundness

Authors Francesco Dagnino , Paola Giannini , Elena Zucca

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.7.pdf
  • Filesize: 1.04 MB
  • 31 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Theory of computation → Type structures
Keywords
  • Effects
  • monads
  • type soundness

Metrics

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

Abstract

We introduce the abstract notions of monadic operational semantics, a small-step semantics where computational effects are modularly modeled by a monad, and type-and-effect system, including effect types whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usual in the non-monadic case, we can express progress and subject reduction, and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects, equipped with an expressive type-and-effect system We provide proofs of progress and subject reduction, parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies.

Cite As Get BibTex

Francesco Dagnino, Paola Giannini, and Elena Zucca. Monadic Type-And-Effect Soundness. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.7

Author Details

Francesco Dagnino
  • DIBRIS, Università di Genova, Italy
Paola Giannini
  • DiSSTE, Università del Piemonte Orientale, Vercelli, 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. Jirí Adámek, Nathan J. Bowler, Paul Blain Levy, and Stefan Milius. Coproducts of monads on set. CoRR, abs/1409.3804, 2014. URL: https://arxiv.org/abs/1409.3804.
  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, 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. Michael Barr. Relational algebras. In S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski, editors, Reports of the Midwest Category Seminar IV, number 137 in Lecture Notes in Mathematics, pages 39-55, Berlin, Heidelberg, 1970. Springer Berlin Heidelberg. Google Scholar
  4. 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.
  5. Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 1(2), 2005. URL: https://doi.org/10.2168/LMCS-1(2:1)2005.
  6. Francesco Dagnino. A meta-theory for big-step semantics. ACM Transactions on Computational Logic, 23(3):20:1-20:50, 2022. URL: https://doi.org/10.1145/3522729.
  7. Francesco Dagnino, Viviana Bono, Elena Zucca, and Mariangiola Dezani-Ciancaglini. Soundness conditions for big-step semantics. 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 169-196. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_7.
  8. 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.
  9. Francesco Dagnino, Paola Giannini, and Elena Zucca. Monadic type-and-effect soundness (extended version). CoRR, 2025. URL: http://arxiv.org/abs/2504.10159.
  10. Francesco Dagnino and Giuseppe Rosolini. Doctrines, modalities and comonads. Mathematical Structures in Computer Science, pages 1-30, 2021. URL: https://doi.org/10.1017/S0960129521000207.
  11. 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.
  12. 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.
  13. Samuel Eilenberg and John C. Moore. Adjoint functors and triples. Illinois Journal of Mathematics, 9(3):381-398, 1965. URL: https://doi.org/10.1215/ijm/1256068141.
  14. Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès. Towards a formal theory of graded monads. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures, 19th International Conference, FoSSaCS 2016,, volume 9634 of Lecture Notes in Computer Science, pages 513-530. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_30.
  15. 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.
  16. 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.
  17. 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.
  18. Alexander Grothendieck. Catégories fibrées et descente. In Revêtements étales et groupe fondamental, pages 145-194. Springer, 1971. Google Scholar
  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. Martin Hyland, Gordon D. Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical Computer Science, 357(1-3):70-99, 2006. URL: https://doi.org/10.1016/J.TCS.2006.03.013.
  21. 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.
  22. Mauro Jaskelioff and Eugenio Moggi. Monad transformers as monoid transformers. Theoretical Computer Science, 411(51-52):4441-4466, 2010. URL: https://doi.org/10.1016/J.TCS.2010.09.011.
  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. 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.
  27. 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.
  28. Ernest G. Manes. Algebraic Theories. Graduate Texts in Mathematics. Springer, 1976. URL: https://doi.org/10.1007/978-1-4612-9860-1.
  29. 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.
  30. 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.
  31. 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.
  32. 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.
  33. 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.
  34. 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.
  35. 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.
  36. 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.
  37. 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.
  38. 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.
  39. 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.
  40. 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.
  41. Emily Riehl. Category theory in context. Courier Dover Publications, 2017. Google Scholar
  42. 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.
  43. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. URL: https://doi.org/10.1016/0022-4049(72)90019-9.
  44. 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,, 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.
  45. 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.
  46. 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.
  47. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
  48. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in coq. Proceedings of the ACM on Programming Languages, 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
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