为 OCaml 添加效应系统

我将展示有关代数效应和 OCaml 效应系统的在研工作。我会先解释效应处理器，再演示一个在类型中追踪效应的原型，包括一种推理局部可变状态的方法。

副作用是计算除返回值以外可观察到的结果。代数效应提供了一种方法，将效应操作的描述与实现它的上下文分开。这只是对概念的直观解释，而不是完整的数学定义。

假设一个计算获取整数状态，将其加一，再写回。在 get 操作处，我们可以暂停计算，请周围的上下文提供结果，再用这个值恢复剩余部分。描述计算时无须决定 get 和 set 如何实现。

当我们需要语言本身不提供的操作时，这种方法就很有用。即便 OCaml 已经有状态、操作系统交互和异常，我们仍可能需要其他类型的效应。这里的动机例子是并发。

考虑一个递归函数：它执行 fork 启动并发工作，再执行 yield 让另一个计算运行。代码描述需要的操作；效应处理器赋予它们含义。一个小型调度器可以维护工作队列，决定接下来运行哪个续延。

当计算让出执行权时，处理器接收代表暂停后剩余计算的续延，将其放入队列，然后恢复另一个任务。当计算执行 fork 时，调度器将当前续延入队，并在处理器下运行新函数。运行这个例子会得到交错的输出。

执行并处理效应的结构与异常相似。从运行时行为上直观理解，代数效应就像可以恢复的异常。普通异常展示了不可恢复的情况：搜索函数找不到元素时可以抛出 Not_found。

处理器可以将 Not_found 转成 None，将成功的值转成 Some。OCaml 的 match-with-exception 形式比范围较宽的 try 块更精确地限定所处理的计算：match 所检查的表达式之外抛出的无关异常不会被意外捕获。

生成器是另一个例子。一个偶数生成器反复增加计数器，每遇到偶数就执行 Return 效应。我们无须在语言中增加专门的生成器功能，而是可以描述操作并为它编写处理器。

一个统计前 N 个结果之和的处理器，会把每个返回值加到累加器中、增加计数，然后恢复续延，直到收集到足够多的值。如果生成器正常终止，处理器可以返回累计总和。对于无限偶数生成器，不会走到正常返回分支。

我们也可以实现简单的状态效应。阶乘计算请求 get 和 set 操作；处理器把它转换成接收初始状态的函数，并在剩余计算中传递更新后的状态。这类似于状态 monad 的标准构造方式。

在运行时，进入处理器会创建一个堆上分配、可动态调整大小的新栈。执行效应时，这个栈被包装为续延，控制返回前一个栈上的处理器。继续执行时，捕获的栈会恢复，计算从暂停处接着运行。

这里有一个问题：计算可能在没有相应处理器的上下文中执行效应。未处理的 Not_found 异常是熟悉的例子；生成器的 Return 操作未被处理时，失败的根本原因相同。我们希望在运行程序之前发现这种不匹配。

Monad 是在类型中表示效应的一种方法。异常式结果会在搜索函数和结果的类型中明确显示可能出现 Not_found，而不是让异常保持隐含。这有助于避免遗漏处理。

但 monadic 代码可能需要为纯函数和有效应的函数分别提供高阶操作，比如 map 和 monadic map。组合多个效应可能需要 transformer 或新的组合 monad。中间数据结构和闭包也可能给编译器优化和内联带来更大压力。

效应系统提供了另一种方法：给每个表达式同时赋予值类型和效应描述，并在函数类型中包含效应。执行 get 的函数可以在类型中说明，周围上下文需要提供合适的 get 处理器。

效应描述可以理解为安全运行函数所需的处理器。不同标签的操作可以在描述中调整顺序；相同标签的重复操作则可能有重要的顺序要求。支持更多效应的上下文可以安全运行需要较少效应的函数。

对于一个在空列表上抛出 Empty 的 head 函数，原型会在函数类型中显示 Empty。没有合适处理器的调用会遭到拒绝。同样，生成器的类型也会记录 Return，而不是误导性地看起来像普通的 unit 到 unit 函数。

高阶函数需要效应变量。如果传给列表 map 的函数执行了某种效应，调用 map 也会执行该效应。效应变量记录了这一关系，无须为每种可能的效应单独编写一个 map。

大多数高阶函数会以规则的方式传递参数函数的效应。原型用简写的箭头语法表示常见的效应变量，保持类型简洁。Map 在效应上是多态的：它既可以处理纯函数，也可以传播非纯函数的效应。

为了测试更大的例子，我改造了伦敦一位同事编写的并发库。原始库用 fiber 类型表示并发计算，并使用 return 和 bind。它的接口包括 fork、future、wait、yield 和 run。

在基于效应的接口中，fork 接收一个执行异步效应的普通函数并返回 future；wait 和 yield 也记录 async 效应。Run 接收带有该效应的计算并提供处理器，得到不再带该效应的函数。类型让处理器的作用变得可见。

