BotOf Tech — 技术与植物养护笔记

译文系列（1/4）：① 问题、预备知识与上下文范式 · ② 动态组合演算 · ③ Cordis 实现与 Koishi · ④ 系统边界、相关工作与结论

论文：Yifan Shi、Wei Zhang、Tianyi Cui，A Programming Paradigm for Spatiotemporal Composability，2026 年 8 月 13 日预印本。作者单位：北京大学、DeepSeek-AI。本文依据 88 页预印本翻译；术语统一为 effect「副作用」、coeffect「协同效应」、revertible effect「可逆副作用」、reactive coeffect「响应式协同效应」。公式、定义、定理和章节编号遵循原文；为适配网页阅读，部分逐行等式证明合并成等价的中文推导，参考文献题名保持原文。

摘要

从插件系统到能够自我演化的 Agent Harness，现代软件越来越依赖动态组合，但这类系统的形式化基础仍不充分。本文指出问题有两个相互正交的维度：时间可组合性，即组件被移除时能够完整撤销它产生的副作用；空间可组合性，即组件能够声明组件间依赖，并由运行时对这些依赖进行响应式管理。

论文把经典 effect 与 coeffect 概念提升为运行时机制。对于前者，作者形式化了可逆副作用：每次上下文变换都携带一个由运行时跟踪的逆变换。对于后者，作者形式化了响应式协同效应：上下文每次变化时，运行时都根据组件的协同效应规格通知组件。随后，论文把副作用上下文与协同效应上下文统一为一种上下文类型，由此形成一种编程范式。

在此基础上，论文把两种机制合并为「组件」，给出动态组合演算，并用元理论把单个组件的时空可组合性推广到多个交错执行组件构成的完整系统。作者又把这些思想实现为 Cordis：一个面向时空可组合性的元框架，核心库提供副作用跟踪和协同效应解析，声明式组件加载器则提供配置协调与热模块替换。

1. 引言

组合——由较简单的部分装配复杂系统——是软件工程的基础原则。传统组合是静态的：函数调用、模块导入和类继承在编译期解析，并在整个执行期间保持不变。现代软件却越来越需要动态组合，即在运行时加载、卸载和重新配置组件。插件架构和自我演化的 Agent Harness 都要求系统能够即时、安全地增删功能；当前实践往往退回到粗粒度机制，只能通过重启完成重配置，并丢弃运行时状态。与静态组合已有的丰富形式化框架相比，动态组合的理论仍明显不足。

1.1 可组合性的两个维度

除已有研究充分讨论的代数组合性质外，动态组合还包含两个正交维度：

时间可组合性处理时间维度：组件移除时，它对共享环境造成的修改必须被完整、安全地撤销。系统要跟踪组件执行的每一次资源分配、事件注册和状态变更，并在移除时保证这些资源按顺序回收。
空间可组合性处理空间维度：组件必须能以结构化且可验证的方式声明、发现和解析彼此依赖。系统要管理依赖拓扑，并在依赖发生变化时协调组件生命周期。

在静态场景中，时间可组合性可退化为词法作用域，例如 RAII 或 bracket 模式；空间可组合性可退化为模块导入解析。在组件运行时到达和离开的动态场景里，两者都会变难：时间一侧要处理超出词法边界的长期、有状态副作用；空间一侧要处理执行过程中出现、消失或身份改变的依赖。

1.2 动机示例

1.2.1 插件系统

插件系统是动态组合的典型实例。论文以 VS Code 为例。

时间维度的局限。 VS Code 把所有扩展运行在共享的 extension host 进程中。扩展虽可动态安装，却不能在运行时单独卸载代码。一个扩展的 activate 执行后，禁用或卸载它需要重启整个 host，连带影响所有扩展。主题、快捷键、snippet 等纯声明式扩展可以自由移除，但作者在 2026 年 6 月 9 日统计安装量前 100 的扩展时发现，其中 87 个包含可执行代码，移除时都需要重启。deactivate 只是在 host 退出时提供优雅停机回调，并不支持在线卸载；而且副作用创建位于 activate，清理却位于另一个钩子，这破坏了关注点局部性，也使完整清理难以验证。

