第 5 课：余效应：计算需要环境给什么

一句话版：效应管「程序对世界做了什么」，余效应管「世界要求程序依赖什么」——余效应回答的是「计算需要环境给什么」（要访问的资源、要具备的能力、要依赖的服务），它与效应方向相反、互为对偶。

1. 对偶开场：一个问「我改了什么」，一个问「我需要什么」

先做两个思想实验，都是你每天都在经历的事。

点外卖：这是「效应」。 你按下「下单」，世界真的变了——商家开始备餐、骑手接了单、你的钱包少了一笔钱、路上多了一个外卖箱。程序（这个下单动作）对世界造成了影响，而这种影响是从程序流向世界的。

打工拿工资：这是「余效应」。 你是刚入职的程序员，工位、电脑、网络、数据库权限、项目文档……没有一样是你自带的，全靠公司提供。没有这些，你一行代码都写不出来；工资更是明明白白的「世界给你什么」。在这里，是环境（公司）在给程序（你）提供东西，方向正好反过来。

把这两个例子翻译成论文里的话，就是这一课的题眼：

效应刻画程序对世界的影响，而余效应刻画世界对程序的约束。

• 点外卖 = 程序改变世界 → 效应
• 打工 = 世界向程序提供资源、能力与报酬 → 余效应

那「世界对程序的约束」具体长什么样？论文给出了一个清单：它描述计算对其环境的要求，例如：

在类型系统里，余效应长这样：普通判断是 Γ ⊢ t : T（在上下文 Γ 下，t 的类型是 T）；余效应系统把判断写成 Γcoeffect ⊢ t : T——上下文 Γ 本身被一个「余效应代数」的元素标注，这个标注就是「这段计算对环境的要求」。

对照上面的图，记住这个「对偶」就够了：效应是计算指向世界（我改了什么），余效应是世界指向计算（我需要什么）。一个丰富的是类型，另一个丰富的是上下文。

2. 余单子余效应：程序是「泡在环境里」的

上一课我们认识了单子——「把值装进盒子里」的设计模式。这一课的对偶叫余单子（comonad）：单子把副作用装进盒子，余单子则假设程序本来就泡在上下文（环境）里，每一步都可以从环境里「取」东西。

论文里最直觉的一个例子是环境余单子，写成：

D(X) = E × X

不用怕这个公式，它说的其实是：每一个计算 X，都随身携带一份环境 E 一起跑。就像你的手机 App 永远带着「当前时间」和「当前位置」这两个环境值，你在任何一步都能读到它们。

余单子有两个基本动作，直觉上就是：

• ε（取）：从上下文里抽出当前值——「从上下文中抽取当前值」。程序想读环境？伸手一掏就有。
• δ（复制）：把上下文复制一份，交给嵌套的内层计算——「复制上下文，以供嵌套访问」。内层函数想读环境？环境跟着它走。

论文还提到一个流余单子，写成 D(X) = ℕ → X：ℕ 是自然数（可以理解成时间点），给一个时刻就返回一个值。它刻画的是对时序数据的依赖——比如一个组件要跟着时钟走、跟着数据流走。

🐟 打个比方：单子里的程序像一个密封盒子，把世界关在外面；余单子里的程序像一条鱼，无时无刻不泡在水（环境）里，每一次呼吸（每一步计算）都要从水里获取氧气。鱼游到哪，水就跟到哪——这就是「上下文依赖计算」。

所以「余单子余效应」一句话版本就是：程序的结果取决于它所在的环境，而环境会主动把需要的东西交给它。

3. 分级余效应：给「需要多少」贴一张重量标签

光说「程序依赖环境」还不够——依赖多少也很重要。某个变量被用了 0 次还是 100 次，对资源消耗的差别是天壤之别。

分级余效应（graded coeffects）的做法，是给每个「需求」贴一张重量标签。论文里这套标签系统是一个半环，写成：

S = (S, ≤, +, ×, 0, 1)

