时空可组合性的编程范式：让「插件」真正能被插拔

> 研读《A Programming Paradigm for Spatiotemporal Composability》 > ——Cordis 元框架，与一套把 effect / coeffect 运行时化的理论 > 作者：Yifan Shi、Wei Zhang（北京大学）、Tianyi Cui（北京大学 / DeepSeek-AI），八十八页

---

一句话

把经典的「效应」与「共效应」从类型系统的静态注解，提升为运行时的一等机制；二者合一为一「上下文类型」，遂成一编程范式——组件可于运行时自由插拔，卸载即彻底回滚其副作用，依赖生灭即自动重连。

---

缘起：卸载一个插件，为何如此之难

夫软件之「组合」，古来有三法：函数调用、模块导入、类继承。三者皆定于编译之时，行于运行之始，终身不变。然今之系统，渐求「动态组合」——组件可于运行间装载、卸载、重配。插件架构、自演化 Agent harness，皆是也。

然卸载一组件，其于共享环境所留之痕迹，如何尽数抹去？此非易事。

VS Code 之困

以 VS Code 为例。其扩展宿主（extension host）一进程，载百千扩展。扩展一旦 activate，纵使停用或卸载，亦须重启宿主——波及所有已载扩展。

盖因 VSCode 但提供 deactivate 钩子，仅为「优雅收尾」之回调，非「就地卸载」之机制；且钩子将「效应之创」与「效应之消」割裂，清理能否周全，全凭作者自觉。此即 locality of concern 之失。

更有一层：跨扩展依赖，VSCode 几无。top 100 扩展中，惟 7 个声明了对非内置扩展之依赖。何也？其扩展点（commands、views、language features）乃宿主所定之固定表面，扩展彼此鲜有相赖。纵有 extensionDependencies，所交之值 untyped（any），依赖者无从恃一可检之接口。

此困非 VSCode 所独有，插件系统皆然，惟程度异耳。

自演化 Agent harness：更迫切

今之 Agent harness，须于服务请求之同时，自改其组件——工具集、执行环境、权限沙箱、记忆系统、子 Agent 编排。每一次自改，皆一动态组合之实例。

若无时间可组合性，每次自改皆须全量重启，丢弃进程内累积之态（缓存、连接、半成之算），可用性随之受损；更险者，一次有误之自改，可令「赖以恢复之进程」自身瘫废。

若无空间可组合性，每模块须于依赖生灭、易主之际自行侦测适配，惟逞 ad hoc 之巧；而朴素之「代码替换」策略，或悄然折断依赖者，或引入环依赖，待重载方现。

粗粒度变通：代价不菲

或曰：操作系统与容器编排，岂非已供粗粒度之替代？然代价不菲。

• 时间上，每次重启弃尽进程内之态，重建耗秒乃至分；维持可用，须冗余副本，虚耗资源。
• 空间上，容器级编排不能表达同地址空间内组件间之依赖，且跨交互平添网络开销。

二者皆行于进程／容器之界，而今之系统，组合日趋于更细之粒度。粒度之不匹，正须一组合抽象，于组件自身之粒度上，管理效应与依赖。

---

两维：时间可组合性 与 空间可组合性

本文识得动态组合之两正交维度，恰与经典 effect / coeffect 系统相对：

维度	所问	经典所司	动态之所须
时间可组合性 Temporal	卸载时，其所改环境能否彻底、安全回滚？	effects（效应描述一计算如何改其环境）	长期有态、作用域非词法所囿之副作用，须可追踪、可复原
空间可组合性 Spatial	组件间之依赖，能否声明、解析、随变而协？	coeffects（共效应描述一计算如何倚其环境）	依赖于运行间生灭、易主，须响应式管理其拓扑

然经典 effect / coeffect 系统，皆静态之器：效应于词法固定之作用域内追踪，由编译时 handler 销；共效应注解，对照运行前既定之上下文而验。动态组合所须之保证，却行于运行间到来离去之组件、持续演化之上下文。

故本文之核心一手：不于静态类型系统上敷更多注解，而把 effect 与 coeffect 之概念结构「实体化」（reify），使运行时得直接操作之——此即经典理论所无、本文所立之动态保证。