空间维度的局限。 VS Code 提供 extensionDependencies，但同一统计样本里只有 7 个扩展声明了对非内置扩展的依赖。其 API 主要暴露命令、视图、语言能力等固定、表层扩展点，扩展更常把能力贡献给 host，而非依赖其他扩展。扩展间交互也缺少结构化契约：vscode.extensions.getExtension(...).exports 默认返回 any，依赖方无法依赖一个经过检查的接口。这个问题并非 VS Code 独有，而是插件系统普遍存在、程度不同的限制。

1.2.2 自我演化的 Agent Harness

现代 AI Agent 依赖运行时 Harness。它们组合工具集和执行环境，管理权限与沙箱，维护会话状态和持久化，提供上下文与记忆系统，编排子 Agent 和多 Agent 工作流，并向用户与自动化系统开放接口。未来的 Harness 可能持续服务请求，同时生成并部署对自身组件的修改。模型生成的可复用工具，已经是组件级自修改的早期形态。每一次这种修改本质上都是动态组合。

由于修改会持续发生，且人工监督有限甚至不存在，动态可组合性不可或缺。缺少时间可组合性时，每次自修改都迫使进程整体重启，丢掉进程内积累的缓存、连接和进行中任务；频繁重启会积累可观的不可用时间，错误修改甚至可能破坏负责恢复的进程本身。缺少空间可组合性时，每个模块都要用临时办法自行侦测依赖的出现、消失和身份变化；粗暴替换代码还可能悄悄破坏依赖方，或引入直到重载时才暴露的环形依赖。

1.2.3 粗粒度替代方案

动态可组合性长期未被充分形式化，一个原因是操作系统和容器编排器已提供粗粒度替代：操作系统在进程粒度提供时间可组合性，容器编排器在服务粒度提供空间可组合性。实践中，异常模块靠重启进程处理，服务依赖交给编排器管理。

代价同样明显。时间上，重启会丢掉所有进程内状态，重建缓存、连接和部分计算可能需要数秒至数分钟；为维持可用性，还要用冗余副本补偿无法单独恢复组件的问题。空间上，容器级编排无法表达同一地址空间内组件间的依赖，并把原本可以是本地函数调用的交互变成网络调用。进程、容器边界与现代软件的细粒度组合不匹配，因此需要一种在组件同一粒度管理副作用和依赖的抽象。

1.3 贡献

动态组合的两个维度分别回答「计算怎样修改环境」和「计算怎样依赖环境」。effect system 为前者提供形式化词汇，coeffect system 为后者提供形式化词汇，但经典形式只在编译期、词法固定的作用域内推理，不能覆盖组件运行时到达和离开的情形。论文的五项贡献是：

形式化可逆副作用：每个上下文变换携带显式逆变换；跟踪和恢复都保持组合，因此组件移除后能恢复上下文，建立局部时间可组合性。
形式化响应式协同效应：组件把环境需求声明为规格；上下文变化后，运行时把变化分类为激活、停用或中性，建立局部空间可组合性。
把副作用上下文与协同效应上下文统一为一种上下文类型，并以协同效应上的观测等价关系为副作用提供独立性，形成时空可组合性编程范式。
给出动态组合演算：把两种机制结合为组件及其生命周期操作语义，并把局部保证推广到交错执行的完整系统。
在 Cordis 中实现该理论：核心库负责副作用跟踪和协同效应解析，声明式加载器负责配置协调与热模块替换。

2. 预备知识

2.1 副作用

在简单类型 λ 演算中，判断 Γ ⊢ t : T 表示项 t 在上下文 Γ 下具有类型 T。副作用系统细化结果类型，说明计算可能产生哪些副作用：

