ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
Tue 3 Sep 2024 10:30 - 10:48 at Green 1-2-3 - Algebraic and Computational Effects Chair(s): Patrick Bahr

Many effect systems for algebraic effect handlers are designed to guarantee that all invoked effects are handled adequately. However, respective researchers have developed their own effect systems that differ in how to represent the collections of effects that may happen. This situation results in blurring what is required for the representation and manipulation of effect collections in a safe effect system.

In this work, we present a language $\lambda_{\mathrm{EA}}$ equipped with an effect system that abstracts the existing effect systems for algebraic effect handlers. The effect system of $\lambda_{\mathrm{EA}}$ is parameterized over \emph{effect algebras}, which abstract the representation and manipulation of effect collections in safe effect systems. We prove the type-and-effect safety of $\lambda_{\mathrm{EA}}$ by assuming that a given effect algebra meets certain properties called \emph{safety conditions}. As a result, we can obtain the safety properties of a concrete effect system by proving that an effect algebra corresponding to the concrete system meets the safety conditions. We also show that effect algebras meeting the safety conditions are expressive enough to accommodate some existing effect systems, each of which represents effect collections in a different style. Our framework can also differentiate the safety aspects of the effect collections of the existing effect systems. To this end, we extend $\lambda_{\mathrm{EA}}$ and the safety conditions to \emph{lift coercions} and \emph{type-erasure semantics}, propose other effect algebras including ones for which no effect system has been studied in the literature, and compare which effect algebra is safe and which is not for the extensions.

Tue 3 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00
Algebraic and Computational EffectsICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Patrick Bahr IT University of Copenhagen
10:30
18m
Talk
Abstracting Effect Systems for Algebraic Effect Handlers
ICFP Papers and Events
Takuma Yoshioka Kyoto University, Taro Sekiyama National Institute of Informatics; SOKENDAI, Atsushi Igarashi Kyoto University
DOI
10:48
18m
Talk
Parallel Algebraic Effect Handlers
ICFP Papers and Events
Ningning Xie University of Toronto; Google DeepMind, Daniel D. Johnson University of Toronto; Google DeepMind, Dougal Maclaurin Google DeepMind, Adam Paszke Google DeepMind
DOI
11:06
18m
Talk
Abstract Interpreters: A Monadic Approach to Modular Verification
ICFP Papers and Events
Sébastien Michelland Université Grenoble-Alpes - Grenoble INP - LCIS, Yannick Zakowski Inria, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS
DOI Pre-print
11:24
18m
Talk
Algebraic effects and handlers for arrowsJFP First Paper
JFP First Papers
Takahiro Sanada Fukui Prefectural University
11:42
18m
Talk
How to Bake a Quantum Π
ICFP Papers and Events
Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University
DOI