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

Effect handlers are a modern and increasingly popular approach to structuring computational effects in functional programming languages. However, while their traditional operational semantics is well-suited to implementation tasks, it is less ideal as a reduction theory. We therefore introduce a fine-grained reduction theory for deep effect handlers, inspired by our existing reduction theory for shift0, along with a standard reduction strategy. We relate this strategy to the traditional, non-local operational semantics via a simulation argument, and show that the reduction theory preserves observational equivalence with respect to the classical semantics of handlers, thus allowing its use as a rewriting theory for handler-equipped programming languages – this rewriting system mostly coincides with previously studied type-based optimisations. In the process, we establish theoretical properties of our reduction theory, including confluence and standardisation theorems, adapting and extending existing techniques. Finally, we demonstrate the utility of our semantics by providing the first normalisation-by-evaluation algorithm for effect handlers, and prove its soundness and completeness. Additionally, we establish non-expressibility of the lift operator, found in some effect-handler calculi, by the other constructs.

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 / Google DeepMind
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