Γ ⊢ t : T_effect                                      (1)

结果类型由副作用代数中的元素标注，从而能够对有状态计算做组合式推理。Lucassen 与 Gifford 最早用 kind 区分类型、副作用和区域，以发现并行程序的调度约束。

单子副作用。 Moggi 首先用范畴论中的单子 (T, η, μ) 建模计算副作用，Wadler 随后在 Haskell 中推广。T(A) 封装带副作用计算，η : A → T(A) 把纯值提升进去，μ : T(T(A)) → T(A) 对嵌套计算排序。Maybe、State 与 IO 分别对应部分性、可变状态和外部交互。

代数副作用。 Plotkin 与 Power 证明代数操作能够确定单子，由此可以把副作用接口与实现分离。签名 Σ 声明操作，例如状态的 get : () → S、put : S → ()；程序自由调用，而不先选定解释。effect handler 再以延续语义解释操作：

handle e with { op(v, κ) ↦ … }                        (2)

处理器拿到参数 v 与定界延续 κ，可以调用它零次、一次或多次，从而以统一框架表达异常、协程和非确定性。Koka、Eff、OCaml 5 已采用不同取舍的代数副作用。

2.2 协同效应

与副作用对偶，协同效应系统丰富的是上下文而非结果类型：

Γ_coeffect ⊢ t : T                                    (3)

上下文由协同效应代数中的元素标注，说明计算对环境的要求，例如可访问资源、必须持有的权限或依赖服务。副作用描述程序对世界的影响，协同效应描述世界对程序施加的约束。

余单子协同效应。 Uustalu 与 Vene 用对称（半）幺半余单子组织依赖上下文的计算，作为 Moggi 单子副作用框架的对偶。余单子 (D, ε, δ) 中，ε : D(A) → A 从上下文取出当前值，δ : D(A) → D(D(A)) 为嵌套访问复制上下文。环境余单子 D(X)=E×X 表达对固定环境 E 的依赖，流余单子 D(X)=ℕ→X 表达对时序数据的依赖。

分级协同效应。 更细粒度的系统以预序半环 S=(S,≤,+,×,0,1) 作为协同效应代数。元素标注变量绑定的使用量：0 未使用，1 线性使用，n 有界使用，∞ 无限制。乘法与加法分别组合顺序和并行的协同效应，支持精确资源跟踪、敏感度分析和信息流控制。

2.3 与动态可组合性的关系

时间可组合性要求组件卸载时撤销它对共享环境造成的持久状态变换，因此相关副作用必须具有逆。
空间可组合性要求声明并响应式管理组件依赖，而依赖正是协同效应描述的对象；管理它们意味着把每项需求与环境供给进行解析。

经典 effect/coeffect 系统是静态工具：副作用在词法固定作用域里跟踪，由编译期 handler 消解；协同效应标注针对执行前已经确定的上下文验证。动态组合却要让保证作用于运行时到达和离开的组件，并面对持续演化的上下文。部署后才加载的插件没有固定词法作用域，运行时配置产生的依赖也不可能由编译期上下文预知。

因此，作者不再继续向静态类型系统叠加标注，而是把 effect 与 coeffect 的概念结构具体化，让运行时直接操作，从而在动态阶段建立静态系统原本提供的保证。

3. 可逆副作用与响应式协同效应

本章把 effect 与 coeffect 提升为运行时机制。核心做法是把承载它们的 typing context 变成可以由运行时操作的上下文类型，将上下文具体化为一等实体。副作用侧被建模为带逆变换的上下文变换，得到局部时间可组合性；协同效应侧被建模为携带依赖信息的类型，得到局部空间可组合性；协同效应上的观测等价再为副作用提供独立性。统一上下文本身构成一种编程范式。

3.1 可逆副作用

时间可组合性意味着组件可在运行时装入和卸载，且卸载后共享环境回到组合前状态。每一项修改都必须可跟踪、可恢复。论文把副作用建模为：

