A Programming Paradigm for Spatiotemporal Composability

发表时间: 2026-07 · Paper by Peking University / DeepSeek-AI (github.com/cordiverse/paper)

Yifan Shi, Wei Zhang, Tianyi Cui (Peking University, DeepSeek-AI)

速读

一句话结论 本文提出了一种基于可逆效应和响应式协效应的统一编程范式及元框架 Cordis，解决了现代软件中组件动态加载与卸载时的状态恢复和依赖协调问题，并在拥有 4000 多个插件的 Koishi 平台上验证了其有效性。

要解决什么问题 现代软件（如插件系统和自进化智能体）越来越需要动态组合能力，即在运行时加载、卸载和重新配置组件。现有的动态组合实践常依赖重启进程或容器等粗粒度机制，导致运行时状态丢失。这一卡点在机制上表现为两个正交维度的理论基础缺失：一是时间可组合性，即在移除组件时，必须能够完全且安全地撤销其对共享环境所做的修改。这要求系统精确跟踪资源分配、事件注册和状态突变，并在卸载时保证有序回收；二是空间可组合性，即组件必须能够以结构化和可验证的方式声明、发现和解析它们之间的依赖关系。这要求系统能够动态管理依赖拓扑，并响应依赖变化来自动协调组件的生命周期。传统的效应和协效应系统局限于编译时的静态分析和词法固定作用域，无法应对运行时不断到达和离开的组件以及持续演变的环境，亟需一种能在运行时直接操作这些概念的新范式。

怎么做的 核心思路是将静态的效应和协效应概念具体化到运行时，使系统可直接操作它们。为绕开状态丢失卡点，方法设计了三个关键部件。首先是用于实现时间可组合性的“可逆效应”，它将每个上下文转换配备一个显式的逆函数。系统定义效应上下文为当前状态与恢复函数的组合 $\partial\Gamma := \Gamma \times \mathfrak{F}_\Gamma$。当函数 $f$ 修改状态时，系统通过以下机制跟踪效应并复合逆函数： $$ \operatorname{track}_\Gamma(f): (\gamma, \varphi) \mapsto (f(\gamma), \varphi \circ f^{-1}) $$ 卸载组件时，只需执行累积的逆函数 $\varphi$ 即可完全恢复初始状态。其次是用于实现空间可组合性的“响应式协效应”，它构建了一个类型化的依赖上下文 $\Sigma$。组件声明其环境依赖集 $d$，系统定义满足度谓词为： $$ \sigma \models d := \forall k \in d . k \in \mathrm{dom}(\sigma) $$ 基于此，系统引入了响应式通知机制，当依赖从不满足变为满足，或从满足变为不满足时，自动触发组件的激活或停用。此外，还引入了隔离领域和拦截机制以支持多租户和横切行为。最后是“组件生命周期模型”，它将上述两者与控制流结合。组件由协效应规范和效应函数共同定义，其目标状态由依赖是否满足决定。为了保证安全，系统引入了幂等守卫确保逆函数最多运行一次，并使用效应迭代器支持多步执行和后进先出顺序的恢复。为了防止组件绑定到过期的依赖，系统在迭代步骤边界使用 Epoch 机制检查依赖新鲜度： $$ \varepsilon_d(\sigma) := \langle \sigma(k) \mid k \in d \rangle $$ 若 Epoch 不匹配则中止转换并回滚。对于异步计算，系统采用惯性状态机，确保转换运行至完成后再响应新的目标状态。这些设计最终被统一为一个递归的上下文结构，开发者只需提供原子操作的逆，系统即可自动完成复杂的动态组合。

