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