Γ → Γ × (Γ → Γ)

它接收当前上下文，返回新上下文以及一个显式逆函数。提供逆使副作用可撤销；把逆交给运行时使它可跟踪。运行时持续组合这些逆，就能把完整恢复变成结构保证。

3.1.1 副作用上下文

任意不纯函数 f_impure : X → Y 都可纯化为 f : Γ×X → Γ×Y，所有副作用都表现为对 Γ 的变换。固定输入 x 后，γ ↦ pr₁(f(γ,x)) 独立于返回值地表示副作用。Γ→Γ 在函数复合 ∘ 下形成幺半群：顺序执行仍是副作用；复合满足结合律；id_Γ 是单位元。

定义 1（扭曲复合）。 给上下文变换及其左逆配对，逆只要求 g∘f=id，不要求 f∘g=id：

(f₁,g₁) ⊙ (f₂,g₂) := (f₁∘f₂, g₂∘g₁)                 (4)

正向变换按执行顺序复合，逆按相反顺序积累。(Γ→Γ)×(Γ→Γ) 因而成为扭曲复合幺半群 𝕋_Γ，单位元为 (id_Γ,id_Γ)。

定义 2（副作用上下文）。

∂Γ := Γ × (Γ → Γ)                                    (5)

状态 (γ,φ) 中，γ 是当前上下文，φ 是此前所有副作用之逆的复合，也是恢复到初态的累加器。初始副作用上下文为 (γ₀,id_Γ)；还可以继续构造 ∂²Γ=∂Γ×(∂Γ→∂Γ)。

定义 3（跟踪）。

track_Γ(f,g)(γ,φ) := (f(γ), φ∘g)                     (6)

它执行正向函数，并把候选逆接到累加器之后。

定理 4。 投影与跟踪可交换：pr₁∘track_Γ(f,g)=f∘pr₁。证明只需展开定义：投影 (f(γ),φ∘g) 的第一项正是 f(γ)。

定理 5。 track_Γ 是从 𝕋_Γ 到 ∂Γ→∂Γ 的幺半群同态：单位元映到单位元；两个 pair 的扭曲复合映为两个 track 的函数复合。关键是逆累加为 φ∘g₂∘g₁。

定义 6（恢复）。

recover_Γ(γ,φ) := (φ(γ), id_Γ)                       (9)

恢复函数把累加器应用于当前状态，并把累加器重置为单位元。

定理 7。 若 g(f(γ))=γ，则：

recover_Γ(track_Γ(f,g)(γ,φ)) = recover_Γ(γ,φ)        (10)

因为左侧展开为 (φ(g(f(γ))),id_Γ)=(φ(γ),id_Γ)。序列情形由定理 5 直接得到：若每个逆都能撤销它实际作用状态上的变换，组合累加器就把最终状态送回起点。φ(γ)=γ₀ 被称为 ∂Γ 状态的健全性不变量。

3.1.2 可逆副作用函数

固定 pair 的模型要求在看到状态前就选定同一个逆，且 recover 只能全有或全无。实践中，逆通常要在副作用发生点根据当时状态生成，而且系统需要选择性撤销一个副作用而保留其他副作用。因此输入侧让函数返回逆，输出侧又让提升后的函数返回自身的逆。

定义 8。 副作用函数与带见证的副作用函数：

𝔈_Γ  := Γ → Γ × (Γ → Γ)
𝔈*_Γ := e : 𝔈_Γ，并对每个 γ，若 e(γ)=(δ,g)，则 g(δ)=γ   (12)

见证条件只约束逆在本次作用点上确实恢复原状态；它无需在所有状态上都成为统一逆。

定义 9（副作用复合）。 若 f,g∈𝔈_Γ：

(f ⋄ g)(γ) :=
  let (δ,s)=g(γ)
  let (ε,t)=f(δ)
  in (ε, s∘t)                                         (13)

