译者说明
本文是非官方中文翻译。原题为 A Programming Paradigm for Spatiotemporal Composability,作者为 Yifan Shi、Wei Zhang、Tianyi Cui,版本为 v8 / Draft of August 13, 2026,对应原仓库 commit 13f28585668a28106b2f53bedada36e45bc1ed3e。请从 cordiverse/paper 获取原文。原仓库未声明许可证,原文与版权归作者所有;如权利人认为本文不宜公开,请联系删除。
摘要
现代软件——从插件系统到自演化智能体运行框架——日益需要动态组合,但其形式化基础仍未得到充分发展。我们识别出这一问题的两个正交维度:时间可组合性,即在移除组件时完全撤销其副作用的能力;以及空间可组合性,即声明并以反应式方式管理组件间依赖的能力。我们通过将经典的效应与余效概念提升为运行时机制来处理这两个维度。具体而言,我们形式化了可逆效应,其中每个上下文变换都携带一个由运行时追踪的逆变换。我们还形式化了反应式余效,其中上下文的每次变化都会依据组件的余效规约向该组件发出通知。我们将效应上下文和余效上下文统一为单一的上下文类型,由此构成一种编程范式。随后,我们把这些机制结合到组件这一概念中,并给出一种动态组合演算;其元理论将时空可组合性从单个组件推广到由交错运行的组件组成的整个系统。我们在 Cordis 中实现了这些思想。Cordis 是一个时空可组合性元框架,它既提供具有效应追踪和余效解析能力的核心库,也提供支持配置协调与热模块替换(HMR)的声明式组件加载器。
1. 引言
组合——由较简单的部分组装出复杂系统——是软件工程的一项基本原则 [1]。传统上,组合是静态的:函数调用、模块导入和类继承在编译时解析,并在整个执行过程中保持不变。然而,现代软件日益需要动态组合,即在运行时加载、卸载和重新配置组件。插件架构 [2] 和自演化智能体运行框架都要求系统能够即时、安全地添加和移除功能;但当前实践依赖粗粒度机制 [3],这类机制只能通过重启来重新配置,并会丢弃运行时状态。尽管动态组合在实践中愈发重要,但与静态组合已有的丰富形式化框架相比,其理论基础仍未得到充分发展。
1.1 可组合性的维度
为刻画动态组合的要求,我们在组合中已得到充分研究的代数层面之外,识别出两个正交维度:
- 时间可组合性处理时间维度:移除组件时,该组件对共享环境所做的修改必须得到彻底且安全的撤销。这要求追踪组件执行的每一次资源分配、事件注册和状态变更,并保证在移除组件时按序回收这些内容。
- 空间可组合性处理空间维度:组件必须能够以结构化且可验证的方式声明、发现并解析彼此之间的依赖。这要求管理依赖拓扑,并在依赖发生变化时协调组件生命周期。
在静态情形下,时间可组合性可归结为词法作用域(例如 RAII [4]、bracket 模式 [5]),空间可组合性则可归结为模块导入解析 [6]。在动态情形下,组件会在运行时到来和离开,两个维度都会变得困难得多:时间可组合性必须处理长期存在且有状态的效应,而这些效应的作用域并不受词法边界约束;空间可组合性则必须处理执行期间出现、消失或改变身份的依赖。
1.2 动机示例
1.2.1 插件系统
插件系统是动态组合的典型实例。我们以最广泛使用的可扩展集成开发环境之一 Visual Studio Code(VSCode)作为代表性示例。
时间方面的局限。 VSCode 在一个名为扩展宿主(extension host)的共享进程中运行所有扩展。尽管可以动态安装扩展,但该宿主没有提供在运行时卸载单个扩展代码的机制。一旦某个扩展的 activate 函数执行完毕,若要禁用或卸载该扩展,就必须重启整个宿主,从而影响所有已加载的扩展。主题、快捷键绑定和代码片段等纯声明式扩展不包含代码,因此可以自由移除。然而,在按安装量排名前 100 的扩展中,有 87 个包含可执行代码1,因而在移除时需要进行上述重启。虽然 VSCode 提供了 deactivate 钩子,但它仅在宿主进程终止期间充当优雅关闭回调,因此无法实现在线移除。此外,该钩子将效应的处置与效应的创建(位于 activate 中)分离开来,违背了关注点的局部性,也使得完整清理难以验证。
空间方面的局限。 VSCode 确实提供了 extensionDependencies,用于声明扩展之间的依赖,但它很少得到使用:在按安装量排名前 100 的扩展中,只有 7 个通过 extensionDependencies 声明了对非内置扩展的依赖。1 这种稀少性反映了扩展 API 的形态:该 API 暴露命令、视图和语言功能等固定的表层扩展点。扩展通过这些扩展点向宿主贡献功能,而不是彼此依赖,因此扩展间依赖很少出现。此外,VSCode 的扩展间交互机制没有提供结构化契约:它通过 vscode.extensions.getExtension(...).exports 向其他扩展暴露某个扩展的功能,但返回值没有类型(默认为 any),因此依赖方无法信赖经过检查的接口。简言之,VSCode 将扩展引导至宿主提供的一组固定扩展点,却没有为扩展彼此依赖提供安全且结构化的方式。
这两个局限并非 VSCode 所独有;它们普遍存在于插件系统中 [2, 7],只是在程度上有所不同。
1.2.2 自演化智能体运行框架
现代 AI 智能体依赖运行时智能体运行框架 [8–10]。这些系统可以组合多种工具套件 [11] 和执行环境,管理权限与沙箱化,维护会话状态和持久化,提供上下文管理与记忆系统 [12],编排子智能体及多智能体工作流 [13],并向用户和自动化系统暴露接口。未来的运行框架或许会在持续处理请求的同时,生成并部署对自身组件的修改。由模型合成的可复用工具,是迈向组件级自我修改的一种范围更窄的前身 [14]。每一次此类修改本身都是动态组合的一个实例。
由于这些修改会持续发生,且只受到有限甚至完全没有人工监督,动态可组合性变得不可或缺。如果没有时间可组合性,每次自我修改都会迫使系统完全重启,从而丢弃所有进程内积累的状态;在如此频繁的修改下,累积的不可用时间将变得十分可观,正在执行的任务也会反复中断;更糟的是,一次有缺陷的自我修改可能会使恢复工作所依赖的进程本身失效。如果没有空间可组合性,每个模块都必须自行检测并适应其所依赖模块的变化,包括这些模块的出现、消失或身份改变,而且只能通过临时拼凑的方式做到这一点;更糟的是,朴素的代码替换策略可能会悄然破坏依赖方,或引入直到重新加载时才暴露的循环依赖。
1.2.3 粗粒度权宜方案
动态可组合性仅受到有限形式化关注的一个原因是,操作系统和容器编排器已经提供了一种粗粒度的替代方案。操作系统在进程粒度上提供时间可组合性;容器编排器 [3] 在服务粒度上提供空间可组合性。实践中,大多数软件通过诉诸这些粗粒度机制来容忍细粒度可组合性的缺失:通过重启进程来处理行为异常的模块,并由容器编排器管理服务依赖。
然而,这种权宜方案代价高昂。在时间方面,每次重启都会丢弃所有进程内积累的状态(例如缓存、连接和部分完成的计算),而重建这些状态需要数秒乃至数分钟 [15];要在此期间维持可用性,就需要冗余副本,由于无法恢复单个组件而不得不承担额外的资源开销。在空间方面,容器级编排无法表达共享同一地址空间的组件之间的依赖,而且会为原本可通过本地函数调用完成的交互引入网络开销。这两种机制都作用于进程和容器的边界,但现代系统越来越多地在更细粒度上进行组合。这种粒度错配要求一种组合抽象,能够在与组件本身相同的层级上管理效应和依赖。
1.3 贡献
动态可组合性的两个维度分别关乎计算如何修改其环境,以及计算如何依赖其环境。这两个方向正是效应系统 [16, 17] 和余效系统 [18, 19] 所形式化的内容:效应为推理环境修改提供形式化词汇,余效则为推理环境要求提供形式化词汇。然而,现有形式化方法将推理局限于针对词法上固定作用域的编译时分析,无法扩展到组件在运行时到来和离开的动态场景。通过将效应提升为可逆的运行时模型,并将余效提升为反应式依赖解析机制,我们为动态可组合性建立了统一的形式化基础;这一基础与编程语言无关,并适用于任何需要动态组合的软件架构。我们作出以下贡献:
- 我们形式化了可逆效应(第 3.1 节):每个上下文变换都携带一个由运行时追踪的显式逆变换,而且追踪和恢复都保持组合,因此在移除组件时能够恢复上下文。这建立了局部时间可组合性。
- 我们形式化了反应式余效(第 3.2 节):组件以规约的形式声明其所需的余效,而上下文每次发生变化时,都会依据该规约,以激活、停用或中性三种结果之一通知组件。这建立了局部空间可组合性。
- 我们将效应上下文和余效上下文统一为单一的上下文类型(第 3.3 节);在这一类型中,余效上的观察等价为效应赋予独立性,由此构成一种编程范式。
- 我们给出了一种动态组合演算(第 4 节),它将上述两种机制结合到组件这一概念中,并为组件的生命周期配备操作语义。其元理论将时空可组合性从单个组件推广到由交错运行的组件组成的整个系统。
- 我们在 Cordis 中实现了这些思想(第 5 节)。Cordis 是一个时空可组合性元框架,它既提供通过效应追踪和余效解析来实现形式化模型的核心库,也提供支持配置协调与热模块替换(HMR)的声明式组件加载器。
1 数据于 2026 年 6 月 9 日从 Visual Studio Code Marketplace 获取。 ↩ ↩
2. 预备知识
本节简要概述效应系统与余效系统——二者是本研究所依托的两大理论支柱。我们假定读者熟悉基本的类型论与范畴论;本节旨在统一记号,并介绍将在第 3 节中被操作化为运行时机制的关键抽象。
2.1. 效应
在简单类型 λ 演算(STLC)[20, 21] 中,类型判断
这里,结果类型由效应代数中的一个元素标注,该元素描述计算可能产生哪些副作用,从而支持对有状态计算进行组合式推理。这一方法源自 Lucassen 和 Gifford [22];他们引入了一种区分类型、效应与区域的带种类类型系统,用以发现并行程序中的调度约束。
单子效应。 Moggi [16] 最早通过单子,以范畴论方式对计算效应建模;Wadler [23] 随后在 Haskell 中推广了这一方法。范畴
代数效应。 Plotkin 和 Power [17, 24] 证明了代数操作可以确定单子,由此建立了一个将效应接口与其实现解耦的框架。效应签名
处理器接收操作参数
2.2. 余效
与效应对偶,余效系统 [18, 31] 精化的是上下文而非类型,由此得到如下形式的判断:
这里,上下文由余效代数中的一个元素标注,该元素描述计算需要从其环境中获得什么,例如需要访问的资源、需要持有的权限或需要依赖的服务。效应对程序给世界造成的影响建模,而余效则对世界施加于程序的约束建模。
余单子余效。 使用余单子来组织上下文依赖型计算的思想,最早由 Uustalu 和 Vene [32] 提出;他们以对称(半)幺半余单子作为 Moggi 的单子效应框架的对偶,从而刻画数据流、属性求值等概念。Petricek 等人 [18] 在此基础上提出余效,将其作为对上下文依赖关系的一种统一静态分析。余单子
分级余效。 为实现更细粒度的追踪,分级余效系统使用预序半环
2.3. 与动态可组合性的关系
效应系统与余效系统沿两个互补方向组织关于计算的推理:效应描述计算如何修改其环境,余效则描述计算如何依赖其环境。这两个方向分别对应第 1 节所识别出的动态可组合性的两个维度:
时间可组合性要求组件对共享环境所做的修改能够在卸载时被撤销。与此相关的是有状态效应,它们会持久地改变该环境;要撤销这样的改变,就要求它存在逆变换。
空间可组合性要求组件间依赖能够被声明并以反应式方式管理。这些依赖正是余效所捕获的内容,而对它们进行管理,就相当于将每项依赖与环境所提供的内容逐一解析。
然而,经典的效应系统和余效系统都是静态工具:效应在词法上固定的作用域内被追踪,并由编译时处理器消解;余效标注则依据执行前确定的上下文进行验证。相比之下,动态组合要求这些保证对运行时到来和离开的组件仍然成立,并且面对的是持续演化的上下文。任何固定的词法作用域都无法界定部署之后才加载的插件;任何编译时上下文都无法预见由运行时配置所产生的依赖。
这促使我们转换视角:与其为静态类型系统增加更多标注,不如将效应和余效的概念结构具体化,使运行时能够直接操作它们,从而动态地建立这些系统在静态层面提供的保证。
3. 可逆效应与反应式余效
本节将第 2 节介绍的效应与余效概念提升为运行时机制,由此构建动态组合理论。其核心思想是:将承载效应和余效的类型上下文转化为上下文类型,即可由运行时操作、并将上下文本身具体化为一等实体的类型。对于效应类型,我们将其建模为上下文变换与其逆变换组成的配对,从而实现局部时间可组合性。对于余效上下文,我们将其建模为携带依赖信息的类型,从而实现局部空间可组合性。随后,余效上的观察等价为效应提供独立性。这个同时承载效应与余效的统一上下文本身便构成了一种编程范式。
3.1. 可逆效应
时间可组合性是指在运行时加载和卸载组件,并且在卸载后将共享环境恢复到组合前状态的能力。这要求组件对环境所做的每一项修改都既可追踪又可恢复。因此,我们将效应建模为类型为
3.1.1. 效应上下文
给定任意非纯函数
- **封闭性:**两个效应的顺序组合仍然是一个效应;
- **结合性:**复合效应不依赖于括号如何放置;
- 单位元:
,即 上的恒等函数,是复合运算的单位元。
为了对可撤销的效应建模,我们将每个变换
定义 1. 上下文变换对的扭曲组合定义为
与
为了在上下文本身之中追踪效应,我们引入如下定义:
定义 2. 给定上下文
它可以理解为一个二元组
是当前上下文状态; 是累加器,即迄今为止所执行效应之逆变换的复合,也是将上下文恢复到初始状态的函数。
特别地,初始效应上下文可表示为
我们还记
由于累加器
定义 3. 在上下文函数对上定义变换
这一变换把前向函数
定理 4. 对每个
f
Γ ─────────→ Γ
↑ ⇓ ↑
pr₁ track pr₁
│ │
∂Γ ─────────→ ∂Γ
f′其中
证明. 对所有
定理 5.
; - 对所有
,
证明.
- 单位元被映射为单位元,因为
。 - 对于乘法,任取
:
定义 6. 在
这一变换把恢复函数
f₁ fₙ
Γ ───────────→ Γ ┄ ┄ ┄ ┄ ┄ → Γ ───────────→ Γ
⇓ track ⇓ track ⇓ track
∂Γ ───────────→ ∂Γ ┄ ┄ ┄ ┄ → ∂Γ ───────────→ ∂Γ
f′₁ f′ₙ
↑ │
└──────────────── recover ─────────────────┘图中,上方每个变换
定理 7. 对每个
证明.
对于一列这样的函数对,无须另行论证。设
取
恢复操作通过量
3.1.2. 可逆效应函数
上一小节的 track/recover 模型将逆函数视为先验给定:recover 是全有或全无的:它无法在保留其他效应的同时选择性地撤销某一个效应。为同时解决这两个问题,我们从输入侧和输出侧增强该模型:
在输入侧,我们不仅变换
,还随之返回一个逆函数,使逆函数在应用效应之处提供: ,即 ; 在输出侧,我们不仅变换
,还随之返回一个逆函数,从而可以撤销某一个效应而保留其他效应: ,即 。
这一增强在输入与输出之间保持了结构一致性,因此我们仍然可以定义相应的理论,使 track 的数学性质得以保持。由此得到效应函数
定义 8. 效应函数
其中,
是新的上下文; 是当前效应的逆函数。
由于效应函数
定义 9. 给定函数
定理 10. 效应组合将
是一个幺半群,其单位元为 ; 赋值
是从 到 的幺半群同态。
证明。
结合律和单位元律逐分量地由
的相应性质推出。 记
;则 这正是
的像,而 映射到 。
定理 11. 见证性在效应组合下得以保持,并且一个统一的逆函数能够在每个状态提供见证。即:
是 的子幺半群; 定理 10 中的同态将每个满足
的二元组映入 。
证明。
因为
,所以单位元属于 。对于封闭性,取 以及任意 ,并令 、 ,于是 。此时 且 ,因此 。 给出每个 处的 ,所以这种二元组的像在每个状态都有见证。
正如 track 将 effect,将
定义 12. 效应函数变换
由于 track。通常的追踪规则再次适用:撤销该效应本身也是一个效应,它通过 track 的规定,组合到传给它的累加器上。
现在,我们可以证明 effect 具有与 track 类似的性质。
定理 13. effect 保持
证明。 取任意
那么
其中,第一步分别在
下图展示了这两个层级之间的关系。上方三角形是定义 8 所给出的
在两个层级之间,投影
定理 14. 令
; 对每个
,提升后的逆函数 与在该处作为见证的逆函数 满足 。
证明。
由定义 12,
,其状态为 。 这就是将定理 4 应用于
。
通过计算提升后的逆函数返回什么,即可确定下方三角形是否闭合:
定理 15. 令
状态被精确恢复。当且仅当
证明。 由定义 12,
这里使用了
因此,只有当在
这正是定理 7 对累加器所作假设的全部内容,因此撤销操作不会改变恢复目标。
若按照效应应用顺序的逆序来撤销效应,则不需要任何额外条件,因为每个逆函数此时都会遇到由其自身对应的应用所产生的状态:
定理 16. 设
每次撤销都会恢复到其对应应用运行时所面对的上下文状态;
每个中间状态都满足健全性不变量。
证明。 每一步都是一次应用或一次撤销。一次应用把
3.1.3. 效应的独立性
定理 16 讨论的是在某个效应自身的应用所产生的状态处撤销该效应;本小节则讨论在任意其他状态处撤销效应。后一种情形有两类需求。其一,在后续效应仍然存在时就可能运行某个逆函数,这正对应于从运行中的系统撤回一个组件;其二,一个序列可能交错执行多个组件的效应,每个组件分别保存自己的逆函数,因而某一组件的各次逆操作会被另一组件的应用隔开。在这两种情况下,逆函数都会遇到已被外来效应移动过的状态;它是否仍能撤销当初为之构造的那个效应,取决于交换性:一个效应所能执行的每种变换,都必须与另一个效应所能执行的每种变换交换,其中既包括前向映射,也包括所产生的逆函数。单一的累加器无法解决这两种情形中的任何一种,因为
定义 17. 对于效应函数
由二元组
引理 18. 交换性可由生成元确定,而
如果
的每个生成元都与 的每个生成元交换,那么 的每个元素都与 的每个元素交换; 。
证明。
与
的每个生成元交换的映射构成 的一个子幺半群,因为 属于其中,并且只要 和 属于其中, 也属于其中。根据假设,该子幺半群包含 的生成元,因此包含 。固定 后,与 交换的映射同样构成一个子幺半群;它包含 的生成元,因此包含 。 根据定义 9,
的前向映射为 ;它在任意状态产生的逆函数均为 ,其中 由 产生, 由 产生。因此, 的每个生成元都是这两个效应的生成元的复合。
定义 19. 当满足以下条件时,称效应函数
一方的每个变换都与另一方的每个变换交换:
任何一方的变换都不会扰动另一方所产生的逆函数:
并且交换
与 后的同一条件也成立。
如果对于每个
对于由二元组
在独立性成立时,可以在后续效应已经移动过的状态处运行某个逆函数;它在该处撤回的恰好是自身的贡献,而不会撤回任何其他贡献:
定理 20. 设
因此
且 ; 每个满足
的 在 处产生的逆函数,与它在 处产生的逆函数 相同。
证明。
第一个等式可对
作归纳证明。当 时,该等式为 ,这正是 的定义。对于归纳步骤, 其中中间的等式使用了定义 19 的条件 (1),应用于
和 ;由于 ,它们是该族中两个不同位置的效应。对于第二个等式,条件 (1) 使 可以向外穿过 之后应用的各个前向映射,从而最终能够在 的见证条件所适用的唯一状态处使用该见证: 最后一个等式依据的是
,这正是定义 8 要求 在 处满足的见证条件。 由 (1),状态
为 ,且 ,因此,定义 19 中关于 和 的条款 (2) 给出
□
条款 (1) 确定了一个逆函数所到达的状态:无论在该效应之后又应用了哪些效应,这一状态都与从未应用该效应时,同一序列本会到达的状态相同。条款 (2) 确定了其他效应的逆函数在该状态下是什么;二者结合起来,便可将该定理再次应用于更短的序列:
推论 21. 设
证明。 对
□
LIFO 顺序正是这样的排列之一,而定理 16 在完全不需要任何假设的情况下就能按该顺序进行还原。独立性带来的是其余所有顺序,并由此能够处理多个组件的效应彼此交错形成的序列;第 4.4.2 节将这一结论提升到整个系统的迹。
这些构造共同组成了可逆效应:
这一判据遗漏了两件事,而二者都会在多个组件共同参与时出现:不按累加器规定的顺序进行还原,以及一个与其他组件的效应彼此交错的序列。独立性提供了这两项能力(推论 21);它是施加于效应的条件,而非该构造本身的性质。第 3.3.2 节将找出满足这一条件的约束规则,第 4.4.2 节则会就整个系统的迹来陈述这一保证。当独立性不成立时,顺序必须由其他地方承载:在单个组件内部,由累加器承载;无论效应为何,它都会按 LIFO 顺序进行还原(第 4.3.2 节);而在组件之间,则由已声明的余效承载,它规定一次激活相对于另一次激活的顺序(第 4.3.1 节)。
3.2. 反应式余效
空间可组合性,是指组件能够声明彼此之间的依赖,并且系统能够在运行时解析、提供和撤回这些依赖。为此,每当共享上下文发生变化时,都必须重新求值依赖的满足情况,使组件在其依赖变得可用时激活,并在这些依赖被撤回时停用。因此,我们将组件的依赖建模为一个规约,并依据该规约将上下文的每次变化分类为激活型、停用型或中性。依据规约进行分类,负责检测满足状态的变化;响应分类结果,则负责驱动激活与停用。我们将这样的余效称为反应式余效:通过对上下文变化进行分类,并据此驱动激活与停用,正确的余效顺序便成为一种结构性保证。
3.2.1. 余效上下文
传统的控制反转(IoC)容器 [38] 通常将依赖建模为简单的键值映射。本节将 IoC 形式化为一种余效上下文;它与可逆效应协同作用,为动态组合提供数学基础。
定义 22. 给定类型族
其中,
表示函数应用(当 时有定义); 表示在 处绑定 、在其他位置均与 一致的表; 表示限制操作(当 时有定义); 表示成员关系。
使用类型族
定义 23.
其中,
值得注意的是,
定义 24. 键
其前两个分量组成
该式在
将
3.2.2. 规约与通知
上述定义描述了如何注册和访问各个依赖。然而,访问一个不存在的依赖会导致运行时失败。因此,组件不应以乐观方式访问依赖、再在其中某个依赖缺失时失败,而应当仅在其声明的全部依赖都已存在后才激活。这引出了两个问题:组件所声明的依赖是否被共同满足,以及当这一状态发生变化时系统应当如何响应。余效上下文
这一谓词是可判定的(因为
定义 25. 余效规约为:
它表示组件声明需要从环境获得的依赖集合。
这一规约之所以具有反应性,在于它对状态迁移的分类方式。任何将
定义 26. 给定余效规约
由于
该判据涵盖了余效顺序的一个方向,却未涵盖另一个方向。如果组件
3.2.3. 隔离与拦截
基本的余效上下文
实现方式。 这两种机制与
定义 27. 上下文上的效应函数允许采用两种实现方式:
原位实现会修改上下文,并返回一个非平凡的逆函数;后继状态是输入的别名,恢复过程通过运行逆函数来撤销该修改。
派生式实现保持输入不变,并返回一个由它派生出的新上下文,同时以恒等映射作为逆函数;恢复过程会丢弃这个派生上下文。定义 32 的递归结构所承载的,正是这种由另一个上下文派生出的上下文。
在纯函数式环境中,这两种实现方式彼此重合;命令式宿主则可以为每个操作任选其一。第 5.1.2 节同时实现了二者。隔离和拦截被直接规定为派生式实现:二者都会产生一个新上下文,其自身的表与继承而来的表有所不同;因此,下文将二者定型为从上下文到上下文的映射,而不是效应函数。共享表没有发生任何变化,所以既没有需要追踪的逆函数,也没有任何内容需要定义 12 来提升;恢复时,只需将派生上下文连同它所携带的调整一起丢弃。对派生表的赋值会覆盖继承表在该键处原有的任何内容,因此这两个操作都不带前置条件。
余效隔离。 余效隔离通过引入隔离域,使同一个依赖可以在不同上下文中绑定到不同的值。这一机制广泛适用于多租户系统、测试环境和组件沙箱。
定义 28. 带隔离的余效上下文定义为:
它可以表示为一对
是隔离域表,为每个被隔离的键指派一个隔离域标识符;不在 中的键会解析到以它自身为标识的隔离域,因此在这种情况下记 ( ); 是依赖表,即从隔离域标识符到具有相应类型之值的依赖偏函数。
这种双层映射结构将逻辑层与存储层解耦,使依赖访问能够感知上下文。访问键
定义 29.
其中,
余效隔离机制实质上实现了一套运行时特设多态系统。通过隔离域标识符,同一个依赖键可以在不同上下文中解析为完全不同的值,而且这种多态性可以在运行时动态调整。与传统依赖注入相比,余效隔离提供了粒度更细的控制,能够针对特定组件进行定制化隔离;
余效拦截。 第二种机制是余效拦截,它将横切元数据附加到依赖访问之上,从而在不修改依赖值的情况下添加行为。这些元数据既可以由上下文携带,也可以由组件声明,因此我们同时扩展余效上下文和余效规约:
定义 30. 带拦截的余效上下文与规约定义为:
上下文
定义 31. get、set 和 intercept 操作如下:
其中,get 和 set 对提供者表分别具有定义 23 中的前置条件,即
当规约为
3.3. 上下文范式
第 3.1 节和第 3.2 节都作用于上下文:前者将上下文作为效应的载体,后者将其作为余效的载体,但二者并未说明同时承载效应与余效的单一上下文应当是什么样子。本节为这种统一给出一个具体构造,从余效中组装出一种观察等价关系,以补足第 3.1.3 节悬而未决的效应独立性,并论证由此得到的上下文类型本身构成一种编程范式。
3.3.1. 统一上下文
对于上下文
定义 32. 上下文类型
其中三个投影分别为:
:当前上下文状态(递归); :用于恢复本层效应的累加器; :携带依赖信息的余效上下文。
在此定义下,effect 将 set、get)作用于
层次化组合。
加载组件对应于执行其效应(插入);
卸载组件对应于恢复其效应(拔出,且不影响其他正在运行的组件);
层次结构中不同层级的组件可以彼此独立地加载和卸载;父上下文聚合并管理其所有子组件的效应,从而支持任意深度的嵌套组合。
3.3.2. 观察等价
第 3.1 节的恢复保证断言状态之间相等(定理 7),但这是一种理想化,因为物理状态不可能恢复到原来所处的确切形态。例如,free 会把内存块释放给分配器,却不会恢复堆在执行 malloc 之前的布局;生成式名称也不会由丢弃该名称的逆操作恢复,因为下一次创建会取得一个全新的名称 [39]。因此,第 3 节中的等式都应在某种等价关系
定义 33. 若两个余效上下文将同一组键绑定到彼此相关的值,则二者相关;若一个上下文的两个状态的余效投影相关,则这两个状态相关:
这里以
由此,状态中未被任何键绑定的部分会被遗忘;正是这种遗忘,才使定理 7 能够在
将该关系称为观察等价,实际上是对每个
定义 34. 设
引理 35. 不可区分性是操作所尊重的最粗关系。也就是说:
的每个操作都在定义 24 的意义下尊重 ; 凡是被每个操作都尊重的等价关系,都包含于
。
因此,
证明。
设
,并将 应用于某个参数。在测试前添加一个字母后,所得仍是测试,因此正向映射到达的值仍然不可区分;任何一个由操作产生的逆映射从不可区分的参数出发所到达的值也同样不可区分。单字母测试保证该操作在两者上要么都有定义、要么都无定义,并保证其结果相等。 设
为这样的等价关系,且 。测试中的每个字母,都是某项操作的正向映射或该操作产生的逆映射;尊重性使 沿这两类映射均得以保持,从而在每个字母处,所到达的值始终相关,所得结果始终相等。因此,每个测试在 和 上的表现均一致。
仅仅在所有地方都以
定义 36. 若映射
则称
尊重
定义 37. 在
; 尊重 ;
则
若取
引理 38. 按定义 37 解读
证明。 累加器是若干逆函数的复合;根据定义 37(2),每个逆函数都尊重
定义 19 所要求的交换性,也由同一引理在
定义 39. 若操作
并且在交换
对于不同的键,该条件直接成立。
定理 40. 位于不同键上的操作彼此独立。
证明。 设
若一个键的值是一张表,且表项可以彼此独立地添加和删除,那么该键就是可交换的;注册路由或事件监听器便是典型情形:两次注册无论以何种顺序进行,最终得到的表都会以相同方式回答每个测试;而且,任一注册都能在另一注册仍然存在时单独撤回。若一个键的值是一条有序链,那么它就不是可交换的,因为插在另一中间件之前的中间件会看到不同的请求,并且无论采用哪种顺序,都无法在不干扰另一项的情况下撤回其中一项。开篇示例中的分配器,则依据其接口所公开的内容而分属两种情况。若该键的任何操作都不会比较其发放的句柄,
组件所执行的是一个操作序列,其中每个操作都可能依赖先前操作产生的结果;以下定理讨论的,正是这种形态的效应函数。
定义 41. 余效中介的效应函数构成最小集合
仍然是该集合的成员。每个阶段执行一个操作,并依据该操作的结果选择后续步骤,因此,一个参数可以依赖已经获得的结果。某个成员中出现的操作,是该成员的各个阶段在每一种结果选择下所执行的操作。
定理 42. 设
证明。 对定义 41 的构造作归纳可知,
对于定义 19 的第 (1) 项,根据引理 18(1),只需证明
对于第 (2) 项,取
于是该阶段在
组件与其环境之间的每次交互都通过上下文进行,而类型族
这种分解所划分的,是计算中的可交换部分与顺序敏感部分。可交换部分由效应承载:组件按照自身任务所需的任意顺序执行这些效应,而推论 21 允许系统按照自己认为方便的任意顺序撤销它们,任意两个组件都不会彼此制约。顺序敏感部分则由余效承载,因为如果一个键的操作不可交换,其顺序就必须从效应外部施加,而有两个位置可以施加这种顺序。在单个组件内部,累加器施加顺序,以 LIFO 顺序撤销效应所做的一切(定理 16)。在组件之间,声明的余效施加顺序:一个组件提供另一个组件所声明的内容,并且“提供”先于“声明得到满足”发生(第 3.2.2 节)。由此,可组合性是在组件而非单个效应的粒度上获得的,而这正是第 4 节所采用的尺度。
该定理有两个值得明确指出的限制。其一,将每个共享位置绑定到一个键,是该范式要求遵循的纪律,而非构造本身固有的性质;因此,系统无法具体化为余效的位置,既位于第 6.1 节所述的系统边界之外,也随之位于该定理的适用范围之外。其二,一个键是否可交换,是该键所公开接口的性质;因此,满足可交换性是提供该键的组件所承担的义务,而不是消费该键的组件所承担的义务。
3.3.3. 上下文范式的定位
各种编程范式的根本差异,在于它们处理副作用的方式。两个既有的极点界定了这一光谱:
显式状态传递(函数式)。 为了保持引用透明性,纯函数式语言将副作用建模为对状态的显式变换。State 单子
隐式修改(命令式/面向对象)。 主流命令式语言允许组件修改共享状态并访问依赖,而无须在调用点显式声明。在效应一侧,一个代表性示例是 React 的 useEffect Hook:它会在组件的内部纤程(fiber)上注册一个持久效应,但效应目标和注册机制都不会作为显式参数出现——其标识依赖于隐藏运行时状态中的调用顺序位置。在余效一侧,Java 的服务定位器模式(例如 Spring 的 ApplicationContext.getBean(...))会在运行时从进程级注册表中取得依赖,因此每个调用点都需要进行空值检查和类型转换;依赖关系是隐式的,并散布于整个代码库。更一般地说,要理解 f() 如何修改系统或依赖系统,就必须传递式地阅读其实现。重构也会变得脆弱,因为移动或删除一次调用,可能会悄无声息地破坏远处的不变式。
上下文范式将函数式方法的可追踪性与命令式方法的人体工程学优势结合起来。效应和余效都通过一个显式上下文参数来中介。因此,每个操作都可归属于调用它的特定上下文,并进而归属于该上下文所属的组件。
上下文范式不仅结合了两个极点各自的优势,还允许开发者逐一处理每项效应和依赖,并自动将它们组合成系统行为。对于可逆效应,开发者只需提供每个原子操作的逆操作,任何复合操作的逆操作都会通过组合自动得到(第 3.1 节),因此组件的拆卸过程由其加载过程推导而来,无须另外手写一套拆卸逻辑。对于反应式余效,组件只需声明自身需要的依赖,运行时便会自动解析并重新连接这些依赖(第 3.2 节);随着提供者被添加、移除或替换,这些依赖始终能保持一致连接。在这两个方向上,原本需要依赖开发者纪律来保证的正确性,都转化为该范式的一项结构性性质。
4. 动态组合演算
第 3 节仅以局部形式建立了空间可组合性与时间可组合性。要把二者推广到整个系统,就需要将系统分解为若干组件;每个组件都把一份余效规约与一个带见证的效应函数配对,从而使与共享环境的每一次交互都可归属于其中某个组件。以下各节为这种分解赋予操作语义,并以全局形式建立空间可组合性与时间可组合性。
第 4.1 节和第 4.2 节给出能够用规则刻画生命周期的最小演算,其中假定每次迁移都是原子的、即时的且不会失败;第 4.3 节放宽这三项假设——其中原子性会按迁移可能运行的两个方向各放宽一次——纳入运行时可在一次迁移开始与结束之间插入的各种控制流形式,最终得到真实运行时所实现的演算;第 4.4 节则建立该演算的元理论,即保持性、全局时间可组合性与空间可组合性、进展性以及合流性。
4.1. 组件与纤程
本节确定规则所作用的对象:组件;纤程(fiber),即组件的一个实例化,它携带自己的生命周期状态;以及注册表,它保存一个状态所携带的纤程,并由此读出余效上下文。
组件。 一个组件由一个三元组给出,其余效侧被拆分为它从环境中读取的内容,以及它向环境提供的内容。
定义 43. 在同时承载效应与余效的上下文
它表示一个三元组
是定义 25 的余效规约,声明需要从环境中获得的依赖; 是供给,声明组件可能提供的余效键;其效应函数不会写入 之外的任何键; 是定义 8 的带见证效应函数,定义组件处于活跃状态时所贡献的效应,以及用于撤回这些效应的逆函数。
这两项声明构成同一个接口的两个方向:
本章与第 3.2.3 节的区别正在于要求供给集彼此不相交。定义 28 的隔离机制允许一个键经由隔离域表进行解析,因而两个纤程可以在不同隔离域中提供同一个键;若演算带有隔离域,就可以把“不相交”放宽为“在同一隔离域内不相交”,并根据声明某个键的纤程所处的隔离域来解析该键。这里不引入隔离域,而是让每个键都在一个共享隔离域中读取;正因如此,上述不相交条件才是正确的条件,并且每个键的提供者才是唯一的(定义 45)。这一条件限制的是组件能够被实例化的次数:供给集非空的组件同一时间只能有一个纤程;因此,下文出现的多个实例,来自不提供任何内容的组件——这也是仅消费依赖或注册其他组件的组件所处的常见情形。
运行系统中的组件实例会随时间而激活和停用,因此它携带一个生命周期状态;迁移则负责把它从一个生命周期状态推进到另一个生命周期状态:激活会执行