先别被符号吓到——把它理解成「一套可以加减乘除的称重系统」就行。标签有四种含义，非常生活化：

两种运算则对应两种「组合方式」：

• ×（乘）：顺序组合——先做完 A 再做 B，重量相乘。比如「先读一次文件，再读一次文件」就是 1 × 1。
• +（加）：并行组合——A 和 B 同时进行，重量相加。

💡 打个比方：这就像给家里装了水电表。你声明「这段代码最多读 n 次这个文件」，系统就能在你运行之前检查有没有超量；两个任务同时开跑，系统就把它们的用量加起来算总账。

有了这套「称重系统」，论文说可以在一个统一的代数框架内做到几件以前做不到的事：

1. 精确的资源跟踪——这个变量到底被用了多少次，一查便知；
2. 敏感度分析——谁的输入会影响谁的输出、影响多大，一目了然；
3. 信息流控制——敏感数据能不能流到不安全的地方去，全程可查。

一句话：分级余效应 = 余效应 + 用量账本，把「需要什么」升级成「需要多少」。

4. 从静态到动态：与可组合性的关系

现在回到这篇论文真正关心的问题：动态可组合性（还记得吗？组件装上能拆下、拆下不留痕）。论文 2.3 节把效应和余效应分别对应到可组合性的两个维度：

• 时间可组合性 → 有状态效应。时间可组合性要求「组件对共享环境的修改，在组件卸载时可逆」。真正持久改变环境的是有状态效应（写文件、改数据库）；要让这种改变可逆，这个变换就必须存在逆变换（能撤销）。
• 空间可组合性 → 余效应。空间可组合性要求「声明组件之间的依赖，并以反应式方式管理」。这些依赖正是余效应所捕获的内容——管理依赖，就是根据环境实际提供的东西，把每个依赖逐一解析掉。

那么问题来了：经典的效应系统、余效应系统，能直接支撑动态组合吗？

论文的答案很直接：不能，因为它们是静态工具。

• 效应是在词法上固定的作用域里被跟踪、并由编译期处理器消去的；
• 余效应标注则是依据执行之前就已经确定的上下文来验证的。

这两条在「世界在编译时就定型了」的假设下成立，但动态组合的世界不是这样：

⚠️ 所以论文在这里转换了视角：不再靠增加更多标注来扩展静态类型系统，而是把效应与余效应的概念结构具体化，让运行时能够直接操作它们——从而在运行时动态地建立起这些系统在静态情况下提供的保证。

这就是从「编译期证明」到「运行时机制」的关键一跃。至于怎么具体化、怎么让运行时操作它们，就是论文第 3 节的内容了，下一课见。

关键点回顾

这一课信息不少，记住这五句话就够了：

1. 对偶：效应问「我改了什么」（程序对世界的影响），余效应问「我需要什么」（世界对程序的约束）；点外卖是效应，打工拿工资是余效应。
2. 余效应标注的是上下文：Γcoeffect ⊢ t : T 中，上下文被余效应代数元素标注，描述计算对环境的要求——要访问的资源、要具备的能力、要依赖的服务。
3. 余单子 = 泡在环境里的计算：环境余单子 D(X) = E × X 表示每个计算都带着环境跑；ε 从环境取当前值，δ 复制环境给嵌套计算。
4. 分级余效应 = 用量账本：半环 S = (S, ≤, +, ×, 0, 1) 的标签量化使用——0 未用、1 线性、n 有界、∞ 不受限；× 顺序组合、+ 并行组合，支撑资源跟踪、敏感度分析、信息流控制。
5. 从静态到动态：时间可组合性对应有状态效应（可逆修改），空间可组合性对应余效应（依赖）；静态系统圈不住运行时加载的插件，所以论文把效应/余效应提升为运行时可直接操作的机制。

🚀 下一课我们进入论文第 3 节的第一个主角：可回退效应——「装得上去，拆得下来」。效应怎么才能在运行时真正撤销？这正是时间可组合性的答案。