定理 10。 (𝔈_Γ,⋄) 是以 η_Γ(γ)=(γ,id_Γ) 为单位元的幺半群；从固定 pair (f,g) 到 γ↦(f(γ),g) 的映射是 𝕋_Γ→𝔈_Γ 的幺半群同态。

定理 11。 见证在 ⋄ 下保持，因此 𝔈*_Γ 是子幺半群；若统一逆满足 g∘f=id_Γ，其诱导的副作用函数在每个状态上都有见证。复合情形中，t(ε)=δ、s(δ)=γ，所以 (s∘t)(ε)=γ。

定义 12（副作用提升）。

effect_Γ(e)(γ,φ) :=
  let (δ,g)=e(γ)
  in ((δ,φ∘g), track_Γ(g, pr₁∘e))                    (14)

effect_Γ(e) 本身属于 𝔈_{∂Γ}。撤销一个副作用本身也是副作用：它以 g 为正向变换，而再次执行原副作用的正向部分可撤销这次撤销。

定理 13。 effect 保持复合：effect_Γ(f)⋄effect_Γ(g)=effect_Γ(f⋄g)。

定理 14。 提升前后的正向图和逆向图都通过第一投影交换。若 f=pr₁∘e，提升后的正向图为 f'，则 pr₁∘f'=f∘pr₁；在某状态产生的提升逆 g' 满足 pr₁∘g'=g∘pr₁。

