With or Without You: Programming with Effect Exclusion

Matthew Lutze, Magnus Madsen, Philipp Schuster, Jonathan Immanuel Brachthäuser

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Abstract

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' 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. 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 effect exclusion 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 λg calculus. We prove the standard progress and preservation theorems as well as a non-standard effect safety theorem: no excluded effect is ever performed. 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.

Original languageEnglish
JournalProceedings of the ACM on Programming Languages
Volume7
IssueICFP
Pages (from-to)448-475
Number of pages28
ISSN2475-1421
DOIs
Publication statusPublished - Aug 2023

Keywords

  • effect exclusion
  • polymorphic types and effects
  • without construct

Fingerprint

Dive into the research topics of 'With or Without You: Programming with Effect Exclusion'. Together they form a unique fingerprint.

Cite this