效果如何 实验并未采用传统的基准测试，而是通过在生产环境中部署 Koishi 聊天机器人平台进行系统级验证。该平台拥有超过 4000 个由社区贡献的生产环境插件，涵盖即时通讯适配器、数据库驱动等真实业务组件。对比基线主要为代表手动编写迁移函数路线的动态软件更新（DSU）、代表局部作用域限制路线的 React 框架、代表传统依赖注入路线的 Spring，以及代表传统插件系统路线的 VSCode。运行结果表明，该范式具有极强的通用性，同一套模型可无缝应用于 Node.js 后端和浏览器前端环境。在时间可组合性上，与 VSCode 必须重启宿主不同，该方法在控制台禁用插件或进行热模块替换（HMR）时能就地撤销效应，开发者无需编写卸载路径即可消除资源泄漏风险；在空间可组合性上，运行时切换存储后端等底层依赖，只会精准重新激活解析结果发生变化的依赖组件，在独立贡献者组成的开放生态中维持了严格的一致性。该方法的代价与局限在于：它要求开发者必须为底层原子操作提供逆函数，时间可组合性强依赖于闭包机制和运行时的模块加载能力，而空间可组合性则依赖于类型级的依赖声明和运行时的 Proxy 访问拦截。

核心问题与主要贡献

现代软件工程中，组合（Composition）是构建复杂系统的基础原则【1，On the criteria to be used in decomposing systems into modules + 1972 + Communications of the ACM + doi: 10.1145/361598.361623】。传统的组合通常是静态的（如函数调用、模块导入），但在插件系统【2，On Plug-ins and Extensible Architectures + 2005 + ACM Queue + doi: 10.1145/1053331.1053345】和自进化智能体框架等现代软件中，越来越需要动态组合（在运行时加载、卸载和重新配置组件）。目前的实践通常依赖于粗粒度的机制【3，Borg, Omega, and Kubernetes + 2016 + Communications of the ACM + doi: 10.1145/2890784】（如重启进程或容器），这会丢失运行时状态。与静态组合丰富的形式化框架相比，动态组合的理论基础仍然很不完善。

为了刻画动态组合的需求，本文识别了超出传统代数组合的两个正交维度：
* 时间可组合性（Temporal composability）：在移除组件时，必须完全且安全地撤销其对共享环境所做的修改。这要求跟踪资源分配、事件注册和状态突变，并保证在卸载时有序回收。
* 空间可组合性（Spatial composability）：组件必须能够以结构化和可验证的方式声明、发现和解析它们之间的依赖关系。这要求管理依赖拓扑并响应依赖变化来协调组件生命周期。

本文提出了一种统一的形式化基础和编程范式来解决上述问题，主要贡献如下：
1. 形式化可逆效应（Revertible effects）：将每个上下文转换配备一个显式的逆函数，使得效应跟踪和恢复成为保持组合的操作，为动态时间可组合性提供代数基础。
2. 形式化响应式协效应（Reactive coeffects）：构建一个类型化的依赖上下文，组件在其中声明需求为依赖集，基于满足度的通知机制自动触发组件的激活和停用，为动态空间可组合性提供代数基础。
3. 建立组件生命周期模型：使可逆效应和响应式协效应与多种控制流交互，产生一个将效应和协效应上下文集成到连贯编程范式中的统一上下文类型。
4. 实现Cordis元框架：提供了一个包含效应跟踪和协效应解析的核心库，以及一个带有配置协调和热模块替换（HMR）的声明式组件加载器，并在拥有4000多个社区插件的Koishi聊天机器人平台上验证了该设计。

背景知识与设计原则

效应系统（Effect Systems）的基础概念：在简单类型Lambda演算（STLC）【19，A Formulation of the Simple Theory of Types + 1940 + The Journal of Symbolic Logic + doi: 10.2307/2266170】【20，Types and Programming Languages + 2002 + MIT Press】中，效应系统通过记录计算可能产生的副作用来细化类型，形式化为 $\Gamma \vdash t : T_{effect}$。Moggi【15，Notions of computation and monads + 1991 + Information and Computation + doi: 10.1016/0890-5401(91)90052-4】首次通过单子（Monads）对副作用进行分类建模，随后Wadler【22，Monads for functional programming + 1993 + Program Design Calculi】将其在Haskell中推广。Plotkin等人【16，Adequacy for Algebraic Effects + 2001 + Foundations of Software Science and Computation Structures】【23，Notions of Computation Determine Monads + 2002 + Foundations of Software Science and Computation Structures】引入了代数效应，将效应接口与实现解耦。

