Abstracting Effect Systems for Algebraic Effect Handlers
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 SepDisplayed 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 18mTalk | 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 18mTalk | 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 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 Université Grenoble-Alpes - Grenoble INP - LCIS DOI Pre-print | ||
11:24 18mTalk | Algebraic effects and handlers for arrowsJFP First Paper JFP First Papers Takahiro Sanada Fukui Prefectural University | ||
11:42 18mTalk | 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 |