一句话：首次将用户定义代数效应处理器与可并行计算结合，给出 λp/Fp 形式化、类型安全证明及 Haskell 实现。
现有代数效应设计通常要求效应按顺序执行，难以支持可并行计算。本文研究并行代数效应处理器，形式化 λp 演算，建模效应处理器与受 Dex 启发的 for 表达式所表示的并行计算，并给出多个可表达示例。为以类型安全方式实现该设计，作者提出 Fp——在 λp 上增加轻量值依赖类型系统的高阶多态 λ 演算，证明 Fp 保持 λp 语义并满足语法类型可靠性。最后提供镜像 λp 与 Fp 的 Haskell 库实现，揭示其与 free applicative functor 的新联系，所有示例均可编码。作者认为这是首个结合用户定义效应处理器与并行计算的研究，为后续设计与实现奠定基础。
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 p that extends λ p with a lightweight value dependent type system, and prove that F p preserves the semantics of λ p and enjoys syntactic type soundness. Lastly, we provide an implementation of the language design as a Haskell library, which mirrors both λ p and F p 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Xie0MP24,
title = {Parallel Algebraic Effect Handlers},
author = {Ningning Xie and Daniel D. Johnson and Dougal Maclaurin and Adam Paszke},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674651}
}