---

可逆效应：每个变换，都随身奉上「逆」

时间可组合性者，装载与卸载组件于运行时，卸载则共享环境复归未组合前之态。其要：组件对环境之每一改动，皆可追踪、皆可复原。

故建模一 effect 为函数 Γ → Γ × (Γ → Γ)：施于当前上下文，不仅给出新上下文，更随身奉上「逆函数」。奉上逆，方得回退；交还逆于运行时，方得追踪。此谓可逆（revertible）。追踪并复合诸逆，则环境之完整复原，成结构之保证。

> 譬若拆乐高：每装一块，便记「此块当如何取下」。及至拆整座，依相反之序，逐块取下，城复归空台。所异者，乐高之序天定；而运行时诸组件交错，逆须在任意序下仍中各块之所改——此则须「独立性」。

效应上下文与累积器

定义效应上下文 ∂Γ ≔ Γ × (Γ → Γ)，记为 (γ, φ)。

• γ：当前上下文态。
• φ：累积器（accumulator），乃诸已施效应之逆之复合，亦即复原函数。

初态为 (γ₀, idΓ)。

trackΓ(f, g) 将一「前向 f + 候选逆 g」转成 ∂Γ 上之变换：施 f 于 γ，并将 g 复合入 φ。Theorem 5 证 trackΓ 为幺半群同态——追踪与复合，两不相妨。

recoverΓ(γ, φ) ≔ (φ(γ), idΓ)：以 φ 复原 γ，并将 φ 归零。

Theorem 7（soundness invariant）：recover 之前后，φ(γ) = γ₀ 恒成立。换言之，无论施几许效应，只要所奉之逆真为逆，复原总能归零至初态。

独立性 与 Corollary 21

多组件交错，一组件之逆或于「他组件效应已移其态」之后方行。此时该逆还能否只撤己之所改？

答曰：当两效应之「变换幺半群」彼此交换（Definition 19），则任取一序施其逆，皆可达 γ₀。此即 Corollary 21——独立性买得「任意序」，含交错多组件之序。

---

响应式共效应：依赖声明成规约，上下文一变即通知

空间可组合性者，组件能声明彼此之依赖，系统能于运行时解析、供给、撤回之。其要：依赖之满足，须于共享上下文每有变动时重估——依赖既足则激活，依赖既撤则停用。

故建模依赖为一「规约」（specification）。上下文每变，以此规约判之，别为三类：激活（activating）、停用（deactivating）、中性（neutral）。判之，则变易可知；应之，则激活停用由是驱动。此谓响应式（reactive）。

> 譬若租户与物业：组件声明「我须水、电、网」（coeffect specification）；物业（运行时）一有变动，即通知——通了便搬入（激活），断了便搬出（停用）。惟于满足其规约之态方入住，故永不强住一缺席之户。

共效应即效应，效应即可逆

共效应上下文 Σ ≔ (k:K) ⇀ 𝒱ₖ：一依赖键 k，配以特异之值类型 𝒱ₖ。get / set 操作，恰为效应函数（𝔈∗Σ）——是故共效应操作，本就是可逆效应！ 此即二者之 synergism：coeffect 操作即 effect，而 effect 可逆。set 一依赖、notify 一变动，自动追踪、自动复原。

隔离与拦截

• 隔离（isolation）：同键于不同上下文可解析为异值（isolate 引入 realm）。
• 拦截（interception）：于依赖访问处附以横切元数据（intercept 以 monoid 合并），不改其值而改其用。

二者皆「派生实现」（derived realization）：生一新上下文，旧表不动，故无需逆、无需追踪，复原惟弃派生者。

---

统一上下文 Γ∞：两机制合一，成一编程范式

效应载于上下文（carrier of effects），共效应亦载于上下文（carrier of coeffects）。二者合一，其状何如？

定义 Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ。三投影：

• 当前态；
• 累积器（复原此层效应）；
• 共效应上下文（载依赖）。

Σ 结构化并入——依赖操作（set/get）行于 Σ，其逆转由累积器追踪。且 Σ 之下值类型族 𝒱 无拘，凡系统须跨组件共享之态，皆可编码为一依赖，故 Σ 包举一切共享可变态，非惟组件间依赖。每组件与其环境之交互，皆过此一实体。

