代数效应与处理器

形式陈述 ​

代数效应先声明操作签名 $\mathsf{op}:A\to B$：操作接收 $A$ 型参数，恢复后向调用点提供 $B$ 型结果。计算以 perform op(v) 触发操作，处理器写成

$$\mathsf{handle}e\mathsf{with}\{\begin{array}{l}\mathsf{return}x\mapsto e_r;\\ \mathsf{op}(x,k)\mapsto e_{op}\end{array}.$$

若被处理计算返回 $D$、处理器整体返回 $C$，则 return clause 在 $x:D$ 下产生 $C$，operation clause 在 $x:A$、$k:B\to C$ 下产生 $C$。这是一种声明式类型边界；带效应标注公理库效应系统Effect system · Type-and-effect system在结果类型之外静态近似表达式可能执行的读写、异常、输入输出或控制效应的类型系统。的系统还可从处理后效应行中移除 op。具体检查算法负责核对所有操作分支、结果类型和效应行，却不定义运行时恢复行为。

令 $E$ 是从操作点延伸到当前处理器、且中间不跨过另一个匹配处理器的求值上下文。一个 deep handler 的核心转移公理库操作语义Operational semantics用执行判断、转移规则或抽象机定义程序如何运行。为

$$\begin{array}{rl}\mathsf{handle}v\mathsf{with}H& ⟶e_r[v/x],\\ \mathsf{handle}E[\mathsf{perform}\mathsf{op}(v)]\mathsf{with}H& ⟶e_{op}[v/x,(\lambda y.\mathsf{handle}E[y]\mathsf{with}H)/k].\end{array}$$

因此 $k$ 是从操作点到该 handler 的受限恢复点公理库续延Continuation表示计算余下部分、接收当前结果并产生最终结果的对象。，不是整个无界程序续延。上式在恢复时重新安装 $H$；shallow handler 则采用不同规则。$k$ 能否调用零次、一次或多次也取决于 one-shot/multi-shot 语义及资源类型，不能默认任意复制。

若当前 handler 没有匹配 op 的 clause，该操作必须连同从原操作点到当前边界的恢复上下文继续向外传播，由更外层 handler 处理。传播规则不能丢掉这段上下文；若操作最终到达顶层仍无人处理，语义应把它列为显式的未处理操作结果或运行错误，而不是让配置无规则可走。

“代数”来自操作及其方程生成自由模型、handler 作为保持这些操作结构的解释或 fold 的观点。它要求先说清操作方程；受限控制、作用域操作和资源生命周期未必都由同一简单代数覆盖。

直觉 ​

perform 不决定操作最终怎么实现，它只是向最近处理器发出一项请求。处理器既看到请求参数，也拿到“如果给请求一个结果，原计算将如何继续”的恢复点。于是同一程序中的操作可以被解释成真实 I/O、纯模拟、收集日志或测试桩，而调用点不必硬编码策略。

return clause 处理没有再触发操作、正常走到终点的计算。若只写 operation clauses，普通返回值就没有进入处理器结果的路径；这也是 handler 不能简化成异常 catch 的原因。

例子与边界 ​

异常是最简单的非恢复例子：raise:E→0 的处理分支忽略 $k$，直接产生替代结果，对应异常语义公理库异常语义Exception semantics把正常返回与异常传播作为不同控制结果描述的语义。丢弃当前普通续延。非确定选择 choose:1→Bool 的处理器可分别以 true、false 调用 $k$，再合并两条结果；这需要 multi-shot 恢复或安全复制被捕获的上下文。

状态操作 get:1→S、put:S→1 可由 handler 显式携带当前状态：get 把状态交给 $k$，put 以新状态继续。这个例子展示把效应重新解释为纯状态传递，但全局状态、动态作用域资源或带析构保证的操作可能需要额外方程、scoped effects 或线性恢复，不能由一句“所有效应都代数化”概括。

若 multi-shot handler 重放含文件句柄、锁或外部 I/O 的续延，效果可能重复，资源也可能被非法复用。one-shot 限制、子结构类型或运行时复制检查是不同解决路线；处理器语法本身不自动保证安全。

推论与应用 ​

代数效应与处理器可统一表达异常、非确定性、生成器、状态解释和可测试的服务接口。编译实现可把 handler 翻译成受限 CPS；正确性要求源 perform/handle 转移由目标续延调用模拟，并保持正常返回、未处理操作与恢复次数等观察。

类型安全通常陈述为保持与进展：良类型转移保持结果类型；若程序没有未处理效应，则闭合良类型计算要么返回值、要么继续运行。若语言允许操作冒出最外层，“未处理操作”应作为显式结果，而不是误判为语义卡住。

参考资料

• Gordon D. Plotkin and Matija Pretnar, “Handlers of Algebraic Effects,” ESOP, 2009。
• Gordon D. Plotkin and John Power, “Algebraic Operations and Generic Effects,” Applied Categorical Structures 11, 2003。
• Andrej Bauer and Matija Pretnar, “Programming with Algebraic Effects and Handlers,” Journal of Logical and Algebraic Methods in Programming 84(1), 2015。