协效应系统（Coeffect Systems）的基础概念：与效应相反，协效应系统丰富了上下文而不是类型，形式化为 $\Gamma_{coeffect} \vdash t : T$。它描述了计算对环境的要求（如资源、能力或服务）。Petricek等人【17，Coeffects: unified static analysis of context-dependence + 2013 + ICALP'13 + doi: 10.1007/978-3-642-39212-2_35】【30，Coeffects: a calculus of context-dependent computation + 2014 + ICFP '14 + doi: 10.1145/2628136.2628160】基于余单子（Comonads）提出了协效应作为上下文依赖的统一静态分析。分级协效应（Graded coeffects）进一步使用预序半环来实现更细粒度的资源跟踪。

静态理论向动态组合的转化原则：经典的效应和协效应系统是静态工具，局限于词法固定作用域和编译时分析。然而，动态组合要求这些保证适用于在运行时到达和离开的组件，以及不断演变的环境。因此，本文的设计原则是：不扩展静态类型系统，而是将效应和协效应的概念结构具体化（Reify），使运行时可以直接操作它们，从而在动态场景中建立这些系统在静态下提供的保证。

核心方法细节

3.1 可逆效应（Revertible Effects）

效应上下文的构建：为了实现时间可组合性，必须使组件对环境的每次修改都可跟踪且可逆。对于任何不纯函数，可以将其转换为纯函数形式 $f : \Gamma \times X \to \Gamma \times Y$。假设每个效应的逆是先验可用的，允许的效应构成对称群 $\mathrm{Sym}(\Gamma)$ 的一个子群 $\mathfrak{F}_\Gamma$。为了在上下文内部记录效应，定义效应上下文为 $\partial\Gamma := \Gamma \times \mathfrak{F}_\Gamma$。它由当前状态 $\gamma \in \Gamma$ 和恢复到初始状态的转换 $\varphi \in \mathfrak{F}_\Gamma$ 组成。

效应的跟踪与恢复机制：定义转换 $\operatorname{track}_\Gamma : (\Gamma \to \Gamma) \to \partial\Gamma \to \partial\Gamma$，其映射关系为 $f \mapsto (\gamma, \varphi) \mapsto (f(\gamma), \varphi \circ f^{-1})$。当在状态 $(\gamma, \varphi)$ 中执行 $\operatorname{track}_\Gamma(f)$ 时，$f$ 的逆与 $\varphi$ 复合，从而在上下文中跟踪 $f$ 的效应。定理表明 $\operatorname{track}_\Gamma$ 保持了复合操作 $\circ$。进一步定义恢复操作 $\mathrm{recover}_\Gamma : \partial\Gamma \to \partial\Gamma$，映射为 $(\gamma, \varphi) \mapsto (\varphi(\gamma), \mathrm{id}_\Gamma)$。该操作将恢复函数 $\varphi$ 应用于当前状态 $\gamma$，并将 $\varphi$ 重置为恒等，从而完全恢复所有效应。

交换图：track操作 ``

可逆效应函数的增强设计：在实践中，效应的逆并非先验已知，且 $\mathrm{recover}$ 是全有或全无的。因此，在输入端，函数不仅转换 $\Gamma$ 还返回相应的逆函数 $\Gamma \to \Gamma \times (\Gamma \to \Gamma)$；在输出端，不仅转换 $\partial\Gamma$ 还返回逆函数实现部分恢复 $\partial\Gamma \to \partial^2\Gamma$。定义严格效应函数 $\mathfrak{E}_\Gamma^*$，其中返回值包含新上下文 $\delta$ 和逆函数 $g$，并约束 $g(\delta) = \gamma$。定义效应函数转换 $\mathrm{effect}_\Gamma$，将操作从 $\mathfrak{E}_\Gamma$ 提升到 $\mathfrak{E}_{\partial\Gamma}$。

