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

f 装 拔 深度研究 · 论文精读 · 2026-08-21 时空可组合性的编程范式 让「插件」真正能被插拔 把经典的「效应」与「共效应」，从类型系统里的静态注解，提升为运行时的一等机制；二者合一为一「上下文类型」，遂成一编程范式——组件可于运行时自由插拔，卸载即彻底回滚其副作用，依赖生灭即自动重连。 原论文 A Programming Paradigm for Spatiotemporal Composability 作者 Yifan Shi · Wei Zhang（北京大学）· Tianyi Cui（北京大学 / DeepSeek-AI） 体量 八十八页 · 八节 · 一百二十四条参考 实现 Cordis 元框架 实证 Koishi（4000+ 社区插件） 目次 一句话，与它为何要紧 缘起：卸载一个插件，为何如此之难 VS Code 之困自演化 Agent harness：更迫切粗粒度变通：代价不菲 两维：时间可组合性 与 空间可组合性 可逆效应：每个变换，都随身奉上「逆」 效应上下文与累积器独立性 与 Corollary 21 响应式共效应：依赖声明成规约 共效应即效应，效应即可逆隔离与拦截 统一上下文 Γ∞：两机制合一 层级组合：插拔之字面隐喻观测等价 ≃范式之定位 动态组合演算 与 元理论 Cordis 实现：元框架之三层 核心库之要加载器：调和与 HMR 案例：Koishi，四千插件之生态 讨论中之真知 与相关工作之分野 结语：为自演化而备 01一句话，与它为何要紧 Thesis 把经典的「效应」（effect）与「共效应」（coeffect）从类型系统的静态注解，提升为运行时的一等机制；二者合一为一「上下文类型」，遂成一编程范式——组件可于运行时自由插拔，卸载即彻底回滚其副作用，依赖生灭即自动重连。 此语听来平常，实则动了根。 论文英文原题 A Programming Paradigm for Spatiotemporal Composability。「时空」非物理之时空，乃「时间维」与「空间维」两正交之组合能力。经典效应系统，其追踪行于词法作用域之内，其销毁托于编译期之 handler；而动态组合所要之保证，恰行于「组件来来去去、上下文持续演化」之运行时。二者错位。本文所为，是把那套原本长在类型层的概念结构，整体搬到运行时去，让运行时能亲手操作它。 02缘起：卸载一个插件，为何如此之难 夫软件之「组合」，古来有三法：函数调用、模块导入、类继承。三者皆定于编译之时，行于运行之始，终身不变。然今之系统，渐求动态组合——组件可于运行间装载、卸载、重配。插件架构、自演化 Agent harness，皆是也。 然卸载一组件，其于共享环境所留之痕迹，如何尽数抹去？此非易事。 VS Code 之困 以 VS Code 为例。其扩展宿主（extension host）一进程，载百千扩展。扩展一旦 activate，纵使停用或卸载，亦须重启宿主——波及所有已载扩展。 盖因 VS Code 但提供 deactivate 钩子，仅为「优雅收尾」之回调，非「就地卸载」之机制；且钩子将「效应之创」与「效应之消」割裂，清理能否周全，全凭作者自觉。此即 locality of concern 之失。 「关注点之局部性」——创建与销毁本应写在一处、由同一段代码同时交代。一旦割裂成两个回调，正确性便退化为纪律问题。 更有一层：跨扩展依赖，VS Code 几无。top 100 扩展中，惟 7 个声明了对非内置扩展之依赖。何也？其扩展点（commands、views、language features）乃宿主所定之固定表面，扩展彼此鲜有相赖。纵有 extensionDependencies，所交之值 untyped（即 any），依赖者无从恃一可检之接口。 此困非 VS Code 所独有，插件系统皆然，惟程度异耳。 自演化 Agent harness：更迫切 今之 Agent harness，须于服务请求之同时，自改其组件——工具集、执行环境、权限沙箱、记忆系统、子 Agent 编排。每一次自改，皆一动态组合之实例。 若无时间可组合性，每次自改皆须全量重启，丢弃进程内累积之态（缓存、连接、半成之算），可用性随之受损；更险者，一次有误之自改，可令「赖以恢复之进程」自身瘫废。此为最要之一处：自演化系统若无法就地回滚，其自我修改便是在锯自己坐的那根枝。 若无空间可组合性，每模块须于依赖生灭、易主之际自行侦测适配，惟逞 ad hoc 之巧；而朴素之「代码替换」策略，或悄然折断依赖者，或引入环依赖，待重载方现。 粗粒度变通：代价不菲 或曰：操作系统与容器编排，岂非已供粗粒度之替代？然代价不菲。 时间上，每次重启弃尽进程内之态，重建耗秒乃至分；维持可用，须冗余副本，虚耗资源。 空间上，容器级编排不能表达同地址空间内组件间之依赖，且跨交互平添网络开销。 二者皆行于进程／容器之界，而今之系统，组合日趋于更细之粒度。粒度之不匹，正须一组合抽象，于组件自身之粒度上，管理效应与依赖。 03两维：时间可组合性 与 空间可组合性 本文识得动态组合之两正交维度，恰与经典 effect / coeffect 系统相对： 两维之界说，及其与经典理论之对位 维度所问经典所司动态之所须 时间可组合性Temporal卸载时，其所改环境能否彻底、安全回滚？effects——描述一计算如何改其环境长期有态、作用域非词法所囿之副作用，须可追踪、可复原 空间可组合性Spatial组件间之依赖，能否声明、解析、随变而协？coeffects——描述一计算如何倚其环境依赖于运行间生灭、易主，须响应式管理其拓扑 空间可组合性 → 依赖可声明、可响应式重连 时间可组合性 → 卸载即彻底回滚 经典静态组合 函数调用 · 模块导入 · 类继承 定于编译期，行于运行始，终身不变 装了就不能拔，依赖也无从声明 依赖可声明，卸载须重启 OSGi · extensionDependencies 拓扑说得清，痕迹擦不净 清理仰赖作者自觉 · 值多为 untyped 能卸载，依赖靠手写 容器编排 · 进程级隔离 回滚干净，但粒度太粗 弃尽进程内之态 · 跨界添网络开销 Cordis：本文所立之范式 可逆效应 —— 每变换随身奉上其逆 响应式共效应 —— 依赖声明成规约 正确性由「作者自律」升为「结构属性」 两维正交，划出四象限。经典静态组合居左下；容器编排以「重启」换回滚，居左上而粒度太粗；OSGi 一路能说依赖而不能就地清理，居右下。惟右上一格，须两维同时立住——此即本文之落点。 然经典 effect / coeffect 系统，皆静态之器：效应于词法固定之作用域内追踪，由编译时 handler 销；共效应注解，对照运行前既定之上下文而验。动态组合所须之保证，却行于运行间到来离去之组件、持续演化之上下文。 故本文之核心一手： 不于静态类型系统上敷更多注解，而把 effect 与 coeffect 之概念结构「实体化」（reify），使运行时得直接操作之——此即经典理论所无、本文所立之动态保证。 04可逆效应：每个变换，都随身奉上「逆」 时间可组合性者，装载与卸载组件于运行时，卸载则共享环境复归未组合前之态。其要：组件对环境之每一改动，皆可追踪、皆可复原。 故建模一 effect 为函数 Γ → Γ × (Γ → Γ)：施于当前上下文，不仅给出新上下文，更随身奉上「逆函数」。奉上逆，方得回退；交还逆于运行时，方得追踪。此谓可逆（revertible）。追踪并复合诸逆，则环境之完整复原，成结构之保证。注意此签名之妙：逆不是另写一个 cleanup 函数放在别处，而是前向操作返回值的一部分。写不出逆，就交不出这个操作。 譬若拆乐高：每装一块，便记「此块当如何取下」。及至拆整座，依相反之序，逐块取下，城复归空台。所异者，乐高之序天定；而运行时诸组件交错，逆须在任意序下仍中各块之所改——此则须「独立性」。 效应上下文与累积器 定义效应上下文 ∂Γ ≔ Γ × (Γ → Γ)，记为 (γ, φ)。 γ：当前上下文态。 φ：累积器（accumulator），乃诸已施效应之逆之复合，亦即复原函数。 初态为 (γ₀, idΓ)。 trackΓ(f, g) 将一「前向 f + 候选逆 g」转成 ∂Γ 上之变换：施 f 于 γ，并将 g 复合入 φ。Theorem 5 证 trackΓ 为幺半群同态——追踪与复合，两不相妨。幺半群同态之实义：先复合再追踪，与先各自追踪再复合，结果一致。故「组合」这件事不会把追踪弄坏——这是整篇文章最省力的一块砖。 recoverΓ(γ, φ) ≔ (φ(γ), idΓ)：以 φ 复原 γ，并将 φ 归零。 Theorem 7（soundness invariant）：recover 之前后，φ(γ) = γ₀ 恒成立。是故无论施几许效应，只要所奉之逆真为逆，复原总能归零至初态。 ( γ₀ , idΓ ) 初态 · 累积器为恒等 track(f₁,g₁) ( γ₁ , g₁ ) γ₁ = f₁(γ₀) track(f₂,g₂) ( γ₂ , g₁ ∘ g₂ ) 逆按 LIFO 之序复合 recoverΓ(γ, φ) = ( φ(γ) , idΓ ) 不变式（Theorem 7）：φ(γ) = γ₀ —— 沿途任一点皆成立 ∂Γ ≔ Γ × (Γ → Γ) 态 + 复原函数 效应上下文 ∂Γ 之流转。前向每施一效应，逆便压入累积器；recover 一唤，整条路径一次退回。虚线框中之不变式，是全篇时间保证的支点：只要每个原子操作交出的逆确为其逆，则沿途任一时刻，累积器施于当前态都恰得初态。 独立性 与 Corollary 21 多组件交错，一组件之逆或于「他组件效应已移其态」之后方行。此时该逆还能否只撤己之所改？ 答曰：当两效应之「变换幺半群」彼此交换（Definition 19），则任取一序施其逆，皆可达 γ₀。此即 Corollary 21——独立性买得「任意序」，含交错多组件之序。这条推论是「多组件并行插拔」得以成立的通行证。若诸效应互不干涉，卸载先后便无所谓；干涉者则须由排序定理另行约束（见第 7 节 Theorem 63）。 装载：效应依序压栈 effect₁ → 交出 g₁ effect₂ → 交出 g₂ effect₃ → 交出 g₃ 栈顶在下，后来者居上 ⇄ unload 卸载：逆按 LIFO 出栈 g₃ ① 先撤最后所为 g₂ ② g₁ ③ 末撤最先所为 诸效应独立 ⇒ 此序可任意（Cor. 21） 核心库以 LIFO 序复原（Algorithm 1）。LIFO 是最保守、最不需要额外假设的顺序；一旦诸效应可证独立，Corollary 21 便解除这一约束，允许任意交错——这正是多组件同时插拔所需。 05响应式共效应：依赖声明成规约，上下文一变即通知 空间可组合性者，组件能声明彼此之依赖，系统能于运行时解析、供给、撤回之。其要：依赖之满足，须于共享上下文每有变动时重估——依赖既足则激活，依赖既撤则停用。 故建模依赖为一规约（specification）。上下文每变，以此规约判之，别为三类：激活（activating）、停用（deactivating）、中性（neutral）。判之，则变易可知；应之，则激活停用由是驱动。此谓响应式。 譬若租户与物业：组件声明「我须水、电、网」（coeffect specification）；物业（运行时）一有变动，即通知——通了便搬入（激活），断了便搬出（停用）。惟于满足其规约之态方入住，故永不强住一缺席之户。 共效应规约 需 { db , adapter } 由组件自行声明 非宿主预设之扩展点 Σ 之一次变动 Σ ≔ (k:K) ⇀ 𝒱ₖ set / delete / 换提供者 运行时以规约重估之 激活 activating 依赖既足 → 行效应函数，搬入 停用 deactivating 依赖既撤 → LIFO 复原，搬出 中性 neutral 与我无关 → 不动，不重载 关键：get / set 本身即效应函数（𝔈∗Σ）——故共效应之操作，天然被可逆效应所追踪。 共效应之三判。「中性」一档看似平常，实为性能之要：绝大多数上下文变动与某组件无关，判为中性即完全不惊动它，故重载开销只落在真正受影响的那一小片依赖子树上。 共效应即效应，效应即可逆 共效应上下文 Σ ≔ (k:K) ⇀ 𝒱ₖ：一依赖键 k，配以特异之值类型 𝒱ₖ。get / set 操作，恰为效应函数（𝔈∗Σ）——是故共效应操作，本就是可逆效应！ 此即二者之 synergism：coeffect 操作即 effect，而 effect 可逆。set 一依赖、notify 一变动，自动追踪、自动复原。此处最见巧思：不必为共效应另造一套回滚机制，它落在效应系统之内，白得一份复原保证。两个机制不是并列拼接，而是一个嵌进另一个。 隔离与拦截 隔离（isolation）：同键于不同上下文可解析为异值——isolate 引入 realm。 拦截（interception）：于依赖访问处附以横切元数据——intercept 以 monoid 合并，不改其值而改其用。 二者皆派生实现（derived realization）：生一新上下文，旧表不动，故无需逆、无需追踪，复原惟弃派生者。 06统一上下文 Γ∞：两机制合一，成一编程范式 效应载于上下文（carrier of effects），共效应亦载于上下文（carrier of coeffects）。二者合一，其状何如？ 定义 Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ。三投影：μ 者，递归类型之不动点也。上下文之中含上下文，故可层层嵌套——此即父子上下文之数学出处。 当前态； 累积器（复原此层效应）； 共效应上下文（载依赖）。 Σ 结构化并入——依赖操作（set / get）行于 Σ，其逆转由累积器追踪。且 Σ 之下值类型族 𝒱 无拘，凡系统须跨组件共享之态，皆可编码为一依赖，故 Σ 包举一切共享可变态，非惟组件间依赖。每组件与其环境之交互，皆过此一实体。 父上下文 Γ∞ 聚合诸子之一切效应，成树形控制结构 γ 当前态 φ 累积器 · 复原此层 Σ 共效应 · 载依赖 子上下文 A γ φ Σ 可独立插拔，不动其兄弟 其逆，本身即父之一效应（∂²Γ） 子上下文 B γ φ Σ 可再含孙上下文，任意嵌套 粒度自定，不受进程界所囿 Γ∞ ≔ μΓ. Γ × (Γ→Γ) × Σ 插 = 行其效应 ctx.use(component) 拔 = 复原其效应 不动其他运行中之组件 Σ 包举一切共享可变态 非惟组件间依赖 ≃ 观测等价 商去理想化之相等 统一上下文之结构与层级。μΓ 之递归让上下文可嵌上下文，于是「插拔」不再是隐喻而近乎字面——父上下文如一排插座，子上下文各占其位，各自带着自己的复原函数。子之逆本身即父之一效应，此谓 ∂²Γ。 层级组合：插拔之字面隐喻 Γ∞ 之递归结构，支持层级控制——父上下文聚合诸子效应，成树形控制结构。 装载组件 = 行其效应（插）； 卸载组件 = 复原其效应（拔 ），不动其他运行中之组件； 不同层级之组件，可独立插拔；父上下文聚合管其子之一切效应，可任意嵌套组合。 观测等价 ≃：把「理想化之相等」拉回现实 复原之保证，第 3.1 节证为一「态之相等」，然此乃理想化——物理之态不可尽复：free 不复原 heap 之布局；生成之名不复原，盖下次创生另取新名。 故相等须读作观测等价 ≃：两态不可区分，当无可观测者能辨之。各共效应自带其 ≃ₖ，上下文之关系，由诸 ≃ₖ 组装而成（Definition 33）。以此商去，方买得第 3.1.3 节所须之独立性。这一步很务实：若坚持「字节级相等」，则任何真实系统都不可能复原。改判为「无人能分辨」，理论便落到了地上，且独立性正好在这个商结构里成立。 范式之定位：兼函数式之可溯 与 命令式之 ergonomic 显式状态线程 函数式，如 State monad 长 可组合保证强，效应显于类型 短 ergonomic 代价大，调用链每函数皆须携态参 隐式变更 命令式／OOP，如 React useEffect、Java service locator 长 便捷 短 效应与依赖皆隐于隐式、散于码间，重构易碎 上下文范式兼二者之长：效应与共效应皆经一显式上下文参数中介，每操作皆可归责于其被唤起之上下文、其所属之组件。更进者—— 可逆效应：作者惟奉每原子操作之逆，复合之逆自随组合而生——卸载即由装载推导，非另写于侧； 响应式共效应：作者惟声明所需依赖，运行时自动解析重连。 双向之中，原须仰赖作者自律之正确性，一变而为范式之结构属性。 07动态组合演算 与 元理论 第 4 节将系统析为组件：每组件以「共效应规约 + 目击效应函数」配对。演算（calculus）赋其操作语义，并将时空可组合性由单组件推至整个交错组件之系统。 关键定理五则： Theorem 59Preservation 保持——良形注册表下，步骤保持系统不变量。 Theorem 61Recovery exactness 恢复精确性——累积器所复原之态，精确等于初态（在 ≃ 下）。 Corollary 62Terminal recovery 终态恢复——离去组件对终态之贡献为零。 Theorem 63Ordering 排序——提供者撤回其绑定前，一切依赖者须先停用。此即空间之序，由声明式共效应所强加。 Theorem 73Confluence 收敛——至一寂静（quiescent）态，诸合法步骤序列，经重排（依依赖序 ⊲ 线性化），皆达 ≃ / ≈ 相关之同一态。 是故无论编排器以何序增删组件、替换提供者、回退替换，系统终抵「若自始便写下该终组合」所应有之态。 此定理，许人以「静态组装」之心思推理一 Cordis 应用；亦划定保证之界：它所言者乃状态，非系统沿途之「排放」（emission）——此即第 6.1 节所辨「获取」（acquisition，边界内、被追踪）与「排放」（emission，跨界、行为如恒等）之分。 此界须记牢：已经发出的邮件、已经打进对方账户的一笔钱，不在保证之内。可逆者惟系统边界之内的状态；越界之排放，只能补偿，不能撤回。 08Cordis 实现：元框架之三层 Cordis 者，元框架（meta-framework）也。与锁定特定域（Web 路由、ORM、UI）之应用框架异：其唯 supply 普适之动态组合语义，不负具体场景。 ③ 应用框架 —— 如 Koishi 域特异之词汇：IM 适配器 · 数据库驱动 · 控制台 · 终端功能。Web 控制台自身即第二独立 Cordis 应用。 4000+ 插件 ② 组件加载器 —— 声明式配置树 增量调和（reconciliation）· 热模块替换 HMR（Alg. 8–10）· 事务性重载与失败回滚 配置之变 → fiber 操作 ① 核心库 —— 直实现 effect 与 coeffect 系统 Alg. 1 ctx.effect：唯一变异原语 · LIFO 复原 · armed 自我处置 · 父组合（∂²Γ） Alg. 2/3 ctx.