Paper accepted for publication at ICFP 2023
Our paper “With or Without You: Programming with Effect Exclusion” (Matthew Lutze, Magnus Madsen,
Philipp Schuster
ResearcherPhilipp Schuster, and 
Jonathan Brachthäuser
Head of the SE research groupJonathan Immanuel Brachthäuser) has been accepted for publication at the International Conference on Functional Programming (ICFP 2023).
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 lambda-C 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.