{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:51Z","timestamp":1780994751108,"version":"3.54.1"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100014013","name":"UKRI","doi-asserted-by":"crossref","award":["MR\/T043830\/1"],"award-info":[{"award-number":["MR\/T043830\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system would require adding extensive effect annotations to the millions of lines of existing code in these languages. Recent proposals seek to address this problem by removing the need for explicit effect polymorphism. However, they typically rely on fragile syntactic mechanisms or on introducing a separate notion of second-class function. We introduce a novel approach based on modal effect types.<\/jats:p>","DOI":"10.1145\/3720476","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1130-1157","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Modal Effect Types"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-6589-3821","authenticated-orcid":false,"given":"Wenhao","family":"Tang","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7046-3035","authenticated-orcid":false,"given":"Leo","family":"White","sequence":"additional","affiliation":[{"name":"Jane Street, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4609-9101","authenticated-orcid":false,"given":"Stephen","family":"Dolan","sequence":"additional","affiliation":[{"name":"Jane Street, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4730-9315","authenticated-orcid":false,"given":"Daniel","family":"Hillerstr\u00f6m","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1360-4714","authenticated-orcid":false,"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3538-9688","authenticated-orcid":false,"given":"Anton","family":"Lorenzen","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30829-1_1"},{"key":"e_1_2_1_3_1","volume-title":"Algebra and Coalgebra in Computer Science","author":"Bauer Andrej","unstructured":"Andrej Bauer and Matija Pretnar. 2013. An Effect System for Algebraic Effects and Handlers. In Algebra and Coalgebra in Computer Science, Reiko Heckel and Stefan Milius (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201316. isbn:978-3-642-40206-7"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527320"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408993"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000039"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622871"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_9"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_1_18_1","volume-title":"Syntax and semantics of modal type theory. Ph. D. Dissertation","author":"Gratzer Daniel","unstructured":"Daniel Gratzer. 2023. Syntax and semantics of modal type theory. Ph. D. Dissertation. Aarhus University."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-17(3:11)2021"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Daniel Hillerstr\u00f6m and Sam Lindley. 2016. Liberating effects with rows and handlers. In TyDe. ACM 15\u201327.","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000040"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.7488\/era\/2122"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00005-0"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000131"},{"key":"e_1_2_1_29_1","volume-title":"Foundations of Software Science and Computation Structures","unstructured":"Shin-ya Katsumata. 2018. A Double Category Theoretic Analysis of Graded Linear Exponential Comonads. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham. 110\u2013127. isbn:978-3-319-89366-2"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/BSL.2023.14"},{"key":"e_1_2_1_31_1","volume-title":"Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP","author":"Leijen Daan","year":"2005","unstructured":"Daan Leijen. 2005. Extensible records with scoped labels. In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005, Marko C. J. D. van Eekelen (Ed.) (Trends in Functional Programming, Vol. 6). Intellect, 179\u2013194."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290325"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622860"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622814"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_43_1","volume-title":"Plotkin and Matija Pretnar","author":"Gordon","year":"2013","unstructured":"Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Log. Methods Comput. Sci., 9, 4 (2013)."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:21)2014"},{"key":"e_1_2_1_45_1","unstructured":"Didier R\u00e9my. 1994. Type Inference for Records in a Natural Extension of ML. In Theoretical Aspects of Object-Oriented Programming: Types Semantics and Language Design."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/361011.361061"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.12300"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632896"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2407.11816"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","unstructured":"Wenhao Tang Leo White Stephen Dolan Daniel Hillerstr\u00f6m Sam Lindley and Anton Lorenzen. 2025. OOPSLA25 Artifact for Modal Effect Types. https:\/\/doi.org\/10.5281\/zenodo.14982742 10.5281\/zenodo.14982742","DOI":"10.5281\/zenodo.14982742"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2302.01415"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775050.2633358"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563289"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674655"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607850"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2404.16381"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2022.2"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473580"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720476","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720476","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:11:18Z","timestamp":1760029878000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720476"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":61,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720476"],"URL":"https:\/\/doi.org\/10.1145\/3720476","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}