时空可组合性的编程范式 A Programming Paradigm for Spatiotemporal Composability
把效应与余效应提升为运行时机制，为动态组件组合提供可逆撤销与响应式依赖的形式基础
前置知识
效应系统（Effect Systems）
在类型论中为程序标注可能产生副作用的机制，判断形如 $\Gamma \vdash t : T^{effect}$，由 Lucassen 与 Gifford 提出，经 Moggi 用单子、Plotkin 与 Power 用代数效应发展。它把『程序对环境做了什么』从具体实现中解耦出来，使有状态计算可以被组合地推理、调度与解释。
本文的第一根支柱就是把这种编译期效应追踪提升为运行时的『可逆效应』：理解效应系统才能看懂『每个上下文变换都随身携带逆变换』这一核心形式化。
余效应系统（Coeffect Systems）
与效应对偶的概念：效应描述程序对环境做了什么修改，余效应描述环境对程序提出了什么要求。判断形如 $\Gamma^{coeffect} \vdash t : T$，用余单子（Uustalu-Vene）或分级半环标注上下文，可表达资源使用次数、敏感性分析、信息流控制等对环境的依赖约束。
本文将余效应具体化为运行时组件的依赖声明（inject/provide）与响应式解析，是空间可组合性的理论支柱。
单子与余单子
单子 $(T, \eta, \mu)$ 在范畴论中封装效应计算：$\eta: A \to T(A)$ 提升纯值，$\mu$ 串联嵌套计算，如 Haskell 的 State/IO monad。余单子 $(D, \varepsilon, \delta)$ 对偶地刻画依赖上下文的计算，如环境余单子 $D(X) = E \times X$ 表示计算依赖固定环境 $E$。
论文第 2 节用这对概念统一表述效应与余效应，读者需要这套词汇才能理解 $\mathcal{E}_\Gamma$、$\Gamma^\infty$ 等类型构造的设计动机。
操作语义与元理论
用归约规则（如 $\gamma \Rightarrow \delta$ 编排步、$\gamma \to \delta$ 生命周期步）精确描述系统如何一步步演化。典型元理论性质包括保持性（规则保持注册表良构）、进展性（非静止态总有规则可用）与合流性（归约次序不影响最终归约结果）。
第 4 节的动态组合演算就是 9 条操作语义规则，论文的主要贡献正是它的一系列元定理：恢复精确性、排序、活性、合流性。
观测等价（Observational Equivalence）
不比较状态内部表示而比较行为：若任何观察者用可用操作进行的任何有限测试都无法区分两个状态，则二者观测等价（记作 $\simeq$）。具体关系取决于观察者被允许使用哪些操作，是由接口生成的关系。
物理状态不可能逐位还原（malloc 后 free 不恢复堆布局），本文所有恢复保证都读作『在 $\simeq$ 意义下成立』，而 $\simeq$ 由每个键的操作集生成，是全文等式成立的前提。
控制反转容器与依赖注入
IoC 容器（如 Spring、Guice、Inversify）用键值映射管理依赖：组件声明需要什么，容器在初始化时查找提供者并注入实例。传统实现是一次性绑定，运行中提供者消失或被替换时，既有依赖方既不会失效也不会自动重建。
论文明确把 IoC 容器形式化为余效应上下文 $\Sigma$（带类型的部分函数表），并指出它缺少的响应式重解析正是本文要补足的空间可组合性。
热模块替换（HMR）
前端开发中不重启进程就替换已加载模块的技术，webpack 与 Vite 均支持，但要求开发者显式标注模块边界的 accept 回调，未覆盖的改动会触发整页刷新甚至重启。
Cordis 的 HMR 利用可逆效应自动卸载并重装组件 fiber，无需任何开发者标注的接受边界，是时间可组合性最直观的工程收益展示。
研究动机
现代软件越来越依赖动态组合——在运行时加载、卸载、重配组件——但其形式基础严重滞后于静态组合。论文用 VSCode 插件生态给出量化证据：在安装量最高的 100 个扩展中，87 个包含可执行代码，它们一旦安装就无法在运行时单独卸载，禁用或卸载都必须重启整个 extension host 进程（数据取自 2026 年 6 月 9 日的 Marketplace）；VSCode 虽提供 extensionDependencies 声明依赖，但同样的 Top 100 中只有 7 个对非内置扩展声明了依赖，且扩展间经 getExtension(...).exports 交互的返回值默认无类型（any），没有结构化契约。deactivate 钩子把副作用的创建（activate）与销毁分离在两处，正确性全靠作者自觉，遗漏即静默泄漏。对自进化 AI 智能体框架问题更尖锐：智能体持续生成并替换自身组件，每次自我修改若都触发重启，会反复丢弃进程内累积状态、打断在途任务，错误的修改甚至可能杀掉负责恢复的进程。业界通行的绕行方案是退到粗粒度机制——操作系统提供进程粒度的时间可组合性，容器编排器提供服务粒度的空间可组合性——但每次重启丢弃缓存、连接等状态需数秒到数分钟重建，还需冗余副本维持可用性，且容器间交互引入网络开销，无法表达共享地址空间内的组件级依赖。粒度错配要求一个与组件同粒度的组合抽象。
本文的目标是论文要为动态组合建立一套语言无关的形式基础与可落地的实现，具体拆成两个正交维度：时间可组合性——组件被移除时，它对共享环境做过的全部副作用（资源分配、事件注册、状态修改）必须被完整、有序地撤销，使环境恢复到组合前状态；空间可组合性——组件能以结构化、可验证的方式声明彼此依赖，运行时在依赖出现、消失或更换提供者时被动地驱动组件的激活与去激活。最终交付物包括：把经典效应/余效应概念提升为运行时机制的理论构造（可逆效应与响应式余效应）、统一二者的上下文范式、一个带完整元理论（保持性、恢复精确性、排序、解析一致性、活性、合流性）的动态组合演算，以及实现该范式的元框架 Cordis（核心库 + 声明式组件加载器 + 热模块替换），使插件系统与自进化智能体框架可以在不重启进程的前提下安全地热插拔功能组件。
与已有工作不同的是，关键缺口在于：效应系统与余效应系统虽然恰好形式化了『修改环境』与『依赖环境』这两个方向，但它们都是静态工具——效应在词法固定的作用域内被追踪、由编译期 handler 消解，余效应标注在执行前确定的上下文上验证；没有任何固定词法作用域能圈住部署后才加载的插件，也没有编译期上下文能预知运行时配置才会产生的依赖。作者的转向是：与其给静态类型系统追加更多标注，不如把效应与余效应的概念结构具体化（reify）为运行时可直接操作的一等实体，让运行时动态建立这些系统静态提供的保证。此外，作者用观测等价把『恢复』从逐位相等弱化为行为不可区分，把跨组件独立性化归为每个键上的交换性见证，使交错效应的全局保证变得可证——这与 DSU 的前向状态迁移、OSGi 的回调式清理、React hooks 的非组合 cleanup 在方法论上有本质分野。
核心方法
直觉上整个范式可压缩成两句话：每个副作用都随身携带撤销自己的逆操作，每条依赖都被声明并被人监视。技术路线上，论文先把任意非纯函数 $f: \Gamma \times X \to \Gamma \times Y$ 的副作用抽象为上下文变换 $\Gamma \to \Gamma$，再定义效应函数 $\mathcal{E}_\Gamma \equiv \Gamma \to \Gamma \times (\Gamma \to \Gamma)$：应用于当前上下文 $\gamma$ 时返回新状态 $\delta$ 与逆函数 $g$，见证条件要求 $g(\delta) = \gamma$，即逆操作只需在施加它的那个状态处成立。运行时把状态包装成效应上下文 $\partial\Gamma \equiv \Gamma \times (\Gamma \to \Gamma)$，其中累积子 $\varphi$ 以扭对称合成 $(f_1,g_1) \circ (f_2,g_2) \equiv (f_1 \circ f_2,\ g_2 \circ g_1)$ 按 LIFO 顺序收集所有逆函数，recover 执行 $(\gamma,\varphi) \mapsto (\varphi(\gamma), \mathrm{id}_\Gamma)$ 完成恢复。加载序列被读作效应迭代器 $\mathfrak{I}_\Gamma = \mu\mathfrak{I}.\ \Gamma \to \Gamma \times (\Gamma \to \Gamma) \times \mathsf{Maybe}(\mathfrak{I})$，即具体化的界定续延，直接映射到主流语言的 yield/生成器。空间一侧，余效应上下文 $\Sigma \equiv (k: K) \rightharpoonup \mathcal{V}_k$ 是键到带类型值的有限部分函数表，满足性谓词 $\sigma \models d \equiv \forall k \in d.\ k \in \mathrm{dom}(\sigma)$ 可判定，每次上下文变更被对照组件声明分类为 activating/deactivating/neutral 以驱动生命周期。二者统一进递归上下文类型 $\Gamma^\infty \equiv \mu\Gamma.\ \Gamma \times (\Gamma \to \Gamma) \times \Sigma$，每个键携带值类型与操作集并由提供者见证交换性，最终在第 4 节收束为组件三元组与 9 条规则的操作演算。
核心创新有三层。其一，可逆效应把『撤销』从开发者的义务变成类型结构：与代数效应 handler 用解释器消解效应、与 OSGi/VSCode 把清理写进独立的 unload 回调不同，这里每个效应返回的逆函数由见证 $g(\delta)=\gamma$ 绑定到施加点状态，效应合成算子 $\diamond$ 保持见证，于是复合效应的逆自动由逆函数复合得到——React 的 useEffect 虽也有结构性配对，但 hook 不能在条件/循环/嵌套函数中调用、不能异步、不能组合成更大的效应，而这里的效应是自由可组合的普通操作，组装已有效应时甚至完全不用手写逆。其二，响应式余效应用目标视图与已承诺视图的逐项比较驱动生命周期：$\omega_n$ 记录激活时每个声明键解析到的提供者 fiber，$\mathrm{target}_n(\gamma)$ 重算当前应然解析，二者不一致即触发 L-Divert/L-Leave 去激活——依赖被更换提供者与依赖消失走同一条路，且承诺记录的是提供者身份而非值，避免等值替换被误判。其三，上下文范式通过观测等价 $\simeq$ 把独立性变成接口性质：物理状态不可逐位还原，但只要每个键的操作集相互交换（由提供者在定义处见证，设计手法如每条注册占据独立表项、CRDT 的唯一标签、CompCert 式的句柄重命名），不同组件的效应即可任意交错而互不干扰；合流性定理进一步保证『动态历史无痕』——系统静止态等于把最终配置从头静态装载一次的结果。
方法步骤详情
完整步骤如下。第一步，效应建模：副作用表示为见证效应函数 $e \in \mathcal{E}^*_\Gamma$，返回 $(\delta, g)$ 并满足 $g(\delta)=\gamma$；track 把 $(f,g)$ 提升为 $(\gamma,\varphi) \mapsto (f(\gamma), \varphi \circ g)$，recover 执行 $(\gamma,\varphi) \mapsto (\varphi(\gamma), \mathrm{id}_\Gamma)$，声音不变量 $\varphi(\gamma)=\gamma_0$ 保证任意带见证的交错序列后恢复仍回到初态（定理 7、16）。第二步，加载序列化为效应迭代器，每次迭代产出（新状态、逆函数、续延），转换可在任意迭代边界被 L-Divert 中断，实现转换中途的部分回滚。第三步，余效应上下文 $\Sigma$ 上 get/set 均为 $\mathcal{E}^*_\Sigma$ 型效应：set 返回的逆即注销绑定，满足性变化经 notify 分类后由 refresh 重算 fiber 的目标视图。第四步，隔离与拦截：$\Sigma_{iso} \equiv (K \rightharpoonup R) \times ((r: R) \rightharpoonup \mathcal{V}_r)$ 用两层映射 $k \to \rho(k) \to \sigma(\rho(k))$ 实现运行时特设多态（同一键在不同上下文解析到不同绑定），$\Sigma_{inter}$ 用元数据幺半群 $(\mathcal{M}_k, \oplus_k, \epsilon_k)$ 在访问点合并上下文携带与组件声明的元数据（右偏，环境可覆盖组件）。第五步，统一上下文 $\Gamma^\infty$ 中每个键携带 $(\mathcal{V}_k, \mathcal{A}_k)$ 与交换性见证（定义 46），上下文中介迭代器（定义 30/56）限定效应函数只能由操作、提供、实例化三类阶段构成，由此推出受限性（写不出声明之外的绑定、读不到控制字段）。第六步，演算：组件 $(d, p, e) \in \mathfrak{C}_\Gamma$（声明、提供、见证效应函数）实例化为 fiber $\langle d, p, e, \pi, \sigma, \tau, \theta \rangle$，四态生命周期由 O-Insert/O-Retire/O-Remove 三条编排规则与 L-Begin/L-Iter/L-Finish/L-Divert/L-Leave/L-Unload 六条生命周期规则驱动；L-Unload 以 $\neg\,\mathrm{relied}_n(\gamma)$ 为守卫——提供者必须等所有承诺视图解析到它的消费者去激活完毕才撤出绑定，而 $\sigma_\gamma$ 只对 Active fiber 取并，保证守卫不会死锁。第七步，元理论：证明保持性（定理 64）、恢复精确性（定理 68、推论 69）、排序（定理 70）、解析一致性（定理 71）、活性（定理 73，$S(n) \le (K+3)(V(n)+1)$）与合流性（定理 80）。第八步，TypeScript 实现 Cordis：10 个算法落地全部构造，加载器在其上做声明式配置调和与三阶段热模块替换。
技术新颖性
技术新颖性体现在四方面。第一，这是首个把效应/余效应这对静态类型论概念整体提升为运行时机制的系统性工作：与 ZIO、Effect-TS 等单子式库要求程序写在效应类型内部不同，Cordis 是覆盖普通宿主代码的覆盖层，效应追踪不改变代码的写法；与 Effekt 把效应类型重释为词法作用域内的二等能力不同，这里的能力（余效应）是一等的、跨作用域运行时解析的。第二，见证式逆函数的精度设计：逆操作只被要求在施加点状态成立而非满足全局一致逆 $g \circ f = \mathrm{id}_\Gamma$，且允许每状态选取不同逆函数，显著放宽了可逆性要求；定理 15 还精确刻画了均匀逆在提升一层（$\partial\Gamma \to \partial^2\Gamma$）时何时完全恢复累积子。第三，把 scalable commutativity rule 的方法论移植到组件系统：交换性不再是内部状态相等而是『任何测试不可区分』，于是 POSIX 的 open 强制返回最小描述符导致不交换、mmap/creat 可交换这类系统设计经验变成每个键的接口设计准则，且证明义务（定义 46 的交换性见证）落在提供键的一方而非消费方。第四，元理论的完备链条：恢复精确性（运行累积子恰好抹去该 fiber 自己的贡献）、排序（提供者的 episode 严格包含消费者的 episode）、解析一致性（转换中承诺视图不漂移）、活性与合流性共同构成的全局保证，在动态组合文献中没有先例——DSU 关注前向状态迁移、OSGi 缺少异步卸载协议、FRP 的反应性停在值粒度而非组件生命周期粒度。
实验结果
本文的『实验结果』是元理论定理链与一个生产级案例研究。理论侧：定理 5/10/13 证明 track 与 effect 都是幺半群同态，逐个追踪与整体追踪一致；定理 7 确立声音不变量 $\varphi(\gamma)=\gamma_0$，任何带见证的效应序列之后 recover 都回到初始状态；定理 16 证明按施加逆序回滚时每个逆恰好拿到自己施加时产生的状态；定理 43 证明在两两独立条件下 $n$ 个效应的逆按 $\{1,\dots,n\}$ 的任意排列施加都能回到 $\gamma_0$——这是『卸载单个组件无需其它组件排队等待』的关键。演算侧：定理 64（保持性）证明 9 条规则保持注册表良构；定理 68 与推论 69（恢复精确性）证明在一个 fiber 的 episode 内运行其累积子后，状态与『中间所有外部步骤照常发生而该 fiber 从未启动』的情形 $\simeq_K$ 等价，且卸载后该 fiber 的表为空使 O-Remove 无需额外检查；定理 70（排序）证明 $b < b'$ 且 $u' < u$，即消费者的整个 episode 严格嵌套在提供者的 episode 内，提供者必然活得比消费者久；定理 71 证明每次转换的所有迭代都对着同一个承诺视图运行；定理 73（活性）在 $\prec$ 无环、迭代长度 $\le K$、fiber 名集合有限的前提下证明无死锁与终止界 $S(n) \le (K+3)(V(n)+1)$；定理 80（合流性）证明任意调度序列的静止态在 $\simeq$ 与名字重命名意义下唯一，等于按依赖序一次性静态装载的规范形，即『动态历史无痕』。实现侧：Koishi 案例研究显示该模型支撑了一个 4000 多个社区插件、历经四年开发的生产级聊天机器人框架，且同一模型复用于服务器端与浏览器端两个独立运行时；HMR 引擎的三阶段（不动点模块分类、陈旧条目检测、事务性重载）做到了 webpack/Vite 做不到的事——无需开发者标注 accept 边界即可在保存时重应用被编辑的插件，且任一模块导入失败时整体回滚、系统绝不处于半重载状态。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 组件卸载恢复 | 恢复精确性（定理68/推论69） | 卸载后状态与『该组件从未激活、其余步骤照常』的状态 $\simeq_K$ 等价 | VSCode Top100 扩展中 87 个含可执行代码，移除需重启整个 extension host | 免重启、就地完整撤销副作用，清理由抽象保证而非作者自觉 |
| 依赖撤出顺序 | 排序性质（定理70） | 消费者 episode $[b',u']$ 严格嵌套于提供者 episode $[b,u]$（$b<b'$ 且 $u'<u$） | OSGi/iPOJO 依赖手写同步卸载回调，无协议可等待异步清理 | 结构化保证提供者晚于消费者消失，且拆卸期间依赖仍可读 |
| 调度无关收敛 | 合流性（定理80） | 任意生命周期步序列的静止态等于按依赖序静态装载一次的规范形（up to $\simeq$ 与重命名） | DSU/HMR 需手写迁移函数且无调度无关的等价保证 | 动态历史无痕，可按静态方式推理运行中的系统 |
| 系统活性 | 无死锁与终止界（定理73） | $S(n) \le (K+3)(V(n)+1)$，一切极大序列终止于静止态 | 守卫式撤销（等待依赖方先退出）通常存在死锁风险 | 在可判定前提（$\prec$ 无环、迭代长度有界）下给出终止证明 |
| 生产生态验证 | 插件规模与运行年限 | Koishi：4000+ 社区插件、4 年开发、服务器端与浏览器端双运行时 | — | 存在性-采用性证据（作者自评为观察性结果而非定量对照） |
局限与改进
作者承认的局限：案例研究证据来自单一生态（Koishi）与单一宿主语言（TypeScript），无法把范式的优点与其 TypeScript 实现、聊天机器人领域特性分开；研究属观察性而非对照实验，只能算存在性-采用性结果，抽象的运行开销与对开发效率的量化影响留作未来工作。边界问题：恢复保证只覆盖系统边界内的位置，发射类副作用——已发出的网络包、已写入外部的字节——本质上不可逆，只能靠推迟提交或补偿动作，而补偿的交换性要对照比 $\simeq$ 更粗的等价关系重新证明。我自己的观察：其一，两个见证条件（逆函数真的可逆、键上操作真的交换）运行时并不检查，完全依赖组件作者自觉，与论文批评的 deactivate 回调存在同类的信任缺口，只是义务被局部化到了单个效应与单个键；其二，终止定理假设依赖关系 $\prec$ 无环且 fiber 名集合有限，相互依赖虽可静态报告，但推荐的分解方案会让集成组件数随组件数 $n$ 平方增长，损害开发者体验；其三，演算在单一 realm 中工作，多提供者要靠 realm 或 service broker 绕行，realm 运行时重搬移（Algorithm 7）逻辑相当精巧复杂；其四，失败 fiber 被排除在合流性之外，重试语义（revision）比较粗糙；其五，Proxy 逐属性拦截、每效应闭包分配、每次 set 触发的全 fiber notify 扫描没有任何性能测量；其六，依赖链接是纯名义的键等价，接口漂移与键碰撞问题只给出三个方向（命名空间、peer dependency、结构兼容）而未解决。
独立分析的弱点
独立分析的弱点：第一，正确性义务错位风险——见证 $g(\delta)=\gamma$ 与键交换性由作者人工保证而无机械检查，一个写错的逆函数（如忘记释放嵌套资源）会静默破坏定理 68 的前提，最终违背论文自己的核心承诺；改进方向是仿照 Kim 与 Rinard 对集合/映射数据结构的做法，用证明助手机械验证每个操作的逆与交换条件，或设计语言级效应 DSL 让逆从操作的类型自动导出。第二，运行时开销未量化——ctx.effect 每次分配闭包、属性访问全走 Proxy get trap、set 每次触发全 fiber 扫描的 notify，在每秒数千次事件的高频场景可能成为瓶颈；应提供微基准与剖析数据，并设计批量/降级通知模式。第三，状态不前传——重载组件时其内存状态被丢弃后从零重建，长会话状态（已建立的连接、缓存的模型）必须外移到更长命的依赖中；论文承认与 DSU 的前向迁移互补、二者分层是未来工作。第四，卸载风暴——依赖链很深时，撤销根提供者会级联去激活整棵子树，guard 逐层等待可能造成长尾延迟；可探索对无交集子树并行去激活、重叠调度。第五，生态治理缺位——名义键链接使接口漂移与键碰撞在开放生态中真实存在，npm peer dependency 依赖语义化版本的自觉约定且单版本解析阻断多版本共存；对一个以『开放生态依赖协调』为卖点的系统，这是工程上最薄弱的一环。第六，形式化未机器化——81 个编号条目的证明全部人工书写，合流性这类冗长论证值得 Coq/Lean 化以排除疏漏。
未来方向
作者提出的方向：把 Cordis 应用于自进化智能体框架——在持续、少人监督的组件自替换下验证时间保证（快速替换下的完整恢复）与空间保证（频繁拓扑变化下的依赖协调），这是超越人工维护插件生态的下一个验证场；与语言共生设计——让上下文成为语言的隐式构造（同时获得人机工学与安全收益：组件无法经闭包或全局变量误触另一组件的上下文），效应迭代器编译为单一状态机，余效应规格进入类型系统使循环依赖在编译期报告、依赖可按类型结构比较；与操作系统共生设计——OS 把内存、文件描述符等资源作为余效应提供并统一记录归属，事务性存储或写时复制文件系统可把发射类操作也变为可逆。基于成果可延伸的方向：用 Coq/Lean 机械化演算与全部元定理；把合流性从状态扩展到可观测副作用流（论文明确指出定理 80 只谈状态不谈 emissions）；为跨进程/分布式上下文形式化一致性语义（6.2 节的 cross-process broker 目前只有非形式化讨论）；统一值级反应性（signals/FRP）与组件级余效应反应性，7.4 节已指出二者互补；以及把结构兼容性谓词（行类型/子类型）纳入依赖解析，从根上解决接口漂移与键碰撞的版本化问题。
复现评估
复现条件评估：理论部分完全自包含——9 条规则、全部定义与证明都在论文正文（共 81 个共享计数的定义/引理/定理条目加 10 个算法），数学工具限于基础类型论、幺半群与轨道式的不动点论证，具备 PL 基础的研究生可以通读；但要完整验证含合流性在内的冗长证明建议借助证明助手，工作量在数周到数月。实现部分：Cordis 以 TypeScript 实现，文中给出 10 个算法的完整伪代码与理论-实现对应表（Table 2），核心库可据 Algorithm 1-6 独立重实现；需注意 Koishi 生产环境用的是 Cordis v3，论文呈现的是精炼了效应/余效应语义并重设计加载器的 v4，文中未给出 v4 的开源仓库链接，但 Cordis v3 与 Koishi 均为公开开源项目可作参考。案例数据可复现：VSCode 统计来自 2026 年 6 月 9 日的 Marketplace 抓取（Top 100 中 87 个含可执行代码、仅 7 个声明非内置依赖），Koishi 的 4000+ 插件生态公开可查。算力需求几乎为零（纯软件系统，无模型训练）。总体难度估计：实现最小核心（effect 跟踪 + 四态生命周期状态机）约一到两周；完整实现加载器、HMR 与隔离/拦截约一到两个月；向其它语言移植需按 6.4 节检查前提——闭包、运行时可驱逐的模块注册表（或 dlopen/dlclose）、透明的访问拦截原语（Proxy/描述符协议/宏）。
论文图表
execute 驱动效应迭代器：每步从迭代器取逆函数并以 $inverse \leftarrow value \circ inverse$ 前插合成（LIFO 恢复序），每步前检查守卫，守卫失效即停止迭代只保留已累积的逆。effect 包装器增加 armed 自弃标志（恢复至多触发一次）与父组合 $ctx.dispose \leftarrow dispose \circ ctx.dispose$，即 $\partial^2\Gamma$ 递归结构的工程形态。
这是全系统唯一的上下文变异原语：可逆效应理论（$\partial\Gamma$、累积子）到代码的第一次落地，其余一切操作都归约为它。
get 经 $ ho(k) \to \sigma( ho(k))$ 两层解析读取隔离绑定；set 把值写入 store、调用 notify 传播变更、返回执行删除并再次 notify 的逆函数，整体经 ctx.effect 注册从而自动获得跟踪与恢复。
展示了『余效应操作本身是可逆效应』这一协同设计的具体代码形态，也是反应式通知链路的起点。
notify 遍历所有存活 fiber，检查变更键是否在其 inject 声明中且解析到同一 realm 符号，命中则调用 refresh 重算该 fiber 的目标视图并收集受影响者供调用方等待。
这是定义 22 三分类（activating/deactivating/neutral）的运行时实现，是『依赖变化驱动生命周期』这一空间可组合性承诺的直接机制。
ctx.use 把组件与 config 绑定成 fiber：callback 作为父 fiber 中被跟踪的效应执行时调用 refresh 启动子生命周期，其返回的闭包把子 fiber 目标置为 $ot$ 并触发 unload——即定义 52 的实例化原语，父组件卸载由此自动级联到子组件。
说明组件实例化本身也是普通可逆效应，层级化组合因此完全不出演算的管辖范围。
refresh 比较目标视图决定发起 reload 或 unload 任务（惯性状态机入口，第 10 行先标 UNLOADING 停止提供服务）；reload 在第 14 行提交承诺视图、执行 apply、完成后校验目标是否漂移，未漂移则转 ACTIVE 并 notify，漂移则链入 unload；unload 第 25 行先等待所有被通知的依赖方到达 INACTIVE（guard），再执行 dispose，最后按目标视图回到 INACTIVE 或链入 reload。
三行关键代码（第 14/10/25 行）恰好承载定理 70 的余效应排序：承诺视图先建后撤、先停止服务再调度逆函数、先排空依赖方再恢复。
resolve 沿 fiber 链上行：第一个承诺视图中含该键的 fiber 授权访问并返回绑定；声明了该键但尚未承诺则抛 INACTIVE_ACCESS；走到根仍未声明则抛 UNDECLARED_ACCESS。
展示依赖声明如何兼作能力式访问控制：未声明即不可访问；且读取承诺视图而非 store，正是『拆卸中的组件仍可读其依赖』这一排序保证的实现点。
patch_isolation 对每个发生 realm 变更的键写入新分隔符标签，用 $\gamma'[\delta_k] = d_1$ 判定『该上下文派生自 entry 的上下文』（式 64），据此决定绑定是否随 entry 迁移到新的 realm 符号，最后以受影响者谓词调用 notify 通知依赖方。
隔离 realm 的运行时搬移是论文中最精巧的工程问题：单一符号可能被多个 fiber 共享而提供者只有一个，分隔符技巧是解开这一歧义的关键。
以变更文件集 stashed 为种子、externals 为拒绝边界做不动点迭代：某模块只要有一个 import 被接受则接受，所有 import 均被拒绝则拒绝，处于导入环中悬而未决的模块默认拒绝。
HMR 第一阶段：用依赖子图的分类决定哪些改动可以热替换、哪些必须触发完全重启。
对每个组件条目用 get_dependencies 沿导入树遍历（以 declined 为边界收集传递导入），树与 accepted 相交则该条目陈旧，并把整棵树并入 accepted 供下一阶段统一失效。
把模块级变更精确映射到组件级重载单元，决定 HMR 的影响面，避免不必要的大范围重载。
失效已接受模块的缓存并备份，逐个陈旧条目 dispose 旧 fiber、以新模块重建；任何导入失败（如语法错误）则恢复缓存备份、从 backup[entry.url] 重建全部已更换条目并抛出错误——保证系统绝不处于半重载状态。
事务性回滚是可逆效应思想在模块级的又一次体现，也是 Cordis HMR 与 webpack/Vite HMR 的本质差异所在。