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

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 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