Algebraic effect handlers support composable and structured control-flow abstraction. However, existing designs of algebraic effects often require effects to be executed sequentially. This paper studies parallel algebraic effect handlers. In particular, we formalize 𝜆p, a lambda calculus which models two key features, effect handlers and parallelizable computations, the latter of which takes the form of a for expression, inspired by the Dex programming language. We present various interesting examples expressible in our calculus. To show that our design can be implemented in a type-safe way, we present a higher-order polymorphic lambda calculus F𝑝 that extends 𝜆p with a lightweight value dependent type system, and prove that Fp preserves the semantics of 𝜆p, and prove its syntactic type soundness. Lastly, we provide an implementation of the language design as a Haskell library, which mirrors both 𝜆𝑝 and Fp and reveals new connections to free applicative functors. All examples presented can be encoded in the Haskell implementation. We believe this paper is the first to study the combination of user-defined effect handlers and parallel computations, and it is our hope that it provides a basis for future designs and implementations of parallel algebraic effect handlers.
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 |