Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

线性效应

(Linear Effects)

普通代数效应（algebraic effects）的灵活性来源于：一个操作（operation）的 resume 续延可以被调用零次、一次或多次——这赋予了异常处理（零次）、非确定性搜索（多次）、生成器（一次）等丰富语义。但这种灵活性是有代价的：编译器通常必须为效应操作捕获续延（continuation），并通过单子化翻译（monadic translation）将其表示为首类值，以便运行时能灵活地控制续延的调用次数。

线性效应是一类受到严格控制流线性（control-flow linearity）约束的效应——它要求其所有操作的 resume 必须恰好被调用一次，且位于处理子句的尾部（tail-resumptive），同时这些操作自身也只能使用线性效应。这种约束让编译器可以完全免除单子化翻译，使得“仅使用线性效应的代码“在运行时更紧凑、更高效。

控制流线性：四种分类

微软研究院的技术报告《Qualified Effect Types》形式化了控制流线性的概念。一个函数（或表达式）的控制流线性属性可分为四类 ：

分类英文返回次数典型代表
线性linear恰好一次普通纯函数、尾恢复操作
中止性abortive永不返回abort、exit、无限循环
仿射性affine至多一次可能抛异常的函数
自由性wild可能零次或多次非确定性选择、回溯搜索

Koka 的核心洞察是 ：在 Koka 这类基于代数效应的语言中，改变控制流的唯一途径就是通过效应操作。因此，如果一个函数只使用被线性处理器处理的效应操作，那么这个函数本身就是控制流线性的（恰好返回一次）。

基于此，Koka 允许在效应声明中标注其控制流线性属性 ：

effect abort exn    { throw(e: exception): a }   // 中止性
effect linear out   { println(x: string): () }   // 线性
effect wild amb     { flip(): bool }             // 自由性

整个效应行（effect row）的线性属性定义为其各组成效应线性属性的 join（上确界）。

线性效应的定义与约束

当用户说“线性效应“时，指的是满足以下三条约束的效应 ：

  1. 操作是尾恢复的（tail-resumptive）：处理子句中 resume 的调用必须出现在尾部位置——即 resume(...) 是子句返回前的最后一个动作。这保证了 resume 在编译后可以展开为一个简单的跳转/循环回边，而非需要捕获续延。

  2. resume 恰好调用一次：处理子句必须且只能调用 resume 一次。这排除了：

    • 零次调用（如异常处理 throw → abortive）
    • 多次调用（如非确定性 flip → wild）

  3. 操作只能使用线性效应：该效应的操作本体（以及其处理子句）自身只能引用其他线性效应，从而形成封闭的“线性效应世界“。

这三条约束共同保证了：任何只使用线性效应的表达式，在运行时的控制流是线性的（恰好返回一次） 。

为什么能免除单子化翻译

普通效应操作的 resume 续延是**多射（multi-shot）**的——它可能被调用零次或多次。为了让程序能灵活控制调用次数，编译器必须：

  • 将续延捕获为堆分配的首类值（continuation object）
  • 通过证据传递（evidence passing） 或类似的机制，在调用栈中传递效应操作的字典
  • 在处理子句中通过 resume(...) 显式调用续延

这就是所谓的“单子化翻译“——效应的存在迫使编译器把代码重写成带有续延传递的风格，带来：

  • 堆分配开销：续延对象需要分配内存
  • 间接调用开销：resume 是通过函数指针/字典调用的
  • 代码膨胀：需要生成续延的封装与传递逻辑

而线性效应的 resume 恰好被调用一次且位于尾部——这让编译器可以做一个关键优化：尾恢复处理子句（tail-resumptive handler）可以直接编译为简单的循环，无需堆分配、无需捕获续延、无需协程机制 。

技术报告《Qualified Effect Types》证明 ：如果表达式的类型声明它只使用线性效应，那么运行时的控制流确实是线性的。这一类型系统保证与效应处理器的结合，让我们可以在局部推理程序——确保外部资源的使用约束得到满足，同时完全免除单子化翻译的开销。

示例：线性效应 vs 普通效应

普通效应（需要续延捕获）

// 普通 state 效应——ctl 表示 control 效应，续延是多射的
effect state
  ctl get(): int
  ctl put(n: int): ()

// 标准 state 处理器——resume 被调用恰好一次，但不在尾部
// 因为 resume 的结果还要参与后续计算（如 resume(s)(s)）
fun state(action: () -> <state|e> a): e (a, int)
  var s := 0
  with handler
    return(x) -> (x, s)
    ctl get() -> resume(s)           // resume 的结果被使用
    ctl put(n) -> { s := n; resume(()) }
  action()

这里 ctl get() 的 resume(s) 虽然被调用一次，但 resume 的结果 resume(s) 还要被应用 (s)——resume 不在尾部位置。编译器必须捕获续延。

线性效应（尾恢复，免除单子化）

// 线性 out 效应——操作是尾恢复的
effect linear out
  println(x: string): ()

// 线性处理器——resume 恰好调用一次且在尾部
fun capture-output(action: () -> <out|e> a): e (a, list<string>)
  var lines := []
  with handler
    return(x) -> (x, lines.reverse)
    println(msg) -> {              // 尾恢复子句
      lines := Cons(msg, lines)
      resume(())                    // resume 在尾部，恰好调用一次
    }
  action()

println 的处理子句中 resume(()) 是最后一个动作——尾恢复。编译器可以将其编译为一个简单的循环：每次 println 操作被“执行“时，实际上就是循环的一次迭代，无需堆分配续延。

多次 resume 的对比

// 非确定性选择——wild 效应，resume 被调用两次
effect amb
  flip(): bool

