paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Effect handlers via generalised continuations

基于广义续延的效应处理器
JFP vol.302020匹配度 1/10 · 论文研究函数式语言中效应处理器的实现基础(CPS 变换与 CEK 抽象机),属于 PL 理论与编译方向;与用户关注的静态分析、LLM/Agent 程序分析、浮点程序分析及贝叶斯程序分析均无直接交集,仅在广义 PL 形式上存在非常宽泛的联系。引用 36 inbox
DANIEL HILLERSTRÖM, SAM LINDLEY, ROBERT ATKEY
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:为深度、浅层和参数化效应处理器提出基于广义续延的 CPS 变换与 CEK 抽象机实现。

Plotkin 与 Pretnar 的效应处理器为用户自定义效应提供了模块化编程抽象。本文关注已提出的三类处理器的实现基础:深度、浅层和参数化。深度处理器由计算树折叠定义,浅层处理器由计算树上的情况分派定义,参数化处理器则是带有状态值穿线的深度扩展。作者既直接给出扩展,也通过编码到深度处理器来定义它们,并说明直接实现可避免生成不必要闭包。核心方法是将续延概念推广为效应处理器栈,并给出两类基础实现:CPS 变换和 CEK 风格抽象机。CPS 变换经过一系列精化:从一阶、未类型 lambda 中管理续延与处理器栈,到去柯里化获得尾递归,再到更内涵化的续延表示以支持不同处理器,最后高阶化以在变换期收缩管理性 redex。抽象机复用相同的广义续延表示。两类实现及扩展已作为 Links Web 编程语言的后端实现。

问题
如何为文献中的深度、浅层与参数化三类效应处理器建立统一且高效的实现基础,并避免直接实现中不必要的闭包生成。
方法
将续延推广为效应处理器栈,形式化 CPS 变换与 CEK 风格抽象机;CPS 变换经一阶到高阶的精化,抽象机复用同一广义续延表示。
评估
将抽象机与 CPS 变换(含扩展)实现为 Links Web 编程语言的后端,并通过直接实现与深度处理器编码的对比说明直接实现可避免不必要闭包。
原文摘要(Abstract)

Abstract Plotkin and Pretnar’s effect handlers offer a versatile abstraction for modular programming with user-defined effects. This paper focuses on foundations for implementing effect handlers, for the three different kinds of effect handlers that have been proposed in the literature: deep, shallow, and parameterised. Traditional deep handlers are defined by folds over computation trees and are the original construct proposed by Plotkin and Pretnar. Shallow handlers are defined by case splits (rather than folds) over computation trees. Parameterised handlers are deep handlers extended with a state value that is threaded through the folds over computation trees. We formulate the extensions both directly and via encodings in terms of deep handlers and illustrate how the direct implementations avoid the generation of unnecessary closures. We give two distinct foundational implementations of all the kinds of handlers we consider: a continuation-passing style (CPS) transformation and a CEK-style abstract machine. In both cases, the key ingredient is a generalisation of the notion of continuation to accommodate stacks of effect handlers. We obtain our CPS translation through a series of refinements as follows. We begin with a first-order CPS translation into untyped lambda calculus which manages a stack of continuations and handlers as a curried sequence of arguments. We then refine the initial CPS translation by uncurrying it to yield a properly tail-recursive translation and then moving towards more and more intensional representations of continuations in order to support different kinds of effect handlers. Finally, we make the translation higher order in order to contract administrative redexes at translation time. Our abstract machine design then uses the same generalised continuation representation as the CPS translation. We have implemented both the abstract machine and the CPS transformation (plus extensions) as backends for the Links web programming language.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{HillerstromLA20,
  title = {Effect handlers via generalised continuations},
  author = {DANIEL HILLERSTRÖM and SAM LINDLEY and ROBERT ATKEY},
  journal = {Journal of Functional Programming},
  volume = {30},
  year = {2020},
  doi = {10.1017/s0956796820000040}
}