第 6 课：可回退效应：装得上去，拆得下来

一句话版：可回退效应把「副作用」改造成「变换 + 逆变换」——每次修改环境都自动配好一把「逆钥匙」，装上时记进账本、拆下时按逆序自动还原；从此「卸载不留痕」不用手写清理代码，而是由结构本身保证。

第 1 步：回顾——时间可组合性要求「拆得下来」

上一课我们用「盒子（单子）」把副作用变得显式、可控。但显式只是第一步，这篇论文真正想要的是动态组合：运行时把组件装上去，用完了再拆下来——就像操作系统加载驱动、DSH 挂载插件。

论文给这种能力起了一个正式名字：时间可组合性（time composability）。它要求：

• 组件可以在运行时加载；
• 组件可以在运行时卸载；
• 卸载时，共享环境必须恢复到组合前的状态——你装之前什么样，拆之后还得什么样。

🏠 打个比方：宿舍新搬来一位室友，在墙上打了钉子挂装饰画。等室友搬走，墙必须恢复原样——不然下一位室友住进来，看到的是一面千疮百孔的墙。

这引出一个硬性要求：组件对环境所作的每项修改，都必须既可跟踪、又可逆。

• 可跟踪（trackable）：系统得知道它改过什么；
• 可逆（invertible）：系统得能把每一处改动原样撤销。

不满足这两条会怎样？最典型的后果就是清理逻辑靠手写：每个组件卸载时自己写一段「还原代码」。写多了就会漏、会错、会忘——忘掉一处，环境就被悄悄污染，而且越积越多、无从查起。论文的答案是：别让程序员手写清理，把「撤销」做成效应本身的结构性属性。

第 2 步：核心思想——每个变换都配一把「逆钥匙」

怎么做才能「不用手写清理」？论文的思路非常朴素：把效应建模成「变换 + 逆变换」的函数。

一个纯函数形式的效应长这样：

f : Γ × X → Γ × Y

看不懂没关系，翻译成人话：输入一个环境 Γ 和一份输入 X，输出改过的环境和返回值 Y。 而关键升级在这一行：

效应 : Γ → Γ × (Γ → Γ)

意思是：把效应应用到当前环境后，除了拿到改过的环境，还额外返回一个显式逆函数（从 Γ 到 Γ 的函数）。这个逆函数就是「逆钥匙」：

• 装上时：环境从 γ 变成 f(γ)；
• 拆下时：拿出逆函数 f⁻¹，环境从 f(γ) 变回 γ。

🚿 打比方（厨房版）：你要装一台洗碗机。装的时候改了水管、动了电路——每一步改动都记下来：「我把进水管接到了这里，把电路从那里挪到了这里」。将来拆掉洗碗机，不用回忆，照着笔记一步步还原，厨房就恢复原样了。

🧳 打比方（行李版）：出差住酒店，你把房间布置成自己喜欢的样子（把台灯挪到床头、把书摆上书架）。退房时不需要记得每样东西原来的位置——只要有一份「还原清单」，照着放回去就行。逆变换就是这份清单。

把逆函数返回给运行时，这招一箭双雕：

• 可逆：有了 f⁻¹，任何改动都能撤销；
• 可跟踪：运行时收集到所有 f⁻¹，就知道组件改过什么。

论文把这类效应叫做可回退效应（revertible effect）：执行期间记录并组合这些逆函数后，完整恢复环境就不再是程序员的义务，而是一种结构性保证。

图中三块：装组件时执行变换 f、抽屉里自动存下 f⁻¹；卸载时应用 f⁻¹、环境还原——装上时记录，拆下时还原，中间没有一行手写的清理代码。

第 3 步：效应上下文 ∂Γ = Γ × 𝔉Γ——「状态 + 账本」

逆钥匙有了，把它存哪儿？论文发明了一个新东西：效应上下文（effect context）。

先引入记号：设 𝔉Γ 是所有「可接受效应」的集合（𝔉 是花体 F）。这些效应满足三条公理：

把这三条合起来，𝔉Γ 在复合运算 ∘ 下构成一个群——数学上保证「怎么装都能怎么拆」。注意一个作用域限制：Γ 只建模系统完全掌控的内部状态；网络请求、文件 I/O 这类指向系统外部的操作并不修改 Γ，从 𝔉Γ 的角度看它们等于什么都没做（idΓ），由领域特定的策略（比如补偿事务）另行处理。

接下来是本节最重要的定义：

定义 1（效应上下文）：给定上下文 Γ，效应上下文定义为 ∂Γ = Γ × 𝔉Γ

它可以理解为二元组 (γ, φ)：

• γ ∈ Γ：当前的上下文状态；
• φ ∈ 𝔉Γ：把上下文恢复到初始状态的变换（累积的逆变换账本）。

特别地，初始状态是 (γ₀, idΓ)——状态是最初的 γ₀，账本还是空的（恒等变换）。

🧳 行李版：∂Γ 就是「行李箱 + 还原清单」。γ 是行李箱当前的样子，φ 是清单上累积的还原步骤。刚出发时，行李箱是原样 γ₀，清单空空如也（idΓ）。