交换图：effect操作 ``

效应函数的复合操作：由于效应函数不再是上下文上的自同态，定义了新的操作 $\diamond$ 来表达效应复合。给定 $f, g \in \mathfrak{E}_\Gamma$，$f \diamond g$ 会先执行 $g$，再执行 $f$，并将它们的逆函数复合。定理证明 $\mathrm{effect}$ 保持了 $\diamond$ 操作。这构成了可逆效应的基础：加载组件相当于应用一系列效应函数（在 $\varphi$ 中累积逆），卸载相当于应用 $\varphi$ 恢复上下文。

3.2 响应式协效应（Reactive Coeffects）

协效应上下文的基础定义：为了实现空间可组合性，系统必须在共享上下文改变时重新评估依赖满足度。给定类型族 $\mathcal{V} : K \to \mathrm{Type}$，定义协效应上下文为依赖部分函数类型 $\Sigma := (k : K) \to \mathcal{V}_k$，将每个键 $k$ 映射到类型为 $\mathcal{V}_k$ 的值。基于此定义了 $\mathrm{get}$ 和 $\mathrm{set}$ 操作，特别地，$\mathrm{set}(k, v)$ 的类型为 $\mathfrak{E}_\Sigma$，即协效应上下文上的效应函数，因此它可以直接应用可逆效应机制，实现自动跟踪和恢复。

协效应规范与响应式通知：定义协效应规范 $\mathfrak{D}_\Sigma := \mathrm{Set}(K)$，表示组件声明的环境依赖集。定义满足度谓词 $\sigma \models d := \forall k \in d . k \in \mathrm{dom}(\sigma)$。任何将 $\sigma$ 转换为 $\sigma'$ 的效应，都可以通过 $\mathrm{notify}_d(\sigma, \sigma')$ 分类为：如果从不满足变为满足则为 $\mathrm{activating}$；如果从满足变为不满足则为 $\mathrm{deactivating}$；否则为 $\mathrm{neutral}$。这种通知机制自动驱动组件的激活和恢复，确保了正确的依赖顺序。

协效应隔离机制：为了支持多租户和沙箱，引入隔离领域（Isolation realms）。定义带有隔离的协效应上下文 $\Sigma^{\mathrm{iso}}$ 为 $(\rho, \sigma)$，其中 $\rho$ 是逻辑键到领域标识符的映射表，$\sigma$ 是领域标识符到值的映射表。访问键时，先通过 $\rho(k)$ 解析出领域 $r$，再获取 $\sigma(r)$。这提供了一种运行时的临时多态性，且所有操作（如 $\mathrm{isolate}$）仍是效应函数。

协效应拦截机制：为了在不修改依赖值的情况下附加横切行为，引入协效应拦截。上下文 $\Sigma^{\mathrm{inter}}$ 包含上下文携带的元数据 $\iota$ 和提供者函数 $\sigma$。组件规范 $\mathfrak{D}^{\mathrm{inter}}$ 携带组件声明的元数据。访问依赖时，系统将组件声明的元数据与上下文携带的元数据合并（$\iota$ 优先级更高），并将提供者函数应用于合并结果。

3.3 组件生命周期（Component Lifecycle）

组件的基础定义与状态机：组件定义为 $\mathfrak{C}_\Gamma := \mathfrak{D}_\Gamma \times \mathfrak{E}_\Gamma$，包含协效应规范 $d$ 和效应函数 $e$。组件的目标状态由两者共同决定：效应已被应用且依赖被满足（$\sigma \models d$）时为 ACTIVE，否则为 INACTIVE。状态变化会触发转换：RELOAD 执行效应函数，UNLOAD 应用累积的逆函数恢复上下文。