定理 15。 设 e(γ)=(δ,g)，effect_Γ(e)(γ,φ)=(Δ,g')，则：

g'(Δ) = (γ, φ∘g∘f)                                  (16)

上下文状态被精确恢复；累加器在且仅在 g∘f=id_Γ 时也完全恢复。无论如何，(φ∘g∘f)(γ)=φ(γ)，所以健全性不变量保持。

定理 16。 从 (γ₀,id_Γ) 顺序应用 e₁…eₙ∈𝔈*_Γ，再按相反顺序撤销时，每一次撤销都会恢复到对应应用发生前的状态，所有中间状态都保持健全性不变量。LIFO 顺序把每个逆送回它自己的正向变换刚刚产生的状态，不需要额外独立性假设。

3.1.3 副作用的独立性

真实系统可能在后续副作用仍保留时撤销前一个副作用，或让多个组件的副作用交错。此时逆遇到的是被其他副作用移动过的状态。要保证它仍只撤销自己的贡献，需要两个组件可能执行的所有正向与逆向变换彼此可交换。

定义 17。 𝔐(e) 是由 e 的正向图以及 e 在所有状态上可能返回的逆共同生成的变换子幺半群：

𝔐(e) := ⟨ {pr₁∘e} ∪ {pr₂(e(γ)) | γ∈Γ} ⟩             (17)

引理 18。 若两个变换幺半群的生成元两两交换，则其中任意元素两两交换；而 𝔐(e₁⋄e₂) 不超出由 𝔐(e₁)∪𝔐(e₂) 生成的幺半群。

定义 19。 e₁,e₂ 独立，当且仅当：

两边任意变换交换：∀f∈𝔐(e₁),g∈𝔐(e₂). f∘g=g∘f；
一方的变换不会改变另一方在某状态上选择的逆，并对交换方向也成立。

这比只要求 e₁⋄e₂=e₂⋄e₁ 更强，因为还必须检查正向图与对方逆之间的交换，以及状态变化不会让对方选出不同逆。

定理 20。 对两两独立的 e₁…eₙ，从 γ₀ 顺序执行后，任取第 j 个副作用并在更晚状态撤销，所得状态等于从未执行 e_j 而执行其余序列的状态；其他副作用在这个状态上选择的逆也与原来相同。

推论 21。 两两独立副作用执行完后，可以按任意排列撤销所有逆，最终都到达 γ₀。LIFO 只是其中一种排列；独立性购买的是所有其他撤销顺序，以及多个组件副作用的安全交错。

这组构造给出局部时间可组合性：组件加载就是执行一列副作用并在 φ 中累积逆，组件卸载就是应用 φ。组件内部的顺序敏感操作由 LIFO 累加器处理；跨组件若不独立，则需要由后文的协同效应声明提供外部顺序。

3.2 响应式协同效应

空间可组合性要求组件声明依赖，系统在运行时解析、提供和撤回依赖。共享上下文变化时必须重新检查依赖满足关系：依赖齐全时激活组件，依赖被撤回时停用组件。论文把组件依赖建模为规格，并将每次上下文变化分类为激活、停用或中性变化。

3.2.1 协同效应上下文

定义 22。 给定类型族 𝒱 : K→Type，协同效应上下文是有限依赖偏函数：

Σ := (k:K) ⇀ 𝒱_k                                      (20)

σ(k) 读取已绑定 key；σ[k↦v] 增加绑定；σ∖k 删除绑定。类型族保证每个 key 对应确定值类型。不能重复提供已有 key，也不能撤销不存在的 key；违反前置条件即报错且不发生转换。也可以把偏函数内部化为 Maybe 单子中的全函数。

定义 23。

get(k)(σ)     := σ(k)
set(k,v)(σ)   := (σ[k↦v], λσ'. σ'∖k)                  (21)

set(k,v) 恰好具有 𝔈*_Σ 类型，因此第 3.1 节的跟踪和恢复机制可以直接自动跟踪依赖注册。协同效应操作是副作用，而副作用可逆。

定义 24。 key k 上的协同效应是三元组 (𝒱_k, ≃_k, 𝒜_k)：值类型、比较值时采用的等价关系、组件可执行的操作集合。操作 a∈𝒜_k 具有参数 X_a、结果 B_a，并作用于 key 对应值：

a : X_a → 𝒱_k ⇀ 𝒱_k × (𝒱_k ⇀ 𝒱_k) × B_a             (22)

前两项是带见证副作用函数，第三项是结果。操作必须尊重 ≃_k，并可提升为只读写 Σ 中 key k、保持其他 key 不变的操作 a_Σ。类型本身就把操作限制在自己的 binding 上。

3.2.2 规格与通知

对规格 d⊆K，满足关系定义为：

σ ⊧ d  :=  ∀k∈d. k∈dom(σ)                            (24)

dom(σ) 有限，因而满足关系可判定；所有 σ 的变化都经过可逆副作用边界，因此每一次满足关系变化都可被观察。

定义 25。 协同效应规格 𝔇_Σ := Set(K)，即组件声明的依赖 key 集合。

定义 26。 对状态变化 σ→σ'：

notify_d(σ,σ') = activating    若 σ ⊭ d 且 σ' ⊧ d
                 deactivating  若 σ ⊧ d 且 σ' ⊭ d
                 neutral       其他情况                     (26)

激活变化触发组件副作用并完整跟踪；停用变化触发累加器恢复。由此得到局部空间可组合性：组件只在规格满足时激活，所以不会读取缺失 binding；每次上下文变化都被分类，所以依赖丢失会在发生处被发现并触发停用。

若 A 提供 k、B 声明 k∈d_B，B 只能在 A 激活并提供 k 后激活。但反方向尚未保证：卸载 A 会删除 k，通知虽可要求 B 停用，却不能单靠自己让 k 在 B 清理期间继续可读，也不能阻止 A 在 B 清理完成前恢复。全局撤回顺序将在第 4.3.1 节解决。

3.2.3 隔离与拦截

平坦依赖表还不够：同一逻辑依赖可能需要在不同组件上下文中解析为不同值；横切策略也需要在不修改依赖值的前提下影响访问。

定义 27。 副作用函数有两种实现方式：

原地实现：修改上下文，返回非平凡逆；恢复时执行逆。
派生实现：输入保持不变，返回从输入派生的新上下文，逆为单位元；恢复时直接丢弃派生上下文。

隔离和拦截采用派生实现，不改变共享表，也不需要跟踪逆。

定义 28（隔离上下文）。

Σ_iso := (K ⇀ R) × ((r:R) ⇀ 𝒱_r)                    (27)

ρ:K⇀R 把逻辑 key 映射到 realm；未显式隔离的 key 解析到自身 realm。σ 从 realm 映射到实际值。访问 k 时先求 ρ(k)，再读 σ(ρ(k))。

定义 29。 get 和 set 沿 ρ(k) 工作，isolate(k,r) 则派生一个新上下文，把 k 重定向到 realm r 而继承原依赖表。隔离因此像运行时 ad-hoc 多态：同一依赖 key 可在不同上下文解析成完全不同的值；set 仍可逆，isolate 只派生上下文。

定义 30（拦截上下文与规格）。

Σ_inter := ((k:K)→M_k) × ((k:K)⇀(M_k→𝒱_k))
𝔇_inter := (k:K) ⇀ M_k                               (29)

上下文 (ι,σ) 中，ι 是 context 携带的元数据，σ 把 key 映射到「从元数据生成值」的 provider 函数；组件规格 d 也为每个 key 携带元数据。每个 M_k 具有幺半群结构 (M_k,⊕_k,ε_k)。

定义 31。 get(k,μ) 计算 σ(k)(μ⊕_kι(k))；set(k,ψ) 注册 provider 并返回删除它的逆；intercept(k,ν) 派生上下文，把 ν 合并进继承元数据。合并右偏，所以上层上下文可以覆盖组件声明，例如收紧组件使用某项能力时的权限。

3.3 上下文范式

3.3.1 统一上下文

定义 32。 把递归副作用上下文与 Σ 合并：

Γ∞ := μΓ. Γ × (Γ → Γ) × Σ                            (31)

三项分别是递归的当前上下文、恢复本层副作用的累加器和承载依赖信息的协同效应上下文。effect 在 Γ∞ 内自映射，把原先的 ∂ 塔统一为自相似类型。𝒱 不受限制，系统要跨组件共享的任何状态都可以编码成有确定值类型的依赖，因此 Σ 不只容纳服务依赖，也能容纳所有共享可变状态。组件与环境的交互都通过同一实体。

递归结构支持层级组合：父上下文聚合多个子级副作用，形成树状控制结构。加载组件是执行副作用，即「插入」；卸载组件是恢复副作用，即「拔出」；各层组件可以独立加载和卸载，父上下文统一管理任意深度的组合。

3.3.2 观测等价

物理状态通常无法逐比特恢复。free 释放内存块，却不会把堆布局恢复成 malloc 前的样子；丢弃生成式名称后，下次创建会得到新名称。第 3.1 节的相等应理解为某个等价关系 ≃ 下的相等。论文选择观测等价：观察者无法区分的状态视为相同。观察者能做的事由上下文携带的协同效应操作决定，因此上下文等价由各 key 自己的等价关系组装。

定义 33。 两个协同效应上下文在绑定同一组 key，且每个 key 上的值按 ≃_k 等价时等价；两个状态在其协同效应投影等价时等价：

σ ≃ σ' := dom(σ)=dom(σ') ∧ ∀k∈dom(σ). σ(k)≃_kσ'(k)
γ ≃ γ' := σ_γ ≃ σ_γ'                               (32)

未被任何 key 绑定的状态被有意遗忘，这使堆布局、生成式名称等不可观察差异不妨碍恢复。相关状态具有相同 domain，因此对规格满足和 notify_d 的分类也一致。

定义 34。 对操作集合 𝒜，一次 test 是由其正向图和可能返回的逆构成的有限操作序列。两个值若所有测试要么在两边都可定义、要么都不可定义，并产生相同结果，则记为 v≈_𝒜v'。

引理 35。 不可区分关系 ≈_𝒜 是所有操作都尊重的最粗关系：每个操作都保持它；任何被全部操作保持的等价关系都包含在它之内。因此每个允许的 ≃_k 都不比 ≈_{𝒜_k} 更粗，而 ≈_{𝒜_k} 本身可作为合法选择。

定义 36。 变换 f 尊重 ≃，当 γ≃γ' 蕴含 f(γ)≃f(γ')。两个变换若在所有状态上得到等价结果，则彼此等价；副作用函数返回的状态与逆都按该关系比较。