层级组合：插拔之字面隐喻

Γ∞ 之递归结构，支持层级控制——父上下文聚合诸子效应，成树形控制结构。

• 装载组件 = 行其效应（插）；
• 卸载组件 = 复原其效应（拔），不动其他运行中之组件；
• 不同层级之组件，可独立插拔；父上下文聚合管其子之一切效应，可任意嵌套组合。

观测等价 ≃：把「理想化之相等」拉回现实

复原之保证，第 3.1 节证为一「态之相等」，然此乃理想化——物理之态不可尽复（free 不复原 heap 之布局；生成之名不复原，盖下次创生另取新名）。

故相等须读作「观测等价」≃：两态不可区分，当无可观测者能辨之。各共效应自带其 ≃ₖ，上下文之关系，由诸 ≃ₖ 组装而成（Definition 33）。以此商去，方买得第 3.1.3 节所须之独立性。

范式之定位：兼函数式之可溯 与 命令式之 ergonomic

极	所长	所短
显式状态线程（函数式，如 State monad）	可组合保证强，效应显于类型	ergonomic 代价大，调用链每函数皆须携态参
隐式变更（命令式/OOP，如 React useEffect、Java service locator）	便捷	效应与依赖皆隐于隐式、散于码间，重构易碎

上下文范式兼二者之长：效应与共效应皆经一显式上下文参数中介，每操作皆可归责于其被唤起之上下文、其所属之组件。更进者——

• 可逆效应：作者惟奉每原子操作之逆，复合之逆自随组合而生——卸载即由装载推导，非另写于侧；
• 响应式共效应：作者惟声明所需依赖，运行时自动解析重连。

双向之中，原须仰赖作者自律之正确性，一变而为范式之结构属性。

---

动态组合演算 与 元理论

第 4 节将系统析为组件：每组件以「共效应规约 + 目击效应函数」配对。演算（calculus）赋其操作语义，并将时空可组合性由单组件推至整个交错组件之系统。

关键定理：

• Theorem 59（Preservation 保持）：良形注册表下，步骤保持系统不变量。
• Theorem 61（Recovery exactness 恢复精确性）：累积器所复原之态，精确等于初态（在 ≃ 下）。
• Corollary 62（Terminal recovery 终态恢复）：离去组件对终态之贡献为零。
• Theorem 63（Ordering 排序）：提供者撤回其绑定前，一切依赖者须先停用——此即空间之序，由声明式共效应所强加。
• Theorem 73（Confluence 收敛）：至一寂静（quiescent）态，诸合法步骤序列，经重排（依依赖序 ⊲ 线性化），皆达 ≃/≈ 相关之同一态。

> 是故无论编排器以何序增删组件、替换提供者、回退替换，系统终抵「若自始便写下该终组合」所应有之态。

此定理，许人以「静态组装」之心思推理一 Cordis 应用；亦划定保证之界：它所言者乃状态，非系统沿途之「排放」（emission）——此即第 6.1 节所辨「获取」（acquisition，边界内、被追踪）与「排放」（emission，跨界、行为如恒等）之分。

---

Cordis 实现：元框架之三层

Cordis 者，元框架（meta-framework） 也。与锁定特定域（Web 路由、ORM、UI）之应用框架异：其唯 supply 普适之动态组合语义，不负具体场景。三层：

1. 核心库（core library）：直实现 effect 与 coeffect 系统。 2. 组件加载器（component loader）：于核心之上，加配置调和（configuration reconciliation）与热模块替换（HMR）。 3. 应用框架（如 Koishi）：于前两层之上，建域特异之功能。

核心库之要