fun collect-all(action: () -> <amb|e> a): e list<a>
  with handler
    return(x) -> [x]
    flip() ->
      val false-branch = resume(False)
      val true-branch = resume(True)   // resume 被调用两次 → wild
      false-branch ++ true-branch
  action()

flip() 的处理子句调用 resume 两次——这是 wild 效应，必须捕获续延（实际上需要捕获两份续延，或用其他机制实现回溯）。这与线性效应的“恰好一次、尾部“形成鲜明对比。

性能收益

对于仅使用线性效应的程序，Koka 编译器可以：

  1. 消除续延堆分配：因为 resume 尾恢复且调用一次，编译器可以将其编译为直接的跳转/循环回边，无需在堆上分配续延对象 。

  2. 消除证据传递开销：普通效应需要通过证据传递（evidence passing）在调用栈中传递操作字典 ；线性效应因为控制流是线性的，可以通过更直接的代码生成来避免这部分开销。

  3. 生成紧凑代码：尾恢复处理子句编译后等价于一个简单的 while 循环或尾递归——与手写命令式代码效率相当 。

技术报告中的实证 ：对于迭代、可选（optional）、状态（state）、读取器（reader）等常见模式——这些都可以表达为线性效应——其运行时开销与直接命令式实现相比，没有任何额外代价。

线性效应的类型级保证

Koka 的类型系统通过 qualified types 框架 传播控制流线性约束。当你写一个函数：

fun process(items: list<int>): <out|e> int
  match items
    Cons(x, xs) -> { println(x.show); process(xs) }
    Nil -> 0

类型 <out|e> 中的 out 是一个 linear 效应。编译器由此推断：process 的控制流是线性的（恰好返回一次），且它只使用线性效应。这一保证让：

  • 局部推理成为可能：你可以确保外部资源的使用约束得到满足，而无需理解完整的程序
  • 优化是安全的：编译器可以放心地免除单子化翻译，因为类型系统已经静态保证了控制流线性

限制与注意事项

线性效应虽然高效，但也有其限制：

⚠️ 操作必须是尾恢复的：如果你写的线性效应处理子句中 resume 不在尾部（如 resume(x) + 1），编译器要么报错，要么退回到普通效应翻译。Koka issue #72 记录了这样一个案例：effect fun() { resume(f()) } 是尾恢复的，而 fun() { f() } 经效应行展开后会包裹 .open 调用，导致尾恢复分析失效 ——这说明尾恢复分析对语法形式敏感。

⚠️ resume 恰好一次：线性效应禁止零次或多次 resume。如果需要异常语义（零次）或非确定性（多次），必须使用普通效应（abortive 或 wild）。

⚠️ 闭世界假设：线性效应构成封闭的“线性世界“——其操作只能使用其他线性效应。如果需要与 wild/abortive 效应交互，需要通过效应行的 join 操作，此时整体线性属性退化为较弱的分类（affine 或 wild）。

与其他语言的对比

线性效应的思想与以下概念相关但不同：

  • Haskell 的 LinearTypes 扩展：a %1 -> b 要求参数被使用恰好一次——这是值级别的线性，而 Koka 的线性效应是控制流级别的线性
  • Clean 的唯一性类型（uniqueness types）：保证引用被使用恰好一次，用于安全 in-place 更新
  • Rust 的所有权系统：通过所有权保证每个值有且仅有一个所有者

Koka 的线性效应独特之处在于：它将控制流线性编码进效应类型系统，与 Koka 既有的行多态效应类型（row-polymorphic effect types）无缝集成 。你无需显式标注 %1 或所有权修饰符——只需声明效应为 linear，编译器会自动跟踪并优化。

小结

线性效应是 Koka 类型系统的一项强大特性：

  • 语法层面：在 effect 声明中标注 linear 关键字，约束其操作为尾恢复且 resume 恰好一次
  • 语义层面：线性效应保证控制流线性（恰好返回一次），且操作只能使用其他线性效应
  • 编译层面：因为 resume 尾恢复且调用一次，编译器可以完全免除单子化翻译，将处理子句编译为简单的循环，无堆分配、无续延捕获、无协程机制
  • 性能层面：仅使用线性效应的代码，其运行时效率与手写命令式代码相当 ——迭代、状态、读取器等常见模式零开销
  • 安全层面：类型系统静态保证控制流线性，使局部推理成为可能，确保外部资源使用约束得到满足

线性效应体现了 Koka “类型级效应跟踪“与“零开销抽象“设计哲学的完美结合——你用 linear 关键字给编译器一个承诺，编译器回报你极致的运行时效率。

📌 译注：本章节核心概念对应——

  • linear effect：线性效应
  • tail-resumptive：尾恢复（指 resume 调用位于处理子句的尾部位置）
  • control-flow linearity：控制流线性
  • monadic translation：单子化翻译
  • exactly once resume：恰好一次恢复

参考微软研究院技术报告《Qualified Effect Types — Taming Control-Flow through Linear Effect Handlers》（MSR-TR-2023-42） ，该报告由 Jonathan Brachthäuser 实习期间在 Microsoft Research 完成，形式化了控制流线性的类型理论，并证明了“若表达式类型声明仅使用线性效应，则运行时控制流是线性的“这一核心定理 。

关键要点：线性效应通过约束操作“尾恢复且 resume 恰好一次“，让编译器能完全免除单子化翻译，将效应处理编译为高效的循环结构。这是 Koka 实现“零开销效应处理“的核心机制之一——与证据传递（evidence passing）技术 互补，共同保证了 Koka 效应系统在提供强大表达力的同时，不牺牲运行时性能。