幂等恢复与迭代执行：为了保证安全，每个逆函数必须最多运行一次。引入幂等守卫 $\mathrm{idem}$，通过生成私有句柄来标记状态，使得返回的清理器（disposer）在首次调用后失效。为了支持多步执行，引入效应迭代器 $\mathfrak{E}_\Gamma^{\mathrm{iter}}$，每步返回修改后的上下文、逆函数和延续（continuation）。迭代器模型天然支持在步骤边界中断转换，从而实现 LIFO 顺序的效应恢复。

状态一致性与Epoch机制：当依赖在运行时被快速替换时，为了防止组件绑定到过期的依赖，引入 Epoch 机制 $\varepsilon_d(\sigma) := \langle \sigma(k) \mid k \in d \rangle$。转换开始时记录目标状态的 Epoch，在每个迭代步骤边界检查当前 Epoch 是否匹配，不匹配则中止转换并回滚。这使得生命周期扩展为多维星形结构。

异步转换的惯性状态机：当转换涉及异步计算时，外部状态可能在执行期间改变。将 RELOAD 和 UNLOAD 提升为惯性状态（Inertial states）：一旦进入，转换将运行至完成，然后再响应目标状态的改变。如果目标在执行中发生改变，系统会在当前惯性状态结束后触发反向转换。

3.4 上下文范式（The Context Paradigm）

统一上下文结构的构建：将效应上下文和协效应上下文统一为递归结构 $\Gamma_\infty := \mu\Gamma . \Gamma \times (\Gamma \to \Gamma) \times \Sigma$。包含当前上下文状态、用于效应恢复的累积逆函数，以及携带依赖信息的协效应上下文。这种递归结构支持层级控制，父上下文可以聚合管理多个子级效应。

上下文范式的定位：显式状态传递（函数式）通过状态单子保证引用透明，但存在人体工程学成本；隐式突变（命令式/OOP）如 React 的 useEffect 或 Java 的服务定位器，易用但依赖关系隐蔽且难以重构。上下文范式结合了前者的可追踪性和后者的易用性。所有操作归因于显式上下文参数，开发者只需提供原子操作的逆，系统自动复合逆函数并响应依赖变化，使正确性成为范式的结构属性。

4.1 核心库实现（Core Library）

效应跟踪的实现机制：所有上下文突变都通过核心原语 ctx.effect 进行。该方法接收一个回调并返回一个清理闭包。在底层，execute 引擎驱动回调作为效应迭代器运行，并在每步检查守卫条件，将产生的逆函数按 LIFO 顺序复合。ctx.effect 在此基础上增加了幂等自毁机制，并将生成的清理器追加到父上下文的 ctx.dispose 中，实现递归嵌套。

# Algorithm 1: Effect tracking (Pseudocode translation)
async function execute(callback, guard):
    iter = callback()
    inverse = id
    while guard():
        value, done = await iter.next()
        if value:
            inverse = value o inverse
        if done:
            break
    return inverse

function effect(ctx, callback):
    armed = true
    task = execute(callback, () -> armed)
    
    async function dispose():
        if not armed: return
        armed = false
        recover = await task
        recover()
        
    ctx.dispose = dispose o ctx.dispose
    return dispose

协效应操作的实现：上下文携带 @@store、@@isolate 和 @@intercept 三个符号键槽。ctx.get 通过隔离表解析领域标识符，再从存储中获取值。ctx.set 被实现为一个 ctx.effect 回调，负责在存储中绑定值，返回的清理器负责删除该值，两者都会调用 notify。notify 遍历所有活跃的 Fiber，检查其声明的依赖，若发生匹配则调用 refresh 重新评估状态。

# Algorithm 2: Coeffect operations (Pseudocode translation)
function get(ctx, key):
    realm = ctx[@@isolate][key]
    return ctx[@@store][realm]

