时空可组合性：让运行时组件可安全拆装的编程范式
A Programming Paradigm for Spatiotemporal Composability
- 发表日期
- 机构
- Peking University × DeepSeek-AI
- 作者
- 3 位
展开全部作者（3）
Yifan Shi · Wei Zhang · Tianyi Cui
2 维
时间 × 空间可组合性
6 项
核心形式化保证
10
生命周期操作规则
3 层
Cordis 实现架构
4,000+
Koishi 社区插件（论文口径）
87/100
VS Code 热卸载样本缺口
TL;DR · 60 秒速览
这篇论文到底说了什么
动态插件真正缺的不是一个 unload API，而是两种正交保证：组件移除后能撤销自己留下的状态（时间可组合性），依赖变化时能自动停用、重连和恢复（空间可组合性）。论文把 effect 与 coeffect 提升为运行时对象，以可逆副作用、反应式依赖和统一 Context 构造组件演算，并在 Cordis 中实现配置协调与事务式 HMR。形式化结果给出恢复精确性、依赖顺序、无死锁、终止与合流性，但保证有严格前提：共享状态必须经 Context 中介，逆操作要正确，依赖无环、独立操作可交换；网络发送和外部写入等不可撤销 emission 仍在系统边界之外。
摘要（编译）
现代软件从插件系统到可自我演化的 Agent harness，都需要在不中断进程的情况下动态组合组件。本文把这一需求拆为时间可组合性与空间可组合性：前者要求组件卸载时完整撤销副作用，后者要求组件声明依赖并随运行时上下文变化自动调整生命周期。作者提出 revertible effects 与 reactive coeffects，将二者统一到一等 Context，给出带 fiber、依赖解析和加载/卸载转换的组件演算及其元理论，并实现 TypeScript 元框架 Cordis。Cordis 的核心库、声明式加载器和热模块替换机制已支撑 Koishi 插件生态；论文同时明确，外部 emission、恶意代码隔离和实证性能评估不由该模型自动解决。
01 · The Problem
动态加载不等于动态组合：还要能撤销、能重连
插件被加载之后会注册命令、监听事件、打开连接、提供服务，也会依赖其他插件。传统框架往往只解决“把代码放进进程”，却把清理与依赖编排留给组件作者。结果是组件即使能被载入，也未必能在运行中安全移除；依赖一旦缺失或替换，消费者也不知道何时停用、何时恢复。
论文把问题拆成两个正交维度：时间可组合性要求组件移除后，系统回到仿佛它从未存在过的可观察状态；空间可组合性要求组件声明自己需要什么、提供什么，由运行时根据上下文变化驱动生命周期。只有两者同时成立，系统才可以在保持进程内状态和在途任务的同时重组。
作者用 VS Code 说明现实缺口：在 2026 年 6 月 9 日按安装量排名前 100 的扩展中，87 个包含可执行代码，移除时需要重启 Extension Host；只有 7 个声明了非内置 extensionDependencies。deactivate 更像宿主关闭钩子，而不是实时卸载语义。
- Temporal组件加载产生的每项副作用都要带逆操作，卸载时只撤回自己的贡献，保留其他组件与进程状态。
- Spatial组件声明 coeffect 依赖；服务出现、消失或换源时，运行时自动激活、停用或重载消费者。
- 粗粒度方案进程、容器和微服务可以隔离失败，却只能在服务粒度组合，并引入状态丢失、资源冗余与网络通信成本。
02 · Runtime Semantics
把 Effect 与 Coeffect 从类型注记变成运行时协议
经典语义里，effect 描述程序会对环境做什么，coeffect 描述程序需要环境提供什么；它们通常是静态、词法范围内的分析对象。本文的关键转向是把二者运行时化：effect 不再只是“发生了一个修改”，还必须携带恢复函数；coeffect 不再只是类型约束，而是一份可被 Context 持续检查的依赖规格。
这让 Context 从普通依赖注入容器升级为动态组合的控制平面。组件只能通过 Context 触碰系统状态；Context 记录逆操作、解析服务来源，并在解析结果变化时通知组件。加载与卸载、服务注册与撤销、依赖满足与失效因此落在同一套语义里。
Effect 回答“组件改变了什么”，Coeffect 回答“组件依赖什么”；运行时 Context 同时保存两者，才知道卸载时撤回什么、依赖变化时唤醒谁。
03 · Revertible Effects
副作用不是被禁止，而是必须自带逆操作
可逆 effect 把一次上下文变换写成“新状态 + 逆函数”。运行时通过 track 把逆函数累积到恢复器中；新 effect 的逆操作排在旧逆操作之前，因此卸载按 LIFO 顺序撤销。组件不再手写一套容易漂移的 dispose 流程，teardown 由加载时实际执行过的动作机械地导出。
论文进一步用 witnessed effect 允许逆函数依赖执行时看到的状态，并定义独立性：若两个组件的变换与 witness 在交换执行顺序后仍等价，就可以脱离全局栈、按组件单独卸载。运行时负责记录和调用逆操作，但不证明作者给出的逆操作真的正确；这是模型的契约，不是自动事务。
track(f, g)(γ, φ) = (f(γ), φ ∘ g) · recover(γ, φ) = (φ(γ), id)f 是正向变换，g 是其逆操作，φ 是当前累积的恢复器；逆操作以反序组合。
04 · Reactive Coeffects
依赖不是启动前检查，而是会随 Context 变化的信号
每个组件声明 coeffect 规格 d（需要哪些 key），激活后提供自己的 key 表。Context 比较变化前后的满足状态，并把通知分成 activating、deactivating 与 neutral：依赖从不满足变为满足就加载，从满足变为不满足就卸载；若 key 仍满足但 provider 改变，则针对新的解析结果重载。
依赖解析还支持两个重要扩展。isolation realm 让同一个 key 在不同 Context 分支解析到不同 provider，适合多租户或并行实例；interception 在不改变“是否满足”的前提下附加元数据与策略，可用于路由、配置与访问控制。组件只声明能力，不再持有全局单例。
- 声明消费者只写需要的 key 集合，避免把加载顺序、查找和重试逻辑散落在业务代码中。
- 解析Context 保存 key → provider 的 committed view，使组件整个激活 episode 使用一致的依赖来源。
- 通知provider 的增加、移除或替换只触发受影响的依赖者，不要求重启整个应用。
05 · Context Paradigm
统一 Context：以可观察等价代替字节级复原
论文用递归 Context 把当前状态、逆操作累积器和 coeffect 存储合在一起。Context 可以派生子 Context，形成与组件嵌套一致的树；子组件的 effect 归属自己的 fiber，服务解析则沿 realm 和拦截规则发生。它兼有函数式追踪能力与命令式 API 的工程手感。
这里的“恢复”是可观察等价，不是内存镜像回滚。释放后重新申请的对象可以有不同地址，重新注册的服务也可以得到新 ID；只要 coeffect 可见的行为等价即可。不同 key 默认独立，同一 key 上的共享操作则必须满足可交换性；未被建模为 key 的共享可变位置，不会凭空获得合流保证。
Γ∞ = μΓ. Γ × (Γ → Γ) × Σ递归 Context 同时包含当前上下文 Γ、恢复累积器 Γ → Γ，以及 coeffect 上下文 Σ。
06 · Component Calculus
从四态生命周期到恢复、顺序、进展与合流
组件可被多次实例化，每个实例称为 fiber，保存所需 coeffects、所提供服务、effect 迭代器、父 fiber、committed view 与生命周期状态。简单的 Inactive / Active 被细化为四态：Reloading 逐步安装 effect，Unloading 在依赖者退出后执行累积逆操作；L-Divert 与 L-Raise 处理依赖在加载中变化和执行失败。
这套演算最有价值的地方不是状态图本身，而是把工程直觉写成可检查的结论。下面六项是论文给出的主要保证；它们都不是无条件结论，后文的独立性、无环、有限性与 totality 假设必须同时阅读。
| 结果 | 编号 | 工程含义 |
|---|---|---|
| 恢复精确性 | Theorem 61 | 卸载一个 fiber 只撤回它自己的贡献，保留独立交错步骤 |
| 终态恢复 | Corollary 62 | 无论正常完成、转向或失败，关闭 episode 后均恢复其贡献 |
| 依赖顺序 | Theorem 63 | provider 先激活；consumer 完成退出后 provider 才撤销 |
| 解析一致性 | Theorem 64 | 一次加载针对同一 committed resolution，变化则安全转入回滚 |
| 进展与终止 | Theorem 66 | 在无环、有限和有界条件下无死锁，最终到达 quiescent state |
| 合流性 | Theorem 73 | 相同最终组件配置在独立调度下得到等价唯一正规形 |
07 · Cordis
理论如何落进 TypeScript：一个只负责组合语义的元框架
Cordis 不提供路由、ORM 或聊天机器人能力，而是作为 application framework 之下的 meta-framework，只处理动态组合。实现分三层：core library 直接实现 effect/coeffect；component loader 加入声明式配置协调与 HMR；Koishi 等应用框架在其上定义领域服务。
所有上下文变更都经过 ctx.effect(callback)，callback 返回或 yield 逆操作；ctx.get / set、isolate、intercept 对应 coeffect 操作。ctx.use 实例化 fiber，fiber.dispose 保存累积恢复器，fiber.committed 固定本次激活使用的 provider 视图。论文用 10 个伪代码算法把 effect tracking、通知、生命周期、代理访问、realm 切换和热重载串起来。
08 · Loader & HMR
声明式配置与事务式热重载：由最终状态驱动，而非堆命令
Cordis Loader 把配置树视为权威目标状态。每个条目声明 id、url、isolate、intercept、config 与 disabled；协调器对旧树和新树做增量比较，只插入、移除或更新受影响的 fiber。因为 calculus 已保证进展、依赖顺序和合流，配置操作不必人为维护一条脆弱的命令序列。
HMR 分三步：分类发生变化的模块并寻找可接受边界，定位依赖该模块的 stale 配置项，再执行事务式 reload。若新模块导入失败，Loader 恢复模块缓存并从备份重建全部 stale entries，避免应用停在半热更状态。这里的“事务”覆盖 Cordis 管理的模块与组件状态，仍不等于撤销已经跨系统边界发出的消息。
- Reconcile以配置树的最终形态为准，只重算变化路径；相同最终配置不依赖操作到达顺序。
- Dependencyprovider 替换时，只有解析结果变化的 consumer 退出并重新激活。
- Rollbackimport 或重载失败时恢复缓存和 stale entries，避免遗留部分加载的新版本。
09 · Case Study
Koishi 证明“能长期运行”，但没有证明“成本更低”
论文以开源聊天机器人框架 Koishi 为案例：其服务端机器人与 Web Console 是两个独立 Cordis 应用；四年间形成 4,000+ 社区插件。适配器、数据库驱动与功能插件组成依赖拓扑，插件可实时启停，缺少依赖的插件保持 Inactive，服务恢复后再激活；其他插件的缓存、连接与会话无需随宿主整体重启。
这是一份有分量的 existence proof：同一抽象能支撑两个不同应用和大规模插件生态。但论文没有受控性能实验、内存或延迟开销、故障率对比，也没有开发效率研究；案例使用的是 Cordis v3，而正文介绍 v4。它证明范式可实现且被采用，不证明相对传统框架更快或更省人。
- 外部效度案例集中于一个生态和一种宿主语言，跨 Web、桌面、Agent runtime 的泛化仍需验证。
- 版本差异生产案例基于 Cordis v3，论文形式化与实现描述面向 v4，二者并非完全同一系统。
- 缺失指标没有吞吐、延迟、内存、HMR 恢复时间或开发者生产力基线，无法量化抽象成本。
10 · Boundaries & Commentary
点评：它提供的是可组合协议，不是无条件的全局回滚
对插件系统和可自我修改的 Agent harness，这套范式比“出错就重启进程”更精细：它保留进程内记忆与在途任务，限制变化的爆炸半径，并让服务缺失成为正常生命周期状态。尤其在 Agent 能写入或替换自身工具时，自动记录 effect 与依赖拓扑也是恢复通道不被一次错误修改一起摧毁的基础。
但落地时应先画清系统边界。文件描述符、监听器和服务注册属于 acquisition，通常可以释放；已经发出的网络请求、写入外部数据库的记录和现实世界动作属于 emission，一般没有真正逆操作，只能采用延迟提交、幂等、补偿事务或外部协调。对不可信插件，Proxy 与 capability-like API 也替代不了进程、VM 或语言沙箱。
因此最准确的评价是：论文把动态组合从 API 习惯提升成了可证明的运行时语义，并给出可信的工程实现；它的上限则由中介覆盖率决定。只要组件还能绕过 Context 修改共享状态，或把不可撤销外部动作伪装成普通 effect，形式化保证就会在真实系统中断裂。
这篇论文最重要的工程判断，是把“能否安全卸载”从组件作者的自律，提升为 Context 可执行、演算可推理的协议。
- 逆操作契约每个 effect 的 inverse 必须正确；框架记录执行顺序，但无法自动证明补偿语义。
- 独立性交错组件需满足 effect/witness 独立，同一共享 key 的操作需可交换，否则只能依赖更严格顺序。
- 进展条件无死锁与终止要求依赖 precedence 无环、fiber 名称集合有限、effect 迭代长度有界。
- 合流条件Theorem 73 还要求无失败、组件对其 provision 为 total，以及相同 orchestration steps。
- 安全边界访问控制可由 coeffect 与 interception 表达；恶意代码隔离仍需宿主之外的安全机制。