{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:14:42Z","timestamp":1767928482015,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>Type and effect systems have been successfully used to statically reason about effects in many different domains, including region-based memory management, exceptions, and algebraic effects and handlers. Such systems\u2019 soundness is often stated in terms of the absence of effects. Yet, existing systems only admit indirect reasoning about the absence of effects. This is further complicated by effect polymorphism which allows function signatures to abstract over arbitrary, unknown sets of effects.<\/jats:p>\n          <jats:p>\n            We present a new type and effect system with effect polymorphism as well as union, intersection, and complement effects. The effect system allows us to express\n            <jats:italic>effect exclusion<\/jats:italic>\n            as a new class of effect polymorphic functions: those that permit any effects except those in a specific set. This way, we equip programmers with the means to directly reason about the absence of effects. Our type and effect system builds on the Hindley-Milner type system, supports effect polymorphism, and preserves principal types modulo Boolean equivalence. In addition, a suitable extension of Algorithm W with Boolean unification on the algebra of sets enables complete type and effect inference. We formalize these notions in the \u03bb\n            <jats:sub>\u2201<\/jats:sub>\n            calculus. We prove the standard progress and preservation theorems as well as a non-standard effect safety theorem: no excluded effect is ever performed.\n          <\/jats:p>\n          <jats:p>We implement the type and effect system as an extension of the Flix programming language. We conduct a case study of open source projects identifying 59 program fragments that require effect exclusion for correctness. To demonstrate the usefulness of the proposed type and effect system, we recast these program fragments into our extension of Flix.<\/jats:p>","DOI":"10.1145\/3607846","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"448-475","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["With or Without You: Programming with Effect Exclusion"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2904-5099","authenticated-orcid":false,"given":"Matthew","family":"Lutze","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7510-8724","authenticated-orcid":false,"given":"Magnus","family":"Madsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8011-0506","authenticated-orcid":false,"given":"Philipp","family":"Schuster","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0020-0190(98)00106-9"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_1_3_1","volume-title":"The mathematical analysis of logic","author":"Boole George","unstructured":"George Boole. 1847. The mathematical analysis of logic. Macmillan, Barclay and Macmillan."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0747-7171(89)80054-9"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527320"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0747-7171(87)80065-2"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796820000039"},{"key":"e_1_2_1_9_1","volume-title":"Type assignment in programming languages. Ph. D. Dissertation","author":"Damas Luis","unstructured":"Luis Damas. 1984. Type assignment in programming languages. Ph. D. Dissertation. The University of Edinburgh."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_12"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503301"},{"key":"e_1_2_1_12_1","volume-title":"The Java language specification","author":"Gosling James","unstructured":"James Gosling, Bill Joy, and Guy Steele. 1996. The Java language specification. Addison-Wesley Professional."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_1_14_1","article-title":"The principal type-scheme of an object in combinatory logic","author":"Hindley Roger","year":"1969","unstructured":"Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society (AMS).","journal-title":"Transactions of the American Mathematical Society (AMS)."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796816000320"},{"key":"e_1_2_1_16_1","volume-title":"Type inference and equational theories. \u00c9cole polytechnique","author":"Kennedy Andrew J.","unstructured":"Andrew J. Kennedy. 1996. Type inference and equational theories. \u00c9cole polytechnique, Paris, France."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.1406.2061"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349230"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0890-5401(03)00088-9"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_1_22_1","unstructured":"Leopold L\u00f6wenheim. 1908. \u00dcber das Aufl\u00f6sungsproblem im logischen Klassenkalkul."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428222"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485487"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0747-7171(89)80013-6"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6_5"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057392"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143202"},{"key":"e_1_2_1_31_1","unstructured":"Sergiu Rudeanu. 1974. Boolean functions and equations."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363520"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01018828"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908086"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607846","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607846","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607846"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":36,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607846"],"URL":"https:\/\/doi.org\/10.1145\/3607846","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}