function set(ctx, key, value):
    function callback():
        realm = ctx[@@isolate][key]
        ctx[@@store][realm] = value
        notify(ctx, [key])
        return function():
            delete ctx[@@store][realm]
            notify(ctx, [key])
    return ctx.effect(callback)

# Algorithm 3: Reactive notification
function notify(ctx, keys):
    for fiber in all_fibers:
        for key in keys:
            if key in fiber.inject and fiber.ctx[@@isolate][key] == ctx[@@isolate][key]:
                refresh(fiber)
                break

组件实例化与生命周期管理：ctx.use 实例化一个 Fiber，绑定配置并生成子上下文。生命周期由 refresh、reload 和 unload 协同管理。refresh 计算 Epoch，如果不匹配且无进行中的转换，则触发 reload 或 unload。reload 执行组件代码，完成后再次检查 Epoch，决定是进入 ACTIVE 还是链式调用 unload。这实现了异步惯性状态机。

# Algorithm 4 & 5 snippet: Component instantiation and lifecycle
function use(ctx, component, config):
    fiber = Fiber(parent: ctx, inject: component.inject)
    fiber.ctx = ctx[fiber -> fiber]
    fiber.apply = () -> component.apply(fiber.ctx, config)
    
    function callback():
        refresh(fiber)
        return function():
            fiber.epoch = ⊥
            unload(fiber)
            
    ctx.effect(callback)
    return fiber

function refresh(fiber):
    epoch = ε_d(σ)
    if epoch == fiber.epoch: return
    fiber.epoch = epoch
    if fiber.inertia: return
    if epoch != ⊥:
        fiber.inertia = create_task(reload(fiber))
    else:
        fiber.inertia = create_task(unload(fiber))

代理介导的上下文访问：除了 get/set API，Cordis 支持通过属性访问（如 ctx[key]）获取依赖。系统使用 Proxy 拦截访问，向上遍历 Fiber 树，只有在组件的 inject 规范中声明了该键时才允许访问（调用 get），否则抛出未声明访问异常。这在运行时强制执行了协效应规范。

4.2 组件加载器（Component Loader）

声明式配置层：为了组装预先存在的组件，加载器引入了声明式配置层。配置树由 Entry 组成，记录了模块 URL、隔离/拦截注解、配置数据等。当配置发生变化时，加载器执行增量协调（Reconciliation）：仅对改变的字段应用最小破坏性操作（如仅更新配置而不重载组件，或重写领域映射表）。

热模块替换（HMR）：HMR 引擎将可逆效应模式应用于模块级别。由于 Fiber 已经绑定了组件的所有效应，替换模块只需销毁旧 Fiber 并用新模块实例化新 Fiber，无需开发者手动编写接收边界。引擎分三阶段运行：1. 模块分类（计算受影响的依赖图）；2. 识别陈旧 Entry；3. 事务性重载（备份缓存，销毁旧 Fiber，加载新 Fiber，若出错则回滚）。

实验环境与配置

本文的验证并非传统的机器学习基准测试，而是通过在生产环境中部署 Koishi 聊天机器人平台来进行系统级验证。
* 软件配置/依赖：Cordis 框架（本文提出的元框架，使用 TypeScript 实现，利用 Proxy 和模块化特性）。
* 应用规模：Koishi 平台是一个开源聊天机器人框架，拥有超过 4000 个由社区贡献的生产环境插件。
* 组件类型：包括即时通讯（IM）适配器、数据库驱动程序、管理控制台和终端用户功能插件。

实验结果与分析