有了这个二元组，装上/拆下就变成了两个自动化的操作——track 和 recover。

track：装上时自动记账

定义 2（trackΓ）： trackΓ = f ↦ (γ, φ) ↦ (f(γ), φ ∘ f⁻¹)

读法：把普通变换 f 变成「边做边记逆」的版本。执行 trackΓ(f) 时：

• 状态部分：应用 f，γ 变成 f(γ)；
• 账本部分：把 f 的逆 f⁻¹ 追加进 φ（用 ∘ 复合），φ 变成 φ ∘ f⁻¹。

装上组件 = 改环境 + 逆变换自动入账。 组件完全不用管记账的事。

论文还给了两条保证（定理 3、定理 4），直观理解就行：

• 定理 3（跟踪不改变行为）：pr1 ∘ trackΓ(f) = f ∘ pr1——track 版在「状态分量」上的表现和原变换一模一样，加了个账本但不影响正常使用；
• 定理 4（跟踪保持复合）：trackΓ(f ∘ g) = trackΓ(f) ∘ trackΓ(g)——先复合再跟踪，等于先跟踪再复合。意思是逆变换的记账可以放心叠在一起：装了 10 个组件，账本里就有 10 个逆变换，结构不乱。

recover：拆下时自动还原

定义 5（recoverΓ）： recoverΓ = (γ, φ) ↦ (φ(γ), idΓ)

读法：把账本 φ 整体应用到当前状态 γ 上，得到还原后的环境 φ(γ)；然后清空账本，φ 重置为恒等变换 idΓ。

由于 φ 里累积的是逆变换，而且新逆变换排在后面、先被应用，恢复时正好后装的先拆、逆序撤销——像一串自动播放的撤销操作，把环境一步步推回最初的 γ₀。

第 4 步：装上自动记账，拆下自动还原

把 track 和 recover 拼起来，就是完整的「装上 → 拆下」循环：

初始          (γ₀, idΓ)
装上 f₁       →  (f₁(γ₀), idΓ ∘ f₁⁻¹)
装上 f₂       →  (f₂(f₁(γ₀)), f₁⁻¹ ∘ f₂⁻¹)
装上 f₃       →  (f₃(f₂(f₁(γ₀))), f₁⁻¹ ∘ f₂⁻¹ ∘ f₃⁻¹)
拆下 recover  →  (γ₀, idΓ)

看最后一行：recover 把三个逆变换按逆序依次应用，环境精确回到 γ₀，账本清空——整个循环是闭合的。

🎮 生活版：想象一款游戏里，你给角色连续加了三个 buff（力量、速度、护盾）。系统在你加 buff 的同时自动记下对应的「撤销卡」。加错了 buff？点一下「还原」，系统按后加的先用的顺序把 buff 一个个撤掉，角色回到加 buff 前的状态，一张卡都不会漏——你没有手写过任何一行「撤销逻辑」，它由机制本身保证。

为什么这算「结构性保证」，而不是又一种「自动帮你清理」的魔法？因为保证来自结构本身：

1. 𝔉Γ 的逆元公理：每个变换都有逆变换，所以每个改动都可撤销；
2. 定理 4 的复合保持：逆变换任意复合仍然可撤销，所以装了再多的组件，一次 recover 就能全部还原；
3. track 把记账内建进效应本身，程序员没有机会漏记——漏记是手写方案才有的 bug。

换句话说：只要组件通过 track 施加变换、卸载时通过 recover 收尾，环境还原就是数学上保证成立的事，跟程序员记不记得住无关。

💡 串回主线：这正是 DSH「装上能拆下、拆下不留痕」的理论来源——智能体在运行时挂载/卸载插件之所以安全，是因为底层每个效应都自带逆变换，卸载 = 播放逆变换。

关键点回顾

1. 时间可组合性 = 运行时能加载/卸载组件，卸载时共享环境恢复原状；要求每项修改既可跟踪、又可逆。
2. 可回退效应 = 把效应建模成「变换 + 逆变换」：Γ → Γ × (Γ → Γ)，逆函数返回给运行时，撤销就成了一种结构性保证。
3. 效应上下文 ∂Γ = Γ × 𝔉Γ：二元组 (γ, φ)——γ 是当前状态，φ 是累积的恢复变换（逆变换账本），初始为 (γ₀, idΓ)。
4. trackΓ 把普通变换变成「边做边记逆」的版本：(γ, φ) ↦ (f(γ), φ ∘ f⁻¹)；recoverΓ 把 φ 整体应用后重置为 idΓ：(γ, φ) ↦ (φ(γ), idΓ)。
5. 结构性保证：逆元公理保证可撤销、定理 4 保证任意复合可一键撤销、track 把记账内建进效应——所以不需要手写清理逻辑。

🚀 下一课「第 7 课：效应函数与组合：逆变换自动组合」，我们会仔细看逆变换是怎么自动组合的——定理 4 到底在保证什么，多个效应叠加时「一键撤销」为什么依然成立。