定义 37。 把定义 8 提升到观测等价：e∈𝔈*_Γ 必须作为 Γ→∂Γ 的映射尊重 ≃；若 e(γ)=(δ,g)，则 g(δ)≃γ，且 g 本身尊重 ≃。

引理 38。 在这个定义下，第 3.1 节所有关于状态相等的结论把 = 换成 ≃ 后仍成立；从 (γ₀,id_Γ) 可达状态的每个累加器都尊重 ≃。原因是累加器只是若干个尊重等价关系的逆的复合。

定义 39。 两个 coeffect 操作独立，当它们对所有参数提升成的副作用函数独立，且一方的变换不改变另一方的返回结果。某 key 上任意两个操作都独立时，该 key 是可交换的。

定理 40。 不同 key 上的操作天然独立。每个提升操作只读写自己的 binding；不同 key 的生成元交换，也不会改变对方选择的逆或产生的结果。

典型可交换 key 是由独立条目组成的表，例如路由表或事件监听器表：两次注册换序后，所有测试观察到的表相同，任意一个注册也可独立撤回。中间件有序链通常不可交换，因为插入顺序会改变请求经过的处理顺序。内存分配是否可交换取决于接口是否允许观察地址身份。

定义 41。 coeffect-mediated 副作用函数从单位元开始，每个阶段执行某个 key 上的操作，并可根据操作结果选择下一个阶段。它能表达后续参数依赖此前输出的实际组件逻辑。