• Algorithm 1（effect 跟踪）：ctx.effect 为一切上下文变异之唯一原语。它将回调驱为「效应迭代器」，逐步折叠所奉之逆，成单一复合逆；以 LIFO 序复原。且自带「自我处置」（armed 标志，确保复原至多一次）与「父组合」（子效应之逆，本身即父之一效应——∂²Γ 之递归结构）。
• Algorithm 2 / 3（共效应操作）：ctx.set 即一 ctx.effect 调用，自动追踪复原；notify 将绑定变动，依各纤维之 inject 重估（激活／停用）。
• Algorithm 4 / 5（组件生命周期）：ctx.use 将组件实例化为 fiber；fiber 为一惯性状态机（inertial state machine）。reload 与 unload 皆「惯性」：一旦进入，必行至完成，方应目标态之变。reload 提交解析视图、行效应函数，毕则察目标态是否未变——未变则 ACTIVE，已变则链入 unload；unload 以 LIFO 复原诸追踪效应，然后 INACTIVE 或链回 reload。

三行承载 Theorem 63 之序：reload 于 Line 14 提交视图、unload 待诸逆尽行方弃之；refresh 于 Line 10 先标 UNLOADING（停止供给，依赖者先于其逆被排定前即重算）；unload 于 Line 25 待诸被通知之依赖皆抵 INACTIVE（L-Unload 之守卫）。

组件加载器：声明式配置 + 增量调和 + HMR

加载器以声明式配置树描述所欲之组合，将配置之变，译为对应之命令式 fiber 操作。调和（reconciliation）增量进行，非推倒重来——Theorem 73 许「寂静态唯系于终配置」、Theorem 66 许「系统必寂静」、Corollary 62 许「离去纤维之贡献为零」，故调和必成且影响局部。

HMR（Algorithm 8–10）：模块分类（accepted / declined 不动点）、陈旧条目检测（依赖树触及变更模块者）、事务性重载（缓存备份 + 失败回滚），无需如 Webpack / Vite 那般作者手注接受边界。

---

案例：Koishi，四千插件之生态

Koishi 者，建基于 Cordis 之开源聊天机器人框架也。四载之间，聚社区插件逾 4000，自即时通讯适配器、数据库驱动，至管理控制台、终端用户功能，无所不包。其规模与多样，足为生产环境验证。

其证三事：

一、元框架之表达力与普适性。 Koishi 服务端之每一功能，皆以 context 原语实现之插件；Koishi 自身惟供聊天机器人域之词汇。其 Web 控制台，乃第二独立 Cordis 应用，插件组合浏览器与 UI 之原语，非服务端者。足证模型（1）表达力足荷一完整生产系统；（2）普适——固定于 effect / coeffect 如何组合，而舍其义于各应用，故不预设特定域、特定运行时。

二、无认知开销之时间可组合性。 插件系统（第 1.2.1 节）卸载单扩展之效应，非重启宿主不能；Koishi 例行为之——控制台禁用一插件，其效应就地撤回；开发中 HMR 于存档之际重施已改插件，而存缓存态与别处活连接。Cordis 令此移除「非惟可能，且对插件作者毫不费力」——经上下文之效应既被追踪、其逆自随组合，纵生手作者，亦得有序清理，毋庸另写卸载路径。此即第 1.2.1 节所憾 locality of concern 之复得：原须仰各作者之勤，今由抽象一肩担之。

三、横跨开放生态之空间可组合性。 与第 1.2.1 节插件系统（互依赖几无）异，Koishi 生态呈真依赖拓扑——IM 适配器供各消息平台之访问，数据库驱动供持久存储，功能插件声明此等为共效应而取之。运行时重配一提供者（如换存储后端、重连适配器），惟重激其解析依赖已变之依赖者；依赖未具之插件，静待其至，不报错。此组合，行于独立撰写之码间——插件与其依赖，通常异人所作，所协惟连接其二者之共效应，故响应式共效应，于一开放贡献者生态中，维系组合之一致。

---

讨论中之真知（择要）

