Programming with Effect Exclusion - Type and Effect Systems

Explore a groundbreaking presentation from ICFP 2023 that introduces a novel type and effect system with effect polymorphism, union, intersection, and complement effects. Delve into the concept of effect exclusion, a new class of effect polymorphic functions that allow reasoning about the absence of effects. Learn how this system builds on the Hindley-Milner type system, preserves principal types, and enables complete type and effect inference through Boolean unification. Examine the formalization of these concepts in the λ∁ calculus and understand the proof of standard progress, preservation theorems, and a non-standard effect safety theorem. Discover the practical implementation of this system as an extension of the Flix programming language and review a case study identifying 59 program fragments requiring effect exclusion for correctness. Gain insights into how this innovative approach enhances static reasoning about effects in various domains, including region-based memory management, exceptions, and algebraic effects and handlers.

[ICFP'23] With or Without You: Programming with Effect Exclusion