图 1|基础组件生命周期
纤程。 同一个组件可以被多次实例化,每个实例都携带自己的生命周期状态。我们把这样的实例称为纤程。一个纤程记录产生它的组件、它是在何纤程之下被实例化的、它所提供的余效,以及它目前处于生命周期中的哪个位置。
定义 44. 固定一个纤程名称集合
、 和 分别是定义 43 的余效规约、供给和效应函数; 是父级,即当前纤程是在其下被实例化的那个纤程,或者根标记 ; 是该纤程自身的余效表(定义 22);在纤程开始激活之前它为空,并在纤程的效应运行时由这些效应写入; 是退役标志;新建纤程中的值为 ,而编排器一旦将该纤程退役,其值便为 ; 是生命周期状态;在第 4.2 节的双状态模型中,它为
其中,
已提交视图
注册表。 一个状态按名称保存其纤程;纤程的身份,以及第 3.2 节的余效上下文,都从这种安排中读出。
定义 45. 以
它是一个有限偏函数,其父指针构成一棵以
纤程名称赋予纤程一个能够在自身发生变化后继续保持的身份:以下每条规则都只重写一个纤程的生命周期状态,而让其他纤程保持不变,因此规则必须指出它所作用的是哪个纤程;此外,还有两个字段引用纤程而非描述纤程,即父级
每个纤程各自拥有一张表,这意味着余效上下文并非被存储起来,而是派生而来:它就是所有活跃纤程共同提供的内容。
这个并集是良定义的,因为一个纤程只会写入其声明的键,即 set 操作;这些操作落入
于是,第 3.2.2 节的满足关系可以原封不动地应用,并以
4.2. 基础演算
本节只给出图 1 所示双状态生命周期的演算:每个纤程用来比较的目标,以及推动它前进的五条规则。
目标视图。 规则会把每个纤程与一个目标进行比较;该目标说明它是否应该运行,以及应当针对其依赖的哪一种解析结果运行。目标并非单个纤程自身的性质,因为纤程所声明的键需要针对整个状态进行解析;因此,目标是该状态上的一个谓词。
定义 46.
当每个纤程都已到达其目标视图时,状态是静止的:
目标仅取决于两件事,除此之外不取决于任何内容:一是经由
定义 44 的已提交视图与目标视图具有相同的类型,而生命周期由二者的比较驱动:fiber.committed 中,并把它的哈希值保存在 fiber.target 中(第 5.1.3 节)。
规则。 基础演算假定每次迁移都是原子的、即时的且不会失败:一次激活会在单个步骤中应用其效应函数,一次停用会在单个步骤中应用累加器,并且二者都必定成功。第 4.3 节将放宽这三项假设。
五条规则生成两种关系。以 O- 为前缀、记作 L- 为前缀、记作
插入与退役是仅有的外部输入:编排器请求某个纤程存在或停止存在,但绝不会直接设置其生命周期状态。O-Retire 不以纤程的状态为条件,因为退役只是一项请求,而真正执行这项请求的是生命周期规则。出于同样的原因,退役与移除彼此分离:一个已经退役但仍处于 O-Insert 的最后一个前提施加了单一来源规则:编排器不得接纳第二个声明同一键的组件,因此一个键只有一个可能的提供者。
L-Reload 在安装逆函数的同时安装已提交视图;L-Unload 应用逆函数并丢弃已提交视图。两者都由同一种比较驱动:当纤程没有已提交视图且其目标视图不为 L-Reload 触发;当纤程持有的已提交视图不等于其目标视图时,L-Unload 触发。这就是第 3.2 节的反应式规则,只不过它读取的目标除了响应余效之外,也会响应退役状态:只要目标视图发生变化,就会启动一次迁移,而不论是哪一方面使它发生了变化。
实例化。 一个组件在安装自身效应时,可以实例化另一个组件;插件宿主在某个插件加载它自己的插件时,做的正是这件事。到目前为止,规则只允许编排规则修改注册表,因此这种实例化无处发生。下面用一个原语为它提供发生的位置。
定义 47. 对 O-Insert,并以对注册所得纤程执行的 O-Retire 作为逆操作。该规则在满足 O-Insert 新鲜性前提的条件下抽取一个名称,并将该名称交给效应函数。
逆操作执行退役而非移除,原因在于逆操作无论在何处被执行,都必须能够适用。O-Remove 带有前提,因此用它构造的逆操作可能无法适用:若父级的子级仍处于 O-Retire 的唯一前提是
让一个子级退役会设置 O-Retire 是无条件的,父级不会被迫等待;因此,无论子级是否已经离开,L-Unload 都可以应用于父级。孙级则逐层触达:子级自己的累加器会让该子级所注册的组件退役。定理 66 会同时涵盖这一连锁过程,以及第 4.3.1 节沿余效施加的连锁过程。
局限性。 有了上述唯一的例外之后,就可以规定效应函数必须遵守的规则。它一方面限制一次应用可以写入的内容,使应用该函数的规则能够涵盖其他所有变化;另一方面限制一次应用可以读取的内容,使纤程只能看到自己所声明的余效,而不能看到注册表中的更多内容。限制写入,正是第 4.4 节能够把表 1 视作完整写入清单的原因。
定义 48. 若映射
(写入。)
;对于每个满足 的 ,都有 ;而 与 仅在 上有所不同。 (读取。) 若两个状态在
、每个 的限制 ,以及状态中未被任何纤程表命名的部分上都一致,则 会把它们映射到仍在这三方面一致的状态。
若效应函数
一次注册只会在其抽取的那个名称处写入 O-Insert 所写入的条目,除此之外不写入任何内容;作为逆操作产生的 O-Retire 只会写入该名称对应的
条款 (2) 说明了组件为何可以读取其声明的值:这些值位于其提供者的表中,因此,如果效应函数除了
这些规则是非确定性的:可能有多个纤程所持有的已提交视图不同于其目标视图,而该关系并不规定它们之间的执行顺序。这些规则也仅仅是反应式的,因为没有任何规则提到调度器;步骤可以是任意规则应用序列,所以,针对所有这类序列证明的定理,对运行时可能采用的每一种调度策略都成立。
4.3. 进行中的迁移
本节在四种情形下扩展基础演算。第一种情形补充了第 3.2 节所要求、但第 4.2 节无法表达的内容:一次停用可以延展为一段时间区间,而它的依赖者可以在这段区间内完成自己的停用。其余三种情形则放弃了“迁移是原子的、即时的且不会失败”这一理想化假设;真实运行时中的迁移并不具备其中任何一项性质。这里放弃的是“整个迁移只包含一个步骤”,而不是“一步只应用一条规则”;四种情形具有同一个结构性后果,这里统一处理:如果一次迁移不是一个步骤,那么它在进行期间就需要占据一个状态,并且迁移可能运行的每个方向都各需一个这样的状态。
定义 49. 本节的生命周期状态将
其中,
当纤程处于三个携带累加器和已提交视图的状态之一时,称该纤程已安装;当它携带一个错误结果时,称该纤程已失败:
若已安装的纤程
第 4.1 节的各项定义都延续到这个状态空间上,但需要明确两种解读。第一,第 4.2 节的 O-Insert 的结论中读作 O-Remove 的前提中读作
图 2 描绘了这些状态所形成的生命周期,下面四个小节则给出其各条边上的规则。