• 系统边界（6.1）：每效应皆携逆，而逆之分量，定于系统边界。内能独占修改并复原者在界内（追踪可逆）；否则在界外（行为如 idΓ，不追踪不复原）。边界按「位置」划，非按「媒介」。操作越界，通常两阶段：获取（acquisition，于界内装一记录，可逆效应）与排放（emission，经此通道推送数据，行为如 idΓ，跨界）。
• 服务多路复用（6.2）：共效应模型呼应 OSGi 之 service，而多出「服务代理」（service broker）——多提供者共存，代理分派请求；滚动更新（rolling update）由基础设施级操作，降为应用级组合模式。
• 访问控制与沙箱（6.3）：依赖访问机制（proxy 中介属性），本即 capability-based 访问控制的雏形——惟能取其所声明之依赖，未声明之取则报错。拦截机制，更可将细粒度策略（如文件系统依赖附「可读写哪些路径」之元数据）施于上下文，且不触发任何重载。
• 语言无关性（6.4）：上下文范式语言无关——时空两组合性，惟由其两维定义，故任何满足两端要求之语言皆可实现。时间上须闭包（逆须作为值捕获）；空间上须依赖声明与注入之机制（DI 问题）。TypeScript 之 Proxy、Python 之描述符协议，皆可中介访问。
• 相互依赖与粒度（6.5）：依赖环，惟令相关组件永 inactive——此状可由声明 alone 预言，运行时装载即报。多数表面互依，可析为更细组件以破环（如 server-core / access-control-core / request-mediation / policy-management），代价是组件数可随 n 二次增长，然不影响正确性、运行时性能（组件轻量）。
• 依赖类型与版本（6.6）：共效应模型惟按「键名」nominal 链接，无版本／结构链接，故生「接口漂移」与「键碰撞」二患。三策：键命名空间（最耦）、peer 依赖（Cordis 现采）、结构兼容（语言无关最难，类结构子类型，然行为契约难定、参数多态下不可判定）。统一模型，仍 open problem。
• 与语言／OS 协同设计（6.7）：语言可令上下文复隐（implicit）而保其语义；可使 effect / coeffect 为编译器所知（依赖环编译期报、结构兼容类型级支持）。OS 可供给沙箱、以共效应供其资源（内存、文件描述符之追踪复原，内核层已有先例），并使部分「惟可 withholding / compensation」之操作，变可真正可逆（事务性写入、copy-on-write 回滚）。

---

与相关工作之分野（择要）

• 经典 effect 系统（ZIO、Effect-TS、fp-ts）：以 monadic 嵌入买追踪，程序须写入效应类型内；要求由解释 discharged，服务既撤，其操作之留痕犹在。Cordis 以覆盖层（overlay）追踪普通宿主码之效应，且每效应配逆、随提供者来去重解析要求。
• 可逆效应语义（Heunen et al. 之 dagger arrows）：最接近——亦每效应配逆。然彼于指称、范畴设定中，可逆为全局属性（每计算皆可逆，逆为双侧），Cordis 于运行时追踪逆，所须更少——非全计算可逆，惟每原子效应须单侧逆，由调用者于施处奉上，复合之逆自随组合。
• 分级类型（Graded types, Granule）：于类型级统 effects（分级 monad）与 coeffects（分级 comonad）。Cordis 之贡献与之正交：举同一二概念，升为运行时机制，故能处动态组合。
• AOP（面向切面）：亦处「横切关注」之同一问题，然其 crosscutting 限于各组件所声明之共效应，reach 恰为其所声明之表面，故有确定性、可溯性；且跨切之变，载于组件效应，卸载即退、响应式传于依赖者——此动态组合模型内之一着，非 standalone 操作。

---

结语

本文举经典 effect / coeffect，升为运行时机制，立动态组合之形式基础。可逆效应，主局部时间可组合性；响应式共效应，主局部空间可组合性；二者统一为单一上下文类型，observational 等价供效应以独立性，遂成一编程范式。组件概念合此二者，成一动态组合演算，其元理论将时空可组合性，由单组件推至交错组件之全系统。Cordis 元框架实现之，Koishi 以 4000+ 插件证于生产。

夫本文之志，不止于人策之插件生态。其结语所瞩，乃自演化 Agent harness——AI 自主连续生成、替换其自身组件，而少人监。于此境中施 Cordis，可验「快速替换下完整复原」之时间保证，与「频繁拓扑变易下依赖协调」之空间保证。是可回收、可协调、连续自演化之基。

---

*参考：Shi Y., Zhang W., Cui T. 《A Programming Paradigm for Spatiotemporal Composability》. 北京大学 / DeepSeek-AI, 2026（八十八页）。案例 Koishi 现用 Cordis v3，本文呈 Cordis v4，核心组合模型两版共享。*