Cordis：面向时空可组合性的编程范式（技术报告 2026）
原题：A Programming Paradigm for Spatiotemporal Composability
一句话总结：Cordis 把动态组件的两类困难分别归结为“卸载时能否完整撤销副作用”和“依赖变化时能否自动重连”，用运行时跟踪的可撤销效应（revertible effect）与反应式协效应（reactive coeffect）统一处理；论文给出组合演算与元理论，并以超过 4000 个社区插件的 Koishi 证明可落地，但没有性能对照实验，而外部代码证据表明 DeepSeek Harness 已把这一框架用于其全插件化智能体运行时。
问题与动机
传统组合通常在编译期确定函数调用、模块导入和继承关系，插件系统与自演化智能体脚手架却要在进程运行期间装载、卸载和替换组件。现有系统常把问题推给进程重启或容器编排：前者会丢弃进程内缓存、连接和未完成计算，后者只能管理服务级依赖，不能表达同一地址空间内的细粒度组件关系（§1.2）。
论文把动态组合拆成两个正交维度。**时间可组合性（temporal composability）**要求卸载组件时完整撤销它对共享环境的修改；**空间可组合性（spatial composability）**要求组件声明依赖，并在提供者出现、消失或被替换时自动调整生命周期。作者认为，经典效应系统描述“计算如何改变环境”，协效应系统描述“计算需要什么环境”，但两者通常是词法作用域内的静态分析，无法直接覆盖运行时变化的组件集合。
这一问题与智能体系统直接相关：工具、沙箱、记忆、会话状态、子智能体和编排策略都可能成为可替换组件。若修改失败后只能重启整个 harness，长任务会失去进程内状态；若依赖关系靠各模块临时探测，替换工具或状态服务可能留下失效引用。不过，这部分在论文中主要是动机，不是受控评测。
关键观察 / 隐含假设
- 观察 1：副作用撤销与依赖重连是不同问题。 撤销要求记录组件做过什么，重连要求知道组件依赖什么；只提供卸载回调或依赖注入均只能覆盖一侧（§1.1、§2.3）。
- 依赖假设：组件之间的重要交互都能通过统一上下文表达；绕过上下文的全局变量、原生句柄或直接外部写入不受保证。
- 可能失效场景：邮件发送、网络数据报、共享文件写入等越过系统边界的输出没有真正逆操作，只能延迟提交或补偿（§6.1）。
- 观察 2：撤销复合操作不必为整个组件手写卸载路径。 每个原子操作在执行时返回逆操作，运行时按后进先出顺序组合这些逆操作，便可从装载路径结构化地产生卸载路径（§3.1，定理 16）。
- 依赖假设：组件作者给出的逆操作确实能恢复该次操作；Cordis 实现并不在运行时验证这一见证条件（§5.1.1）。
- 观察 3：依赖变化应驱动组件状态机，而不只是改变一次查找结果。 提供者进入或离开活跃状态时，消费者需要停用、完成异步清理，再针对新提供者重新装载（§3.2、§5.1.3）。
- 依赖假设：依赖键及提供者身份足以表示兼容性；接口版本漂移、同名键冲突与行为契约并未由协效应模型解决（§6.6）。
- 观察 4：真实生态能展示可表达性，但不能替代性能与因果证据。 Koishi 在四年中形成超过 4000 个社区插件，服务端与浏览器控制台都建立在 Cordis 上；作者明确把它定位为存在性与采用证据，而非与替代架构的受控比较（§5.3）。
- 假设 1：跨组件效应具有足够的独立性。 全局时间可组合性要求不同组件的正向操作与逆操作可交换；论文通过按键隔离和观测等价给出充分条件，但有序中间件链、外部输出等非交换状态需要额外排序或留在系统边界之外（§3.3.2、§4.4.2）。
核心方法
可撤销效应把一次上下文变换表示为“新状态加逆函数”。ctx.effect(callback) 执行回调、收集它逐步返回的逆操作，并将逆操作组合到所属组件的累加器；组件卸载时按后进先出顺序执行。异步回调通过迭代边界检查撤销请求，使装载过程中途失效的组件先停止继续施加效应，再回滚已经完成的部分（§3.1、算法 1）。
反应式协效应把共享能力放在带键的上下文中。组件以 inject 声明所需键，提供者用 ctx.set 注册值；注册本身也是可撤销效应。键发生变化后，运行时重新计算受影响组件解析到的提供者身份，触发装载、卸载或保持不变。隔离（isolation）让同一个键在不同上下文解析到不同 realm，拦截（interception）则改变依赖的使用策略而不改变绑定本身（§3.2、算法 2–3）。
两者统一为一等上下文：共享状态和依赖都经上下文访问，效应累加器记录如何恢复它，协效应投影定义组件能观察到什么。论文用观测等价忽略不会被公开操作区分的物理差异，再证明不同键上的操作独立；组件内的非交换操作由累加器排序，组件间的顺序敏感关系由显式依赖排序（§3.3）。
组件在 Cordis 中实例化为 fiber。fiber 持有依赖规格、已提交的提供者视图、效应累加器、目标状态和在途异步转换。提供者准备卸载时先停止对外提供服务，通知并等待所有依赖者完成卸载，然后才撤销自身效应；这避免消费者的异步清理访问已经消失的依赖（§4.3、§5.1.3，算法 4–5）。
在核心机制之上，组件加载器把持久配置树协调成 fiber 树：按稳定编号增删、移动或更新条目，并对配置变化选择尽可能小的操作。热模块替换（Hot Module Replacement，HMR）先分类受影响模块，再找出陈旧组件，最后备份模块缓存并事务式替换 fiber；新模块导入失败时恢复旧缓存与旧组件（§5.2，算法 8–10）。
与 DeepSeek Harness 的关系（外部补充）
DeepSeek Harness 官方仓库明确称其由 Cordis 驱动，并采用“一切皆插件”的架构。其架构文档把模型适配器、工具注册表、会话日志和智能体循环都实现为可由配置替换的 Cordis 插件；插件对服务、类型化事件和可撤销效应的贡献汇入共享上下文，卸载时撤销注册。
这不是普通的间接依赖。vendor 清单显示仓库固定并重新命名发布 Cordis 4.0.0-rc.7 的源码副本，同时维护生命周期加固、事务式配置协调和精确 HMR 等 18 组本地修改。由此可以把 DeepSeek Harness 视为 Cordis 在智能体运行时中的直接工程实例：模型、工具、沙箱、持久会话、压缩、子智能体、工作流和自修改能力都落在同一插件树上。
但证据边界必须保留。DeepSeek Harness 官方仍标记为 developer preview，并明确预告破坏性兼容变更；本文 §5 的正式案例和采用证据来自 Koishi，结论又把自演化 harness 写成未来验证方向。因此，外部仓库证明“已经采用并持续改造”，不能替代本文没有提供的 DeepSeek Harness 性能、恢复正确性或生产可用性实验。
设计取舍
- 以运行时纪律换语言无关性：Cordis 可作为 TypeScript 库叠加在现有系统上，不要求新语言或编译器；代价是组件可能持有别的上下文或绕过代理，静态类型也无法证明逆操作正确（§5.1.4、§6.7）。
- 撤销而非状态迁移：替换组件时先撤销旧组件的效应，再从干净状态应用新组件，不需要为每个版本对手写迁移；组件私有内存不会自动跨版本保留，必须移入更长寿命的依赖（§7.3）。
- 细粒度组件换组合能力：拆开双向依赖可以消除环，但最坏会引入二次方数量的集成组件，增加命名、配置和理解成本（§6.5）。
- 应用内组合换有限隔离：依赖声明与拦截能约束经上下文访问的能力，却不能阻止恶意代码直接访问宿主运行时；不可信插件仍需进程、WebAssembly 或容器沙箱（§6.3）。
- 边界条件：结论依赖上下文中效应的可逆性、跨组件操作的独立性和无环依赖；外部不可逆输出、共享可变状态、版本不兼容接口与恶意组件均需要额外机制。
实验与结果
- 本文没有受控性能实验、微基准或消融实验；其主要证据是形式化定义、定理和工程案例，因此 frontmatter 标记
empirical_evidence: none。 - 元理论覆盖保持性、全局时间与空间可组合性、进展性和合流性；这些结论在成对独立、有限组件、良构注册表等前提下成立（§4.4，定理 59、61、63、66、73）。
- Koishi 案例覆盖四年发展、超过 4000 个社区插件，并报告插件可在不中断其余组件的情况下卸载或热替换；这是开放生态的采用证据，不是相对 VSCode、OSGi 或其他架构的定量比较（§5.3）。
- 作者没有测量 Cordis 的运行时开销、开发者生产率、故障恢复率或尾延迟，并将这些项目明确留作后续工作（§5.3）。
- 外部的 DeepSeek Harness 代码显示 Cordis 已承载完整智能体运行时的插件树，但仓库处于 developer preview，不能据此推断生产规模或稳定性。
论断—证据表
| 论断 | 证据 | 评测边界 | 置信度 |
|---|---|---|---|
| 原子逆操作可组合成组件级完整撤销 | §3.1，定理 16；§5.1.1 算法 1 | 逆操作正确，且所有相关效应均经上下文执行 | 强 |
| 依赖者会在提供者撤销前完成异步卸载 | §4.4.3，定理 63；§5.1.3 算法 5 | 良构、无环依赖；不覆盖跨边界不可逆输出 | 强 |
| 最终静止状态只由最终配置决定 | §4.4.5，定理 73；§5.2.1 | 成对独立、有限组件及论文定义的协调规则 | 强 |
| Cordis 足以支撑大型开放插件生态 | §5.3：Koishi 四年、超过 4000 个社区插件 | 单一 TypeScript 生态，无替代架构对照 | 中 |
| Cordis 已用于智能体 harness | DeepSeek Harness 官方 README、架构与 vendor 清单 | 外部代码证据；本文未评测该系统，且其处于 developer preview | 强 |
批判性分析
论证链条
论文的概念分解清楚：环境修改映射到效应，环境需求映射到协效应，统一上下文再把局部性质提升到交错组件系统。理论构造与实现 API 的对应也很紧，表 2 和算法 1–10 能逐项追踪定义如何落地。最强贡献是为动态卸载与依赖重连给出共同词汇和可检验前提，而不只是再造一个插件加载器。
链条的主要缺口在“理论条件是否由真实程序满足”。运行时不验证逆操作，跨组件独立性又依赖所有共享位置都被建模成键；因此形式证明把许多最容易出错的工作留给组件作者和接口设计者。论文证明“遵守范式会得到什么”，没有证明任意 Cordis 插件已经遵守范式。
假设压力测试
智能体工具常有数据库写入、工单提交、消息发送、支付和远程进程等外部副作用，它们恰好落在 Cordis 系统边界之外。自修改组件还会改变配置、磁盘代码和依赖版本；如果这些变更与运行时 fiber 的撤销日志不处于同一事务，卸载并不等于恢复。需要在 长程智能体可靠性 的故障模型下测量重启、网络分区、重复工具调用、模型升级和插件版本漂移。
DeepSeek Harness 对 vendored Cordis 的生命周期与事务协调加固也提供了反向信号：核心抽象可用，但实际 harness 的重入卸载、异步清理、配置写入和 HMR 失败路径比论文伪代码更复杂。这些修改应被视为设计压力测试材料，而非对原始实现正确性的自动背书。
实验可信度
形式部分给出明确前提和证明目标，证据强度高；实现部分提供算法和开源代码，便于复核。Koishi 的规模能证明抽象不是玩具，却只有一个宿主语言和应用领域，也没有故障注入、资源开销、维护成本或开发者对照研究。DeepSeek Harness 扩大了应用范围，但当前公开材料仍不能回答插件频繁替换时的恢复成功率、会话连续性或服务等级目标（Service-Level Objective，SLO）。
系统性缺陷
外部输出缺少统一的恰好一次或补偿协议；依赖只有名义键和包管理器版本约束；不可信插件缺少内建强隔离；组件环需要拆分而非运行时求解；HMR 不保存组件私有内存。论文也未量化上下文代理、通知扫描、fiber 状态机和逆操作闭包的内存与延迟成本。对智能体系统而言，还需统一 Cordis 组件生命周期与持久会话日志，否则进程重启后未必能重建正在撤销或重连的状态。
局限与后续工作
- 局限 1：完整恢复只覆盖系统边界内、经上下文执行且逆操作正确的效应；不可逆外部输出需要提交协议或补偿语义。
- 局限 2：Koishi 是单一 TypeScript 生态的观察性案例，DeepSeek Harness 是尚在快速迭代的外部采用实例，两者都没有提供受控性能比较。
- 局限 3：键身份不能表达接口版本和行为契约，独立开发的组件可能发生接口漂移或键冲突。
- 后续工作 1：在 DeepSeek Harness 上记录组件装载、替换、失败和恢复轨迹，注入进程崩溃、依赖消失与 HMR 导入失败，测量恢复成功率、重复外部副作用率、任务成功率和 P99 恢复时间。
- 后续工作 2：把 Cordis 效应累加器、配置事务与持久会话事件统一为可重放协议，明确进程重启发生在装载、卸载和依赖切换中间时的恢复点。
- 后续工作 3：比较 vendor 中的工程加固与论文算法，提炼可证明的重入卸载、事务式配置协调和跨版本兼容条件。
相关
- 相关概念：动态组合、可撤销效应、反应式协效应、长程智能体可靠性
- 同类系统：DeepSeek Harness、Koishi、OpenHands SDK、SkVM
- 相关主题：Agent-Systems