Abstracting Effect Systems for Algebraic Effect Handlers
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Tue 3 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Algebraic and Computational EffectsICFP Papers and Events / JFP First Papers | ||
10:30 18mTalk | Abstracting Effect Systems for Algebraic Effect Handlers ICFP Papers and Events Takuma Yoshioka Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University | ||
10:48 18mTalk | Parallel Algebraic Effect Handlers ICFP Papers and Events Ningning Xie University of Toronto, Daniel D. Johnson Google Research, Dougal Maclaurin Google DeepMind, Adam Paszke Google Research | ||
11:06 18mTalk | 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 Univ. Grenoble Alpes, Grenoble INP, LCIS, Valence, France DOI Pre-print | ||
11:24 18mTalk | Algebraic effects and handlers for arrowsJFP First Paper JFP First Papers | ||
11:42 18mTalk | How to Bake a Quantum $\Pi$ ICFP Papers and Events Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University |