原型将异步操作组合在一个抽象的 async 效应后面。公开每个操作可以让计算扩展到其他调度器；隐藏细节则让库有自由修改实现。我在这里选择抽象，因为操作很多，设计也仍在变化。

一个小例子反复打印两个字符串，在它们之间让出执行权，派生另一个计算并等待其 future。效应版本去掉了显式的 bind 和 return 调用，因此代码可以采用直接风格。运行后仍会产生预期的交错输出。

这种设计也能自然地配合高阶函数。我可以在列表上用 map 调用 fork，再用普通列表函数遍历并等待这些 future。效应变量传播异步操作，不需要单独的 monadic 列表 API。

另一个例子搜索值为 future 的关联列表，只在需要时等待。它既可以执行异步操作，也可以抛出受追踪的 Not_found 效应。两种效应都出现在类型中；这个例子无须定义特殊的 fiber 与错误组合 monad。

受追踪的 throw 与可恢复的 perform 不同：它不能恢复，因此不需要以相同方式携带续延。这个区别也让实现有机会采用更快的异常处理路径。

目前为止，类型系统追踪的是代数效应。我还想追踪 OCaml 已有的效应，比如可变状态和 I/O，以区分纯函数与非纯函数。纯函数的行为受到约束，通常更容易推理。

设想用 new、get 和 set 效应代替引用的分配、读取和写入。处理器可以维护一个从引用到值的存储，分配位置、读取并更新它们。只要引用属于正确的存储，阶乘例子就可以在这个处理器下运行。

这样的实现会比直接访问内存慢得多。重点并不是替换 OCaml 高效的运行时实现：我们可以在推理时把内置操作看作由外围处理器实现，同时保留快速实现。

文件 I/O 也适用同样的想法。从概念上讲，运行时处理打开和读取文件等操作。在这个原型中，我把内置操作归为一个 io 效应，而不是在普通类型中分别暴露每个操作。

向后兼容很重要。现有的 OCaml 函数箭头继续允许内置效应，而新的双头箭头表示没有这些效应的函数。结合效应变量的简写，少量箭头形式就能描述标准库，无须重写所有现有类型。

原型采用类似 Haskell 的纯度概念：纯函数可以不终止或抛出普通异常，但捕获异常是有效应的。我建议用受追踪的 throw 处理可恢复错误，用普通 raise 表示程序已经出错的异常情况。

为了测试可用性，我改造了较早版本的 OCaml 标准库：约 101 个文件、22,000 行，其中修改了约 4,000 行。大约一半改动是我希望添加的标注；其余许多涉及 printf 的技术细节，更好的推断可以减少这部分工作。

这项工作还暴露了多态比较的问题：由于它们可能检查可变状态，必须视为可能有效应。用特定类型的比较替换它们，可以让隐藏的行为变得明显。最终的列表签名展示了纯函数，并在适当情况下传播传入函数的效应。

数组提供了对比例子：创建或更新可变存储会产生效应，初始化函数本身也可能有效应。一位听众关于箭头记法的问题揭示了一个细节：效应变量是否已经包含 I/O；简洁记法必须保留预期的组合方式。

还有一个难题。阶乘函数创建引用、在局部修改它并只返回结果，从外部观察是纯的，但简单的状态效应会将它标记为非纯。我们希望处理其局部状态，同时不让不同存储的引用混在一起。

提出的解决方案是给引用类型及其状态效应增加区域参数。区域标识引用所使用的程序部分。这类似 Rust 的生命周期追踪，不过讲者指出一个区别：逃逸的引用可能仍作为值存在，但其所需的效应无法执行。

普通引用类型可以用全局区域表示。新的 private 构造引入局部区域并处理其中的状态，让阶乘函数可以被标记为纯函数。试图使用来自区域外的引用会产生效应不匹配，而不是悄悄跨越存储边界。

同样的机制也可以用于可变记录字段，将访问与相关区域关联起来。这些功能仍处于原型阶段；区域及带区域标注的效应也启发了其他追踪局部性的方式。

例如，with-file 函数可以为文件指定区域，只允许在处理该区域的作用域内读写。回答听众问题时，我指出嵌套的文件区域可能被统一，因此系统保留了保证安全所需的局部性，但未必保留文件之间的所有区别。

另一个可能的扩展是分开状态读取和写入。不可变区域可以允许读取而不允许写入；冻结操作则可以先允许局部修改，再返回不可变值。这个例子使用高阶多态，日常使用可能过于繁重。

多处理器是另一个可能的方向：一个处理器可以并排运行两个计算，并同时响应两者的效应。例如，管道可以将一个计算的 send 与另一个计算的 receive 配对，同时规定任一侧提前结束时如何处理。

一位听众问，多处理器是否可以使用不同的类型表示来避免子类型，例如使用 sigma 类型。我解释说，当前方法主要使用多态，并保留了很强的推断能力；如果没有充分理由，我不愿牺牲 OCaml 的类型推断优势。这个具体提议值得在演讲后展开更长的讨论。