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.
@InProceedings{dagnino_et_al:LIPIcs.ECOOP.2025.8, author = {Dagnino, Francesco and Giannini, Paola and Zucca, Elena}, title = {{An Effectful Object Calculus}}, booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)}, pages = {8:1--8:30}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-373-7}, ISSN = {1868-8969}, year = {2025}, volume = {333}, editor = {Aldrich, Jonathan and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.8}, URN = {urn:nbn:de:0030-drops-233017}, doi = {10.4230/LIPIcs.ECOOP.2025.8}, annote = {Keywords: Object calculi, handlers, type-and-effect systems} }
Feedback for Dagstuhl Publishing