第 3 课：贡献回顾与类型判断 Γ ⊢ t : T
一句话版：这篇论文的目标，是让「组件在运行时动态装上、又能干净地卸下」这件事变得可推理、可验证。本课先看论文的全局地图——四大贡献分别撑起哪两块可组合性；再补两小块地基：类型判断
Γ ⊢ t : T到底在说什么，以及效应标注T^effect为什么能让我们「不看实现就知道副作用」。
1. 论文的四大贡献：先看全局地图
论文 1.3 节一口气给出了四大贡献。它们不只是「四个成果」，更是后续每一课的目录：
| 贡献 | 论文章节 | 核心机制（一句话） | 打比方 | 支撑哪种可组合性 |
|---|---|---|---|---|
| 1. 可回退效应 | 3.1 | 每个「修改环境」的操作都配一个显式逆操作，带跟踪与恢复 | 全程录像，随时倒带 | 时间可组合性 |
| 2. 反应式余效应 | 3.2 | 组件用依赖集声明自己需要什么，环境一变就自动通知：激活、停用或中性 | 插座自动通电、断电 | 空间可组合性 |
| 3. 组件生命周期 + 统一上下文类型 | 3.3 / 3.4 | 把「装上→运行→卸下」整个过程操作化，并把效应上下文与余效应上下文合并成一种类型 | 给插件上户口，登记从生到死 | 把两个维度统一成编程范式 |
| 4. Cordis 实现 + Koishi 案例 | 4 | 一个时空可组合性元框架落地：效应跟踪、余效应解析、声明式组件加载器；Koishi 生态超过 4000 个生产插件验证 | 从图纸到量产，还上了流水线 | 证明整套理论可行 |
拆开来看，四大贡献是一条链：
先解决「装上能拆下」（贡献 1，时间维度）→ 再解决「站得稳」（贡献 2，空间维度）→ 把两者装进一个统一模型（贡献 3，编程范式）→ 写成真实框架并用生态验证（贡献 4，落地）。
🎁 打比方：一个插件就像插进主机的「U 盘」——贡献 1 管「拔掉之后系统完好如初」，贡献 2 管「插上之后自动找到它要的驱动」，贡献 3 管「U 盘的整个使用周期都被规范管理」，贡献 4 就是「真造出了一台支持热插拔的电脑」。
💡 后续课程会逐一展开：第 6 课讲可回退效应、第 8 课讲反应式余效应、第 9 课讲生命周期、第 10 课讲统一上下文类型、第 11 至 12 课讲 Cordis 核心库与 Koishi 案例。本课先把这张地图钉在墙上。
2. 类型判断 Γ ⊢ t : T 是什么？
论文第 2 章一开头就说：假定读者熟悉基本类型论与范畴论。先别慌——本课只需要一个概念：类型判断（typing judgment）。它一点都不玄，就是你天天在 TypeScript 里经历的事情，只不过换成了数学记号的写法。（至于范畴论，第 4 课讲单子时会用最朴素的方式带出来。）
在简单类型 lambda 演算（STLC）里，有一个长得像数学公式的记号：
Γ ⊢ t : T
念出来就是一句话：「在类型环境 Γ 之下，项 t 具有类型 T。」 逐符号拆开：
| 符号 | 念法 | 含义 | 用 TypeScript 打比方 |
|---|---|---|---|
| Γ | 伽马（Gamma） | 上下文 / 类型环境：一张「变量名 → 类型」的表 | 当前作用域里编译器记下的那些声明（比如 const x: number = 5 那一行） |
| t | 项（term） | 正在被检查的一段代码 / 表达式 | 函数体里的某个表达式 |
| T | 类型（type） | 项的类型 | number、string 这样的类型 |
| ⊢ | 断定（turnstile） | 把左边和右边连起来的判断关系 | 编译器「拍板」那一下：确认 x + 1 是 number |
把它和 TypeScript 对照，你就完全懂了：
const x: number = 5;
const y = x + 1; // 编译器：x 是 number，x + 1 也是 number
编译器在检查第二行时，心里揣着一张小表「x : number」——这张表就是 Γ；它正在检查的表达式 x + 1 就是 t；它得出的结论「类型是 number」就是 T。所谓类型判断，就是「查表 + 验证 + 下结论」这一整套动作的正式写法。
⚠️ 注意 Γ 的念法：它是大写的希腊字母「伽马」，不是英文字母 G。论文里它永远表示「当前这个作用域里都知道些什么」。
3. 效应标注 T^effect：让类型记住「副作用」
普通类型判断 Γ ⊢ t : T 只回答一个问题：t 返回什么。但真实程序里，一个函数除了返回结果，还会碰外面的世界——读文件、写数据库、改全局变量、发网络请求。这些就是副作用。
效应系统（effect system）对类型做了细化：在类型上面加一个效应标注，得到：
Γ ⊢ t : T^effect
多出来的那个 effect，回答第二个问题：t 除了返回一个 T，还会产生哪些副作用。它不是随手写的标签，而是「效应代数」里的一个元素——效应可以合并、可以比较，像一个能取并集的集合。经典例子：
Maybe效应：可能失败（部分性）State效应：可变状态IO效应：与外部世界交互（读文件、网络）
💡 论文里交代了这段历史：效应标注的思路源于 Lucassen 和 Gifford；单子建模来自 Moggi，由 Wadler 在 Haskell 中推广；代数效应来自 Plotkin 和 Power。本课只需要记住一件事：效应标注 = 类型层面的「副作用说明书」。
为什么这能支持「组合式推理」？
组合式推理（compositional reasoning）是这段话里最值钱的两个词。它的意思是：判断一个组合表达式的属性，只需要看每个组成部分的属性，不需要看它们的实现。
举个具体例子。假设有两个函数：
// f：读文件（带 IO 效应）
// g：纯函数，只做算术（无副作用）
// 那么 f(g(x)) 是什么效应？——IO。
// 不需要读 f 和 g 的源码，只看标注就能断定。
推理过程就一句话：外层 f 带 IO，内层 g 是纯的，副作用不会凭空消失，所以整个 f(g(x)) 一定有 IO。
为什么这么重要？ 因为真实代码库动辄几十万行。如果没有效应标注，你想知道一个函数有没有偷偷改全局变量，只能把它的实现从头读到尾——还得连带读它调用的所有函数。有了标注，副作用和类型一样可以「局部检查」：每个函数自带说明书，组合的时候把说明书拼起来就行。
🎁 打比方：普通类型像「外卖单上的菜名」（你点了什么），效应标注像「过敏原清单」（这道菜里有什么你不能吃的）。组合一桌菜时，你只要把每道配菜的过敏原清单拼起来，就知道整桌能不能吃——不需要进后厨看做法。
4. 把效应、余效应对上两个维度
论文 1.3 节最开头的一句话，是整篇的钥匙：
动态可组合性的两个维度，分别涉及计算如何修改环境，以及计算如何依赖环境。
- 效应 = 回答「计算修改了环境什么」（我改了什么）
- 余效应（coeffect） = 回答「计算需要环境提供什么」（我需要什么）
两个方向恰好相反，下面这张图把它们画在一起：
效应问「我改了什么」（对世界的影响）；余效应问「我需要什么」（世界对我的约束）
传统上，效应和余效应都只能在词法上固定的作用域里做编译时静态分析——也就是说，编译器翻开代码就能看到全部，因为一切在写代码时就已经确定了。但 Cordis 的场景是组件在运行时动态加入、退出：谁也不知道运行时还会装进来什么。所以论文把两者各升一级：
| 维度 | 问的问题 | 传统工具 | 论文的升级 | 打比方 |
|---|---|---|---|---|
| 时间 | 计算如何修改环境 | 效应（编译时静态分析） | 可回退效应：每个修改配显式逆操作，运行时能真正撤销 | 录像可倒带，卸插件不留痕 |
| 空间 | 计算如何依赖环境 | 余效应（编译时静态分析） | 反应式余效应：依赖集 + 满足性通知，自动激活、停用或中性 | 插座有电就工作、断电就待机 |
到这里，四大贡献和两个维度就闭环了：
- 贡献 1（可回退效应） → 时间可组合性：组件一生都在「改环境」，改完要能还原。
- 贡献 2（反应式余效应） → 空间可组合性：组件站在依赖图里，依赖齐不齐要能感知。
- 贡献 3（生命周期 + 统一上下文类型） → 把这两个维度揉进同一个编程模型。
- 贡献 4（Cordis + Koishi） → 证明这套东西真的能跑。
5. 关键点回顾
这一课的内容浓缩成五句话：
- 四大贡献是一条链：可回退效应→时间可组合性；反应式余效应→空间可组合性；生命周期 + 统一上下文类型→编程范式；Cordis + Koishi→落地验证。
Γ ⊢ t : T= 「在类型环境 Γ 下，项 t 具有类型 T」。Γ 就是「变量名 → 类型」的作用域表，和 TypeScript 编译器心里那张表是一回事。- 效应标注
T^effect让类型从「只记返回值」升级为「还记副作用」。 - 效应标注的价值是组合式推理：知道 f 带 IO、g 是纯的，就能断定
f(g(x))带 IO——不用读实现。 - 两个维度两个方向：效应 = 修改环境 = 时间；余效应 = 依赖环境 = 空间。Cordis 把它们从「编译时静态分析」升级成「运行时动态机制」。
🚀 下一课我们讲单子——还记得本节提到的 IO、State、Maybe 吗？它们都是单子的实例。效应标注是「类型层的声明」，单子则是「运行时层的盒子」，两者是同一件事的两张面孔。
自测题 · 贡献与类型判断
完成作答后点击「提交答案」，可以查看对错与解析。