定理 42。 若两个 coeffect-mediated 副作用函数共同触及的每个 key 都是可交换的，则两函数独立。不同 key 由定理 40 保证；相同 key 由可交换性保证；操作结果不受对方变换影响，因此选择的后续阶段和逆也保持一致。

这一结论把计算分成两个部分：

可交换部分由副作用承载，组件按任务需要的顺序执行，系统可以按方便的顺序撤回。
顺序敏感部分由协同效应承载。组件内部由 LIFO 累加器保持顺序；组件之间由「一个组件提供、另一个组件声明」建立先后关系。

理论边界也很明确：系统无法具体化为 coeffect 的共享位置不在定理范围内；key 的可交换性取决于该 key 发布的接口，是 provider 的义务，而不是 consumer 能自动创造的属性。

3.3.3 上下文范式的位置

纯函数式编程通过显式状态传递保持引用透明：State 单子 S→(A,S) 让副作用在类型中可见并可等式推理，但调用链上每个函数都必须接收和返回状态；副作用维度增多时，monad transformer 或 handler 样板迅速膨胀。

命令式/OOP 允许组件隐式修改共享状态、读取依赖。React useEffect 把持久副作用登记到内部 fiber，目标和注册机制不作为显式参数，而依赖隐藏运行时中的调用顺序位置；Spring ApplicationContext.getBean(...) 一类 service locator 从进程级 registry 取依赖，调用点要做空值检查与类型转换。理解函数如何改变或依赖系统，需要递归阅读实现，重构也容易破坏远处不变量。

上下文范式试图同时保留函数式方法的可追踪性与命令式方法的易用性：副作用和协同效应都通过显式 context 进行，因此每次操作可归属到被调用的 context，继而归属到拥有它的组件。开发者只需为每个原子副作用提供逆，组合副作用的逆由运行时自动推导；只需声明组件需要的依赖，provider 增删或替换时，运行时自动解析和重接。原本依赖开发者纪律的正确性，由此变成范式的结构属性。