图 2|带有进行中迁移的生命周期;两种迁移状态以边框标出
4.3.1. 撤回
第 3.2 节要求:依赖方应当在其依赖项之后激活,而被依赖项只有在其依赖方停用之后,才能撤回自身提供的内容。前一半在基础演算中已经成立:一次激活要求
本层将该步骤一分为二,并用下列条件守卫其后半部分。
定义 50. 当某个其他已安装纤程把一个键解析到纤程
L-Leave 只记录停用决定而不立即执行停用:它让该纤程停止提供自身的余效,同时保持该纤程自己的已提交视图以及其他所有纤程的已提交视图不变。L-Unload 应用累加器、丢弃已提交视图,并使该纤程以其携带的结果进入
于是,顺序要求的两个部分由该形式中的不同部分分别承担:可见性部分由已提交视图承担,而 L-Unload 会把丢弃该视图作为它的最后一个动作;顺序部分则由前提
守卫是按绑定而不是按纤程施加的:
这种守卫通常会导致死锁。使这里免于死锁的是
守卫沿余效关系而不是沿纤程树来安排停用顺序:当一个子纤程仍处于
4.3.2. 迭代
一次激活可能依次执行多个效应,而停用必须将这些效应恢复。我们用效应迭代器对这种激活建模;它的每次迭代都会产出修改后的上下文、一个逆函数和一个续延:
定义 51. 将效应迭代器
其中,
是新的上下文; 是当前效应的逆函数; 表示续延: 表示迭代终止; 给出下一次迭代。
这里的见证是在定义 33 的
效应迭代器变换
定义 52. 效应迭代器变换
在每次迭代中,逆函数 yield 运算符 [43] 暴露的正是这种结构,因此该模型可以直接对应到这些语言已经提供的生成器上。
从这里开始,演算中的定义 44 所给出的
每次迭代都会按照定义 52,把新产出的逆函数以
普通效应函数(
4.3.3. 异步性
此前各层允许环境在一次迭代结束与下一次迭代开始之间发生变化,同时假定每次迭代自身都会瞬时完成,即启动与落定发生在同一个步骤中。我们对非即时性作抽象建模:一次迭代产出一个类型为
在这一模型下,一次迭代在某个状态下启动,在另一个状态下落定;在它处于执行中的这段时间里,纤程处于
这个备选分支正是基础演算无法表达的情形。在基础演算中,当迁移发现其目标视图已经转变时,会在发现它的同一步中撤销自身;而在这里,正在执行的迭代必须先落定,因此纤程需要一个状态来停留,以便运行它的逆函数。唯一健全的选择是进入 reload 与 unload 的相互链式调用。
一次停用也可以直接链回一次激活;这是通过规则复合而不是一条单独规则实现的。L-Unload 对目标视图没有任何前提,因此,无论纤程停用期间目标视图变成了什么,累加器都会运行,纤程也都会进入
4.3.4. 失败
到目前为止,每条规则都假定它所运行的效应会成功,但运行时不能作此假定。组件所安装的效应会触及追踪这些效应的上下文之外,而它们所触及的对象可能拒绝操作:端口可能已经被占用,文件可能并不存在,对端也可能没有响应。即使迁移失败,也必须恢复纤程的效应,而不能让这些效应滞留。
令
该见证只约束
L-Raise 先恢复,再记录。纤程进入
失败记录在纤程上,而不会传播至其父纤程;因此,一个组件的迁移失败后,其兄弟组件仍会继续运行。这正是插件宿主所期望的行为,也是结果属于各个纤程而非整个状态之属性的原因。
4.4. 元理论
第 4.3 节给出了十条规则:第 4.2 节的三条编排规则;用于激活的 L-Begin、L-Iter 和 L-Finish;表示激活提前结束的两种方式 L-Divert 和 L-Raise;以及用于停用的 L-Leave 和 L-Unload。本节从这些规则中读出两种可组合性的全局形式:无论其他纤程在其间做了什么,单个纤程的保证都仍然成立;此外,本节还加入了只有整个系统才能被要求满足的性质:系统总能到达其目标所要求的配置,并且该配置与静态组装所产生的配置相同。下文每项性质都是步骤序列的性质,因此我们为步骤编制索引,并从该索引读取状态的各个字段。
有两项约定将第 3.3.2 节带入本节。下文状态之间的每个等式,都像引理 38 解读第 3.1 节中的等式那样,在定义 33 的观察等价
定义 53. 以
表示在
第 4.3 节的每条规则都具有
其中,
例如,在 L-Unload 处,
关系
对于函数类型的字段——例如
表 1 将第 4.3 节的十条规则解读为上述写入操作。累加器、已提交视图和剩余迭代器都是
| 规则 | 被编辑的控制字段 | |||
|---|---|---|---|---|
| O-Insert | 未定义 | |||
| O-Retire | 无约束 | 不变 | ||
| O-Remove | 未定义 | |||
| L-Begin | ||||
| L-Iter | ||||
| L-Finish | ||||
| L-Divert | ||||
| L-Raise | ||||
| L-Leave | ||||
| L-Unload |
表 1| 各条规则对其所作用的纤程
引理 54. 将表 1 与定义 48 一并解读,则对每个步骤
仅当步骤
作用于 时,才可能有 ;该写入位于 内部。 只会在 时出现,只会在 时消失;因此,在 的一个活动期中, 关于 保持不变。 仅当
时,才有 ;没有其他步骤会将 应用于状态。 ,并且 。 、 、 和 与 的条目同时出现,此后再也不会被写入; 是单调的,只会被写为 ,且只有 O-Retire 会执行这一写入。
证明。 设
(1)
(2)
(3)查看第四列可知,累加器只出现在 L-Unload 处:其他规则采用前向映射
(4)
(5)第五列没有任何一行列出
接下来的三项查阅说明了规则看不见什么。第一项是:规则仅通过上述观察来读取状态,因此,整个演算都可下降到
引理 55(
证明。 第 4.3 节的每项前提都属于四类之一,并且每一类读取的组成部分都会被该关系保留。将
对于结论,根据定义 53,有
状态所携带的名称由上述观察中的两项读取,即
引理 56(等变性)。 设
证明。 前提读取名称时,只会将一个名称与另一个名称进行比较:要么直接比较,如 O-Insert 的新鲜性条件
因此,一个序列及其重命名会按相同顺序采用相同规则,并到达仅相差
第二项查阅是:一个除名称之外已被剥去所有内容的条目,对于规则而言不可见。正是这一点,使定义 47 能够在其恢复所得的状态不含某个纤程时退役该纤程,也使引理 72 能够移除被删除活动期所创建的注册。
引理 57(残留条目)。 若在
若一条规则可在
处作用于 ,则它也可在 处作用于 ;两次应用到达的状态仅在 的条目上有差异,并且该条目仍是残留的。 反过来,若一条规则可在
处作用于 ,则它也可在 处作用于 ;但抽取名称 或声明 中某个键的 O-Insert 除外。
证明。 对一条作用于
简化生命周期状态,并一并简化那些在其上进行匹配的规则,会得到一个子演算;并非每项结果都能在这种简化下保留下来。删除第 4.3.1 节是关键情形;从元理论一侧来看,这正是第 4.3 节开头所作的划分:该节的守卫建立了定义 58 的条款 (3) 和 (4),而定理 63 又依赖于该守卫所创建的区间,因此,一旦没有该节,这三者都不成立。其他三个小节所加入的内容则可被简化掉,而不影响下文结果;它们中的每一个都只是在定义 49 所确定的同一个状态空间上添加规则。
4.4.1. 保持性
定义 45 确定了注册表的形状;在下文结果能够为其增添性质之前,必须先依据该形状检查这些规则。本小节指出规则所保持的不变量,其中第一项条款就是该形状,其余条款则是后续结果所采用的假设。
定义 58. 若对于所有
; ; 在 上是全函数,且取值均属于 ; 。
条款 (1) 将定义 45 的树逐边读出,确保父指针落在注册表中。该定义还要求无环性,但这里不需要为此另设条款,因为指针所指名的纤程总是先于持有该指针、因而指名它的纤程完成注册。
定理 59(保持性)。 若
证明。 设
(1)根据表 1,只有 O-Insert 和 O-Remove 会写入
(2)O-Insert 的最后一项前提是
(3)根据引理 54(2),唯一会写入
(4)根据引理 54(2) 和 (4),该条款只可能在下列情形下于
该规则不会写入任意
L-Unload 上的守卫正是条款 (3) 和 (4) 得以成立的原因。O-Remove 的前提
4.4.2. 时间可组合性
局部时间可组合性使用一个累加器恢复一个效应序列(第 3.1.3 节)。注册表为每个纤程保存一个累加器,而各纤程会彼此交错执行:从
定义 60. 对于
在第 4.3.4 节适用之处,应将三元组理解为包裹在
并且还要对
这种意义下的独立性,正是迹理论作为原语采用的概念:可交换动作会在序列上生成一个等价关系,在该关系下,交换两个相邻且独立的动作仍会保持终点不变 [44];引理 71 针对这些规则给出的,正是这样的交换。这里采用族而非集合,是为了将同一组件的两个名称都保留在考察范围内:此时,该条件要求该组件的效应函数与自身独立,亦即要求
在这些条件下,定理 7 的单累加器不变量能够在交错执行中继续成立,并呈现为赋予时间可组合性实际内容的如下形式:运行一个逆函数,只会撤回该纤程的贡献,而不会撤回其他任何内容。
定理 61(恢复精确性)。 设步骤序列两两独立,
也就是说,在
证明。 对
此外,根据定义 48 与定义 47,
设
当规则为 L-Leave、L-Raise、中止迭代的 L-Divert,或
设
这就是在归纳假设后追加
推论 62(终态恢复)。 设步骤序列两两独立,并设
由 O-Remove 移除的纤程同样不会留下任何内容,因为其前提只允许
证明。 根据引理 54(4),
上述结果把两两独立性作为组件所满足的假设,而第 3.3.2 节正是用来解除这一假设的:当组件执行的每项效应都是某个键上的操作,并且每个键都可交换时,由这些操作构建的任意两个效应函数都是独立的(定理 42)。将该结果从效应函数传递到迭代器并不需要任何新条件:由余效介导的效应函数(定义 41)已经依据每个阶段所产生的结果来选择其后内容,而这正是迭代器在其续延中携带的内容。第 3.2 节的余效操作则是完全不需要假设的情形:组件在那里贡献的映射,是集合操作与相应限制操作的复合;只要两项操作涉及的键互不相交,它们就可交换,而定义 58 的条款 (2) 保证了不同纤程的供给彼此不相交。
4.4.3. 空间可组合性
局部空间可组合性要求组件遵守自身规约:只有在其依赖均已得到提供时才激活组件,并依据这些依赖对上下文的每次变化进行分类(第 3.2.2 节)。全局形式则加入了需要量化其他纤程的内容:提供者只有在所有曾将某项绑定解析到它的依赖方都已停用之后,才会撤回该绑定;而某次迁移安装其效应时所依据的解析,也不会在迁移执行期间从其下方发生偏移。余效一侧的两项性质分别给出这两项保证;二者将被一并证明,因为它们是同一个不变量的两个方面,即引理 54(2) 所建立的
定理 63(顺序性)。 纤程只会在其依赖均已得到提供时开始迁移:
进一步设
; ;并且,如果 闭合,则 ; ,且 。
证明。 第一个断言就是 L-Begin 的前提
(1) 即引理 54(2)。
对于 (2),
对于 (3),在
否则,一次分布在多个步骤上的迁移可能会安装基于某项解析计算出的效应,而这项解析在迁移执行期间已经发生变化;有两个前提阻止了这种情况。L-Iter 和 L-Finish 都带有
惯性使得上述性质无法成为关于每个步骤的保证。当目标视图发生变化时,一次已经在执行途中的迭代仍会依据 L-Divert 落定,而这次落定会安装基于某项已经不再成立的解析计算出的效应。因此,这些规则提供的是一个析取;正是第二个分支使第一个分支保持安全。
定理 64(解析相干性)。 设
当纤程离开该区间,即
,且 ; ,并且该活动期在某个 处闭合;与推论 62 相同,此时 。
证明。
对于上述二分情形,
4.4.4. 进展性
只有当一个将提供者撤回推迟到其依赖方全部离开之后的守卫最终会被释放时,它才能给出定理 63。注册表纤程上的一个关系承载了这一论证。
定义 65. 注册表各名称上的优先关系定义为
也就是说,
定理 66 和定理 73 都建立在
纤程的目标视图既取决于其提供者,也取决于创建该纤程的纤程。创建者通过定义 47 的原语写入
进展性断言的是存在某条可以应用的规则,因此,它是针对宿主必须提供的规则来表述的:L-Begin、L-Leave、L-Unload,迭代落定规则 L-Iter、L-Finish 和 L-Raise,以及 L-Divert。其论证从不诉诸 L-Divert 的中止型分支,所以,受第 4.3.3 节惯性约束的宿主同样包含在内。
定理 66(进展性)。 假设
为其目标视图发生变化的次数。则:
- (无死锁。)
蕴含在 处有某条生命周期规则可以应用; - (终止性。)
,并且 与 都是有限的。
因此,每个极大的生命周期步骤序列都终止于静止状态。
证明。 无死锁。 设
且 :L-Begin 可以应用; 且 :由 的值所选出的 L-Iter、L-Finish 或 L-Raise 可以应用; 且 :若 抛出错误,则 L-Raise 可以应用;否则 L-Divert 可以应用,并让该次迭代落定而不是将其中止; 且 :L-Leave 可以应用。
假设没有任何纤程属于上述任何一类,则还剩下某个满足
第二个成员关系来自定理 63(3):
终止性。 用以下两个断言界定
(A) 在
(B) 若
根据 (A),按区间计数便得到
根据 (B),
由于
是良基的,并且定义出的
目标所记录的是提供纤程,而不是一个布尔值;在第 4.2 节的单一来源约束下,二者会驱动相同的迁移,因为在那里一个键只有一个可能的提供者。视图带来的益处,是为上述结果提供表达词汇:定理 63 与定理 64 都谈论纤程激活时所依据的解析;它也使这些结果在第 3.2.3 节的作用域解析下仍然成立,因为在这种解析下,同一个键会在不同隔离域中解析到不同提供者,供给本身不再能唯一确定视图。实现携带了这种作用域,并把该视图保存在 fiber.committed 中(第 5.1.3 节)。
4.4.5. 合流性
迄今为止的结果都针对单个纤程。刻画整个系统的性质是:系统的动态历史不会留下任何痕迹。无论一个运行中的系统经历了怎样的激活与停用序列,它最终静止时所处的状态,都与下述过程产生的状态相同:采用相同的插入与退役操作,按照依赖顺序,将最终处于活动状态的每个组件各加载一次,并且不卸载任何组件。生命周期关系是合流的,而它所收敛到的正规形就是静态组装所得的正规形。对于动态组合而言,这对应于变化传播为增量计算所建立的性质:它与从头开始的求值保持一致 [45]。
该断言只涉及
首先需要三个引理。第一个引理不借助任何步骤序列,便确定最终成为
定义 67. 若一个纤程尚未退役、注册它的纤程受到支持,并且它所声明的每个键都由一个受到支持的纤程提供,则称该纤程在
当该关系良基时(引理 68),记
其中,
这些条款引用了
引理 68(支持关系是良基的)。 设
证明。 按照注册每个名称之步骤的索引,对
最后一个条款读取的是
定义 69. 若一个组件
与独立性(定义 60)一样,这是一个只涉及组件的条件,既不提及生命周期状态,也不提及步骤;而独立性已经界定了它能够失效到何种程度:如果某个组件仅在另一个组件的效应能够到达的上下文状态处才安装某个键,那么它的前向映射就不会与另一个组件的前向映射可交换。因此,一个纤程所安装的键由其组件而非调度确定。完全性额外要求的是,这一固定集合等于整个
引理 70(静止时的支持)。 设
证明。 记右侧为
根据定义 46,右侧成立当且仅当
引理 71(换位)。 设各步骤两两独立,
- 若两个步骤都应用激活规则——即 L-Begin、L-Iter 或 L-Finish——且步骤
在 处可应用,则步骤 也可在步骤 从 产生的状态处应用,并且两种顺序到达同一个 。 - 若步骤
在 处应用激活规则,步骤 在 处应用编排规则,并且步骤 不注册 ,则这两个步骤同样可以交换,且两种顺序到达同一状态。
证明。 对于 (1),根据表 1,
对于 (2),根据表 1,编排步骤满足
引理 72(删除)。 设步骤序列两两独立,每个组件都在其供给上是完全的(定义 69),该序列到达一个静止状态
证明。 被删除的这些步骤合起来,会使状态回到它们开始时的位置。设
其右侧正是
用一个不变量处理余下的后缀。记
没有任何保留下来的步骤会失去前提。一个作用于
定理 73(合流性)。 设一个步骤序列到达静止状态
- (典范形。) 从
出发,可以通过一个序列到达 ,但允许忽略规约化过程中撤回其条目的那些名称;该序列按照原有相对顺序执行相同的编排步骤,其中,作用于编排器所插入纤程的编排步骤先于所有生命周期步骤,其余编排步骤则分别紧随在注册其所作用纤程的步骤之后;对于 的一个将 线性化的枚举 ,该序列按此顺序让每个 恰好经历一个活动期。 - (合流性。) 从
出发、执行相同编排步骤的任意两个此类序列,在按引理 56 进行重命名之后,到达的状态同时由 和 关联。
证明。 对于 (1),序列中的活动期分为两类:一类已经闭合,另一类在
首先通过对闭合活动期的数量作归纳来处理它们。在每个阶段,选取一个纤程
接下来处理编排步骤。作用于编排器所插入之纤程的一个编排步骤,可以借助引理 71(2),逐次越过不同纤程的生命周期步骤而向前移动一个位置;该引理之所以适用,是因为
最后,通过对
对于 (2),根据 (1),两个序列都能规约为一个典范序列,而这两个规约所涉及的是同一个
该陈述排除了失败,因为失败确实会造成分歧,而不应把本演算理解为否认这一点:某个步骤是否抛出错误,取决于它运行时所面对的状态,所以一种调度可能使某个纤程失败,而另一种调度则可能让它完成;此时,两个静止状态中该纤程的生命周期状态并不相同。除此之外,二者不会有任何差异;推论 62 表明,失败纤程对状态的贡献为空。
在第 4.2 节的基础演算中,同一定理仍然成立,而证明只需删去一个条款,无须作其他替换。L-Unload 在那里不带守卫,所以引理 72 的最后一段无需再证;该引理的其余部分只诉诸
该定理使我们可以像面对静态组装的应用那样推理 Cordis 应用。一个编排器添加某个组件、移除它、替换某个提供者,再撤销这次替换之后,保证会到达这样一个状态:若从一开始就写下最终组合,所得到的也正是这个状态;而组件作者在推理哪些余效位于作用域内时,只需考察静止状态。该定理也界定了这项保证的边界:它谈论的是状态,而不是系统沿途产生的发出;第 6.1 节以获取与发出之间的区别表达了这一点——获取留在边界内并受到追踪,发出则跨越边界。
5. 实现与案例研究
本节介绍 Cordis,它将第 3 节的形式模型实现为一种实用的编程抽象。Cordis 是一个面向时空可组合性的元框架:与针对特定领域的应用框架(例如 Web 路由、ORM、UI 渲染)不同,它不规定任何具体场景;它的唯一职责是提供通用的动态组合语义。其实现分为三个层次:(1)核心库(第 5.1 节)直接实现效应系统和余效系统;(2)组件加载器(第 5.2 节)在核心库之上扩展配置协调和热模块替换;(3)Koishi(第 5.3 节)等应用框架在前两个层次之上构建领域特定功能。
5.1 核心库
表 2 总结了理论构造与其运行时对应物之间的关系。具体来说,本节通篇使用下文引入的运行时名称,而将理论符号保留用于说明形式上的对应关系。我们还用 @@name 表示框架内部的符号键,因此 ctx[@@store] 中的方括号表示通过符号键访问上下文中的不透明槽位,而不是对以字符串为键的映射进行索引。
| 理论(第 3 节、第 4 节) | 实现 |
|---|---|
ctx,一等上下文 | |
| 上下文树,以及运行中的系统曾触及的一切 | |
| 返回/产出逆操作的效应回调 | |
ctx.effect(callback) | |
ctx[@@store], ctx[@@isolate], ctx[@@intercept] | |
ctx.get(key), ctx.set(key, value) | |
ctx.isolate(key, realm) | |
ctx.intercept(key, metadata) | |
fiber, | |
通过 ctx.registry 枚举 | |
fiber.uid | |
fiber.inject | |
组件的 provide | |
fiber.apply | |
fiber.parent.fiber.uid,即拥有该组件实例化所在上下文的纤程(fiber) | |
| 派生实现(定义 27) | fiber.ctx,纤程在其中运行的子上下文 |
fiber.state,生命周期状态;其中 LOADING 为 FAILED 为 | |
recover,累加器 | fiber.dispose,即该累加器 |
fiber.committed,已提交的视图 | |
一个 Impl,其提供者纤程处于 ACTIVE 状态 | |
fiber.target,由 refresh(算法 5)重新计算,其中 INACTIVE | |
fiber.inertia,进行中迁移的句柄 | |
O-Insert, O-Retire(定义 47) | ctx.use 及其回调的逆操作(算法 4) |
O-Remove | 纤程从其运行时中移除,同时清除 uid |
L-Begin, L-Iter, L-Finish | execute 的迭代循环(算法 1) |
L-Divert | 在迭代边界处守卫条件失败(算法 1),或 reload 链接至 unload |
L-Leave | refresh 将纤程标记为 UNLOADING(第 10 行) |
L-Unload | unload 及其惯性链接(算法 5) |
L-Unload 上的守卫条件 | unload 等待已收到通知的依赖者(第 25 行) |
L-Raise | 错误记录在纤程上,并将其目标设为 |
表 2|理论与实现的对应关系
本节余下部分将自底向上构建核心库。第 5.1.1 节实现可逆效应——它是改变上下文的唯一原语;第 5.1.2 节在其上实现反应式余效;第 5.1.3 节将二者组合成组件生命周期;第 5.1.4 节则公开基于它们构建的上下文级操作。
5.1.1 效应追踪
本节实现可逆效应(第 3.1 节)。Cordis 中的每一次上下文变更都流经唯一的原语 ctx.effect:余效供给、组件实例化以及其他所有改变上下文的操作,最终都归约为一次 ctx.effect 调用。因此,任何通过上下文执行的操作都会被自动追踪,并在组件卸载时恢复。从操作层面看,ctx.effect 是 dispose 闭包;调用该闭包时,会恢复这一效应。Cordis 通过这一个操作同时接受
算法 1 展示了 ctx.effect 的构造。我们用 id 表示空操作;因此,将每个新的逆操作前置,就能得到后进先出(LIFO)的恢复顺序。
算法 1 效应追踪
1 async function execute(callback, guard)
2 iter ← callback()
3 inverse ← id
4 while guard()
5 (value, done) ← await iter.next()
6 if value then inverse ← value ∘ inverse
7 if done then break
8 return inverse
9 function effect(ctx, callback)
10 armed ← true
11 task ← execute(callback, () ↦ armed)
12 async function dispose()
13 if not armed then return
14 armed ← false
15 recover ← await task
16 recover()
17 ctx.dispose ← dispose ∘ ctx.dispose
18 return dispose引擎 execute 将回调作为效应迭代器(done 标志与 guard 共同实现。
ctx.effect 是 execute 之上的一层轻量包装,额外加入了两项机制。第一,自处置:守卫返回 armed 标志,而返回的 dispose 会将 armed 翻转为 false;这既会停止任何正在进行的迭代,又能保证恢复至多触发一次。若触发两次,第二次就会把逆操作应用到一个并非由该效应的应用所产生的状态上,此时没有任何条件能保证它确实会恢复什么。第二,父级组合:dispose 被前置到外围上下文累积的逆操作 ctx.dispose 中,因此,子效应的逆操作本身就是父级上的一个效应;这正是 execute,但其守卫条件检测的是 fiber.target 的稳定性,而非 armed。
5.1.2 余效操作
本节实现反应式余效(第 3.2 节)。所有余效操作都作用于每个上下文携带的三个符号键槽位:
@@store:值存储,从领域符号映射到有类型的值; @@isolate:领域表,从余效键映射到领域符号; @@intercept:拦截表,为每个键分配其元数据。
前两个槽位组合成两层解析 ctx.get(key)(算法 2)先从 @@isolate 读取领域符号 @@store 读取绑定值 @@intercept 只在访问绑定时才会被查询,它调整的是绑定的使用方式,而不是绑定解析到什么。我们分两部分实现这些操作:(1)供给与通知,负责安装或撤回绑定,并将变化传播给依赖者;(2)隔离与拦截,负责重塑键的解析方式。
供给与通知。 由于 ctx.effect 调用,并继承其自动追踪和恢复机制。算法 2 实现了 ctx.set(key, value),即具体的 dispose 函数则移除该值。安装和移除都会调用 notify,将变化传播给依赖组件。
算法 2 余效操作
1 function get(ctx, key)
2 realm ← ctx[@@isolate][key] ▷ 𝜌(𝑘)
3 return ctx[@@store][realm] ▷ 𝜎(𝜌(𝑘))
4 function set(ctx, key, value)
5 function callback()
6 realm ← ctx[@@isolate][key] ▷ 𝜌(𝑘)
7 ctx[@@store][realm] ← value ▷ 𝜎[𝜌(𝑘) ↦ 𝑣]
8 notify(ctx, [key])
9 return function()
10 delete ctx[@@store][realm] ▷ 𝜎 ∖ 𝜌(𝑘)
11 notify(ctx, [key])
12 return ctx.effect(callback)算法 3 将每一次绑定变化传播给依赖者:对于每个存活的纤程,它检查发生变化的键是否出现在 fiber.inject 中,并且是否解析到同一个领域;若是,便调用 refresh(第 5.1.3 节),依据新状态重新求值该纤程;算法还会返回所有被重新求值的纤程,以便调用者等待它们完成。这就是定义 26 中的反应式分类:若某个变化使满足性发生翻转,它就会激活或停用纤程;而 refresh 的幂等性使中性变化不产生影响。第 5.1.3 节将进一步阐述这种重新求值与不同控制流之间的交互。
算法 3 反应式通知
1 function notify(ctx, keys)
2 affected ← ∅
3 for fiber in all_fibers do
4 for key in keys do
5 if key ∈ fiber.inject and fiber.ctx[@@isolate][key] = ctx[@@isolate][key] then
6 refresh(fiber)
7 affected ← affected ∪ {fiber}
8 break
9 return affected由某个纤程安装的绑定,只有在该纤程处于 ACTIVE 状态时,才会被依赖者视为可用。因此,refresh 会针对活跃的提供者解析每个已声明的键,而不是仅查询存储。这就是定义 46 中的 provided by 关系;也正因如此,撤回会在实际发生前一步对依赖者可见:一旦提供者进入 UNLOADING,它便已停止提供,于是其依赖者会重新计算出一个未满足的目标视图,并在该提供者的所有绑定仍然存在时开始自身的拆卸。
隔离与拦截。 这两个操作在结构上执行相同的工作:二者都派生出一个子上下文,针对 key 调整一张继承而来的表,同时保持父上下文不变。因此,恢复是隐式的:丢弃子上下文即可,无需运行显式的逆操作。ctx.isolate(key, realm) 用 realm 覆盖领域映射 realm,则默认使用一个新生成的符号(实现 isolate,定义 29)。于是,为同一个键分配不同符号的两个上下文会解析到彼此独立的绑定。ctx.intercept(key, metadata) 将元数据合并进拦截表 intercept,定义 31):按照该定义,新元数据会与上下文中 key 已有的元数据组合,并优先于已有元数据。
5.1.3 组件生命周期
组件通过 ctx.use 实例化为纤程。本节赋予第 5.1 节引入的纤程以操作含义:它就是第 4.3.3 节中的惯性状态机。以下算法由两个字段驱动:fiber.parent,即 fiber.ctx 的父上下文,它构成组件层级(fiber.inertia,即进行中的异步迁移句柄(空闲时为 null)。
算法 4 展示组件实例化。组件将余效规约 component.inject(component.apply 配对;实例化把组件的 config 绑定进 fiber.apply(第 9 行),得到应用了配置的效应函数(callback 函数(第 2 行)是在父纤程中追踪的效应:执行时,它通过调用 refresh(算法 5)启动子纤程的生命周期;恢复时,它强制把子纤程的目标设为 unload。这就是定义 47 的注册原语,其中 callback 是其 O-Insert,而 callback 返回的闭包是其 O-Retire:实例化是父级的普通受追踪效应,因此卸载父级会级联卸载其子级。
算法 4 组件实例化
1 function use(ctx, component, config)
2 function callback()
3 refresh(fiber)
4 return function()
5 fiber.target ← ⊥
6 unload(fiber)
7 fiber ← Fiber(parent: ctx, inject: component.inject)
8 fiber.ctx ← ctx[fiber ↦ fiber]
9 fiber.apply ← () ↦ component.apply(fiber.ctx, config)
10 ctx.effect(callback)
11 return fiber算法 5 实现第 4.3.3 节的惯性状态机,其中 reload 和 unload 都具有惯性:迁移一旦进入,就会运行至完成,之后系统才会响应目标状态的变化。它对余效存储使用两个辅助查询:resolve(inject) 返回当前由已声明的键解析出的绑定,provided(fiber) 返回由该纤程安装了绑定的键。refresh 函数从余效存储重新计算 fiber.target;若纤程尚未处于迁移中,则根据目标启动 reload 或 unload 任务2。reload 函数记录当前目标,并执行组件的效应函数 apply。完成后,它检查目标是否仍然匹配:若匹配,纤程进入 ACTIVE;若不匹配(无论新目标是 unload。与之对称,unload 按后进先出顺序恢复所有受追踪效应,随后进入 INACTIVE,或链接至 reload。这种相互递归实现了惯性性质:一旦某次迁移开始,它就会先完成,之后任何新迁移才能开始。
算法 5 组件生命周期
1 function refresh(fiber)
2 target ← target(𝛾, 𝑛)
3 if target = fiber.target then return
4 fiber.target ← target
5 if fiber.inertia then return
6 if target ≠ ⊥ then
7 fiber.state ← LOADING
8 fiber.inertia ← create_task(reload(fiber))
9 else
10 fiber.state ← UNLOADING ▷ 在调度任何逆操作之前停止服务
11 fiber.inertia ← create_task(unload(fiber))
12 async function reload(fiber)
13 target0 ← fiber.target
14 fiber.committed ← resolve(fiber.inject) ▷ 提交视图
15 recover ← await execute(fiber.apply, () ↦ fiber.target = target0)
16 fiber.dispose ← recover ∘ fiber.dispose
17 if fiber.target = target0 then
18 fiber.state ← ACTIVE
19 notify(fiber.ctx, provided(fiber))
20 fiber.inertia ← null
21 else
22 fiber.state ← UNLOADING
23 fiber.inertia ← create_task(unload(fiber))
24 async function unload(fiber)
25 await all(notify(fiber.ctx, provided(fiber)).map(f ↦ f.await())) ▷ 等待依赖者全部完成退出
26 await fiber.dispose()
27 fiber.dispose ← id
28 fiber.committed ← ⊥
29 if fiber.target = ⊥ then
30 fiber.state ← INACTIVE
31 fiber.inertia ← null
32 else
33 fiber.state ← LOADING
34 fiber.inertia ← create_task(reload(fiber))fiber.target 的计算方式,是针对当前余效存储解析每个已声明的键,并将提供该键的纤程之 uid 组成元组,因此它是 uid 每次都会重新生成且绝不复用,因此,即使替代前后的两个提供者给出相等的值,也不会把新提供者误认成它所替代的旧提供者。由于 notify(第 5.1.2 节)会在每次余效变化时重新计算目标,因此,仅当纤程声明的某个键开始由不同纤程提供时,该纤程才会重新加载。所以,提供者在原地覆写自身绑定的行为不会被观察到;若组件希望其替换传播出去,就应撤回绑定并重新安装。
该算法在两个互补层级上运作。在迁移层级,reload 和 unload 会在完成时检查目标,从而支持跨迁移的惯性链接。在每次迁移内部的迭代层级,效应执行(算法 1)会在每个迭代边界检查目标,从而支持单次迁移内的部分回滚。这两种机制分别对应第 4.3.3 节的迁移间链接,以及定理 64 所依赖的迁移内陈旧性检查。
有三行承载着定理 63 的余效顺序,而它们各自所在的位置正是该顺序得以成立的原因。reload 在第 14 行提交已解析的视图,而 unload 只有在每个逆操作都运行后才丢弃该视图,因此,只要纤程仍处于已加载状态——包括其自身的拆卸期间——它所读取的始终是同一组绑定。refresh 在创建迁移任务之前,先于第 10 行把纤程标记为 UNLOADING;这就是 L-Leave 步骤:该纤程停止提供,而依赖者会据此重新计算,且这一切发生在调度该纤程的任何逆操作之前。随后,unload 在第 25 行等待每个收到通知的依赖者进入 INACTIVE,这就是 L-Unload 上的守卫条件;只有当依赖者声明的键解析到与提供者相同的领域符号时,notify 才会纳入该依赖者。这是该守卫条件之要求的运行时形式:依赖者必须从这个纤程取得该键,而不能只是声明该键。等待位于整个恢复过程之前,而不是置于某个正被等待的逆操作内部,因为 fiber.dispose 会并发启动一个纤程的各个效应;若把等待放在其中一个效应内部,其余效应仍将没有顺序约束。终止性来自定理 66:纤程只会等待那些已经无法被满足的依赖者;若某个依赖者自身也是提供者,它也会以同样方式等待自己的依赖者。因此,提供者图是在需要时遍历的,而不是预先分析的。
2 create_task 调度一个异步函数并发运行,并返回它的句柄(存储在 fiber.inertia 中)。为保持语言无关性,我们将它显式写出:在采用急切调度的语言中(例如 TypeScript 的 Promise),调用是隐式的,返回的 Promise 就是句柄;而在采用惰性调度的语言中(例如 Python 协程、Rust future),宿主必须生成该任务,它才会继续推进。 ↩
5.1.4 上下文访问
第 5.1.2 节中的余效操作构成了一套反射式 API:通过 ctx.set(key, value) 写入余效,通过 ctx.get(key) 读取余效,二者都以名称作为键。在这套反射式 API 之上,Cordis 又提供了一种更贴近语言原生风格的方式来扩展和使用上下文:属性访问。组件可以像访问上下文自身的原生结构一样,通过属性 ctx[key] 访问余效,而无须调用方法。在 TypeScript 中,Cordis 使用 Proxy 来实现这一点,其 get 陷阱会中介每一次属性访问。算法 6 展示了上下文如何在第 5.1.2 节的基础 get 操作之上,将这类访问解析为余效。
算法 6 由代理中介的上下文访问
1 function resolve(ctx, key)
2 fiber ← ctx.fiber
3 repeat
4 if key ∈ fiber.committed then return fiber.committed[key]
5 if key ∈ fiber.inject then throw INACTIVE_ACCESS
6 if fiber = root then throw UNDECLARED_ACCESS
7 fiber ← fiber.parent.fiber算法 6 从发起访问的上下文开始,沿纤程链向上遍历:一旦遇到首个其已提交视图绑定了 key 的纤程,就授权此次访问并返回该绑定;如果遍历到某个声明了 key 却尚未提交它的纤程,则说明该纤程尚未加载,访问失败;如果一直到达根纤程都没有任何声明,则以“未声明”为由拒绝访问。这正是代理与裸 ctx.get 的区别所在:ctx.get(key) 只在存储中查找,返回已绑定的值或空值,而且永远不会失败;代理则依据发起访问的纤程自身视图进行解析,并在使用点强制执行余效规约
这种拒绝是在访问发生时执行的运行时检查。由于组件的余效规约 ctx[key]。第 6.4 节将讨论宿主语言的类型级依赖声明与编译期元编程如何恰好实现这种中介。
5.2 组件加载器
核心库为组件开发者提供了用于动态组合的命令式原语,例如 ctx.effect、ctx.use 和 ctx.set。应用编排者面对的则是另一项独立关注点:他们需要将预先存在的组件组装成一个运行中的系统,并在系统的整个生命周期内调整其组合方式。组件加载器通过引入声明式配置层来处理这一关注点:编排者以持久化数据结构的形式规定期望的组合,而加载器则把该规约的变化转化为相应的命令式纤程操作。
5.2.1 声明式配置
第 4 节将一个运行中的系统分解为纤程,每个纤程都是某个组件的一次实例化。一次实例化所需的一切都可以声明出来,因此,编排者可以用声明式配置描述整个系统:这是一份持久记录,由加载器将其实现为纤程,并使其始终与这些纤程保持同步。
条目。 配置由条目组成。每个条目都规定并管理一个纤程,而且二者之间的绑定是双向的:当条目的字段发生变化时,加载器会相应调整纤程;当组件修改自身配置或禁用自身时,这一变化也会被写回其条目。
定义 74. 一个条目声明单个纤程,并记录:
id——稳定标识符;当条目所在分组的子项列表发生变化时,用作协调键;url——要实例化的组件模块 URL;isolate——应用于该条目上下文的隔离标注;intercept——应用于该条目上下文的拦截标注;config——绑定到组件、从而形成其效应函数apply的配置;disabled——该条目是否已被管理性关闭。
条目之所以能够充当忠实的规约,是因为支撑一个纤程所需的信息,恰好就是条目所记录的信息。定义 67 的支撑集读取且仅读取 disabled 给出 url 则选定声明
这些条目组成一棵配置树,它是系统加载内容的权威记录。条目可以是映射到单个纤程的叶节点;它的组件也可以继续加载其他组件,使该条目成为分支节点。Cordis 为这种分组式和嵌套式加载提供了相应组件:@cordisjs/group 以子条目列表作为配置,并将其作为一个子组加载;@cordisjs/include 则加载外部配置文件(YAML 或 JSON),并把其中的条目作为嵌套子树嫁接进来。两者都是建立在定义 47(算法 4)的注册原语之上的普通组件,因此,嵌套树仍处于该演算之内,下文的结果也同样适用于它。
协调。 当条目的记录发生变化时,加载器会进行增量协调,而不是拆掉整个纤程再从头重建。元理论给出了这种协调方式之所以可靠的理由。
- 定理 73 使静止状态仅成为最终配置的函数:无论加载器在此过程中执行了哪些实例化与退役操作,也无论这些操作采用何种顺序,系统最终都会静止在这样一个状态——从头加载最终配置也会得到同一状态。只要每个组件都会安装自己声明的每一个键(定义 69),最终加载哪些组件便可仅从声明中读出;如果某组件声明了一个键,却只在部分配置下安装该键,加载器仍然能够协调该组件,不过此时已加载组件的集合也会取决于这些配置。
- 定理 66 证明了系统确实会达到静止状态,因此,一旦协调所需的实例化与退役操作均已发出,本次协调最终便会完成。
- 推论 62 表明,即将离开的纤程对状态的贡献归于无,因此,重建某个条目会撤回其纤程安装的内容,同时让周围的纤程保持原状。
- 定理 63 允许同时实例化各个条目,编排者无须安排加载顺序:如果某纤程所声明的键尚未得到提供,它会在自己的 L-Begin 处等待;如果其提供者离开,它会先于提供者被停用。因此,依赖约束的是纤程何时激活,而不是何时获取并求值其模块;加载器由此可以并发加载模块,而大型配置的启动时间主要就花在这些模块加载工作上。
在条目所声明的纤程之上,加载器会根据条目中发生变化的字段进行分派,并针对每个字段采用干扰最小的操作。
id、url——重建条目,因为条目的身份或组件已经改变;isolate——重新分配条目的域(算法 7);intercept——原地更新,因为拦截元数据是在读取时查询的,无须重新加载;config——交给组件,由组件决定如何应用新的载荷;通常做法是将其与上一份配置求差异,仅在发生实质变化时才重新加载。特别地,@cordisjs/group条目的config就是其子条目列表,因此它会以子项id为键,对更新执行差异比较,逐个创建、移除或更新子项;由于更新一个仍然存在的子项会再次进入同一套逐字段分派,分组协调与条目更新会共同沿配置树递归向下进行;disabled——设置时卸载纤程,清除时重新加载纤程。
受管域。 核心库中的隔离会派生出一个子上下文,并在某个键上覆写域表 isolate 字段会为每个键选择两种作用域规则之一。值为 true 表示要求一个局部域:它为该条目私有,以条目的 id 为标记,并且无论条目移动到哪里都会随其一同移动;字符串值则表示要求一个全局域:所有指定该字符串的条目共享此域,因此,移动这样的条目会改变它与哪些条目共享绑定,而不会改变它属于哪个域。一旦不再有任何条目指定某个域,该域就会被丢弃。
重新分配条目的域时,需要根据以下三点采取操作:哪些键改变了域;条目本身是否就是某个已更改键的提供者;以及需要通知哪些依赖方。其中第二个问题最棘手,因为同一个域符号可能由多个纤程共享,而其中只有一个是提供者。加载器通过分隔符来回答这个问题:每个键对应一个符号
算法 7 隔离域重新分配
1 function patch_isolation(entry, 𝜌′)
2 𝜌 ← entry.ctx[@@isolate]
3 store ← entry.ctx[@@store]
4 Δ ← {𝑘 | 𝜌(𝑘) ≠ 𝜌′(𝑘)} ▷ 域发生变化的键
5 for 𝑘 in Δ do
6 entry.ctx[𝛿𝑘] ← fresh tag
7 diff[𝑘] ← (𝜌(𝑘), 𝜌′(𝑘), entry.ctx[𝛿𝑘], store[𝜌(𝑘)].fiber.ctx[𝛿𝑘])
8 entry.ctx[@@isolate] ← 𝜌′
9 reload(entry.fiber)
10 for 𝑘 in Δ do
11 (𝑠1, 𝑠2, 𝑑1, 𝑑2) ← diff[𝑘]
12 if 𝑑1 = 𝑑2 and store[𝑠1] and not store[𝑠2] then ▷ 该绑定属于条目自身
13 store[𝑠2] ← store[𝑠1]
14 delete store[𝑠1]
15 function affected(fiber, 𝑘)
16 (𝑠1, 𝑠2, 𝑑1, 𝑑2) ← diff[𝑘]
17 return fiber.ctx[@@isolate][𝑘] ∈ {𝑠1, 𝑠2} and (fiber.ctx[𝛿𝑘] = 𝑑1) ≠ (𝑑2 = 𝑑1)
18 notify(entry.ctx, Δ, affected) ▷ 代替算法 3 中的域检验这一检验取决于分隔符的一项性质。
将这一条件记为
5.2.2 热模块替换
热模块替换(HMR)在模块层面应用了可逆效应模式:当源文件发生变化时——通常是在开发期间——系统会原地替换受影响的模块,而无须重启进程。由于纤程已经界定了其组件的全部效应和余效,本身就是组件的模块只需通过纤程操作即可完成替换:处置旧纤程会撤回该组件安装的一切,而从重新加载的模块实例化一个新纤程,则会重新安装这些内容。因此,与 Webpack [46] 或 Vite [47] 的 HMR 不同,Cordis 的 HMR 不需要由开发者标注接受边界。
@cordisjs/hmr 组件提供 HMR 引擎,其运行分为三个阶段。
阶段 1:模块分类。 引擎接收两个输入:stashed 集合(自上次重新加载以来内容发生变化的文件 URL)与 externals 集合(无法热替换、因而会触发完整重启的模块)。用 get_imports(url) 表示 url 直接导入的模块;引擎据此对这些变更的依赖子图进行分类,将每个模块标记为 accepted 或 declined:
算法 8 模块分类
1 function classify(stashed, externals)
2 accepted ← stashed
3 declined ← externals
4 pending ← ∅
5 for url in stashed do
6 pending ← pending ∪ (get_imports(url) ∖ (accepted ∪ declined))
7 repeat
8 progress ← false
9 for url in pending do
10 if get_imports(url) ∩ accepted ≠ ∅ then
11 accepted ← accepted ∪ {url}
12 pending ← pending ∖ {url}
13 progress ← true
14 else if get_imports(url) ⊆ declined then
15 declined ← declined ∪ {url}
16 pending ← pending ∖ {url}
17 progress ← true
18 else
19 pending ← pending ∪ (get_imports(url) ∖ (accepted ∪ declined))
20 until not progress
21 declined ← declined ∪ pending
22 return (accepted, declined)以 stashed 文件所导入的模块为初始种子,这个不动点过程会在某个模块的任一导入已被接受时接受该模块,并在其全部导入均已被拒绝时拒绝该模块;任何仍未确定、陷在导入环中的模块,默认都会被拒绝。
阶段 2:过期条目检测。 随后,引擎利用 accepted 和 declined 将组件条目筛选为其中的过期条目,也就是依赖树能够到达已变更模块的条目。它使用 get_dependencies 遍历每个条目的依赖树;该函数以 declined 为边界,收集模块的传递导入:
算法 9 过期条目检测
1 function get_dependencies(root, declined)
2 deps ← ∅
3 function traverse(url)
4 if url ∈ deps or url ∈ declined then return
5 deps ← deps ∪ {url}
6 for child in get_imports(url) do traverse(child)
7 traverse(root)
8 return deps
9 function detect(entries, accepted, declined)
10 stale_entries ← ∅
11 for entry in entries do
12 tree ← get_dependencies(entry.url, declined)
13 if tree ∩ accepted ≠ ∅ then
14 accepted ← accepted ∪ tree
15 stale_entries ← stale_entries ∪ {entry}
16 return stale_entries当且仅当一个条目的依赖树与 accepted 相交时,该条目才是过期条目;随后,这棵依赖树也会并入 accepted,使沿途每个过期模块的缓存都在下一阶段失效。
阶段 3:事务式重新加载。 最后,引擎重新加载过期条目。它会使 accepted 模块的缓存失效3,同时备份每一个被移除的模块以支持回滚;随后,它按各过期条目的 url 重新导入其组件模块,并换入一个全新的纤程:
算法 10 事务式模块重新加载
1 function reload(ctx, accepted, stale_entries)
2 backup ← invalidate_caches(accepted)
3 try
4 for entry in stale_entries do
5 entry.fiber.dispose()
6 entry.fiber ← ctx.use(import(entry.url), entry.config)
7 catch error
8 restore_caches(backup)
9 for entry in stale_entries do
10 entry.fiber.dispose()
11 entry.fiber ← ctx.use(backup[entry.url], entry.config)
12 throw error事务保证确保系统绝不会进入只重新加载了一半的状态:如果任何模块导入失败(例如存在语法错误),缓存就会被恢复,而且每个过期条目都会使用 backup[entry.url] 重建;后者正是刚刚恢复缓存的旧组件,由此撤销已经完成的纤程替换。
5.3 案例研究:Koishi
Koishi 是一个基于 Cordis 构建的开源聊天机器人应用框架4。经过四年多的发展,它已经积累了 4000 多个由社区贡献的插件5,涵盖即时通信(IM)适配器、数据库驱动、管理控制台和面向最终用户的功能。它的规模与多样性,使其成为在生产环境中验证 Cordis 动态可组合性的代表性案例。
元框架的表达力与通用性。 Koishi 以服务端机器人形式运行,其中每一项功能都实现为建立在第 5.1 节上下文原语之上的插件;Koishi 自身只提供聊天机器人领域的词汇。同一种模型还出现在完全不同的运行时中:Koishi 的 Web 控制台是另一个独立的 Cordis 应用,其插件组合的是浏览器及其用户界面的原语,而非服务端原语。上述截然不同的场景确立了第 3 节模型的两项性质。(1)它具有表达力:其原语足以承载一个完整的生产系统,宿主框架只需提供领域词汇。(2)它具有通用性:它规定效应与余效如何组合,却把二者的含义留给各个应用决定,因此既不预设特定领域,也不预设特定运行时。
无需额外认知负担的时间可组合性。 第 1.2.1 节所考察的插件系统无法卸载单个扩展的效应,除非重启扩展宿主。Koishi 经常执行这种操作:编排器从控制台禁用某个插件,其效应便会原地撤回;在开发期间,HMR 引擎会在保存时重新应用经过编辑的插件,同时保留缓存状态以及系统其他部分的活动连接。Cordis 不仅使这种移除成为可能,还让插件作者能够毫不费力地做到这一点。由于通过上下文执行的效应都会受到追踪,其逆也会自动组合(第 3.1 节),即便缺乏经验的作者没有编写卸载路径,也能让插件中经上下文中介的效应得到有序清理。这实现了第 1.2.1 节所指出其缺失的关注点局部性:原本有赖于每位作者尽责才能保证的正确性,转而由这一抽象一次性承担。
跨开放生态系统的空间可组合性。 与第 1.2.1 节所述、插件间依赖关系基本缺失的插件系统不同,Koishi 的生态系统呈现出真正的依赖拓扑:即时通信适配器提供对各个消息平台的访问,数据库驱动提供持久化存储,功能插件则将这些能力声明为余效并加以访问。在运行时重新配置提供方,例如切换存储后端或重新连接适配器,只会重新激活那些已解析依赖发生变化的依赖方(第 3.2 节);依赖不可用的插件会保持非活动状态,直到该依赖出现,而不会报错。这个案例研究所证实的是,这种组合能够跨越由不同作者独立编写的代码而成立:插件及其依赖通常由不同作者编写,彼此之间除了连接它们的余效之外无需进行任何协调;因此,反应式余效能够使这个由独立贡献者组成的开放生态系统始终保持组装一致性。
有效性威胁。 此处的证据来自采用单一宿主语言的单一生态系统,因此无法将这一范式本身的优点,与其 TypeScript 实现或 Koishi 特定领域的优点区分开来;而且这些证据来自观察,并非与另一种架构进行的受控比较。因此,这项案例研究所得出的是一个关于该范式确实存在且已获采用的结果,而不是定量结果;衡量这一抽象的开销,并以某个基线为参照评估它对开发者生产力的影响,仍有待未来研究。
3 在 Node.js 上,这意味着同时清除 ES 模块系统与 CommonJS 模块系统的缓存,因为通过 ES 加载器导入的模块可能同时出现在二者之中。 ↩
4 Koishi 目前使用 Cordis v3。本文介绍的是 Cordis v4,它细化了效应与余效语义,并重新设计了加载器;两个版本共享相同的核心组合模型。 ↩
5 Koishi 使用“插件”一词来指代本文形式化为“组件”的概念。 ↩
6. 讨论
前述各节给出的形式化模型与实现引入了一种面向动态可组合性的编程范式。本节考察该范式如何扩展至更广泛的工程问题,并讨论其中的设计张力与开放问题。
6.1. 系统边界
第 3.1 节中的每个效应都携带一个逆,而这个逆究竟意味着什么,由系统边界决定。该边界将系统运行时所面对的环境分为两部分。(1)如果系统能够排他地修改某个位置,并能恢复该位置在修改前的状态,那么该位置就在边界之内;因此,对它的操作会在
由余效形成的边界。 余效通过将外部位置具体化来移动边界:它把对该位置的一切访问都限制在自己所提供的一组操作之中,并且能为其中每项操作提供一个逆;于是,原本表现为
获取与发出。 一个越过边界的操作通常分两个阶段进行。(1)在获取阶段,操作取得访问权,并在边界内安装一条记录:open 安装一个由 close 移除的描述符,malloc 预留一块由 free 释放的内存,fork 启动一个由 kill 终止的子进程。这条记录本身是将该位置具体化的余效的一部分,例如,它可以是余效所维护的映射中的一项;安装该条目则是一个可逆效应。与此同时,这条记录也是数据离开系统所经由的通道。(2)在发出阶段,操作通过该通道推出数据,例如 write 交给文件的字节,或 send 放到网络线路上的数据报;这种推出表现为
暂缓与补偿。 尽管如此,一个必须从发出操作中恢复的系统仍有两种可用方法。其一,暂缓发出,直到能够确定产生该输出的状态将被持久保留;这正是回滚恢复中的输出提交问题 [48]。其二,采用补偿 [49]:执行某项动作,把状态恢复到应用所给出的某种等价关系下;这种等价关系比定义 33 中的
6.2. 服务多路复用
OSGi [50] 等动态组件平台围绕服务来组织组合:服务是提供方依据某个接口发布、消费方随后绑定的一组功能。Cordis 的余效模型与这一概念相呼应,其中,一个服务对应某个键背后的接口。提供服务的组件是该服务的提供方,注入服务的组件则是它的消费方。一个服务可以由多个提供方实现,而这种多重性可以采用两种形式。(1)独占绑定:多个实现共享同一个接口,但任一时刻至多只能绑定其中一个;编排器选择要绑定的实现,而在实现之间切换时,必须先卸载一个提供方,再加载另一个,这会短暂扰动每个消费方的依赖。(2)服务代理器:一个充当该接口入口点的中心服务,同时由后端提供方和消费方注入;这样,多个提供方可以共存,而代理器负责把每项请求分派给它们中的某一个。与独占绑定相比,代理器会吸收这种扰动:更新某个后端提供方时,代理器本身仍保持原位,因此消费方观察不到其依赖发生变化,也不会触发重新加载。
服务代理器构成三种能力的基础:负载均衡、滚动更新和跨进程调用。
负载均衡。 当多个提供方共存时,代理器依据可配置的策略(例如轮询、最小负载或延迟加权),或者依据消费方明确指定的目标,在它们之间分发请求。由于提供方都是普通组件,可以通过添加或移除提供方来扩大或缩减容量;每个提供方都通过一个可逆效应向代理器注册,因此卸载该提供方会撤销这项注册,并自动将其从代理器的路由集合中移除。
滚动更新。 在运行时升级服务实现,可以归结为一次受控的提供方迁移 [51, 52]。执行这项迁移时,新的提供方作为一条额外纤程(fiber)加载,并向代理器注册;当它进入 ACTIVE 状态后,流量便逐步从旧提供方转移至新提供方(例如,通过调整选择权重),而旧提供方则会在不再承载进行中的请求后卸载。这种提供方迁移把传统上属于基础设施层的操作(例如容器编排、蓝绿部署)转化为一种应用层的组合模式。
跨进程调用。 服务代理器还可以跨越进程边界使用 [53]。每个进程都托管自己的 Cordis 上下文及本地提供方;一个协调组件把这些进程连接起来,并将每个进程视为远程提供方。跨进程服务访问由一种保留原接口的 RPC 机制中介,因此这种分布对消费方是透明的。需要注意的是,跨进程调用会引入延迟,也可能在执行途中失败,因此若以同步方式暴露,就会阻塞调用方。为跨进程暴露而设计的接口必须采用异步契约。
6.3. 访问控制与沙箱化
对于一个由独立组件组装而成的应用,保障其安全需要两种互补机制:(1)约束组件可以访问哪些依赖;(2)通过沙箱将不受信任的代码与宿主环境隔离。Cordis 通过依赖声明和拦截支持第一种机制;第二种机制则需要外部沙箱。
基于能力的访问控制。 依赖访问机制(第 5.1.4 节)本身已经构成了对代理所中介属性的一种访问控制:组件只能访问自己声明过的依赖;访问未声明的依赖会引发错误。这在结构上类似于基于能力的安全机制 [54–56]:权限由持有引用来授予,而不是来自环境权限。inject 声明充当能力请求,上下文代理则充当能力中介。由于这些请求是静态声明的,组件所需的、经代理中介的完整能力集合在运行前便已知晓;编排器因而可以在加载时审查并批准这些能力,而不必等到访问实际发生时才发现它们。
借助拦截机制,这种中介还可以推广至细粒度策略。访问控制元数据可以由上下文携带,也可以由组件声明(定义 30);调用依赖时,提供方查询这些元数据,以决定是否允许请求。例如,文件系统依赖可以携带元数据,声明组件能够读取或写入哪些路径,而提供方会逐次根据元数据检查调用。因为这种拦截存在于上下文上,而不在任一方的代码中,所以编排器无需修改提供方,就能调整拦截规则,约束任意组件对依赖的访问;例如,它可以只向社区组件授予数据库只读访问权,同时让核心组件保留完整访问权。此外,由于拦截只影响调用依赖的方式,并不影响依赖是否得到满足,所以可以在运行时安装、重新配置或移除拦截,而不会触发任何重新加载,也不会扰动依赖图。
对不受信任组件进行沙箱化。 当组件代码不可信时,语言层的访问控制并不足够,因为能够访问宿主运行时的恶意组件可以直接接触底层对象,使这类检查形同虚设。沙箱化需要一道语言层手段无法越过的执行边界,例如软件故障隔离 [57]、独立的语言运行时、沙箱进程或虚拟化容器 [58]。无论采用何种机制,不受信任的组件都在自己的沙箱上下文中运行,并通过桥接访问宿主提供的依赖;这是第 6.2 节跨进程调用的推广:同样的透明性论证使这种桥接访问与本地注入无法区分。在宿主一侧,该桥接是一条普通纤程,其能力可以通过上述访问控制机制加以削弱。
6.4. 语言无关性与语言选择
尽管 Cordis 使用 TypeScript 实现,上下文范式却与语言无关:时空可组合性仅由其两个可组合性维度来定义,因此,任何在这两个维度上都满足一定要求的语言,都可以实现这一范式。下面依次沿两个维度分析这些要求。
时间可组合性。 在最基本的层面上,时间可组合性要求语言支持闭包:可逆效应将一个动作与其逆配对,而这个逆必须连同它要恢复的状态一起,被捕获为一个值,以便在拆除时重放。此外,组件代码以及加载组件所产生的副作用,都必须能在运行时引入和撤回。
一种语言如何满足第二项要求,取决于它的执行模型。在托管运行时中,这表现为可由程序操作的模块注册表:已加载的模块可以从注册表中逐出,并在不再被引用后由垃圾回收器回收;例如,Node.js 就暴露了这样的注册表。6 原生代码不暴露模块注册表,因此,引入和撤回表现为显式的动态链接与取消链接(例如 Unix 上的 dlopen/dlclose、Windows 上的 LoadLibrary/FreeLibrary)[59],也就是先把目标代码载入正在运行的进程,之后再将其分离。WebAssembly 采用哪种路径取决于它的嵌入器:在托管式嵌入器(例如 JavaScript 宿主)中,模块实例由宿主的垃圾回收器回收;在原生嵌入器(例如 Wasmtime)中,则在嵌入器丢弃模块实例时释放。贯穿这些机制,可逆效应模型都把加载视为作用于上下文的效应,并由相应的逆撤销模块所引入的符号、类型或处理器注册。
空间可组合性。 空间可组合性要求具备这样一种机制:组件能够声明其依赖,而运行时则能够提供并注入这些依赖。这可以归结为一个依赖注入(DI)问题 [38];该问题体现在两个因语言而异的层面,即如何对依赖赋予类型,以及如何中介对依赖的访问。
在类型层面,语言应当允许开发者表达类型良好的依赖访问。消费方通过从上下文中读取键来取得余效,因此上下文类型(第 3.2.1 节)必须记录每个键的余效。类型类(Haskell)[60] 与 trait(Rust)[61] 允许提供方在其自身模块中,通过 instance 或 impl 扩展上下文类型 [62],从而做到这一点。TypeScript 的模块扩充(module augmentation)[63] 同样允许提供方模块将声明合并到上下文类型中。
在运行时层面,对依赖的访问必须受到动态中介:随着提供方的加载与卸载,一个键背后的余效可能发生变化,而且不同上下文也可能以不同方式解析它。因此,语言需要提供一种能够透明介入访问的方式,同时保持消费方代码不变,例如 JavaScript 的 Proxy 对象 [64] 或 Python 的描述符协议(__get__)[65]。如果缺少此类原语,运行时反射 [66, 67] 也可以动态中介访问,但代价是类型安全与开发者体验的下降。
在这两个层面上,元编程设施可以同时提供类型化与中介能力。注解 [68] 和装饰器为声明附加元数据,再由处理器将其展开为中介访问的访问器;编译期元编程(例如 Rust 过程宏、Scala 宏 [69]、Zig comptime)则会为每项依赖生成一份带类型的声明,以及一个这样的访问器,从而无需通用的拦截原语。
6 CommonJS 通过 require.cache 暴露模块缓存;ES 模块没有公开的逐出 API,但仍可通过引擎内部接口对模块进行管理。 ↩
6.5. 相互依赖与组件粒度
在反应式余效模型中,依赖环只会使环中涉及的组件永久保持非活动状态:给定两个组件
在实践中,大多数表面上的相互依赖都可以通过拆分为粒度更细的组件来消除环。考虑两个组件:服务器(提供网络接口)和访问控制器(执行授权策略)。这两个组件存在双向交互:访问控制器中介到达服务器的请求,而服务器则暴露一个用于修改访问控制策略的端点。在单体设计中,两个组件会彼此依赖。然而,两个交互方向在逻辑上是相互独立的关注点。将它们拆分后会得到四个组件:server-core、access-control-core、request-mediation(同时依赖两个核心组件,以便对传入请求实施访问控制),以及 policy-management(同样依赖两个核心组件,以便通过服务器暴露策略修改能力)。通过这种方法可以消除依赖环,因为两个核心组件都不依赖对方;只有集成组件同时依赖二者。
原则上,这种拆分总是可行的,因为任何双向交互都可以分解为彼此独立的单向绑定;但它会增加组件数量:在一般情形下,给定
缓解这种粒度成本属于工程问题,而不是理论问题。实用策略包括包捆绑(即把相关的细粒度组件组成一个可安装单元)、基于约定的接线(即自动连接名称或类型符合某种模式的组件),以及脚手架工具(即根据声明式规约生成集成组件的样板代码)。这些策略既保留了无环模型的形式化保证,又能把编写负担降低到更接近单体设计的程度。
6.6. 依赖类型化与版本控制
在形式化模型中,依赖链接完全依据键的同一性建立:提供键
接口漂移。 提供方可能会在版本之间修改与
键冲突。 两个独立开发的提供方可能使用同一个键名
这两个问题都指向同一处缺口:余效模型只提供名义链接(按键名),却不提供版本化链接或结构化链接(按接口兼容性)[71]。下面讨论三种弥补方法,按与基础设施耦合程度从最高到最低、也就是从基础设施相关性最强到语言无关性最强排列。
键命名空间化。 将键空间从
对等依赖。 一种耦合较弱的做法,是通过宿主语言的包管理器声明版本约束 [72]。Cordis 目前采用的正是这种方法。组件依赖在语义上属于对等依赖:组件不会把自己的依赖捆绑在内部,而是期望运行时上下文提供这些依赖。支持对等依赖的包管理器(例如 npm)能够强制执行版本兼容性:如果提供某个键的包版本落在消费方声明的对等版本范围之外,那么这种不兼容会在安装时被发现,而不会以运行时故障的形式暴露。不过,这种方法有两个局限:(1)它依赖提供方忠实遵守语义化版本规范,而这只是一项无法强制执行的约定;(2)包管理器通常会把每项依赖解析为单一版本,因此无法在一个应用内加载同一个包的多个版本所提供的组件。
结构兼容性。 一种完全与语言无关的方法,是用兼容性谓词取代成员关系检查
这三种方法处理的是问题的不同侧面。如何设计一种统一的依赖模型,把这些方法结合起来,同时保留余效模型对动态组合的保证,仍是一个开放问题。
6.7. 与语言及操作系统的协同设计
第 6.4 节指出了宿主语言为支持上下文范式至少必须提供什么。本节讨论反过来的问题:与该范式协同设计的语言或操作系统,能在这些最低要求之外提供什么。
与语言协同设计。 围绕上下文范式设计的语言,可以在两个方面超越库:一是它赋予上下文的语义,二是它为效应与余效提供的原语。
这样的语言可以重新让上下文变为隐式,同时保留第 3.3 节的上下文语义。命令式语言已经让每条语句都针对一个隐式上下文运行,但这个唯一的上下文既不追踪效应,也不解析余效。上下文范式则区分多个上下文;一个操作要么修改它所针对的上下文,要么从中派生另一个上下文(定义 27)。原地实现会修改环境上下文,与命令式语言的做法相同。派生式实现则会引入一个独立的上下文,语言必须为此提供一种构造。让上下文变为隐式,既能改善易用性,也能提高安全性。(1)在库式实现中,每个涉及效应或余效的函数,都要像第 5.1 节那样,把上下文作为普通参数或接收者。若由语言隐式提供上下文,函数就不再需要接收它。(2)每个上下文都有自己的生命周期状态和已提交视图(第 4.1 节)。库式实现把上下文作为普通变量传递,因此组件可能通过闭包或全局变量,错误地访问另一个组件的上下文。它安装在那个上下文中的效应随后会泄漏到自身生命周期之外,而从中读取的余效也会逃逸出自身的依赖规约。让上下文变为隐式,可以同时杜绝这两种情况。
这样的语言还可以让编译器感知效应与余效。(1)对于效应,效应迭代器(定义 51)会在每一步都分配一个闭包,把逆与该逆要恢复的状态保存在一起。如果语言提供执行效应的专用语法,编译器就能为整个迭代生成一个状态机,并将这些逆保存在状态机的帧中。(2)对于余效,可以把余效规约纳入类型系统,从而带来两项好处。第一,依赖环可以在编译时报告,而不必留到运行时处理(第 6.5 节)。第二,可以按照依赖类型的结构比较依赖,而不再仅按键的同一性比较,就像行类型所做的那样 [28];这为第 6.6 节的结构兼容性提供了类型层支持。
与操作系统协同设计。 第 1.2.3 节指出了一种动态可组合性的粗粒度替代方案:操作系统以进程为粒度提供时间可组合性,其上的容器编排器则以服务为粒度提供空间可组合性。与该范式协同设计的操作系统将通过两种方式支持细粒度组合:让组件声明的余效规约涵盖它所能访问的一切,并把操作系统自身的资源作为余效提供。
这样的操作系统可以提供第 6.3 节留给语言外部机制实现的沙箱。其做法是把组件能够访问的范围限制在它所声明的依赖之内:加载组件时向它提供这些依赖,而在组件内部不留下任何其他可达对象;这就像 WebAssembly 模块在实例化时从嵌入器接收其导入项一样 [76]。它还可以将第 3.2.3 节的余效隔离与拦截作为操作系统自身的能力,为每个组件以不同方式绑定同一个键,并中介它所提供的访问。
这样的操作系统还可以把自身资源作为余效提供。如果运行时把每次资源获取都记录到发起获取的组件名下,那么原本位于边界之外的资源便可变得可逆(第 6.1 节);每个运行时都会维护一份自己的记录。当操作系统把资源作为余效提供时,只需维护一份这样的记录,因为资源正是由它发放的,它也能够将资源归因于提出请求的组件。内存和文件描述符是最直接的候选对象,而为恢复目的在内核接口处追踪这些资源,已有先例 [77, 78]。此外,对于第 6.1 节认为只能暂缓或补偿的某些操作,操作系统也可以使其变为可逆。以事务方式向持久存储执行写入的系统可以回滚这次写入 [79];构建在写时复制存储或不可变存储之上的系统,则可以通过移动指针返回先前状态 [80, 81]。
7. 相关工作
动态可组合性与若干成熟研究领域相交。本节考察其中最相关的几条研究脉络,并逐一说明我们的贡献与它们之间的区别。
7.1. 效应与余效系统
第 2 节回顾了效应与余效,它们是本研究所依托的理论支柱。我们首先说明如今已广泛应用于工业实践的单子效应系统与本研究之间的关系,随后考察三条沿着与 Cordis 相关的方向扩展效应和余效的研究路线:将代数效应重新解释为能力、为效应赋予可逆语义,以及在统一的分级规约下统一效应与余效。
单子效应系统。 有一类库在现有通用语言的类型系统中编码效应,将其表示为由运行时执行的单子值。Scala 中的 ZIO [82] 将计算建模为 ZIO[R,E,A],TypeScript 中的 Effect-TS [83] 则将其建模为 Effect<A,E,R>;这些泛型类型的参数描述计算结果、类型化错误,以及其上下文必须提供的服务。fp-ts 库 [84] 通过基于 Reader 的单子变换器编码相同的错误通道与要求通道。这些系统与 Cordis 有两个不同之处。第一,追踪能力以单子嵌入为代价:程序必须写在效应类型内部,才能获得这种能力;Cordis 则将效应追踪作为覆盖在普通宿主代码之上的一层机制。第二,一项要求通过解释来消解,即由已安装的服务提供相应操作;当该服务被撤回时,其操作已经产生的结果仍会留在原处。Cordis 则为每个效应配对一个逆函数,并随着提供者的加入和离开重新解析要求(第 3.1 节、第 3.2 节)。
作为能力的代数效应。 代数效应(第 2.1 节)使效应操作对类型系统可见。与本研究最接近的扩展是 Brachthäuser 等人的 Effekt 语言;它将效应类型重新解释为能力 [85, 86]:一个效应类型表达的是计算需要从上下文获得什么,而不是它可能产生哪些副作用。与我们的观点相同,这一视角也把上下文视为能力的中介。Cordis 与 Effekt 在两个方面有所不同。(1) 就目的而言,代数效应使效应可见,是为了支持模块化解释,让同一操作可以具有多种处理器语义;Cordis 使效应可见,则是为了支持追踪与还原,为每个上下文变换配对一个逆变换。(2) 就应用环境而言,Effekt 在类型层面静态约束效应,默认采用基于作用域的推理:能力是二等值并受限于其词法作用域;它又通过装箱恢复一等用法,即在类型中追踪被捕获的能力,从而解除这一限制。Cordis 则在运行时约束效应,目标是在移除组件时完整回收资源;第 6.7 节讨论了让上下文在这一意义上成为二等值的语言能够提供什么。
可逆效应语义。 另一条平行的研究路线为效应赋予可逆语义,而非解释语义。Heunen 等人 [87] 对 Hughes 的箭头加以改造,引入 dagger 箭头与逆箭头,从而在可逆环境中对副作用建模,并捕获序列化、可变存储等其操作具有逆操作的效应。这是与我们的可逆效应最接近的形式化描述:两种方法都为每个效应配备撤销它的手段,而不是通过处理器消解效应。二者的区别在于可逆性位于何处,以及对可逆性的要求有多强。Heunen 等人在指称式的范畴论环境中展开研究;其中,可逆性是一项全局性质,由构造保证,因为每个计算都可逆,而且双侧逆可从范畴结构中恢复出来。Cordis 在运行时追踪逆函数,并且要求更弱:它不要求整个计算可逆,只要求每个原子效应具有单侧逆;该逆函数不是推导出来的,而是由调用者在应用效应时提供,随后可通过组合得到任意复合效应的逆函数(第 3.1 节)。
以分级类型统一效应与余效。 Orchard 等人 [88] 提出将分级模态类型作为同时涵盖效应推理(通过分级单子)与余效推理(通过分级余单子)的统摄性概念,并在 Granule 语言中实现了这一思想,从而证明同一个类型系统可以同时追踪计算做了什么以及它需要什么。较新的研究还将余效扩展到类似 Java 的命令式语言 [89, 90] 和按值压栈(call-by-push-value)[91]。这些工作全都作用于类型层面:效应与余效是静态标注,在编译时针对词法上固定的作用域进行检查。我们的贡献与这种分析正交:我们将相同的两个概念提升为运行时机制,使 Cordis 能够处理动态组合。随着已加载组件的集合不断演化,时间维度上的撤回与空间维度上的依赖会被重新解析,而不是基于固定的程序文本一次性确定。
7.2. 编程范式
第 3.3.3 节将上下文范式确立为一种通过显式上下文来中介效应与余效的编程规约。有两种成熟范式值得明确比较:一种与我们共享“上下文”这一术语,另一种则与我们对横切关注点的处理方式相近。
面向上下文编程。 面向上下文编程(context-oriented programming,COP)[92, 93] 为语言配备了层(layer)——可以根据执行上下文在运行时激活和停用的局部方法定义与类定义,因此行为能够自适应变化,而基础代码无须指明自身的上下文依赖 [94]。COP 与 Cordis 都将上下文视为一等的、可在运行时改变的实体,也都会动态激活和停用行为;不过,这种相似仅停留在名称层面。在 COP 中,“上下文”指周围的执行情境(例如位置、用户或模式),激活操作会在一个动态作用域范围内改变方法分派;层既不追踪其引发的副作用,也不还原这些副作用,而且激活与否并不取决于依赖是否得到满足。在 Cordis 中,上下文是中介效应与余效的
面向切面编程。 面向切面编程(aspect-oriented programming,AOP)[95, 96] 将横切关注点模块化为切面:切点对基础程序中选出的连接点进行量化,通知则被织入每一个这样的连接点。Cordis 处理的是同一个问题,即原本会散布在多个组件中的上下文相关行为;但在 Cordis 中,与切面对应的是余效:它是许多组件声明依赖的共享中介点,因此可以在此处重塑横切行为,而无须编辑任何组件。随后,两种范式在两个维度上表现出差异。(1) 声明与无感知:AOP 切点是无感知且经过量化的,它可以匹配任意连接点,而这些连接点处的代码并不知道自身会收到通知;Cordis 则将横切限定于各组件声明的余效,因此其作用范围恰好就是声明所覆盖的表面。这带来了确定性与可追踪性:应用编排器无须阅读或分析组件源码,就能在配置层检查并管控哪些内容会横切该组件;相比之下,AOP 中的关注点只能通过对它进行量化的切面来理解。(2) 生命周期集成:在 Cordis 中,一项横切变更由组件的效应承载,在组件卸载时得到还原,并以反应式方式传播给其依赖方,因此它只是动态组合模型中的一个动作;动态 AOP 系统 [97, 98] 同样可以在运行时织入和解除织入,但这是一项独立操作,既不绑定到组件生命周期,也不会触发被通知代码之间的重新解析。
7.3. 时间可组合性
时间可组合性关注的是:如何在运行中的程序里替换或移除组件,同时恢复该组件所安装的效应。既有方法可以根据其如何处理离开组件的状态与效应分为四类:将状态向前迁移到后继版本;通过开发者编写的清理逻辑恢复效应;在预先固定的作用域内自动逆转效应;或者由运行时在某个接口上实施中介并积累记录,再依据该记录回收资源。
有状态的向前迁移。 一大类系统通过跨版本向前迁移状态,在不中断服务的情况下替换运行中程序的组件。它们都遵循同一项时序规约:只有当组件到达一个安全且无交互的时点后,才能替换该组件。Kramer 和 Magee 将这一判据确立为静止性(quiescence)[51],Vandewoude 等人随后将其放宽为干扰更小的平静性(tranquility)[52];我们的滚动更新模式(第 6.2 节)会在卸载提供者前排空进行中的请求,从而执行这一判据。动态软件更新(dynamic software updating,DSU)随后通过手写的变换函数向前迁移状态:Hicks 等人面向 C 语言的通用 DSU [99]、Stoyle 等人借助 con-freeness 分析得到的类型安全更新点 [100],以及 Hayden 等人的 Kitsune [101],都会将旧版本数据映射为新版本的表示形式,在原处继承堆对象、已打开文件和连接,同时重新初始化所有未被迁移的内容。同样的规约也可扩展到持久状态:Overeem 等人 [102] 使用手写的升级操作,在保持系统可用的同时,在不同 schema 版本之间转换运行中事件存储的数据。Erlang/OTP [15] 在进程层面采取同一立场:通过 code_change/3 迁移状态,并通过重启受监督进程从故障中恢复,而不是还原这些进程的效应。JavaScript 的热模块替换(例如 webpack [46]、Vite [47])则在模块层面采用相同做法,在重新加载期间通过 module.hot 或 import.meta.hot API 将状态向前传递。与 Cordis 的模块替换(第 5.2 节)相比,这些方法能够更平滑地迁移内存中状态:Cordis 会还原旧组件受追踪的效应,再从干净状态重新应用新组件的效应,因此组件自身的内存中状态无法跨越重新加载而保留,除非将其放入生命周期更长的依赖中;在可逆效应之上叠加 DSU 式向前迁移,仍是未来工作。尽管如此,Cordis 的方法在两个方面更加通用:它不需要 DSU 和 HMR 所要求的手写迁移函数;它还支持彻底卸载组件并回收其资源,而不只是就地更新组件。
由开发者编写的恢复。 第二类方法通过开发者手写的清理逻辑或补偿逻辑来恢复组件的效应。插件生命周期约定(例如 OSGi [50]、Eclipse 的扩展点、IntelliJ 和 VSCode)将清理工作委托给开发者编写的卸载回调;命令模式 [103] 将操作与用于撤销/重做栈的 undo 方法封装在一起;Saga 模型 [49] 将长期事务组织成多个步骤,每个步骤都配有一个补偿动作;代数效应处理器可以附加在拆卸时运行的终结器 [104];事件溯源 [105] 则通过追加补偿事件来撤回状态,根本不执行逆操作。在所有这些方法中,提供逆操作都是一项不受强制约束、且与原操作相分离的职责,因此一旦遗漏,资源便会悄然泄漏(如第 1.2.1 节的实证记录所示)。React 的 useEffect 钩子 [106] 最接近于从结构上为效应配对其逆操作:它返回一个清理函数,由运行时在每次重新执行前以及卸载时调用。它的不足在于可组合性:钩子只能在组件或另一个钩子的顶层调用,绝不能位于条件分支、循环或嵌套函数中,而且其效应函数体既不能接受异步函数,也不能接受迭代器。因此,效应无法由其他效应组装而成,也无法与控制流交错,于是便不存在可据以推导复合逆函数的结构。Cordis 效应没有这种限制:它们是可以自由组合、也可以异步运行的普通操作;只有每个原子效应需要一个手写逆函数,任意复合效应的逆函数则由组合推导出来,因此组装已有的效应完全无须再编写逆函数。每个效应与其逆函数之间的这种结构性配对,使完整恢复成为系统的一项不变量,而不再取决于开发者能否恪守规约。
静态定域的逆转。 第三类方法通过构造自动逆转效应,但把逆转限定在预先固定的作用域内。软件事务内存 [107, 108] 由硬件事务内存 [109] 演化而来;它会记录读/写日志,使一组内存操作要么提交,要么中止并将内存回滚到事务开始前的状态。可逆计算从 Landauer 和 Bennett 的热力学分析 [110, 111] 一路发展到 Janus [112] 等可逆语言,更进一步地让整个计算的每一步都具有全局可逆性。可逆进程演算则把回溯内建到语义本身:RCCS [113] 为每个进程附带一份记忆,并允许在某一步所通向的过去与目标过去因果等价时撤销该步;Phillips 和 Ulidowski [114] 则为 CCS、ACP 与 CSP 统一推导出可逆算子,同时保持它们的前向操作语义。它们采用的因果一致性判据,正是 Cordis 恢复顺序在并发环境下的对应物:累加器按后进先出顺序应用组件自身的逆函数,而第 4.3.1 节的守卫会推迟提供者的撤回,直到其使用者均已停用(定理 63)。不过,这类方法的作用范围由语义固定,执行过的每个动作都始终保持可撤销;Cordis 组件则为每个原子效应提供逆函数,其累加器将上下文带回该组件开始组合时的状态。线性类型 [115]、RAII [4] 以及 Rust 的所有权系统 [61] 把资源释放绑定到词法区域。上述每种方法都静态固定了逆转的作用域与作用范围;相比之下,Cordis 不会预先固定这样的作用域:它会在组件的整个生命周期内还原任意上下文操作,并把词法资源管理视为一种互补机制,适合管理单个组件内部的局部资源。
中介式回收。 第四类方法无须组件自身提供逆函数,而是通过运行时所控制的接口记录组件获取的内容,并据此实施回收。Nooks [77] 包装了跨越 Linux 内核与其可加载扩展之间边界的每一次调用,因此扩展所接触的内核对象都会经过对象追踪器;扩展发生故障时,该追踪器的记录会告诉恢复管理器应当释放哪些对象。影子驱动程序(shadow driver)[78] 从另一侧接入同一组调用,记录决定驱动程序状态的请求与配置,从而可以让重启后的实例恢复到该状态。Akeso [116] 则通过编译器插桩获得记录:它将内核执行划分为可嵌套的恢复域,记录各恢复域的状态变化与跨线程依赖,并将发生故障的请求连同依赖于该请求的每个恢复域一起回滚。因此,回收源自运行时维护的记录,而非开发者记得编写的清理逻辑;这使该类方法成为可逆效应在系统层面最接近的先例。它与 Cordis 的区别在于所用词汇与作用范围。平台固定了哪些内容可以被记录——无论其形式是针对每类内核对象的释放代码、每类驱动程序对应的一个影子,还是每个经过插桩的分配器对应的一个逆函数——因此,组件只能持有平台已经知道如何释放的资源;Cordis 组件则可以引入自己的效应,并为每个原子效应提供逆函数(第 3.1 节)。同样,回收的边界是某个会提交的请求,或同一扩展的一次重启;Cordis 则在组件的整个生命周期上进行还原,并将移除传播给组件的依赖方,后者继而释放自身的效应(第 3.2 节)。
7.4. 空间可组合性
空间可组合性关注如何声明组件对其他组件的依赖,以及如何绑定这些依赖。既有机制可以根据绑定如何响应变化分为三类:仅在初始化时连接依赖;对整个组件的可用性作出反应;或者以单个值为粒度传播变化。
初始化时的依赖连接。 有两种成熟机制会在初始化时把组件连接起来。依赖注入框架 [38](例如 Spring [117]、Guice、Angular、Inversify)会在初始化组件时向其中注入依赖,而 UI 框架的上下文(例如 Vue.js 的 provide/inject 与 React 的 Context API)则沿组件树传递依赖。其中一些机制支持动态作用域(例如 Spring 的 prototype/request 作用域、Angular 的分层注入器),但二者都不会以反应式方式重新解析:在运行时替换或移除提供者时,已有的依赖方既不会被停用,也不会被重新初始化;而且,它们都不提供类似于我们的组件状态机的生命周期管理。Cordis 的反应式余效(第 3.2 节)提供了这种能力:每当满足谓词发生变化,通知机制都会触发生命周期迁移。
对可用性作出反应的组件模型。 与我们的反应式余效最接近的先例会对服务可用性作出反应。OSGi 的 Declarative Services 与 iPOJO [118, 119] 允许组件声明其提供和需要的服务;随着服务出现和消失,运行时会自动激活和停用这些组件。iPOJO 的 Gravity 项目 [119] 明确以根据服务可用性的变化进行自主运行时适应为目标,而它的 provide/require 模型直接预示了 Cordis 的 ctx.provide/ctx.get 模式。R-OSGi [53] 通过 RPC 将同一个抽象透明地扩展到分布式环境,把网络故障映射为服务撤回事件;第 6.2 节将这一模式作为 Cordis 模型的一项扩展加以讨论。所有这些系统都通过停用回调进行恢复,而这种做法存在两个限制。第一,回调由开发者手写,因此资源安全取决于开发者的自律,任何被遗漏的回调都会导致资源悄然泄漏。第二,回调是同步的:如果拆卸需要与即将离开的依赖进行一次异步交互,这些框架并不提供等待该交互的协议,只能迫使程序针对一个可能已经陈旧的引用进行阻塞等待。Cordis 的反应式余效弥补了这两处缺口:停用会还原依赖方所累积的效应,而其具有惯性的
值级反应性。 函数式反应式编程(functional reactive programming,FRP)[120] 及其现代实现(例如 SolidJS 中的 signal [121, 122]、Vue 的反应式系统、Angular Signals)以值级粒度传播变化:当一个 signal 发生变化时,派生计算会同步重新求值,或在调度器控制下重新求值 [123]。Cordis 的反应式余效则作用于组件级粒度,并额外加入值级传播所不建模的异步生命周期语义。在一致性方面,同一项粒度差异又呈现出相反的优势:FRP 在一个轮次(turn)内,依照依赖图确定的顺序传播变化,因此可以要求任何派生计算都不会同时读到已更新输入与陈旧输入的混合;这就是无毛刺性(glitch freedom)[124]。Cordis 没有与轮次对应的概念,编排动作会逐个到来;它只保证任何一次迁移都不会横跨两次不同的余效解析(定理 64)。两者互为补充,而非相互竞争:Cordis 余效本身可以携带反应式值,而组件只根据自己实际使用的部分进行更新,由此将组件级反应性细化为跨越两个层级的、更细粒度的反应式余效。
8. 结论
我们通过将经典的效应与余效概念提升为运行时机制,为动态可组合性提出了一个形式化基础。可逆效应解决了局部时间可组合性:每个上下文变换都携带一个由运行时追踪的逆变换,而且追踪与恢复均保持组合,因此在移除组件时能够恢复上下文。反应式余效解决了局部空间可组合性:每当上下文发生变化时,都会依据组件的余效规约向该组件发出通知,并将每次变化分类为激活型、停用型或中性;余效隔离会改变声明键的解析结果,而余效拦截会改变绑定的使用方式。我们将效应上下文与余效上下文统一为单一的上下文类型,其中,余效上的观察等价关系为效应赋予独立性,由此构成一种面向时空可组合性的编程范式。随后,将这些机制结合到组件这一概念中,便得到一种动态组合演算;其元理论将时空可组合性从单个组件推广到由交错运行的组件组成的整个系统。我们将这一范式实现为 Cordis 元框架,其中既有提供效应追踪与余效解析的核心库,也有支持配置协调与热模块替换(HMR)的声明式组件加载器。Koishi 案例研究在一个拥有 4000 多个社区插件的生产系统中验证了 Cordis 的设计。
除由人工维护的插件生态系统之外,一个值得进一步验证的方向是自演化智能体运行框架(第 1.2.2 节):在这类框架中,AI 智能体会持续生成并替换自身的运行框架组件,且只有很少的人工监督。将 Cordis 应用于这样的环境,既能验证在组件快速替换时实现完整恢复的时间保证,也能验证在拓扑频繁变化时实现依赖协调的空间保证。这种验证将表明,该范式能够作为一种基础,用于在智能体运行框架及其他自主系统中实现可恢复、协调且持续的自我演化。
参考文献
[1] D. L. Parnas, “On the criteria to be used in decomposing systems into modules,” Communications of the ACM, vol. 15, no. 12, pp. 1053–1058, 1972, doi: 10.1145/361598.361623.
[2] D. Birsan, “On Plug-ins and Extensible Architectures,” ACM Queue, vol. 3, no. 2, pp. 40–46, 2005, doi: 10.1145/1053331.1053345.
[3] B. Burns, B. Grant, D. Oppenheimer, E. Brewer, and J. Wilkes, “Borg, Omega, and Kubernetes,” Communications of the ACM, vol. 59, no. 5, pp. 50–57, 2016, doi: 10.1145/2890784.
[4] B. Stroustrup, The Design and Evolution of C++. Addison-Wesley, 1994.
[5] S. Marlow, S. Peyton Jones, A. Moran, and J. Reppy, “Asynchronous Exceptions in Haskell,” in Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, in PLDI '01. New York, NY, USA: Association for Computing Machinery, 2001, pp. 274–285. doi: 10.1145/378795.378858.
[6] L. Cardelli, “Program Fragments, Linking, and Modularization,” in Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), ACM Press, 1997, pp. 266–277. doi: 10.1145/263699.263735.
[7] C. Szyperski, Component Software: Beyond Object-Oriented Programming, 2nd ed. Addison-Wesley, 2002.
[8] R. Lopopolo, “Harness Engineering: Leveraging Codex in an Agent-First World.” [Online]. Available: https://openai.com/index/harness-engineering/
[9] Anthropic, “Harness Design for Long-Running Application Development.” [Online]. Available: https://www.anthropic.com/engineering/harness-design-long-running-apps
[10] L. Wang et al., “A Survey on Large Language Model Based Autonomous Agents,” Frontiers of Computer Science, vol. 18, no. 6, p. 186345, 2024, doi: 10.1007/s11704-024-40231-1.
[11] Y. Qin et al., “Tool Learning with Foundation Models,” ACM Computing Surveys, 2025, doi: 10.1145/3704435.
[12] C. Packer, V. Fang, S. G. Patil, K. Lin, S. Wooders, and J. E. Gonzalez, “MemGPT: Towards LLMs as Operating Systems,” CoRR, vol. abs/2310.08560, 2023.
[13] T. Guo et al., “Large Language Model Based Multi-Agents: A Survey of Progress and Challenges,” in Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, in IJCAI 2024. 2024, pp. 8048–8057. doi: 10.24963/ijcai.2024/890.
[14] T. Cai, X. Wang, T. Ma, X. Chen, and D. Zhou, “Large Language Models as Tool Makers,” in Proceedings of the Twelfth International Conference on Learning Representations, in ICLR 2024. [Online]. Available: https://openreview.net/forum?id=qV83K9d5WB
[15] J. Armstrong, “Making Reliable Distributed Systems in the Presence of Software Errors,” Doctoral dissertation, 2003. [Online]. Available: https://erlang.org/download/armstrong_thesis_2003.pdf
[16] E. Moggi, “Notions of computation and monads,” Information and Computation, vol. 93, no. 1, pp. 55–92, 1991, doi: 10.1016/0890-5401(91)90052-4.
[17] G. Plotkin and J. Power, “Adequacy for Algebraic Effects,” in Foundations of Software Science and Computation Structures, F. Honsell and M. Miculan, Eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2001, pp. 1–24.
[18] T. Petricek, D. Orchard, and A. Mycroft, “Coeffects: unified static analysis of context-dependence,” in Proceedings of the 40th International Conference on Automata, Languages, and Programming - Volume Part II, in ICALP'13. Riga, Latvia: Springer-Verlag, 2013, pp. 385–397. doi: 10.1007/978-3-642-39212-2_35.
[19] M. Gaboardi, S.-ya Katsumata, D. Orchard, F. Breuvart, and T. Uustalu, “Combining effects and coeffects via grading,” in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, in ICFP 2016. Nara, Japan: Association for Computing Machinery, 2016, pp. 476–489. doi: 10.1145/2951913.2951939.
[20] A. Church, “A Formulation of the Simple Theory of Types,” The Journal of Symbolic Logic, vol. 5, no. 2, pp. 56–68, 1940, doi: 10.2307/2266170.
[21] B. C. Pierce, Types and Programming Languages. MIT Press, 2002.
[22] J. M. Lucassen and D. K. Gifford, “Polymorphic Effect Systems,” in Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, in POPL '88. San Diego, California, USA: Association for Computing Machinery, 1988, pp. 47–57. doi: 10.1145/73560.73564.
[23] P. Wadler, “Monads for functional programming,” in Program Design Calculi, M. Broy, Ed., Berlin, Heidelberg: Springer Berlin Heidelberg, 1993, pp. 233–264.
[24] G. Plotkin and J. Power, “Notions of Computation Determine Monads,” in Foundations of Software Science and Computation Structures, Berlin, Heidelberg: Springer Berlin Heidelberg, 2002, pp. 342–356. doi: 10.1007/3-540-45931-6_24.
[25] G. Plotkin and M. Pretnar, “Handlers of Algebraic Effects,” in Programming Languages and Systems (ESOP), Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 80–94. doi: 10.1007/978-3-642-00590-9_7.
[26] M. Pretnar, “An Introduction to Algebraic Effects and Handlers. Invited tutorial paper,” Electron. Notes Theor. Comput. Sci., vol. 319, no. C, pp. 19–35, Dec. 2015, doi: 10.1016/j.entcs.2015.12.003.
[27] D. Leijen, “Koka: Programming with Row Polymorphic Effect Types,” Electronic Proceedings in Theoretical Computer Science, vol. 153, pp. 100–126, Jun. 2014, doi: 10.4204/eptcs.153.8.
[28] D. Leijen, “Type directed compilation of row-typed algebraic effects,” in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, in POPL '17. Paris, France: Association for Computing Machinery, 2017, pp. 486–499. doi: 10.1145/3009837.3009872.
[29] A. Bauer and M. Pretnar, “Programming with algebraic effects and handlers,” Journal of Logical and Algebraic Methods in Programming, vol. 84, no. 1, pp. 108–123, Jan. 2015, doi: 10.1016/j.jlamp.2014.02.001.
[30] K. Sivaramakrishnan et al., “Retrofitting parallelism onto OCaml,” Proc. ACM Program. Lang., vol. 4, no. ICFP, Aug. 2020, doi: 10.1145/3408995.
[31] T. Petricek, D. Orchard, and A. Mycroft, “Coeffects: a calculus of context-dependent computation,” in Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, in ICFP '14. Gothenburg, Sweden: Association for Computing Machinery, 2014, pp. 123–135. doi: 10.1145/2628136.2628160.
[32] T. Uustalu and V. Vene, “Comonadic Notions of Computation,” Electronic Notes in Theoretical Computer Science, vol. 203, no. 5, pp. 263–284, 2008, doi: 10.1016/j.entcs.2008.05.029.
[33] A. Brunel, M. Gaboardi, D. Mazza, and S. Zdancewic, “A Core Quantitative Coeffect Calculus,” in Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410, Berlin, Heidelberg: Springer-Verlag, 2014, pp. 351–370. doi: 10.1007/978-3-642-54833-8_19.
[34] J. Reed and B. C. Pierce, “Distance makes the types grow stronger: a calculus for differential privacy,” SIGPLAN Not., vol. 45, no. 9, pp. 157–168, Sep. 2010, doi: 10.1145/1932681.1863568.
[35] M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke, “A core calculus of dependency,” in Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, in POPL '99. San Antonio, Texas, USA: Association for Computing Machinery, 1999, pp. 147–160. doi: 10.1145/292540.292555.
[36] D. E. Denning, “A lattice model of secure information flow,” Commun. ACM, vol. 19, no. 5, pp. 236–243, May 1976, doi: 10.1145/360051.360056.
[37] U. Dal Lago and F. Gavazzo, “A relational theory of effects and coeffects,” Proc. ACM Program. Lang., vol. 6, no. POPL, Jan. 2022, doi: 10.1145/3498692.
[38] M. Fowler, “Inversion of Control Containers and the Dependency Injection pattern.” [Online]. Available: https://martinfowler.com/articles/injection.html
[39] A. M. Pitts and I. D. B. Stark, “Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's New?,” in Mathematical Foundations of Computer Science 1993 (MFCS 1993), in Lecture Notes in Computer Science, vol. 711. Springer, 1993, pp. 122–141. doi: 10.1007/3-540-57182-5_8.
[40] G. D. Plotkin, “LCF Considered as a Programming Language,” Theoretical Computer Science, vol. 5, no. 3, pp. 223–255, 1977, doi: 10.1016/0304-3975(77)90044-5.
[41] D. R. Ghica, K. Muroya, and T. Waugh Ambridge, “A Robust Graph-Based Approach to Observational Equivalence,” Logical Methods in Computer Science, vol. 21, no. 2, p. 8:1–8:95, 2025, doi: 10.46298/LMCS-21(2:8)2025.
[42] X. Leroy and S. Blazy, “Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations,” Journal of Automated Reasoning, vol. 41, no. 1, pp. 1–31, 2008, doi: 10.1007/s10817-008-9099-0.
[43] R. P. James and A. Sabry, “Yield: Mainstream Delimited Continuations,” in First International Workshop on the Theory and Practice of Delimited Continuations (TPDC 2011), 2011, pp. 20–32. [Online]. Available: https://homes.luddy.indiana.edu/sabry/files/yield.pdf
[44] A. W. Mazurkiewicz, “Trace Theory,” in Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, in Lecture Notes in Computer Science, vol. 255. Springer, 1986, pp. 279–324. doi: 10.1007/3-540-17906-2_30.
[45] U. A. Acar, G. E. Blelloch, and R. Harper, “Adaptive functional programming,” ACM Transactions on Programming Languages and Systems, vol. 28, no. 6, pp. 990–1034, 2006, doi: 10.1145/1186632.1186634.
[46] webpack, “Hot Module Replacement.” [Online]. Available: https://webpack.js.org/api/hot-module-replacement/
[47] Vite, “HMR API.” [Online]. Available: https://vite.dev/guide/api-hmr
[48] E. N. Elnozahy, L. Alvisi, Y.-M. Wang, and D. B. Johnson, “A Survey of Rollback-Recovery Protocols in Message-Passing Systems,” ACM Computing Surveys, vol. 34, no. 3, pp. 375–408, 2002, doi: 10.1145/568522.568525.
[49] H. Garcia-Molina and K. Salem, “Sagas,” in Proceedings of the 1987 ACM SIGMOD International Conference on Management of Data, in SIGMOD '87. 1987, pp. 249–259. doi: 10.1145/38713.38742.
[50] OSGi Alliance, OSGi Core Release 8. OSGi Alliance, 2020. [Online]. Available: https://docs.osgi.org/specification/osgi.core/8.0.0/
[51] J. Kramer and J. Magee, “The Evolving Philosophers Problem: Dynamic Change Management,” IEEE Transactions on Software Engineering, vol. 16, no. 11, pp. 1293–1306, 1990, doi: 10.1109/32.60317.
[52] Y. Vandewoude, P. Ebraert, Y. Berbers, and T. D'Hondt, “Tranquility: A Low Disruptive Alternative to Quiescence for Ensuring Safe Dynamic Updates,” IEEE Transactions on Software Engineering, vol. 33, no. 12, pp. 856–868, 2007, doi: 10.1109/tse.2007.70733.
[53] J. S. Rellermeyer, G. Alonso, and T. Roscoe, “R-OSGi: Distributed Applications Through Software Modularization,” in Proceedings of the ACM/IFIP/USENIX 8th International Middleware Conference, in Middleware '07. 2007, pp. 1–20. doi: 10.1007/978-3-540-76778-7_1.
[54] J. B. Dennis and E. C. Van Horn, “Programming Semantics for Multiprogrammed Computations,” Communications of the ACM, vol. 9, no. 3, pp. 143–155, 1966, doi: 10.1145/365230.365252.
[55] M. S. Miller, K.-P. Yee, and J. Shapiro, “Capability Myths Demolished,” technical report SRL2003–2, 2003. [Online]. Available: http://zesty.ca/capmyths/usenix.pdf
[56] R. N. M. Watson, J. Anderson, B. Laurie, and K. Kennaway, “Capsicum: Practical Capabilities for UNIX,” in Proceedings of the 19th USENIX Security Symposium, 2010, pp. 29–46. [Online]. Available: https://www.usenix.org/legacy/events/sec10/tech/full_papers/Watson.pdf
[57] R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham, “Efficient Software-Based Fault Isolation,” in Proceedings of the 14th ACM Symposium on Operating Systems Principles, in SOSP '93. 1993, pp. 203–216. doi: 10.1145/168619.168635.
[58] A. Barth, A. P. Felt, P. Saxena, and A. Boodman, “Protecting Browsers from Extension Vulnerabilities,” in Proceedings of the 17th Annual Network and Distributed System Security Symposium, in NDSS '10. 2010. [Online]. Available: https://www.ndss-symposium.org/ndss2010/protecting-browsers-extension-vulnerabilities/
[59] W. W. Ho and R. A. Olsson, “An Approach to Genuine Dynamic Linking,” Software: Practice and Experience, vol. 21, no. 4, pp. 375–390, 1991, doi: 10.1002/SPE.4380210404.
[60] P. Wadler and S. Blott, “How to Make Ad-hoc Polymorphism Less Ad Hoc,” in Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, in POPL '89. 1989, pp. 60–76. doi: 10.1145/75277.75283.
[61] N. D. Matsakis and F. S. K. II, “The Rust Language and Type System,” in ACM SIGPLAN ML Family Workshop, Gothenburg, Sweden, Sep. 2014.
[62] D. Dreyer, R. Harper, M. M. T. Chakravarty, and G. Keller, “Modular Type Classes,” in Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, in POPL '07. 2007, pp. 63–70. doi: 10.1145/1190216.1190229.
[63] Microsoft, “Declaration Merging.” [Online]. Available: https://www.typescriptlang.org/docs/handbook/declaration-merging.html
[64] T. Van Cutsem and M. S. Miller, “Proxies: Design Principles for Robust Object-oriented Intercession APIs,” in Proceedings of the 6th Symposium on Dynamic Languages, in DLS '10. 2010, pp. 59–72. doi: 10.1145/1869631.1869638.
[65] R. Hettinger, “Descriptor HowTo Guide.” [Online]. Available: https://docs.python.org/3/howto/descriptor.html
[66] P. Maes, “Concepts and Experiments in Computational Reflection,” in Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 1987, pp. 147–155. doi: 10.1145/38765.38821.
[67] G. Bracha and D. M. Ungar, “Mirrors: design principles for meta-level facilities of object-oriented programming languages,” in Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2004, pp. 331–344. doi: 10.1145/1028976.1029004.
[68] R. Rouvoy and P. Merle, “Leveraging component-based software engineering with Fraclet,” Annals of Telecommunications, vol. 64, no. 1–2, pp. 65–79, 2009, doi: 10.1007/s12243-008-0072-z.
[69] E. Burmako, “Scala Macros: Let Our Powers Combine!,” in Proceedings of the 4th Workshop on Scala, in SCALA@ECOOP '13. 2013, p. 3:1–3:10. doi: 10.1145/2489837.2489840.
[70] S. Raemaekers, A. van Deursen, and J. Visser, “Semantic Versioning and Impact of Breaking Changes in the Maven Repository,” Journal of Systems and Software, vol. 129, pp. 140–158, 2017, doi: 10.1016/j.jss.2016.04.008.
[71] P. Lam, J. Dietrich, and D. J. Pearce, “Putting the Semantics into Semantic Versioning,” in Proceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, in Onward! '20. 2020, pp. 157–179. doi: 10.1145/3426428.3426922.
[72] P. Abate, R. Di Cosmo, R. Treinen, and S. Zacchiroli, “Dependency Solving: A Separate Concern in Component Evolution Management,” Journal of Systems and Software, vol. 85, no. 10, pp. 2228–2240, 2012, doi: 10.1016/j.jss.2012.02.018.
[73] L. Cardelli, “Structural Subtyping and the Notion of Power Type,” in Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, in POPL '88. 1988, pp. 70–79. doi: 10.1145/73560.73566.
[74] B. Meyer, “Applying "Design by Contract",” Computer, vol. 25, no. 10, pp. 40–51, 1992, doi: 10.1109/2.161279.
[75] B. C. Pierce, “Bounded Quantification is Undecidable,” Information and Computation, vol. 112, no. 1, pp. 131–165, 1994, doi: 10.1006/inco.1994.1055.
[76] A. Haas et al., “Bringing the web up to speed with WebAssembly,” in Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ACM, 2017, pp. 185–200. doi: 10.1145/3062341.3062363.
[77] M. M. Swift, B. N. Bershad, and H. M. Levy, “Improving the reliability of commodity operating systems,” in Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP), ACM, 2003, pp. 207–222. doi: 10.1145/945445.945466.
[78] M. M. Swift, M. Annamalai, B. N. Bershad, and H. M. Levy, “Recovering device drivers,” ACM Transactions on Computer Systems, vol. 24, no. 4, pp. 333–360, 2006, doi: 10.1145/1189256.1189257.
[79] D. E. Porter, O. S. Hofmann, C. J. Rossbach, A. Benn, and E. Witchel, “Operating System Transactions,” in Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), ACM, 2009, pp. 161–176. doi: 10.1145/1629575.1629591.
[80] O. Kiselyov and C.-chieh Shan, “Delimited Continuations in Operating Systems,” in Modeling and Using Context (CONTEXT 2007), in Lecture Notes in Computer Science, vol. 4635. Springer, 2007, pp. 291–302. doi: 10.1007/978-3-540-74255-5_22.
[81] E. Dolstra and A. Löh, “NixOS: a purely functional Linux distribution,” in Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), ACM, 2008, pp. 367–378. doi: 10.1145/1411204.1411255.
[82] ZIO, “ZIO: Type-safe, composable asynchronous and concurrent programming for Scala.” [Online]. Available: https://zio.dev/
[83] Effect, “Effect: A TypeScript library for building robust applications.” [Online]. Available: https://effect.website/
[84] G. Canti, “fp-ts: Functional programming in TypeScript.” [Online]. Available: https://github.com/gcanti/fp-ts
[85] J. I. Brachthäuser, P. Schuster, and K. Ostermann, “Effects as capabilities: effect handlers and lightweight effect polymorphism,” Proc. ACM Program. Lang., vol. 4, no. OOPSLA, 2020, doi: 10.1145/3428194.
[86] J. I. Brachthäuser, P. Schuster, E. Lee, and A. Boruch-Gruszecki, “Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back,” Proc. ACM Program. Lang., vol. 6, no. OOPSLA1, 2022, doi: 10.1145/3527320.
[87] C. Heunen, R. Kaarsgaard, and M. Karvonen, “Reversible Effects as Inverse Arrows,” in Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV), in Electronic Notes in Theoretical Computer Science, vol. 341. 2018, pp. 179–199. doi: 10.1016/j.entcs.2018.11.009.
[88] D. Orchard, V.-B. Liepelt, and H. Eades III, “Quantitative program reasoning with graded modal types,” Proc. ACM Program. Lang., vol. 3, no. ICFP, 2019, doi: 10.1145/3341714.
[89] R. Bianchini, F. Dagnino, P. Giannini, E. Zucca, and M. Servetto, “Coeffects for sharing and mutation,” Proc. ACM Program. Lang., vol. 6, no. OOPSLA2, Oct. 2022, doi: 10.1145/3563319.
[90] R. Bianchini, F. Dagnino, P. Giannini, and E. Zucca, “A Java-like calculus with heterogeneous coeffects,” Theoretical Computer Science, vol. 971, p. 114063, 2023, doi: https://doi.org/10.1016/j.tcs.2023.114063.
[91] C. Torczon, E. Suárez Acevedo, S. Agrawal, J. Velez-Ginorio, and S. Weirich, “Effects and Coeffects in Call-by-Push-Value,” Proc. ACM Program. Lang., vol. 8, no. OOPSLA2, Oct. 2024, doi: 10.1145/3689750.
[92] R. Hirschfeld, P. Costanza, and O. Nierstrasz, “Context-oriented Programming,” Journal of Object Technology, vol. 7, no. 3, pp. 125–151, 2008, doi: 10.5381/jot.2008.7.3.a4.
[93] P. Costanza and R. Hirschfeld, “Language constructs for context-oriented programming: an overview of ContextL,” in Proceedings of the 2005 Symposium on Dynamic Languages (DLS '05), ACM, 2005, pp. 1–10. doi: 10.1145/1146841.1146842.
[94] G. Salvaneschi, C. Ghezzi, and M. Pradella, “Context-oriented programming: A software engineering perspective,” Journal of Systems and Software, vol. 85, no. 8, pp. 1801–1817, 2012, doi: 10.1016/j.jss.2012.03.024.
[95] G. Kiczales et al., “Aspect-Oriented Programming,” in ECOOP'97 — Object-Oriented Programming, 11th European Conference, in Lecture Notes in Computer Science, vol. 1241. Springer, 1997, pp. 220–242. doi: 10.1007/BFb0053381.
[96] G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. G. Griswold, “An Overview of AspectJ,” in ECOOP 2001 — Object-Oriented Programming, 15th European Conference, in Lecture Notes in Computer Science, vol. 2072. Springer, 2001, pp. 327–353. doi: 10.1007/3-540-45337-7_18.
[97] A. Popovici, T. Gross, and G. Alonso, “Dynamic Weaving for Aspect-Oriented Programming,” in Proceedings of the 1st International Conference on Aspect-Oriented Software Development (AOSD 2002), ACM, 2002, pp. 141–147. doi: 10.1145/508386.508404.
[98] J. Bonér, “What Are the Key Issues for Commercial AOP Use: How Does AspectWerkz Address Them?,” in Proceedings of the 3rd International Conference on Aspect-Oriented Software Development (AOSD 2004), ACM, 2004, pp. 5–6. doi: 10.1145/976270.976273.
[99] M. Hicks, J. T. Moore, and S. Nettles, “Dynamic Software Updating,” in Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, in PLDI '01. 2001, pp. 13–23. doi: 10.1145/378795.378798.
[100] G. Stoyle, M. Hicks, G. Bierman, P. Sewell, and I. Neamtiu, “Mutatis Mutandis: Safe and Predictable Dynamic Software Updating,” in Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, in POPL '05. 2005, pp. 183–194. doi: 10.1145/1040305.1040321.
[101] C. M. Hayden, K. Saur, E. K. Smith, and M. Hicks, “Kitsune: Efficient, General-Purpose Dynamic Software Updating for C,” ACM Trans. Program. Lang. Syst., vol. 36, no. 4, 2014, doi: 10.1145/2629460.
[102] M. Overeem, M. Spoor, and S. Jansen, “The Dark Side of Event Sourcing: Managing Data Conversion,” in IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, in SANER '17. 2017, pp. 193–204. doi: 10.1109/SANER.2017.7884621.
[103] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns: Elements of Reusable Object-Oriented Software. Boston, MA: Addison-Wesley, 1994.
[104] D. Leijen, “Algebraic Effect Handlers with Resources and Deep Finalization,” technical report MSR-TR-2018-10, Apr. 2018. [Online]. Available: https://www.microsoft.com/en-us/research/publication/algebraic-effect-handlers-resources-deep-finalization/
[105] M. Fowler, “Event Sourcing.” 2005.
[106] J. Lee, J. Ahn, and K. Yi, “React-tRace: A Semantics for Understanding React Hooks,” Proc. ACM Program. Lang., vol. 9, no. OOPSLA2, pp. 471–498, 2025, doi: 10.1145/3763067.
[107] N. Shavit and D. Touitou, “Software Transactional Memory,” in Proceedings of the Fourteenth Annual ACM Symposium on Principles of Distributed Computing, in PODC '95. 1995, pp. 204–213. doi: 10.1145/224964.224987.
[108] T. Harris, S. Marlow, S. Peyton Jones, and M. Herlihy, “Composable Memory Transactions,” in Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, in PPoPP '05. 2005, pp. 48–60. doi: 10.1145/1065944.1065952.
[109] M. Herlihy and J. E. B. Moss, “Transactional Memory: Architectural Support for Lock-Free Data Structures,” in Proceedings of the 20th Annual International Symposium on Computer Architecture, in ISCA '93. 1993, pp. 289–300. doi: 10.1145/165123.165164.
[110] R. Landauer, “Irreversibility and Heat Generation in the Computing Process,” IBM Journal of Research and Development, vol. 5, no. 3, pp. 183–191, 1961, doi: 10.1147/rd.53.0183.
[111] C. H. Bennett, “Logical Reversibility of Computation,” IBM Journal of Research and Development, vol. 17, no. 6, pp. 525–532, 1973, doi: 10.1147/rd.176.0525.
[112] T. Yokoyama and R. Glück, “A Reversible Programming Language and its Invertible Self-Interpreter,” in Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, in PEPM '07. 2007, pp. 144–153. doi: 10.1145/1244381.1244404.
[113] V. Danos and J. Krivine, “Reversible Communicating Systems,” in CONCUR 2004 — Concurrency Theory, 15th International Conference, in Lecture Notes in Computer Science, vol. 3170. Springer, 2004, pp. 292–307. doi: 10.1007/978-3-540-28644-8_19.
[114] I. Phillips and I. Ulidowski, “Reversing Algebraic Process Calculi,” in Foundations of Software Science and Computation Structures, 9th International Conference (FOSSACS 2006), in Lecture Notes in Computer Science, vol. 3921. Springer, 2006, pp. 246–260. doi: 10.1007/11690634_17.
[115] P. Wadler, “Linear Types Can Change the World!,” in Programming Concepts and Methods: Proceedings of the IFIP Working Group 2.2/2.3 Working Conference, North-Holland, 1990, pp. 561–581. [Online]. Available: https://homepages.inf.ed.ac.uk/wadler/papers/linear/linear.ps
[116] A. Lenharth, V. S. Adve, and S. T. King, “Recovery domains: an organizing principle for recoverable operating systems,” in Proceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), ACM, 2009, pp. 49–60. doi: 10.1145/1508244.1508251.
[117] C. Walls, Spring in Action, 6th ed. Manning Publications, 2022. [Online]. Available: https://www.manning.com/books/spring-in-action-sixth-edition
[118] C. Escoffier, R. S. Hall, and P. Lalanda, “iPOJO: an Extensible Service-Oriented Component Framework,” in IEEE International Conference on Services Computing, 2007, pp. 474–481. doi: 10.1109/SCC.2007.74.
[119] H. Cervantes and R. S. Hall, “Autonomous Adaptation to Dynamic Availability Using a Service-Oriented Component Model,” in Proceedings of the 26th International Conference on Software Engineering, in ICSE '04. 2004, pp. 614–623. doi: 10.1109/ICSE.2004.1317483.
[120] C. Elliott and P. Hudak, “Functional Reactive Animation,” in Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming, in ICFP '97. 1997, pp. 263–273. doi: 10.1145/258948.258973.
[121] G. H. Cooper and S. Krishnamurthi, “Embedding Dynamic Dataflow in a Call-by-Value Language,” in Programming Languages and Systems (ESOP 2006), in Lecture Notes in Computer Science, vol. 3924. Springer, 2006, pp. 294–308. doi: 10.1007/11693024_20.
[122] I. Maier and M. Odersky, “Deprecating the Observer Pattern with Scala.React,” technical report EPFL-REPORT-176887, 2012. [Online]. Available: https://infoscience.epfl.ch/record/176887
[123] E. Bainomugisha, A. L. Carreton, T. Van Cutsem, W. De Meuter, and others, “A Survey on Reactive Programming,” ACM Comput. Surv., vol. 45, no. 4, 2013, doi: 10.1145/2501654.2501666.
[124] A. Margara and G. Salvaneschi, “On the Semantics of Distributed Reactive Programming: The Cost of Consistency,” IEEE Trans. Software Eng., vol. 44, no. 7, pp. 689–711, 2018, doi: 10.1109/TSE.2018.2833109.