积木小镇的两个魔法
这是一节特别的课：我们要把一篇 88 页的论文 A Programming Paradigm for Spatiotemporal Composability（一种“时空可组合”的编程范式） 讲给一个 5 岁的小朋友听。不讲数学公式，先讲故事；故事听懂了，再一层一层往深处走。
一句话先懂：这篇论文发明了三个规矩——① 每做一件事，就记下“怎么把它恢复原样”；② 每个人大声说出“我需要什么”；③ 这两件事记在同一个本子上。有了这三条规矩，积木小镇就可以不停地搭了又拆、拆了又搭，而永远不用把整个小镇推倒重来。
论文档案
作者：Yifan Shi、Wei Zhang、Tianyi Cui（北京大学 / DeepSeek-AI）。论文还是 draft（标注日期 2026-08-13）， Tether 仓库把它固定在 上游提交 13f2858， 原文 PDF、来源哈希与许可证提醒归档在 references/cordis-paper。 本页是它的故事化讲解，不代替原文；最后一章会说明它和 Tether 的关系。
阅读地图：你要爬到第几层？
这节课改造成了一座六层的旋转滑梯，从地面一路滑到论文底部。你可以在任何一层停下来。
- 第 0–2 章（5 岁）：问题是什么，以及两个魔法各自长什么样。有可以亲手按的实验。
- 第 3–5 章（10 岁）：两个魔法住在同一个本子里；开店的三件套；最难的一步——礼貌地关门。
- 第 6–8 章（大人）：数学家到底证明了什么；论文怎样变成真实代码；它和 Tether 的关系。
第 0 章 · 问题：为什么拆一块积木这么难？（5 岁）
想象你用积木搭了一座大大的城堡，城堡上有一块会唱歌的音乐积木。 有一天你想把音乐积木拿走，换一块新的。可是妈妈说： “不行哦，要拿走它，只能把整座城堡推倒，重新搭一遍。”
你一定会说：“这太笨了！”——可是，今天绝大部分软件就是这样干活的。
论文里讲了一个真实的例子：很多人用的代码编辑器 VSCode，可以安装各种各样的“扩展”（就是积木）。 但你把任何一个带代码的扩展拿走时，它不能单独离开——整个“扩展宿主”必须重启， 所有扩展一起关掉再开一遍，正在做的事情全部丢掉。
大人的世界里，这个“推倒重来”是有名字的：电脑出了问题就重启进程，服务器出了问题就换一个容器。 论文 §1.2.3 把这叫做粗粒度的 workaround——能用，但代价很大：每次重启都丢掉进程里积累的一切， 为了不中断服务还得准备一堆替补机器。
大人注：论文到底要解决什么
软件越来越需要在运行时装上、卸下、更换部件（插件系统、会自我修改的 AI agent harness）， 但“动态组合”一直没有坚实的理论基础。论文把问题拆成两个互相垂直的维度： 时间可组合性（temporal：部件走后，它留下的痕迹要能完全收拾干净）和 空间可组合性（spatial：部件之间的依赖要能声明、能自动接上、能礼貌断开）。 接下来两章，一个魔法解决一个维度。
第 1 章 · 第一个魔法：撤销清单（5 岁，时间魔法）
现在，给小镇发第一个魔法：每放上一块积木，就在小本子上写一句“怎么把它拿下来”。
- 放上红积木 → 本子上写：“把红积木拿下来。”
- 放上蓝积木 → 本子上写：“把蓝积木拿下来。”
要拆的时候呢？从本子的最后一行往回念——最后放上去的，最先拿下来。 你一定知道为什么：压在下面的积木不能先抽，不然塔就倒啦。
亲手试试：先按彩色按钮放几块积木，看看右边的小本子记了什么；再按“开始拆卸”，睁大眼睛看拆卸的顺序。
积木塔
撤销清单（小本子）
先放几块积木，看看小本子上记了什么。
看到了吗？拆的顺序永远是放的反序。这个规矩有个大人名字，叫 LIFO（last in, first out，后进先出）。 小镇的居民从来不用自己写“拆卸说明书”——因为放的时候已经顺手记下了，拆卸是小本子自动合成的。
大人注：这就是 revertible effect（可撤销的副作用）
论文 §3.1 把“做一件事”形式化为：一个动作不仅改变世界（Γ → Γ），同时交出它的逆动作， 类型写作 Γ → Γ × (Γ → Γ)。运行时把一路收到的逆动作按顺序累加成一个“回收器”（accumulator）， 拆卸就是反序执行它们。论文的定理 7 证明：这样恢复一定回到出发状态； 定理 16 证明：按 LIFO 逐个撤销时，每个逆动作恰好面对它自己造成的那个状态。 插件作者不需要写卸载路径——这是 VSCode 做不到的“locality of concern”。
第 2 章 · 第二个魔法：需要清单（5 岁，空间魔法）
第一个魔法管“收拾得干净”，第二个魔法管“交朋友”。 小镇上要开一家蛋糕店。蛋糕店不能自己种小麦，于是它在门口挂了一块牌子： “我需要：面粉。”——这就是需要清单。
小镇的规矩是：
- 面粉店开张了 → 蛋糕店需要的东西齐了，自己就开张了，不用人催。
- 面粉店要关门 → 蛋糕店先打烊收拾，不报错、不崩溃、不哭。
- 又开了一家新面粉店 → 蛋糕店自己又回来开张。
亲手试试：点“面粉店要关门了”，一步一步看“礼貌关门”的四个步骤；再点“重新开张”，看蛋糕店怎么自己回来。
面粉店
提供者 provider
开张中蛋糕店
需要：面粉（inject）
开张中现在两家店都开着。点上面的按钮，看看“礼貌关门”的四步。
注意刚才关门时发生了什么奇怪的事：面粉店早就挂上“停止接待新顾客”的牌子了，却迟迟没有打包—— 它在等蛋糕店收拾完。蛋糕店收拾的时候，手里还拿着原来那袋面粉，因为它记得这袋面粉是跟谁买的。 这个“记得”在第 5 章会变成论文里最重要的一个设计。
大人注：这就是 reactive coeffect（响应式的环境依赖）
coeffect 是 effect 的对偶：effect 描述“我怎样改变世界”，coeffect 描述“世界要给我什么我才能干活”。 论文 §3.2 让组件把依赖声明成一份 specification（这里的“我需要面粉”）， 环境（一张 key → value 的服务表 Σ）每发生一次变化，就对照每份声明分类： activating（从不满足变成满足 → 激活）、deactivating（满足被打破 → 停用）、 或 neutral（无关）。组件永远不会去读一个不存在的东西——因为它只在满足时才活着。
第 3 章 · 两个魔法住在同一个本子里（10 岁）
现在轮到最妙的一步了。小镇不需要两个本子——撤销清单和开店登记表，都钉在同一块魔法布告栏上。 这块布告栏，论文叫它 Context（上下文），代号 Γ∞。它同时是三样东西：
为什么一定要住在一起？因为这样会出现一个免费的惊喜：
“面粉店在登记表上写下‘我来了’”——这本身就是一件事，所以它也自动记进了撤销清单！ 面粉店以后要走，登记表上那一行会被自动划掉，蛋糕店也就自动知道了。 第 1 章和第 2 章的两个魔法，原来是一枚硬币的两面。
大人注：一个编程范式
论文 §3.3 把这个统一体称为一种编程范式：函数式风格把状态传来传去，看得清但写着累； 命令式风格随手改，好用但没人知道谁改了什么。Context 范式取中间——像命令式一样顺手 （组件直接读写 ctx），像函数式一样可追溯（每次读写都归因到某个组件的 context）。 登记表上的 set 操作类型恰好是 𝔈*Σ，即它天然就是一个可撤销 effect，两个机制由此互相成就。
第 4 章 · 开店三件套与一家店的一生（10 岁）
要在小镇开店，每一家店都要带齐三样东西，写在门口让所有人看见：
三样东西交上去之后，这家店的“一生”就开始了。一家店不是简单地“开”或“关”， 它的一生有四个房间，按顺序走：
大人注：谁按的开关？
论文 §4.2 里，小镇的管理员（orchestrator）只会做两件礼貌的事：O-Insert（“请这家店存在”）和
O-Retire（“请这家店退休”）。管理员从不直接改店的状态——状态的全部迁移都由生命周期规则
自己驱动（L-Reload / L-Unload）。 fiber 每次激活时会记下这次实际绑定的是哪家 provider
（committed view），而“现在应该绑谁”是 target view；两者一比较，就知道该搭、该拆还是原地不动。
这正是 Tether 仓库里 IPlugin.Inject / ApplyAsync / PluginHandle 这套 API 背后的理论原型。
第 5 章 · 最难的一步：礼貌地关门（10 岁，全论文的心脏）
第 2 章的实验里你已经看过了：面粉店关门，不能“啪”地一下消失。 现在我们把这个过程画成一张真正的时刻表——这是整篇论文最值钱的一段，叫 withdrawal ordering（撤退顺序）。
如果顺序反过来会怎样？面粉店先把面粉收走了，蛋糕店做到一半的蛋糕就会“啪”地掉在地上—— 这就是别的插件系统里常见的崩溃。小镇的规矩是：顾客先走，店家后走，而且顾客走的时候手里还有面粉。
“走的时候手里还有面粉”靠的是一个很小的本子，每家店都有一本，叫 committed view（成交记录）：这次开张，我实际是跟哪家店买的面粉？ 它旁边还有另一本叫 target view（今日行情）：现在镇上应该跟谁买？ 两本一对照，店就知道自己该干什么。
大人注：Algorithm 5 的三行关键代码
论文 §5.1.3 把上面这个故事写成了算法：refresh 在收到退休/依赖失效时先把 fiber 标记为
UNLOADING——在任何逆动作被调度之前就先停止提供服务（L-Leave）；
unload 的第一件事是通知所有 dependents 并等它们全部 INACTIVE（drain）；
之后 fiber.dispose 才运行回收器。dependents 在整个 teardown 期间都从 committed view 读旧 binding
（Theorem 63 保证这口“旧面粉”始终可读）。另外两条反直觉但重要的推论：
同一 provider 原地覆盖自己的 binding 不会被任何人察觉，想传播替换必须先撤再装；
记 uid 而不是 value，是为了“同样的面粉、不同的店”也能被区分。
第 6 章 · 数学家到底保证了什么（大人）
故事讲到这里，小朋友的部分结束了。下面这层回答一个大人关心的问题： “永远不乱”是许愿，还是能证明的定理？论文的第 4 章把小镇写成了一整套演算 （calculus），并证明了五件事：
有两块基石值得单独点名：
- “互不打架”是可以判定的。论文 §3.1.3 说：如果两个组件的所有变换两两可交换， 那么拆卸顺序可以任意打乱（Corollary 21）。§3.3.2 接着给出免费午餐： 操作落在不同的 key 上天然互不干扰（Thm 40）；落在同一个 key 上时，只要这个 key 的接口 “可交换”（比如注册路由、注册事件监听——先注册谁结果都一样），独立性的条件就自动满足（Thm 42）。 路由器这类表是安全的，中间件链这种讲顺序的就要靠 LIFO 和依赖声明来排。
- “恢复原样”不是字面一样，是“看起来一样”。free 掉一块内存并不会把堆的布局变回 malloc 之前。 论文用 observational equivalence（观察者分不出区别就算相同）来读所有等号—— 这让定理在现实机器上真正成立。
边界提醒：这些定理都有前提（图底部那一行）。论文从不说“随便什么副作用都能无条件恢复”； Tether 仓库里的差距分析也反复强调：没有这些前提时，只能承诺“可靠的 scoped lifecycle”，不能声称完整的 whole-system recovery。 读论文时把所有“保证”都理解为“在这些结构条件下成立”，就不会被故事带偏。
第 7 章 · 从纸面到代码：Cordis、Loader 与 Koishi（大人）
论文第 5 章把模型落成了真实框架 Cordis（TypeScript）。 理论的每个符号在代码里都有一个对应的名字，下表是论文 Table 2 的“故事版”节选：
| 论文符号 | 运行时代码 | 小镇说法 |
|---|---|---|
| Γ∞（统一 context） | ctx | 唯一的魔法布告栏 |
| effectΓ（可撤销 effect） | ctx.effect(callback) | 做一件事，同时交出“怎么拆” |
| get(k) / set(k, v) | ctx.get(key) / ctx.set(key, value) | 看布告栏 / 贴布告栏（贴也算一件事，自动进清单） |
| isolate(k, r) | ctx.isolate(key, realm) | 同一个名字，在不同的院子里指不同的店（多租户、测试替身） |
| intercept(k, ν) | ctx.intercept(key, metadata) | 给“使用”附加规矩（比如只读权限），不改店主、不触发重开 |
| 组件 (d, p, e) | component.inject / provide / apply | 开店三件套 |
| fiber 的一生 | ctx.use(...) + fiber.state | 开店实例与它的四个房间 |
| target / committed view | fiber.target / fiber.committed | 今日行情 / 成交记录 |
| 回收器 / 惯性 | fiber.dispose / fiber.inertia | 撤销清单 / 过渡一旦开始就走完 |
| O-Insert / O-Retire | ctx.use 及其回调返回的逆 | “请存在” / “请退休”，卸载父店会级联到子店 |
核心库之上，论文 §5.2 又给了声明式 Loader：管理员只维护一份配置树
（每个 entry 描述一家店：id、url、isolate、intercept、config、disabled），
Loader 负责把“配置想要的样子”翻译成 fiber 操作。改 intercept 原地生效；
改 config 由组件自己决定怎么消化；改 url 才重建。
热重载（HMR）则以整组模块为事务：任一模块换新失败，整组恢复旧版本，绝不停在半新不旧的中间态。
能做增量 reconcile 的底气，正是第 6 章的 Confluence：终点只由最终配置决定，与中间步骤的顺序无关。
案例研究是 Koishi：一个建立在 Cordis 上的聊天机器人框架，生态里有 4000+ 个社区插件。在它的控制台里，禁用一个插件、保存一个文件触发热重载，都是日常操作—— 不需要重启，作者也从不用写卸载路径。（论文脚注特意注明：Koishi 目前跑在 Cordis v3 上， 论文呈现的是重做了 effect/coeffect 语义与 loader 的 v4，但核心的组合模型两版共享。）
故事的边界：泼出去的水
最后一个诚实的问题：真的什么都能撤销吗？不能。 你把信投进邮筒，就拿不回来了。论文 §6.1 给小镇画了一条边界：
论文最后讨论了这套范式对宿主语言的最低要求（§6.4）： 时间维度需要闭包（逆动作要能连状态一起打包带走）和运行时可装卸模块 （Node 的模块注册表、原生世界的 dlopen/dlclose、.NET 的可收集 AssemblyLoadContext）； 空间维度需要带类型的依赖声明和访问调停（Proxy、descriptor、宏）。 这正是 Tether 选择用 C# / .NET 重实现时对应得上的几块基石。
第 8 章 · 它和 Tether 有什么关系？
Tether 的 src/Cordis* 就是这套思想的 C# 重实现——更准确地说，Tether 的复刻目标是
deepseek-harness 里 vendored 的 Cordis 行为，而这篇论文是上游对 Cordis v4 的完整理论阐述。
读论文能回答“为什么 Cordis 长这样”，读 Tether 源码能看到“现在落地到哪一步”。
2026-08-24，仓库对同一固定版本论文做过一轮独立对照复核，结论是方向正确、地基扎实 （可等待的 scope cleanup、把子插件登记成父 effect、reactive 激活、publication 批提交、owner 权限、事务式 loader）， 但要成为论文意义上的完整 spatiotemporal composability runtime，还有四个结构性地基要补：
- 原子的 effect acquisition——“拿到资源”和“登记撤销”必须是同一个公开 primitive，不能分两步；
- activation 级的 committed view——第 5 章那本“成交记录”，当前实现还没有；
- 声明式的 provide 图——组件要静态说出“我提供什么”，装载前就能查重、查环；
- context 调停的访问——只能读自己声明过的 key，未声明访问立即失败。
完整分析（含实施顺序与验收测试建议）在 references/cordis-paper/IMPLEMENTATION-GAP-ANALYSIS.md； 想动手读代码，可以从 Cordis 入门、 Cordis API · Fiber 和 运行时不变式 三页继续。
结课：把两个魔法装进口袋
带走三句话：
- 每做一件事，顺手记下“怎么恢复原样”——拆的时候反着来。（时间魔法 · revertible effects）
- 大声说出“我需要什么、我提供什么”——需要没了就先礼貌打烊，需要回来了就自己开张。（空间魔法 · reactive coeffects）
- 两本账记在同一块布告栏上——于是整个小镇可以不停地搭了又拆，而永远不乱。（统一 context · 时空可组合）
下次有人问你“这篇论文讲了什么”，你可以拍拍胸脯说： “它教会电脑里的积木小镇，怎么一边营业一边装修。”