ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Tue 5 Sep 2023 11:30 - 12:00 at A - Grand Ballroom 2 - Effects Chair(s): Ningning Xie

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 \emph{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_\complement$ 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.

Tue 5 Sep

Displayed time zone: Pacific Time (US & Canada) change

10:30 - 12:00
EffectsICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Ningning Xie University of Toronto
10:30
30m
Talk
A General Fine-Grained Reduction Theory for Effect Handlers
ICFP Papers and Events
Filip Sieczkowski Heriot-Watt University, Mateusz Pyzik University of Wrocław, Dariusz Biernacki University of Wrocław
DOI
11:00
30m
Talk
Modular Models of Monoids with Operations
ICFP Papers and Events
Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London
DOI
11:30
30m
Talk
With or Without You: Programming with Effect Exclusion
ICFP Papers and Events
Matthew Lutze Aarhus University, Magnus Madsen Aarhus University, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
DOI