Cordis 时空可组合性：Shi, Zhang & Cui (2026)
把经典 effect / coeffect 体系提升为运行时机制，给动态组合（插件系统、自演化 agent harness）一个形式化基础。Yifan Shi、Wei Zhang（北京大学）+ Tianyi Cui（DeepSeek-AI）三人合作论文，88 页，提出时空可组合性 (spatiotemporal composability) 编程范式，并实现为 Cordis 元框架，已在 Koishi 聊天机器人框架（4000+ 社区插件）生产环境中验证。
核心问题
动态组合 (dynamic composition) 缺少形式化基础：组件在运行时加载、卸载、替换，静态语言学的 effect / coeffect 体系对"作用域"和"上下文"做了编译期假设，没法处理插件和自演化 agent 那种"作用域不固定"的场景。实践中大家用进程级时间可组合性 + 容器编排级空间可组合性这种粗粒度替代——代价是重启丢状态、依赖图要靠调度器推。
两个正交维度
| 维度 | 静态情形 | 动态情形 | 论文机制 |
|---|---|---|---|
| 时间可组合性 (temporal) | 词法作用域 / RAII / bracket | 组件卸载时所有 side-effect 必须可逆 | Revertible Effects：每个 effect 携带 inverse 函数，runtime 自动追踪并 LIFO 撤销 |
| 空间可组合性 (spatial) | 模块 import 解析 | 组件依赖可以出现、消失、改换身份 | Reactive Coeffects：组件声明依赖 specification，context 变化时 runtime 通知三态（激活 / 停用 / 中性） |
形式化核心
- Effect context \partial\Gamma := \Gamma \times (\Gamma \to \Gamma)——状态 + 累加器 (accumulator)；
track函数把"前向 + 逆"对折叠进累加器（Theorem 4-5，track是幺半群同态）。 - Coeffect context——键值表 \Sigma、specification d（Definition 25）与提供集合 p（Definition 43）、观测等价 \simeq_k（Definition 33） ；声明满足关系 \sigma \models d。
- Unified Context——一个类型同时承载 effect 与 coeffect（Definition 32）；coeffect 投影 \sigma_\gamma 提供 effect 独立性（Definition 19），Theorem 42 把"键上操作可交换"作为独立性条件。
- Component = (d, p, e)——依赖声明 + 提供声明 + 已观察 effect 函数。Fiber = \langle d, p, e, \pi, \sigma, \tau, \theta \rangle——组件的一个实例化，\theta 是生命周期状态（Inactive / Reloading / Active / Unloading）。
计算语义 (Section 4)
- Base calculus（Section 4.2）——五种规则 O-Insert / O-Retire / O-Remove / L-Reload / L-Unload，原子、即时、不会失败。
- Transitions in progress（Section 4.3）——拆 L-Unload 为 L-Leave + L-Unload，加
relied_n(γ)守卫，让被卸载者所有已激活的依赖者完成自己的 teardown 之后，才真正跑累加器——这避免了"pool 关闭时连接已归还给已消失的 provider"那种经典竞态。 - Metatheory（Section 4.4）——preservation、global temporal / spatial composability、progress、confluence（Theorem 73） 。任一调度顺序都能归到同一 quiescent state。
实现 (Section 5)
- Core library（5.1）——TypeScript 实现：
ctx.effect注册 effect+inverse，ctx.set/ctx.get读写 coeffect；ctx[key]通过 Proxy 做声明式访问，沿 fiber 链向上 walk（Algorithm 6），unloaded fiber 上的 inject 抛出INACTIVE_ACCESS。 - Component loader（5.2）——声明式配置 树，每条 entry 有 id / url / isolate / intercept / config / disabled；配置改动走增量 reconciliation，Theorem 73 保证最终 quiescent state 只取决于 final configuration。
- Hot Module Replacement（5.2.2）——三阶段：classify (stashed/externals 的传递闭包) → detect stale entries → transactional reload。Algorithm 10 失败时回滚到 backup，不会出现半 reload 状态。
案例：Koishi (5.3)
Koishi 是基于 Cordis v3 的开源聊天机器人框架，4000+ 社区插件。论文呈现的 Cordis v4 重新设计了 loader、细化了 effect / coeffect 语义。验证两件事：
- 表达力：所有 IM 适配器、数据库 driver、admin console 都跑在 Section 5.1 的原语之上；同套原语支撑了 Web Console（浏览器端 Cordis 应用）。
- 跨开放生态的空间可组合性：插件作者之间只通过 coeffect key 协调，无需彼此知晓；运行时切换数据库 backend 只触发依赖图上受影响的 fiber 重激活。
论文与 wiki 的联系
- 论文是 PL 形式化，不在 quant-wiki 的主范围内（CLAUDE.md scope 排除 "unrelated topics / general programming"），但它显式提到"self-evolving agent harness"作为主要用例——这对自演化 quant 策略系统（自动重写 factor 模块 / 插件式回测环境 / agent-trading harness）有直接借鉴价值。
- 因此本条目作为
asset_class: n/a的参考性summary 收录；具体迁移到 quant 语境的概念（如 effect inverse ⇒ strategy rollback、reactive coeffect ⇒ 因子依赖声明）作为 separate notes 单独整理。 - 与本 wiki 现有任何 quant 概念无直接可挂载节点——这是首次引入 PL 形式化主题，index 中以独立章节呈现。
关键贡献清单 (1.3)
- Revertible effects (Section 3.1)——每条 context 变换带显式 inverse，runtime 追踪。
- Reactive coeffects (Section 3.2)——声明式 specification + 变化时三态通知。
- Unified context type (Section 3.3)——effect context + coeffect context 合一为单一类型。
- Calculus of dynamic composition (Section 4)——组件形式化 + 生命周期操作语义 + 全局可组合性元理论。
- Cordis (Section 5)——元框架，含 core lib + declarative loader + HMR。
- Koishi case study (Section 5.3)——4000+ 插件、四年开发积累的生产环境案例研究。
局限与开放问题
- 元理论局限：共享 location 必须 reify 为 coeffect key，否则不在 Theorem 42 的覆盖范围内 （系统边界 Section 6.1）。
- 互依赖分解代价：n 个组件互依赖时 integrator 组件可能二次方增长，需要包打包 / 约定式 wiring / scaffold tooling 缓解。
- 依赖类型化与版本化（Section 6.6）——key namespacing / peer dependencies / structural compatibility 三种补法 ，论文未给出定论。
- Sandboxing 需 OS-level 边界（Section 6.3）——语言层 capability 不够，要 SFI / sandbox process / 容器。
- 威胁到有效性——证据来自单一生态系统 + 单一宿主语言 + 观察式而非对照实验；无性能/开发者效率基线。