通过 Koishi 平台的案例研究，验证了 Cordis 模型的以下特性：
1. 元框架的表达能力与通用性：Koishi 将每个功能都实现为基于 Cordis 核心原语的插件。同样的模型也被应用于完全不同的运行时——Koishi 的 Web 控制台（浏览器环境），证明了该范式不依赖于特定领域或特定运行时。
2. 无认知负担的时间可组合性：传统的插件系统（如 VSCode）无法在不重启宿主的情况下卸载包含代码的扩展。在 Koishi 中，控制台禁用插件或 HMR 重新应用插件时，效应会被就地撤销，同时保留系统其他部分的缓存和连接。开发者无需编写卸载路径，系统自动复合逆函数，消除了资源泄漏的风险。
3. 开放生态系统中的空间可组合性：Koishi 生态系统展现了真实的依赖拓扑（如功能插件依赖数据库驱动）。在运行时重新配置提供者（如切换存储后端）只会重新激活解析结果发生变化的依赖组件。这证明了响应式协效应能够在由独立贡献者组成的开放生态系统中保持一致性。

补充探讨与相关工作

服务多路复用与访问控制：通过服务代理（Service broker）模式，框架支持负载均衡、滚动更新（平滑过渡请求）和跨进程 RPC 调用。在安全方面，依赖声明充当了基于能力（Capability-based）的访问控制请求，而拦截机制允许在不修改组件代码的情况下，由上下文强制执行细粒度的安全策略（如只读文件系统访问）。

语言独立性：该范式与语言无关。时间可组合性依赖于闭包（捕获逆函数和状态）以及运行时的模块加载/卸载机制（如托管运行时的注册表或 Native 的动态链接）。空间可组合性依赖于类型级的依赖声明（如 Rust 的 traits、TypeScript 的模块增强）和运行时的访问拦截（如 Proxy 或反射）。

相关工作对比：
* 效应/协效应系统：与 Effekt 语言【70，Effects as capabilities: effect handlers and lightweight effect polymorphism + 2020 + OOPSLA + doi: 10.1145/3428194】将效应视为能力不同，Cordis 在运行时处理效应以实现资源恢复；与可逆计算【73，Reversible Effects as Inverse Arrows + 2018 + MFPS XXXIV + doi: 10.1016/j.entcs.2018.11.009】要求全局可逆不同，Cordis 仅要求原子效应提供逆函数。
* 编程范式：与面向上下文编程（COP）【78，Context-oriented Programming + 2008 + Journal of Object Technology + doi: 10.5381/jot.2008.7.3.a4】相比，Cordis 通过显式上下文管理生命周期，而不是隐式修改方法分派；与面向切面编程（AOP）【81，Aspect-Oriented Programming + 1997 + ECOOP'97 + doi: 10.1007/BFb0053381】相比，Cordis 的拦截局限于组件显式声明的依赖，避免了 AOP 的不可预测性。
* 时间/空间可组合性：相比于动态软件更新（DSU）【85，Dynamic Software Updating + 2001 + PLDI '01 + doi: 10.1145/378795.378798】的手写迁移函数，或 React useEffect 的局部作用域限制，Cordis 提供了结构化的全局可逆保证。相比于传统依赖注入（如 Spring【100，Spring in Action + 2022】），Cordis 提供了基于生命周期的组件级响应式更新，填补了细粒度动态组合的空白。

结论与展望

本文通过将效应和协效应的类型理论概念提升为运行时机制，为动态可组合性提供了形式化基础。可逆效应为上下文转换配备了显式的逆函数，保证了组件移除时的完全状态恢复。响应式协效应通过基于满足度的通知、隔离和拦截机制，形式化了类型化的依赖上下文。结合支持多种控制流的组件生命周期模型，这些机制产生了一个连贯的编程范式。该范式通过 Cordis 元框架实现，并在 Koishi 生产系统中得到了验证。

未来的工作方向是将该框架应用于自进化智能体（Self-evolving agent harnesses），在这些系统中，AI 智能体在极少人类监督下持续生成和替换自身的框架组件。Cordis 能够为这种高频组件替换和拓扑变化提供完全恢复和依赖协调的保证，有望成为自主系统持续自进化的坚实基础。