中 文 全 译 本

一种时空可组合性的编程范式

A Programming Paradigm for Spatiotemporal Composability
石一帆 1,2 张伟 1 崔天一 2
1 北京大学 2 DeepSeek-AI
全文 88 页 · 完整翻译公式 KaTeX 排版术语统一
翻译说明
  • 本文为 A Programming Paradigm for Spatiotemporal Composability(88 页)的逐页完整中文翻译;数学公式以 LaTeX 重排,编号与原文一致。
  • 图 1、图 2 为原文中的矢量状态图,本页重绘为矢量图并附文字描述;表格重建为 HTML 表格。
  • 参考文献(124 条)按国际惯例保留英文原文;正文中的虚线标记(如「第 12 页」)对应原文页码,便于与 PDF 对照。
  • 文内引用 [n] 可点击跳转至文末对应文献条目。
目录

摘要

现代软件——从插件系统到自进化的智能体框架——越来越需要动态组合(dynamic composition),然而其形式化基础仍然欠发达。我们识别出该问题的两个正交维度:时间可组合性(temporal composability),即在移除某个组件时能够完全撤销其副作用的能力;以及空间可组合性(spatial composability),即能够声明并响应式地管理组件间依赖的能力。我们通过将经典的效应(effect)与共效应(coeffect)概念提升为运行时机制来应对这两个维度。

具体而言,我们形式化了可逆效应(revertible effects):其中每一个上下文变换都携带一个逆变换,并由运行时跟踪维护。我们还形式化了响应式共效应(reactive coeffects):其中上下文的每一次变化都会依据组件的共效应规范对该组件发出通知。我们将效应上下文与共效应上下文统一为单一的上下文类型(context type),由此构成一种编程范式。

在此基础上,我们将这些机制组合成组件(component)这一概念,并给出一个动态组合演算;该演算的元理论将时空可组合性从单个组件推广到由交错组件构成的整个系统。我们以 Cordis 实现了这些思想——一个关于时空可组合性的元框架,它提供了一个具备效应跟踪与共效应解析的核心库,以及一个具备配置协调与热模块替换能力的声明式组件加载器。


第 4 页

1 引言

组合(composition)——由较简单的部分装配出复杂系统——是软件工程的基本原理 [1]。传统上,组合是静态的:函数调用、模块导入和类继承在编译期解析,并在整个执行期间保持不变。然而,现代软件日益需要动态组合(dynamic composition),即组件(component)在运行时被加载、卸载和重新配置。插件架构 [2] 与自进化智能体框架(agent harness)都要求系统能够安全地即时添加和移除功能,然而当前的实践却诉诸粗粒度的机制 [3],只能通过重启来重新配置,从而丢弃运行时状态。尽管动态组合的实际重要性日益增长,但与静态组合(static composition)所拥有的丰富形式框架相比,其理论基础仍不发达。

1.1 可组合性的维度

为了刻画动态组合的需求,我们在组合已被充分研究的代数方面之外,识别出两个正交的维度:

  • 时间可组合性(temporal composability)处理时间维度:当一个组件被移除时,该组件对共享环境所做的修改必须被完全且安全地撤销。这要求跟踪组件执行的每一次资源分配、事件注册和状态变更,并保证在移除时有序地回收它们。
  • 空间可组合性(spatial composability)处理空间维度:组件必须能够以结构化的、可验证的方式声明、发现和解析彼此之间的依赖。这要求管理依赖拓扑(dependency topology),并根据依赖变化协调组件的生命周期(lifecycle)。

在静态情形下,时间可组合性归结为词法作用域(lexical scoping)(例如 RAII(资源获取即初始化)[4]、括号模式(bracket patterns)[5]),空间可组合性归结为模块导入解析(module import resolution)[6]。在动态情形下,组件在运行时到来和离开,两个维度都变得困难得多:时间可组合性必须处理作用域不受词法约束的、有状态的长生命周期效应(effect);空间可组合性必须处理在执行期间出现、消失或改变身份的依赖。

1.2 动机示例

1.2.1 插件系统

插件系统是动态组合的典型实例。我们以 Visual Studio Code(VSCode)——使用最广泛的、可扩展的 IDE 之一——作为代表性示例。

时间方面的局限。 VSCode 在称为扩展宿主(extension host)的共享进程中运行所有扩展。虽然扩展可以动态安装,但该宿主不提供在运行时卸载单个扩展代码的机制。一旦扩展的激活函数(activate function)执行完毕,停用或卸载它就需要重启整个宿主,从而影响所有已加载的扩展。纯声明式的扩展,如主题、键绑定和代码片段,不携带任何

第 5 页

代码,可以随意移除。然而,在按安装量排名的前 100 个扩展中,有 87 个包含可执行代码1,因此在移除时需要这样的重启。尽管 VSCode 提供了停用钩子(deactivate hook),但它只是宿主进程终止期间的一个优雅关闭回调,并不能实现热移除(live removal)。此外,该钩子将效应释放与效应创建(在激活函数中)分离开来,违反了关注点的局部性,使得完整清理难以验证。

空间方面的局限。 VSCode 确实提供了 extensionDependencies 用于声明扩展之间的依赖,但它很少被使用:在按安装量排名的前 100 个扩展中,只有 7 个声明了对非内置扩展的 extensionDependencies1。这种稀缺性反映了扩展 API 的形态:它暴露的是固定的、表层的扩展点,如命令、视图和语言功能。扩展通过这些扩展点向宿主贡献功能,而不是相互依赖,因此扩展间的依赖很少出现。此外,VSCode 的扩展间交互机制不提供任何结构契约:它通过 vscode.extensions.getExtension(...).exports 向其他扩展暴露一个扩展的功能,但返回值是无类型的(默认是 any),因此依赖者无法依赖一个经过检查的接口。总之,VSCode 将扩展引向一组固定的、由宿主提供的扩展点,却没有为它们提供安全、结构化的相互依赖方式。

这两个局限并非 VSCode 所独有;它们普遍存在于各类插件系统中 [2, 7],只是程度不同。

1.2.2 自进化智能体框架

现代 AI 智能体依赖运行时智能体框架 [8–10]。这些系统可以组合多样化的工具套件 [11] 和执行环境,管理权限与沙箱化(sandboxing),维护会话状态与持久化,提供上下文管理与记忆系统 [12],编排子智能体与多智能体工作流 [13],并向用户和自动化暴露接口。未来的框架可能会在持续服务请求的同时,生成并部署对其自身组件的修改。模型合成的可复用工具为组件级自修改提供了范围更窄的先导 [14]。每一次这样的修改本身都是动态组合的一个实例。

由于这些修改持续发生,且人工监督有限甚至没有,动态可组合性变得不可或缺。没有时间可组合性,每一次自修改都会迫使完整重启,丢弃所有进程本地的累积状态;在这样的频率下,累计的不可用时间变得相当可观,进行中的任务被反复打断;更糟的是,一次有缺陷的自修改可能会使本用于恢复的进程本身失效。没有空间可组合性,每个模块都必须自行检测其依赖的模块在出现、消失或改变身份时的变化并作出适应,而且只能通过临时(ad hoc)手段做到这一点;更糟的是,一种天真的代码替换策略可能悄然破坏依赖者,或引入只有在重载时才会暴露出来的循环依赖。

1.2.3 粗粒度的变通方案

动态可组合性之所以得到的正式关注有限,一个原因是操作系统和容器编排器(container orchestrator)已经提供了粗粒度的替代品。操作系统以进程为粒度提供时间可组合性;容器编排器

1 数据取自 Visual Studio Code 扩展市场(Marketplace),检索日期为 2026 年 6 月 9 日。

第 6 页

[3] 以服务为粒度提供空间可组合性。在实践中,大多数软件通过诉诸这些粗粒度机制来容忍细粒度可组合性的缺失:一个行为异常的模块通过重启进程来处理,一个服务依赖由容器编排器来管理。

然而,这种变通方案代价高昂。在时间方面,每次重启都会丢弃所有进程本地的累积状态(例如缓存、连接、部分计算结果),而重建它需要数秒到数分钟 [15];在此期间维持可用性需要冗余副本,以资源开销来弥补无法恢复单个组件的缺陷。在空间方面,容器级编排无法表达共享同一地址空间的组件之间的依赖,并且为本可以是本地函数调用的交互引入了网络开销。这两种机制都在进程和容器的边界处运作,而现代系统却越来越多地在更细的层级上进行组合。这种粒度错配要求一种组合抽象,它能够在与组件本身相同的层级上管理效应和依赖。

1.3 贡献

动态可组合性的两个维度分别涉及计算如何修改其环境,以及如何依赖其环境。这两个方向正是效应系统(effect system)[16, 17] 与共效应系统(coeffect system)[18, 19] 所形式化的内容:效应为关于环境修改的推理提供了形式化词汇,共效应则为关于环境需求的推理提供了形式化词汇。然而,现有的表述把推理限制在词法固定的作用域上的编译期分析,并没有扩展到组件在运行时到来和离开的动态场景。通过把效应提升(lift)为可逆的运行时模型,把共效应提升为响应式的依赖解析机制,我们为动态组合获得了统一的形式化基础——一个与语言无关、适用于任何需要动态组合的软件架构的基础。我们做出如下贡献:

  1. 我们形式化了可逆效应(revertible effects)(第 3.1 节):每一个上下文变换都携带一个由运行时跟踪的显式逆(inverse),且跟踪与恢复都保持组合性,因此组件被移除时上下文得以恢复。这确立了局部时间可组合性。
  2. 我们形式化了响应式共效应(reactive coeffects)(第 3.2 节):组件把其所需的共效应声明为一种规格,上下文的每次变化都会对照该规格把组件通知为激活、停用或中性。这确立了局部空间可组合性。
  3. 我们把效应上下文(effect context)与共效应上下文(coeffect context)统一为单一的上下文类型(context type)(第 3.3 节),其中共效应上的观察等价(observational equivalence)为效应提供了独立性,从而构成了时空可组合性(spatiotemporal composability)的一种编程范式。
  4. 我们给出了动态组合的演算(calculus)(第 4 节),它将这两种机制结合为组件这一概念,并为其生命周期配备了操作语义(operational semantics)。其元理论(metatheory)把时空可组合性从单个组件推广到由交错(interleaved)组件构成的整个系统。
  5. 我们在 Cordis(第 5 节)中实现了这些思想。Cordis 是一个时空可组合性的元框架(meta-framework),它提供了一个核心库(core library),通过效应跟踪(effect tracking)与共效应解析(coeffect resolution)实现上述形式模型,此外还提供了一个声明式(declarative)组件加载器(component loader),支持配置协调(configuration reconciliation)与热模块替换(hot module replacement)。
第 7 页

2 预备知识

本节简要概述效应系统与共效应系统——支撑我们工作的两大理论支柱。我们假定读者熟悉基础类型论与范畴论;此处的目标在于固定记号,并引入第 3 节将作为运行时机制加以实现的核心抽象。

2.1 效应

在简单类型 λ 演算(STLC)[20, 21] 中,类型判断 表示在上下文 下,项 具有类型 。效应系统对类型加以细化,用以描述计算可能产生的副作用,得到如下形式的判断:

此处,结果类型被标注以效应代数中的一个元素,该元素描述计算可能产生的副作用,从而能够对有状态计算进行组合式推理。这一方法源于 Lucassen 与 Gifford [22],他们引入了一种带种类(kind)的类型系统,区分类型、效应与区域,以发现并行程序中的调度约束。

单子效应。 Moggi [16] 首先通过单子以范畴论方式对计算效应建模;Wadler [23] 在 Haskell 中推广了这一方法。范畴 上的单子 将带效应的计算封装为类型 的值,其中 提升纯值, 将嵌套计算顺序串联。经典实例包括 Maybe 单子(用于部分性)、State 单子(用于可变状态)与 IO 单子(用于外部交互)。

代数效应。 Plotkin 与 Power [17, 24] 证明了代数运算确定单子,建立了一个使效应接口与其实现解耦的框架。效应签名 声明一组运算(例如状态的 );程序可以自由地调用这些运算,而不必承诺某种特定的解释。Plotkin 与 Pretnar [25] 随后引入了效应处理器,通过提供续延语义来解释运算:

处理器接收运算参数 与定界续延 ,并可调用后者零次、一次或多次,从而在统一框架内实现异常、协程与非确定性 [26]。Koka [27, 28]、Eff [29] 与 OCaml 5 [30] 等语言已采用代数效应,并体现了不同的设计权衡。

2.2 共效应

与效应相对偶地,共效应系统 [18, 31] 丰富的是上下文而非类型,得到如下形式的判断:

此处,上下文被标注以共效应代数中的一个元素,该元素描述计算从环境中需要什么,例如需要访问的资源、需要持有的权限,

第 8 页

或需要依赖的服务。效应刻画程序对世界的影响,而共效应刻画世界对程序的约束。

余单子共效应。 利用余单子组织上下文相关计算的想法最早由 Uustalu 与 Vene [32] 提出,他们提出了对称(半)幺半余单子,作为 Moggi 单子框架(用于效应)的对偶,用以刻画数据流与属性求值等概念。Petricek 等人 [18] 在此基础上提出将共效应作为上下文相关性的统一静态分析。余单子 刻画上下文相关计算: 从上下文中提取当前值, 为嵌套访问复制上下文。环境余单子 刻画对固定环境 的依赖;流余单子 刻画对时间数据的依赖。

分级共效应。 为进行更细粒度的跟踪,分级共效应系统使用预序半环 作为共效应代数 [33],这一做法后来由 Gaboardi 等人 [19] 与分级效应统一。 的元素标注每个变量绑定,以量化其使用情况: 表示未使用, 表示线性使用, 表示有界使用, 表示无限制使用。半环运算按顺序()与并行()方式复合共效应,从而能够在统一的代数框架 [37] 内实现精确的资源跟踪、敏感性分析 [34] 与信息流控制 [35, 36]

2.3 与动态可组合性的关系

效应系统与共效应系统沿两个互补的方向组织对计算的推理:效应描述计算如何修改其环境,而共效应描述计算如何依赖其环境。这两个方向恰好对应第 1 节所确定的动态可组合性的两个维度:

  • 时间可组合性要求组件对共享环境的修改在卸载时可逆。相关的效应是有状态效应,它们持久地变换该环境;撤销这种变换要求该变换存在逆。
  • 空间可组合性要求组件间依赖被声明,并以响应式方式加以管理。这类依赖正是共效应所刻画的,而管理它们即是将每一依赖对照环境所提供的内容进行解析。

然而,经典效应与共效应系统是静态工具:效应在词法固定的作用域内被跟踪,并由编译期处理器释放;共效应标注根据执行前确定的上下文进行验证。相比之下,动态组合要求这些保证对在运行时到达与离开的组件依然成立,而面对的上下文是持续演化的。任何固定的词法作用域都无法界定部署之后才加载的插件;任何编译期上下文都无法预见由运行时配置产生的依赖。

这促使视角发生转变:与其用更多标注扩展静态类型系统,我们将效应与共效应的概念结构具体化,使运行时能够直接对其操作,从而动态地建立起这些系统静态提供的保证。

第 9 页

3 可逆效应与响应式共效应

本节将第 2 节引入的效应(effect)与共效应(coeffect)概念提升为运行时机制,构建起一套动态组合(dynamic composition)理论。其核心思想是把携带效应与共效应的类型上下文(typing context)转化为上下文类型(context type),即把上下文具体化(reify)为头等(first-class)实体的、可在运行时操作的类型。对于效应类型,我们将其建模为配有一个逆变换(inverse)的上下文变换,从而实现局部的时间可组合性(temporal composability);对于共效应上下文,我们将其建模为携带依赖(dependency)信息的类型,从而实现局部的空间可组合性(spatial composability)。共效应上的一个观察等价(observational equivalence)关系随即赋予效应以独立性。同时携带效应与共效应的统一上下文,其本身便构成了一种编程范式。

3.1 可逆效应

时间可组合性是指这样一种能力:在运行时装载与卸载组件,使得卸载后共享环境恢复到组合之前的状态。这就要求组件对环境所作的每一次修改都既可跟踪又可恢复。因此,我们把效应建模为类型 的函数:将其作用于当前上下文,便得到修改后的上下文以及显式的逆变换。提供这个逆变换正是效应得以被逆转的原因,而把它交还给运行时则使效应可被跟踪。我们把这样的效应称为可逆效应(revertible effects):通过在执行过程中跟踪并复合这些逆变换,环境的完全恢复便成为一种结构性保证。

3.1.1 效应上下文

给定任意不纯函数 ,我们将其变换为纯形式 ,其中 是上下文,所有可能的副作用(side effects)都可以表示为 上的变换。对任意固定的输入 ,诱导映射 独立于返回值地刻画了 的副作用。因此, 上的效应生活在复合运算 下的变换幺半群(monoid) 之中,其中每一条幺半群公理都可以直接读作效应的一条性质:

  • 封闭性(closure):两个效应的顺序复合仍然是一个效应;
  • 结合律(associativity):复合效应与括号的加括方式无关;
  • 恒等性(identity):,即 上的恒等函数,充当复合的单位元(unit)。

为了对可被撤销的效应建模,我们把每个变换 与另一个撤销 的变换 配对,称 的左逆变换,本文以下简称为逆。撤销是单侧的:逆变换所应满足的是 ,而绝不是 。变换对带有它们自己的乘法运算:

定义 1. 定义上下文变换对的扭转复合(twisted composition)如下:

本身一样,左操作数在右操作数之后作用,而逆变换以相反的顺序累积。这使 成为一个以 为单位元的幺半群,即变换幺半群与其反向幺半群(opposite monoid)的乘积,我们称之为 上的扭转复合幺半群(twisted composition monoid)

为了在上下文内部跟踪效应,我们引入如下定义:

第 10 页

定义 2. 给定上下文 ,定义其效应上下文(effect context)为:

它可以理解为二元组 ,其中:

  • 是当前上下文状态;
  • 是累加器(accumulator),即迄今为止所执行的效应的逆变换的复合,也是把上下文恢复到其初始状态的函数。

特别地,初始效应上下文可以表示为

我们还记 ,并依此类推,沿塔逐层向上。

由于累加器 的存在,在 上执行的所有效应都可以被跟踪并恢复。现在我们给出跟踪与恢复的具体构造。

定义 3. 在上下文函数对上定义变换

该变换把正向函数 连同候选逆变换 转化为效应上下文 上的一个变换。将 作用于状态 ,会用 变换 ,并把逆变换 复合到 上,从而在上下文中跟踪 的效应。

定理 4. 对每个 ,下图可交换(commutes),即

证明. 对所有

定理 5. 是从 的幺半群同态(monoid homomorphism)。即:

  1. 对所有

证明.

  1. 单位元被送到单位元,因为
  2. 对于乘法,任取
第 11 页

定义 6. 上定义变换

该变换把恢复函数 作用于当前状态 ,并将 重置为恒等函数。下图说明:在对 依次应用一系列效应 之后, 如何把上下文恢复到其初始状态:

该图表明:被跟踪的效应之后接上 ,会把初始效应上下文送回其自身。每个跟踪步骤所保持的,正是恢复本身的结果——无论从何种状态出发都是如此:

定理 7. 对每个 以及每一对满足 ,有

证明.

对于变换对的序列,无需另行论证。设 出发按顺序依次应用,并记 。由定理 5,复合 是扭转复合 ;若对每个 都有 ,则 。因此该变换对在 处满足定理 7 的前提,对定理应用一次即得

,恢复会把按此方式到达的每一个状态都送回 。满足 的变换对在每一个状态处都满足前提。恢复通过量 来读取状态,我们把 称为 中状态的可靠性不变量(soundness invariant)。

第 12 页

3.1.2 可逆效应函数

上一节的 track/recover 模型把逆变换视为先验给定的: 在任何上下文状态可见之前就固定了 ,因此同一个 必须服务于效应所施加到的每一个状态。然而在实践中,每个效应的逆变换并非先验已知:它必须由调用者在施加效应之处提供。此外,recover 是全有或全无的:它无法在保留其他效应的同时选择性地撤销某一个效应。为了解决这两个问题,我们在输入侧和输出侧同时增强模型:

  1. 在输入侧,我们不仅变换 ,还随之返回一个逆函数,从而在效应施加处提供逆变换:,即
  2. 在输出侧,我们不仅变换 ,还随之返回一个逆函数,从而可以在保留其他效应的同时撤销某一个效应:,即

这一增强保持了输入与输出之间的结构一致性,因此我们仍可定义相应的理论,以保持 track 的数学性质。由此得到的类型是效应函数 及其带见证的细化

定义 8. 定义效应函数 与带见证的效应函数 如下:

其中 产生一个对 ,表示:

  • 是新上下文;
  • 是当前效应的逆函数。

的元素按状态选择其逆变换,约束 将该选择限制为在效应施加处撤销该效应,而在其他任何地方都不对 施加约束。单个满足 即可在所有状态上同时满足该约束,并通过 诱导出 的一个元素;定理 11 表明这是一个同态。该约束可用如下交换图直观表示,确保 所返回的逆变换确实在 施加处的状态上逆转相应的变换:

(图中 之间以两条方向相反的箭头相连: 自左向右、 自右向左; 自上端左侧的 向下指向 向上指向右上角的 竖直向上指向顶部的两条箭头,即把对 的第二分量 投影出来。该图的交换性即见证条件 。)

由于效应函数 不再是上下文上的自同态,它们不能直接复合。为此我们定义一个新的效应复合运算:

定义 9. 给定函数 ,定义它们的效应复合 如下:

第 13 页

定理 10. 效应复合把 的幺半群结构迁移到 上。即:

  1. 是以 为单位元的幺半群;
  2. 指派 是从 的幺半群同态。

证明.

  1. 结合律与单位元律由 的相应性质逐分量成立。
  2. ;则 ,这正是 的像,且 映到

定理 11. 见证性质在效应复合下得以保持,且统一的逆变换在每个状态上都构成见证。即:

  1. 的子幺半群;
  2. 定理 10 的同态把每个满足 的对都映到 中。

证明.

  1. 由于 ,单位元属于 。对封闭性,取 及任意 ,设 ,从而 。则 ,因此
  2. 给出每个 处的 ,因此这样的对的像在每个状态上都被见证。

正如 track 把 上的一对变换提升到 ,我们定义 effect 把 提升到

定义 12. 定义效应函数变换 如下:

由于 本身是 的元素,它所返回的是按定义 8 的含义向上读一层的逆变换。该逆变换本身是对交换效应两个方向后所得之对的 track。普通的跟踪规则再次适用:撤销该效应本身就是一个效应,它以 变换状态;而要撤销这个撤销,只需再次施加该效应——这正是 所做的。因此,该逆变换复合到交给它的累加器上,正如 track 所规定的那样。

现在我们可以证明 effect 与 track 类似的性质。

定理 13. effect 保持 运算。即

证明. 取任意 ,设 ,从而 。则

第 14 页

其中第一步在 处展开定义 12,第二步是定理 5,第三步折叠定义 12。

两个层级之间的关系如下图所示。其上部三角形是 的见证条件(依定义 8),其下部三角形则是 是否像 那样被见证的问题。

(图中上部三角形为 的见证条件: 两条方向相反的箭头相连, 向下指向该三角形的底端, 自底端向上;中部为提升后的对,以 两条方向相反的箭头在 上相连;下部三角形为 的见证条件,结构相同,其底端为 。图中左侧标有 effect 的箭头表示上层的效应箭头 。)

在两个层级之间,投影 把每个被提升的映射与它所提升的映射联系起来,正如它在定理 4 中对 所做的那样。

定理 14.,记 ,并设 ,其正向映射为 。则

  1. 对每个 ,在该处被见证的提升逆变换 与逆变换 满足

证明.

  1. 由定义 12,,其状态为
  2. 这就是定理 4 应用于

下部三角形是否闭合,可以通过计算被提升的逆变换的返回值来判定:

定理 15.,记 。固定 ,设 ,并记 处的值。则

状态被精确恢复。累加器同样被恢复——等价地,——当且仅当 ;并且在任何情形下都有 ,因此可靠性不变量得以保持。

证明. 由定义 12,,所以

第 15 页

利用 。属于 要求它在每个输入处都等于 ;取 可将累加器的相等性转化为 ,而该条件反过来又给出对每个 都成立的累加器相等性。最后,

下三角因此只有在 处被见证的逆变换于每个状态都逆转 时才闭合,所以 不会把 带入 。在所有情形下都成立的,是在 处的一致:,这正是定理 7 对累加器所假设的全部内容,因此逆转不会触及恢复目标。

按与应用相反的顺序逆转效应无需更多条件,因为此时每个逆变换面对的正是其自身应用所产生的状态:

定理 16. 开始按序应用,并按相反顺序逆转。则

  1. 每次逆转都恢复其应用运行所针对的上下文状态;
  2. 每个中间状态都满足可靠性不变量。

证明. 每一步都是一次应用或一次逆转。一次应用将 携带到 ,其中 ,因此由定理 7 它保持 ,而定理 7 的假设正是 的见证条件。按相反顺序逆转时,每个逆变换面对的正是其自身应用所产生的状态,因此由定理 15,该逆转精确恢复前一状态,并同样保持 ;两个结论都不依赖于逆变换所接收到的累加器。

3.1.3 效应的独立性

定理 16 所覆盖的,是在其自身应用所产生的状态上逆转某个效应;本小节所覆盖的,是在任何其他状态上逆转效应。有两种情形需要后者。其一,逆变换可能在后续效应仍处于作用中时运行——这正是从运行中的系统中撤回某个组件所意味的;其二,一个序列可能交错多个组件的效应,每个组件各自保留其自身的逆变换,使得一个组件的逆变换被另一组件的应用所隔开。在这两种情形中,逆变换面对的都是被外来效应移动过的状态,而它是否仍能逆转它被构造出来所要逆转的对象,是一个交换性问题:需要可交换的,是一个效应能执行的每个变换与另一个效应能执行的每个变换,前向映射与产出的逆变换均在其列。单一的累加器无法解决这两种情形中的任何一种,因为 是一个复合(变换),它以单一顺序、一次性运行其持有的所有逆变换。

定义 17. 对于效应函数 ,变换幺半群 的由 的前向映射连同 产出的每一个逆变换所生成的子幺半群,而 的生成元就是该生成集合中的元素:

由对 诱导的效应以 为其生成元,它在每个状态产出的逆变换都是

引理 18. 交换性只需在生成元上判定,且 不扩大任何变换幺半群。即:

  1. 的每个生成元都与 的每个生成元可交换,则 的每个元素都与 的每个元素可交换;
第 16 页

证明.

  1. 的每个生成元都可交换的映射构成 的一个子幺半群: 属于其中,并且只要 属于其中, 也属于其中。根据假设,该子幺半群包含 的生成元,因而包含 。固定 ,与 可交换的映射同样构成一个子幺半群,它包含 的生成元,因而包含
  2. 根据定义 9, 的前向映射是 ,且它在任意状态产出的逆变换是 ,其中 产出, 产出。因此, 的每个生成元都是两者生成元的复合。

定义 19. 效应函数 是独立的,当

  1. 一者的每个变换都与另一者的每个变换可交换,
  2. 任何一者的变换都不扰乱另一者产出的逆变换,

且将 互换后亦然。族 是两两独立的,若对每个 都独立。族可以重复出现同一个效应函数,而令某一效应与其自身独立,即要求 可交换。

对于由对 诱导的效应,由引理 18(1),条款 (1) 即四对 的可交换性,而条款 (2) 无条件成立,因为诱导效应在每个状态只产出一个逆变换。在 之下的可交换性则是另一种性质。 所等同的,是两种次序的复合前向映射彼此相等、两种次序的复合逆变换彼此相等,每个逆变换都在其自身应用所产生的状态处进入复合;而独立性则将一种效应的每个变换与另一种效应的每个变换关联起来,包括前向映射与外来逆变换的配对。

在独立性下,逆变换可以在后续效应已移动过的状态上运行,而它在那里撤回的只是自身的贡献,别无其他:

定理 20. 两两独立,并从 开始按序应用。记 ,令 ,其中 ,并令 在其应用处产出的逆变换。固定 ,记 为序列中省略 后的各状态,从而 。则对每个满足

  1. 每个满足 处产出的逆变换,与它在 处产出的逆变换相同,即

证明.

  1. 第一个等式是对 的归纳。在 处,它读作 ,这正是 的定义。归纳步中,
    中间的等式来自定义 19 对 的条款 (1),二者是族中不同的效应,因为 。对于第二个等式,条款 (1) 将 携带穿过 之后应用的前向映射,使得 的见证只在它成立的唯一状态处被使用:
    最后一个等式依赖于 ,这正是定义 8 要求 处满足的见证。
第 17 页

2. 由 (1) 可知,状态 ,且 ,因此对 应用定义 19 的第 (2) 款,可得

第 (1) 款定位了某个逆变换所到达的状态:即同一序列在效应从未被应用的情况下本会到达的状态,无论在其后应用了哪些效应。第 (2) 款定位了其余效应在那里所持有的逆变换,两者合起来使该定理得以再次应用于更短的序列:

推论 21. 两两独立,并按序从 应用,且 如上所述。按 的任意排列的顺序在 处应用这 个逆变换,均能到达

证明. 作向下归纳。设该排列以 开头。由定理 20 第 (1) 款,在 处应用 可到达 ,即删去 后序列所到达的状态;由定理 20 第 (2) 款,其余效应在那里产生的逆变换正是手头的 。该序列作为子族是两两独立的,因此归纳假设适用于它以及排列的其余部分;空序列到达

后进先出(LIFO)顺序就是这样的一个排列,而定理 16 在该顺序下无需任何假设即可完成逆变换。独立性所带来的是所有其余的顺序,以及随之而来的、交错多个组件的序列,第 4.4.2 节将其推广到整个系统的轨迹。

这些构造共同构成了可逆效应: 中的每个效应函数都显式地提供自身的逆变换,效应(effect)在效应上下文 上跟踪这些逆变换,而 运算在保持可逆性的前提下对它们进行复合。它们所提供的是局部的时间可组合性;之所以说局部,是因为该保证是针对单个组件自身的效应(单独来看)而解读的。我们将此视为如下判据:对于组件所应用的每一个效应函数序列,累加器都能恢复到其起始时的上下文(定理 7),而对序列进行逆变换则会把每个逆变换交到其自身应用所面对的状态上(定理 16)。加载一个组件,就是应用这样一个序列并把它的逆变换累积到 中;卸载它,就是应用

该判据遗漏了两件事,而一旦有多个组件参与,两者都会出现:脱离累加器所施加的顺序进行逆变换,以及交错其他组件效应的序列。独立性提供了这两者(推论 21),而它是关于效应本身的一种条件,而非构造的一种性质——第 3.3.2 节指出满足该条件的纪律(discipline),第 4.4.2 节则就整个系统的轨迹来解读该保证。

当独立性失效时,顺序必须由别处承担:在单个组件内部,由累加器承担——无论效应如何,它都按后进先出(LIFO)顺序逆变换(第 4.3.2 节);跨组件之间,则由一个声明的共效应承担——它把一个激活与另一个激活排序(第 4.3.1 节)。

3.2 响应式共效应

空间可组合性是指组件能够相互声明依赖,且系统能够在运行时解析、提供和撤回这些依赖的能力。这要求每当共享上下文发生变化时都重新评估依赖满足性,从而使组件在其依赖变得可用时激活、在其依赖被撤回时停用。因此,我们把组件的依赖建模为一个规范(specification),并对照该规范,把上下文的每一次变化分类为激活性的、停用性的或中性的。对照规范进行分类,正是检测满足性变化的方式;响应这一分类,则是驱动激活与停用的方式。我们把这类共效应称为响应式的:通过

第 18 页

对上下文变化进行分类并据此驱动激活与停用,正确的共效应排序就成为一种结构性保证。

3.2.1 共效应上下文

传统的控制反转(inversion-of-control,IoC)容器 [38] 通常把依赖建模为简单的键-值映射。本节将 IoC 形式化为一种共效应上下文,它与可逆效应协同,为动态组合提供数学基础。

定义 22. 给定类型族 ,将共效应上下文定义为如下依赖偏函数类型:

其中 是一个有限偏函数,它为每个 赋予一个类型为 的值。我们记:

  • 表示应用(当 时有定义);
  • 表示在 处绑定 、且其余各处与 一致的表;
  • 表示限制(当 时有定义);
  • 表示成员关系。

使用类型族 可确保每个依赖键 都与一个特定的值类型 相关联,从而为依赖访问提供静态类型安全性。扩展与限制都带有前置条件,这些条件由下文中的操作施加:一个依赖不能被提供两次(扩展要求 ),也不能在不存在时被撤销(限制要求 )。违反前置条件会作为错误被报告,且不产生任何转换,因此描述实际发生的转换的效应代数可以不加修改地适用于这些操作。倾向于将失败内化的读者,可以把下文中每个 读作 ,并在 单子中复合(第 2.1 节),代价是把每个恒等变换替换为操作定义域上的偏恒等变换。基于这一上下文结构,我们定义两个核心操作:

定义 23. 上的 操作定义如下:

其中 要求 要求 作为前置条件。值得注意的是, 的类型为 ,恰为共效应上下文上的一个效应函数。因此我们可以直接应用第 3.1 节的效应机制: 提供对依赖注册的自动跟踪与恢复。这正是响应式共效应与可逆效应之间的协同:共效应操作就是效应,而效应是可逆的。

交给组件的只是一个值,而组件能用这个值做什么,取决于该键处的共效应所提供的能力。因此,一个键所承载的不仅仅是值类型:

定义 24. 处的一个共效应是一个三元组 ,其中 是定义 22 的值类型, 上的一个等价关系, 处的值按该等价关系进行比较(第 3.3.2 节), 是一组共效应操作,即绑定在 处的值提供给

第 19 页

持有它的组件的那些操作。一个操作 带有参数类型 与结果类型(outcome type),并且只作用于该值本身:

其前两个组成部分构成 上的一个效应函数——正如定义 8 所要求的;其第三个组成部分则是结果(outcome)。每个操作都必须尊重 :在 相关的值上,它要么在两者处都有定义,要么在两者处都无定义;在有定义之处,它产生 相关的后继、把 相关的值再次映到 相关的值的逆变换,以及相等的结果。一个操作通过其提升(lift)作用于共效应上下文:

该式在 时有定义,其前两个组成部分是 上的一个效应函数。把 的一个操作类型化于 ,正是把它限定在 处的绑定上:提升只读写该绑定,而让所有其他键保持原样,因此无需附加条件即可说明这一点。在隔离生效之处,它到达的绑定正是领域(realm)所解析出的那个绑定(定义 28);共享同一领域的两个键共享同一个绑定。一个行为取决于其他键的操作,会把该键的值读入其参数 ;下一小节的响应式纪律则保证,在读取该值的组件运行的整个期间,该值保持固定(定理 63)。

3.2.2 规范与通知

前面的定义描述了单个依赖如何被注册和访问。然而,访问一个不存在的依赖是一种运行时失败。因此,一个组件只应在它所声明的所有依赖都就绪之后才激活,而不是乐观地访问它们、在某个依赖缺失时失败。这引出了两个问题:组件的已声明依赖是否被共同满足,以及当该状态发生变化时系统应如何响应。共效应上下文 带有一种自然的观察结构,使这两个问题都易于处理:对任意共效应规范 ,定义满足谓词:

该谓词是可判定的(因为 是有限的)。由于对 的所有变更都经由效应函数(其逆变换恢复先前的定义域),满足性的变化在每个效应边界处都是可检测的。这就是响应性的代数基础:效应系统保证每一个共效应变化都被观察到。

定义 25. 共效应规范为:

它表示一个组件向环境声明的依赖集合。使这一规范具有响应性的,是它如何对状态转换进行分类。任何把 变换为 的效应,都可以由规范 根据 的满足状态是否被改变来分类:

定义 26. 给定共效应规范 与状态 ,定义:

第 20 页

这是良定义的,因为 是可判定的,且所有状态转换都由效应函数中介。响应式不变量(reactive invariant)如下:激活转换触发组件效应的执行(带完整的效应跟踪),而停用转换通过应用累加器触发恢复。这些转换的精确操作语义取决于它们与控制流的交互,将在第 4 节中加以展开。

set 与 notify 共同交付的是局部空间可组合性——"局部"与之前的含义相同,即该保证是就单个组件自身的共效应而言的。我们将其表述为如下判据:组件只在满足其规格的状态下激活,因此它绝不会读取一个不存在的绑定;上下文的每一次变化都对照该规格进行分类,因此满足性的丧失会在其发生之处被检测到,并驱动一次停用。这两半都直接由上述定义得出——满足性是组件将要激活之处所检查的一个前置条件,而 在每次转换上都有定义。

该判据覆盖共效应次序的一个方向,而不覆盖另一个方向。若组件 提供键 ,而组件 声明 ,那么由于 要求 只能在 已激活并提供 之后激活。其逆命题不成立:卸载 会从 中移除 ,从而破坏 的满足性;但仅凭一条通知,既无法在 自身拆除所需的期间内保持 可读,也无法让 的恢复一直延迟到 完成。将一次撤回安排在其所导致的停用之后,是对其他组件而非执行动作的组件本身的条件要求,因此它属于该保证的全局形式,第 4.3.1 节提供了实现它所必需的机制。

3.2.3 隔离与拦截

基本共效应上下文 对一张扁平的依赖表建模。然而在实践中,系统可能需要为不同的组件将不同的值绑定到同一个逻辑依赖上。本节以两种机制扩展共效应上下文:共效应隔离(coeffect isolation,即同一个键在不同上下文中解析为不同的值)与共效应拦截(coeffect interception,即依赖访问上的横切行为)。

实现。 这两种机制与 get 和 set 的区别在于它们作用的对象。提供项会写入每个组件都要读取的共享表,因此它是对该表的一个效应,并携带一个用于撤回它的逆。隔离与拦截则调整一个键在某一上下文之下的组件间如何被解析,而使表本身保持原状。将某个操作定型为效应,固定的是它的指称——一个后继状态与一个逆的配对——而不是它的实现;后者决定了该逆如何被执行。

定义 27. 上下文上的一个效应函数具有两种实现:

  • 原地实现(in-place realization)修改上下文,并返回一个非平凡的逆;后继状态与输入互为别名(alias),恢复时运行该逆以撤销修改。
  • 派生实现(derived realization)保持输入原封不动,返回一个由它派生的全新上下文,并以恒等函数为其逆;恢复时丢弃该派生上下文。由另一个上下文派生的上下文,正是定义 32 的递归结构所承载的内容。

在纯函数式设定下,两者是一致的;命令式宿主可以按操作任选其一,第 5.1.2 节实现了这两种。隔离与拦截则直接采用派生实现:

第 21 页

二者各自产生一个全新的上下文,其自身的表与继承来的表不同,因此下文将二者类型化为从上下文到上下文的映射,而非效应函数。共享表中没有任何改变,因此既没有需要跟踪的逆,也没有可供定义 12 提升(lift)的内容,恢复时则连同其携带的调整一并丢弃派生上下文。对派生表的赋值会覆盖继承表在该键上持有的任何内容,这正是两个操作都不携带前置条件的原因。

共效应隔离。 通过引入隔离领域(isolation realm),共效应隔离允许同一个依赖在不同上下文中绑定到不同的值。这在多租户系统、测试环境与组件沙箱中有着广泛的应用。

定义 28. 定义带隔离的共效应上下文为:

它可以表示为一个二元组 ,其中:

  • 是隔离领域表(isolation realm table),为每个被隔离的键分配一个领域标识符;不在 中的键解析到其自身的领域,因此在该处我们记 );
  • 是依赖表,一个从领域标识符到类型化值的偏依赖函数(partial dependent function)。

这种两层映射结构将逻辑层与存储层解耦,使依赖访问具备上下文感知能力。当访问键 时,系统首先解析 以得到领域标识符 ,然后访问 以取得实际的值。

定义 29. 上,get、set 与 isolate 操作如下:

其中 get 与 set 携带定义 23 的前置条件沿 传递后的形式,即 所派生的上下文将领域 赋予 ,并原样继承依赖表,因此一个已被隔离的键会被重新赋值,而不是被拒绝。

共效应隔离机制本质上实现了一个运行时的即席多态(ad-hoc polymorphism)系统。通过隔离领域标识符,同一个依赖键在不同上下文中可以解析为完全不同的值,而且这种多态可以在运行时动态调整。与传统的依赖注入相比,共效应隔离提供了更细粒度的控制,能够为特定组件实现定制化的隔离;set 仍然是一个效应函数(),因而继承了可逆性,而 isolate 则不需要任何逆——它派生一个上下文,而不是写入共享表。

共效应拦截。 第二种机制——共效应拦截——将横切元数据附加到依赖访问上,在不修改依赖值的情况下增加行为。这种元数据既可以由上下文携带,也可以由组件声明,因此我们同时扩展共效应上下文与共效应规格:

第 22 页

定义 30. 定义带拦截的共效应上下文与规范如下:

上下文 是一个二元组 是安装在上下文自身之上的上下文携带元数据(context-carried metadata),默认为空(); 将每个键 映射到一个从元数据 到值 的提供者函数。规范 携带组件声明的元数据,为每个键赋予其元数据 ,其中 充当依赖集合。每个键为其元数据配备一个幺半群 :合并运算 是结合的,以 (空元数据)为单位元。

定义 31. 上的 get、set 与 intercept 操作为:

其中 get 与 set 对提供者表携带定义 23 的前置条件,即 。由 派生的上下文将 合并到在 处继承的元数据上,并原样继承提供者表。

当携带规范 的组件访问键 时,系统求值 :组件声明的元数据与上下文携带的元数据 合并,提供者函数作用于合并结果。这种合并遵循每个键自身的语义(例如标量字段被覆盖、集合值字段取并集),并且是右偏的(right-biased),因此 优先,可以覆盖组件的声明,从而使外围上下文能够在不必修改组件的情况下约束组件如何使用共效应(例如第 6.3 节)。

3.3 上下文范式

第 3.1 节与第 3.2 节都作用于上下文:前者以上下文作为效应的载体,后者以上下文作为共效应的载体,但二者都未曾说明一个同时承载两者的上下文应当是什么样子。本节为这一统一给出具体构造,从共效应中装配出观察等价,以补足第 3.1.3 节留下的效应独立性,并论证所得的上下文类型本身构成一种编程范式。

3.3.1 统一上下文

对于上下文 ,效应上下文 (第 3.1 节)提供了一种更高层的抽象,承载上一层上下文与该层的累加器(定义 2)。使这一结构递归化,并将其与共效应上下文 组合,得到如下类型:

定义 32. 上下文类型 定义为:

其中三个投影分别为:

第 23 页
  • :当前上下文状态(递归的);
  • :累加器,恢复这一层的效应;
  • :携带依赖信息的共效应上下文。

在这一定义下,效应映射 映射到自身,把 塔统一为单一自相似类型。共效应上下文 在结构上被集成:依赖操作(set、get)作用于 ,累加器追踪它们的逆转。由于 底层的类型族 不受约束,系统需要在组件间共享的任何状态都可以编码为带有适当值类型的依赖—— 涵盖所有共享可变状态,而不仅仅是组件间依赖。组件与其环境之间的每一次交互都经过这一单一实体。

分层组合。 的递归结构支持分层控制:父上下文聚合多个子层的效应,形成树形控制结构,在保持模块化的同时支持统一的跨层管理。效应变换实现了字面意义上的"即插即用"(plug-in)隐喻:

  • 加载组件对应于执行其效应(插入);
  • 卸载组件对应于恢复其效应(拔出,且不影响其他运行中的组件);
  • 层级中不同层的组件可独立加载与卸载;父上下文聚合并管理其所有子组件的效应,从而支持任意嵌套的组合。

3.3.2 观察等价

第 3.1 节的恢复保证断言的是状态之间的相等关系(定理 7),这是一种理想化,因为物理状态无法恢复为其原本的样子。例如,free 将一块内存释放给分配器,却不会恢复堆在 malloc 之前的布局;生成式名字(generative name)也不会被丢弃它的逆变换所恢复,因为下一次创建会生成一个全新的名字 [39]。因此,第 3 节中的相等关系都应在等价关系 的意义下理解,而我们取 为观察等价:当没有任何观察者能够区分两个状态时,二者即相关。比较行为而非表示,是程序等价性的既有路径 [40],而这样的比较所得出的关系,取决于观察者被赋予的可用材料 [41]。上下文的观察者被赋予的,是其所携带的共效应,每个共效应都自带一个等价关系(定义 24),因此上下文上的关系由这些等价关系装配而成。装配这一关系正是本小节的任务,而对其取商,正是获得第 3.1.3 节所要求的独立性的途径。

定义 33. 两个共效应上下文相关,当它们将相同的键绑定到相关的值;上下文的两个状态相关,当它们的共效应投影满足:

其中 表示 的共效应投影(定义 32)。

状态中没有任何键绑定的部分由此被遗忘,而正是这种遗忘使定理 7 得以在 的意义下成立:除非某个键绑定了它们,否则上述例子中的堆布局与生成式名字都处于该关系之外。第 3.2.2 节对 的需求由此推出,而非假定。相关的状态具有相同的定义域,因此它们在

第 24 页

满足谓词 以及定义 26 的分类 上一致,因此响应性是 的一个性质。

将这一关系称为观察的,是对每个 的一项断言,即它所区分的不会超过 的操作所能分辨的。一个值的观察者运行这些操作并读取它们的结果。

定义 34. 携带一个操作集合 (含义如定义 24),并记 为效应函数 在所有参数 上的变换幺半群(定义 17)。 上的一个测试(test)是幺半群 )的生成元上的一个有限词,其中每个字母作用于其前面字母所留下的值上;其结果是那些作为操作前向映射(forward map)的字母沿途产生的结果,而在前置条件失败处未定义。当 上的每个测试在两个值处都有定义或都无定义,且产生相同的结果时,值 不可区分,记为

引理 35. 不可区分性是操作所尊重的最粗关系。即:

  1. 的每个操作都按定义 24 的意义尊重
  2. 的每个操作所尊重的每个等价关系都包含于

因此, 的每个可容许选择都包含于 ,而 本身是可容许的。

证明.

  1. ,并设 作用于某个参数。在测试前添加一个字母仍然是测试,因此前向映射所到达的值不可区分,任何单个所产生的逆从不可区分的参数所到达的值也不可区分;单字母测试给出两个值处都有定义或都无定义,且结果相等。
  2. 是这样一个等价关系且 。测试的每个字母都是操作的前向映射或所产生的逆,尊重性沿二者传递 ,使到达的值保持相关且每个字母处的结果相等。因此每个测试在 处一致。

仅仅将全文中的 替换为 是不够的,因为效应函数除返回状态外还返回一个逆变换,而被 视为等同的两个状态,必须产生也被 视为等同的逆变换。

定义 36. 当满足下式时,映射 尊重

两个映射相关,当它们在每个状态处一致; 中的两个二元组相关,当两个分量都相关:

尊重 的映射是能下降到 的映射,而由 关联的两个映射是在商上下降到同一映射的两个映射。效应函数两者都需要:前者使它所计算的状态在商上被确定,后者使它返回的逆变换在商上被确定。

定义 37. 的意义下重读定义 8:当 作为映射 尊重 ,且记 时,对每个

属于

第 25 页

2. 尊重

取为 上的相等,即可恢复定义 8。

引理 38. 按定义 37 理解,第 3.1 节中断言的每个状态等式,在把 替换为 后仍然成立,且从 出发可达的每个状态的累加器都尊重

证明. 累加器是逆变换的复合,其中每个逆变换都按定义 37(2) 尊重 ,而尊重 的映射的复合仍然尊重 ,其基例为 。于是第 3.1 节的证明原样成立——尊重正是把关系穿过逆变换的机制:由 ,尊重给出 ,这正是每次逆变换复合所采取的步骤,而定理 7 的可靠性不变量在该步骤下读作

定义 19 所要求的可交换性,由上述引理在 的意义下解读;正是这种解读才使它得以真正达成:两个操作可以留下被 视为相同的值,却仍可算作可交换。与它们提升所诱导的效应函数相比,定义 19 对两个操作还多要求一点:操作还会产生一个结果。

定义 39. 当操作 的提升作为效应函数(定义 19)在每一对参数处都独立,且其中任一操作的变换都不干扰另一操作所产生的结果时,称 独立:

互换亦然,其中 表示提升 在一切参数上构成的变换幺半群,正如定义 34 以 表示操作本身的变换幺半群。当 中任意两个操作都独立——一个操作也被视为与自身独立——时,称键 可交换。

在不同键之间,该条件无条件成立。

定理 40. 位于不同键上的操作是独立的。

证明.,且 。按定义 24, 的每个生成元都具有 的形式,其中 上的映射,它要么是某个前向映射的提升,要么是某个已产生的逆变换的提升;对 处的 亦然。这样的两个映射可交换——每个映射只读取和写入一个键,而这两个键互不相同——引理 18(1) 再把可交换性从生成元推广到两个幺半群。对于第二个条件, 处产生的内容,无论逆变换还是结果,都只由 决定,而 的每个生成元都保持 不变。

键值为一张可独立增删条目的表时,该键可交换;路由或事件监听器的注册是代表性情形:两种顺序下的两次注册都留下对每个测试给出相同回答的表,且任一注册都可以在另一注册存续期间被撤回。键值为有序链时则不然,因为插入在另一中间件之前的中间件会看到不同的请求,且两种顺序都不能在不干扰对方的情况下被撤回。开篇示例中的分配器按其接口公布的内容而分两种情况:当其发放的句柄不被该键的任何操作所比较时, 可以把两个堆关联到句柄的重命名上——这正是 CompCert 关联一个程序与其翻译的内存状态的方式 [42]——此时分配是可交换的;而当地址是经由相等比较的结果时,任何可接受的 都无法使两种分配顺序一致,该键便不可交换。

第 26 页

组件所执行的是一个操作序列,其中每个操作都可能依赖于其前面的操作所产生的结果;具有这种形状的效应函数正是下面的定理所讨论的对象。

定义 41. 由共效应介导的效应函数构成最小的集合 ,它包含单位元 ,并在如下构造下封闭:对于键 、操作 、参数 以及成员族

仍是成员。每个阶段执行一个操作,并根据其结果选择后续阶段,因此参数可以依赖于已经获得的结果。成员中出现过的操作,是其各阶段在所有结果选择下所执行的那些操作。

定理 42.,且 的操作同时出现的每个键都可交换(定义 39)。则 独立(定义 19)。

证明. 对定义 41 的构造作归纳可知, 位于由 中出现过的操作的生成元所生成的子幺半群之中:单位元生成平凡幺半群,而一个阶段是 与某个成员的 -复合,对此适用引理 18(2)。

因此,对于定义 19 的第 (1) 款,由引理 18(1) 可知,只需 中出现过的某操作的生成元与 中出现过的某操作的生成元可交换即可。当两个操作位于不同的键上时,这正是定理 40;当它们位于同一个键上时,该键同时承载两者的操作,按假设可交换。

对于第 (2) 款,取 ,它是 中出现过的操作的生成元的复合,并对 的构造作归纳。单位元在每个状态处都产生 。在某个阶段,设 ,于是该阶段在 处产生 。把操作的独立性逐个应用于 的每个生成元,可知在 处仍得到 ,于是选择同一个续体 ;第 (1) 款再把该续体运行所自的状态置于 ,归纳假设在那里再次给出 。因此该阶段在 处产生

组件与其环境之间的每一次交互都经由上下文,而类型族 不受约束,因此系统可以把它在组件间共享的每个位置都绑定到自己的某个键上(第 3.3.1 节)。组件的效应函数于是就是某个共效应介导的效应函数沿共效应投影的提升,独立性也随之传递给该提升——其变换只移动投影本身。第 3.1.3 节留下的未决假设由此得到满足,随之而来的便是整个组件系统的时间可组合性。

这种分解所划分的,是计算的可交换部分与其对顺序敏感的部分。可交换部分由效应承载:组件按任务要求的任意顺序执行它们,推论 21 再按系统认为方便的任何顺序将它们逆回,两个组件互不约束。对顺序敏感的部分由共效应承载,因为操作不可交换的键,其顺序必须从效应外部施加,而可供施加顺序的位置有两个。在单个组件内部,累加器施加该顺序,以 LIFO 顺序逆回效应所做的一切(定理 16)。在组件之间,声明的共效应施加该顺序,一个组件提供另一组件所声明的内容,且提供先于声明的满足(第 3.2.2 节)。由此,可组合性在组件的粒度上获得,而非在单个效应的粒度上,这正是第 4 节所工作的尺度。

第 27 页

该定理有两个值得点明的局限。将每个共享位置绑定到键上,是这一范式的纪律而非构造的性质,因此系统无法具体化为共效应的位置,位于第 6.1 节的边界之外,也随之位于定理之外。而键的可交换性是键所公布的接口的性质,因此满足它是提供该键的组件的义务,而非消费它的组件的义务。

3.3.3 上下文范式的定位

编程范式在处理副作用的方式上有着根本性差异。两个既定的端点界定了这一谱系:

显式状态传递(函数式)。 为保持引用透明性,纯函数式语言把副作用建模为对状态的显式变换。State 单子 [23] 将环境穿过每一次计算。这种方法给出很强的组合性保证:效应在类型中可见,且适合等式推理。然而它也带来显著的易用性代价:调用链中的每个函数都必须接受并返回状态参数,即使它只是原样地把状态传递过去。随着效应维度的增多(日志、配置、I/O),单子堆叠或效应处理器样板代码不断增生。

隐式变更(命令式/OOP)。 主流命令式语言允许组件修改共享状态,并在调用点不做显式声明的情况下访问依赖。在效应一侧,代表性例子是 React 的 useEffect 钩子:它在组件的内部纤维上注册一个持久的副作用,但效应目标与注册机制都不作为显式参数出现——识别依赖于隐藏运行时状态中的调用顺序位置。在共效应一侧,Java 的服务定位器模式(例如 Spring 的 ApplicationContext.getBean(...))在运行时从进程级注册表中获取依赖,在每个调用点都要求空值检查与类型转换;依赖关系是隐式的,且散布在整个代码库中。更一般地,理解 f() 如何修改系统或依赖系统,需要传递性地阅读其实现。重构因而变得脆弱,因为移动或删除一次调用可能会悄悄破坏远处的各种不变量。

上下文范式结合了函数式方法的可追溯性与命令式方法的易用性。效应与共效应都通过一个显式上下文参数来介导。因此,每个操作都可归因于它被调用时所处的具体上下文,进而归因于该上下文所属的组件。

除结合两个端点的优势之外,上下文范式还让开发者逐一处理每个效应与依赖,并自动把它们组合进系统的行为之中。对于可逆效应,开发者提供每个原子操作的逆变换,任何复合操作的逆变换都由复合而得出(第 3.1 节),因此组件的拆除由加载推导而来,而非与之并排书写。对于响应式共效应,组件只声明它需要的依赖,运行时自动解析并重新布线(第 3.2 节),在提供者被添加、移除或替换时保持它们始终一致地连接。在这两个方向上,原本依赖开发者纪律的正确性都成为范式的结构性性质。

第 28 页

4 动态组合演算

第 3 节仅以局部形式确立了空间可组合性与时间可组合性。要将它们推广到整个系统,需要把系统分解为若干组件(component),每个组件将一份共效应规范(coeffect specification)与一个带见证的效应函数(witnessed effect function)配对,从而使与共享环境的每一次交互都可归因于其中一个组件。以下各节为这一分解给出操作语义,并以全局形式确立空间可组合性与时间可组合性。第 4.1 节与第 4.2 节呈现能对生命周期赋予规则的最小演算,该演算把每个转换(transition)视为原子的、即时的且不会失败的;第 4.3 节放弃这三项假设——原子性按转换可能运行的每个方向各放弃一次——接纳运行时在转换开始与结束之间插入的各种控制流形式,最终得到真实运行时实现所采用的演算;第 4.4 节确立该演算的元理论,即保持、全局时间与空间可组合性、进展性与合流性。

4.1 组件与纤维

本节确定规则所作用的对象:组件;纤维(fiber)——组件的实例化,携带其自身的生命周期状态(lifecycle state);以及注册表(registry)——存放状态所携带的纤维,并从中读出共效应上下文。

组件。 组件以三元组给出,其共效应一侧被分为它从环境中读取的内容与它向环境提供的内容。

定义 43. 在同时携带效应与共效应的上下文 上的组件(定义 32)定义为:

表示三元组 ,其中:

  • 是定义 25 的共效应规范,声明所需于环境的依赖;
  • 是提供项(provision),声明组件可能提供的共效应键,且 之外的任何键都不是其效应函数所写入的键;
  • 是定义 8 的带见证的效应函数,定义组件激活时所贡献的效应,以及撤回这些效应的逆变换(inverse)。

这两个声明是同一个接口的两个方向: 是组件从环境中读取的内容, 是组件写入环境的内容;第 4.2 节不允许同一注册表中的任意两个纤维的提供项相交。全文统一以下标 取值,共效应上下文是它的一个投影(定义 32),因此定义 25 中的 在此写作

提供项的不相交性正是本章与第 3.2.3 节分道扬镳之处。定义 28 的隔离(isolation)允许一个键通过领域表(realm table)解析,因此两个纤维可以在不同的领域中提供同一个键;携带领域的演算会把不相交性放宽为领域内的不相交性,并按声明该键的纤维所处的领域来解析所声明的键。我们在此不引入领域,而是在一个共享领域中读取每个键,正是这一点使得上述不相交性成为正确的条件,并使每个键的提供者唯一(定义 45)。它限制的是组件可被实例化的频度:提供项非空的组件同一时刻只有一个纤维,因此下文中的多次实例化都是针对不提供任何内容的组件,这正是一个只消费、或只注册其他组件的组件的常见情形。

第 29 页

运行系统中被实例化的组件会随时间被激活和停用,因此它携带一个生命周期状态,而转换正是使它从一个生命周期状态移动到另一个生命周期状态的东西:激活执行 ,在上下文上累积副作用,停用则应用累加器(accumulator)以恢复上下文。其最简单的形式是图 1 的两状态模型,第 4.2 节为它给出规则;第 4.3 节在接纳每种控制流特性时对其加以细化。

L-Unload L-Reload Inactive 未激活 Active(g, ω) 激活
图 1|基础组件生命周期。图中两个状态分别为 Inactive\mathsf{Inactive}(未激活)与 Active(g,ω)\mathsf{Active}(g,\omega)(激活),二者之间由两条转换边相连:上边为 L-Unload(从激活到未激活的卸载转换),下边为 L-Reload(从未激活到激活的重载转换)。

纤维。 一个组件可以被多次实例化,每次实例化携带各自的生命周期状态。我们将这样的实例化称为纤维。纤维记录产生它的组件、它在其下被实例化的纤维、它所提供的共效应,以及它处于生命周期的哪个阶段。

定义 44. 固定一个纤维名集合 。实例化组件 的纤维是一个元组 ,其中:

  • 是定义 43 的共效应规范、提供项与效应函数;
  • 是父纤维(parent),即该纤维在其下被实例化的纤维,或根标记
  • 是纤维自身的共效应表(定义 22),在它激活前为空,并由其效应在运行过程中写入;
  • 是退役标志(retirement flag),新鲜纤维中为 ,一旦编排器(orchestrator)使该纤维退役即为
  • 是生命周期状态,在第 4.2 节的两状态模型中为:

其中 是累加器, 是已提交视图(committed view)。已提交视图 把纤维声明的每个键映射到转换提交时提供该键的纤维的名字。第 4.3 节用进行中的转换所需的扩展取代 ;定义 44 的其余部分对二者一次给出,只是 在第 4.3 节每层引入的更丰富的效应类型下读取。

注册表。 状态按其名字持有其纤维,纤维的身份与第 3.2 节的共效应上下文都从这一安排中读出。

定义 45. 上的纤维集合。状态 携带一个注册表:

这是一个有限偏函数(partial function),其父指针构成一棵以 为根的树,连同 中任何纤维的 都未命名的其余部分。我们用 表示 ,并在状态明确时用下标 简写 的字段,因此 是定义 44 的字段, 所携带的累加器与已提交视图; 分别是与 在某一字段、某一纤维、某一纤维的存在性上不同的状态。

第 30 页

纤维的名字赋予它一种在其自身被修改后依然存续的身份:下文每条规则都只改写一个纤维的生命周期状态而让其他纤维保持不变,因此规则必须指明是哪一个;并且有两个字段是引用纤维而非描述纤维的,即父纤维 与已提交视图 。名字是原子:没有规则计算名字、检查其结构或用相等性以外的任何关系联系两个名字,引入一个纤维只是取出一个尚未使用的名字。这正是动态创建的局部名字的纪律 [39],此处用于纤维身份。

每个纤维拥有一个表意味着共效应上下文是推导出来的而非存储的:它正是活跃纤维共同提供的内容:

该并集是良定义的,因为纤维只写它声明的键,,且不同纤维的提供项互不相交(定义 43),所以每个 都恰好位于一个 纤维的表中,我们把这个纤维的名字记作 ,并称之为 的提供者。因此每个键都恰有一个可能的提供者,由提供项而非状态所决定。

没有规则直接写 :纤维的提供项是其自身效应函数所执行的集合操作,这些操作落入 ,因而已经是 返回的状态的一部分,它们又随累加器一起离开。效应中只有共效应部分以这种方式记录,因为只有共效应部分是其他纤维会据以声明的部分;改变 中其他位置状态的效应由 像其他任何效应一样跟踪,但没有纤维能在规范中指名它们,因此它们不贡献任何排序约束。

第 3.2.2 节的满足关系(satisfaction relation)于是原样适用,用 简写 。一个键位于 中,当且仅当某个 纤维已安装它——提供项是它可能安装的键,而非它已安装的键——因此 已经要求每个声明的键都有 提供者。仅对 纤维取并集,正是让纤维能够在撤回任何东西之前停止提供的原因,第 4.3.1 节将这一点转化为排序纪律。

4.2 基础演算

本节给出图 1 的两状态生命周期的演算,且仅此而已:每个纤维被与之比较的目标,以及移动它的五条规则。

目标视图。 规则将每个纤维与一个目标(target)比较,即它是否应当运行,以及应当按其依赖的哪种解析来运行。目标不是纤维单独的性质,因为纤维声明的键是针对整个状态解析的,所以目标是该状态上的一个谓词。

定义 46. 处的目标视图把每个声明的键映射到其提供者,因此它是一个全映射 ;当 根本不应运行时,它为

当每个纤维都达到其目标视图时,状态是静止的(quiescent):

第 31 页

目标视图只对两件事作出应答,此外再无其他:其一为退役,经由 ;其二为共效应解析,经由 ——每个被声明的键都在定义 43 的那个唯一共享领域中依据 读出。

定义 44 的已提交视图与目标视图具有相同的类型,而生命周期正是通过比较二者来驱动的: 在激活时所依据的解析结果, 则是它应当运行所依据的解析结果;下文每一条规则都在二者相同或相异时触发。记录的是提供者而非值,这一点正是使该比较可用的原因——否则,一个提供了相等值的不同纤维也会被比较为相等。组件读取的值经由视图抵达,因为提供者的表中持有该值;实现将该映射存放于 fiber.committed,并将其哈希存放于 fiber.target(第 5.1.3 节)。

规则。 基础演算将每一条转换都视为原子、即时且不会失败的:一次激活在一步之内应用其效应函数,一次停用在一步之内应用其累加器,且二者都会成功地完成。第 4.3 节将三者全部放弃。

五条规则生成两种关系。编排规则以 O- 为前缀,记作 ,是编排器可以执行的一个动作;其前提说明该动作何时合法,而非何时发生。生命周期规则以 L- 为前缀,记作 ,是系统在前提成立时无须提示便自行迈出的一步。步的序列将二者交错,下文中的 仅指生命周期步。

O-Insert

O-Retire

O-Remove

插入与退役是仅有的外部输入:编排器请求某个纤维存在或不再存在,而从不直接设置其生命周期状态。O-Retire 对纤维的状态是无条件的,因为退役是一个请求,而执行它的是生命周期规则。退役与移除相分离也是出于同一原因:一个已退役但仍为 的纤维必须首先被停用,若更早地移除它,就会丢弃累加器并造成泄漏。前提 通过先于父纤维移除子纤维来保持树的良构性。O-Insert 的最后一条前提正是施加单源纪律(single-source discipline)之处:一个键只有一个可能的提供者,因为编排器不得接纳第二个声明该键的组件。

L-Reload

L-Unload

L-Reload 将已提交视图与逆变换一并安装;L-Unload 应用逆变换并丢弃已提交视图。二者都由同一种比较驱动:L-Reload 在某个纤维未持有已提交视图且其目标视图不为 时触发,L-Unload 在其持有的已提交视图不是其目标视图时触发。这正是第 3.2 节的响应式纪律,从一个既应答退役、也应答共效应的目标视图中读出:每当目标视图发生变化——无论改变它的是二者中的哪一个——就启动一次转换。

实例化。 组件在安装其效应时可以实例化另一个组件,这正是插件宿主在插件加载其自身插件时所做的事。迄今为止的规则把注册表完全留给编排规

第 32 页

则,因此这样的实例化无处发生。一个原语为它提供了发生之处。

定义 47. 的一次应用——或在第 4.3.2 节适用时,其迭代之一的一次应用——可以注册一个组件 。它不取状态映射,而是采用该组件以 的 O-Insert,并以被如此注册的纤维的 O-Retire 作为其逆变换。该规则在 O-Insert 的新鲜性前提的约束下抽取名字,并将其交给效应函数。

逆变换选择退役而非移除,原因在于逆变换必须在到达它的任何地方都能应用。O-Remove 带有前提,因此由它构造的逆变换可能无法应用:一个子纤维仍为 的父纤维无法运行其累加器,而且没有规则会移动该子纤维,因为定义 46 并不读取纤维树。O-Retire 的唯一前提是 。它在注册被采纳时所处的状态处留下的条目是已退役的 ,并持有一张空表,这正是引理 57 的残留条目:它与纤维的不存在之间的差别仅在于控制字段,且没有任何规则能区分二者。

退役一个子纤维会设置 ,从而将其目标视图置为 ,此后常规规则会把它带回 。由于 O-Retire 是无条件的,父纤维无须等待,因此无论子纤维是否已经离开,L-Unload 都适用于父纤维。孙纤维被一层一层地触达:子纤维自身的累加器退役掉子纤维所注册的内容。定理 66 一并涵盖这一级联与第 4.3.1 节沿共效应方向施加的级联。

限定(Confinement)。 有了这唯一的例外在手,就可以给出效应函数所应遵守的纪律。它约束一次应用所能写入的内容,从而使应用它的规则能够说明其余的一切变化;它也约束一次应用所能读取的内容,从而使纤维只能看到它所声明的共效应以及注册表中不多于此的部分。约束写入正是让第 4.4 节得以把表 1 当作这些写入的完整清单来解读的原因。

定义 48. 若对每个满足 ,记 ,以下条件成立,则称映射 被限定于

  1. (写入。);对每个满足 ,有 ;且 仅在 上不同;
  2. (读取。)凡在 上、在每个 的限制 上、以及在未被任何纤维的表命名的状态部分上一致的两个状态,经 携带后仍得到在这同样的三方面一致的状态。

的每一次应用——以及它的每个在第 4.3.2 节适用的迭代的每一次应用——要么注册一个组件(定义 47),要么使其状态映射 与其产出的逆变换都被限定于 时,称效应函数 被限定于 。每个纤维的效应函数都被要求限定于该纤维。

一次注册只写入 O-Insert 在其抽取的唯一个名字处写入的条目,此外不写任何东西;它作为逆变换产出的 O-Retire 只写入该名字的 ,此外不写任何东西。因此,任何一种类型的应用都不会写入已存在纤维的任何控制字段——除那一个 之外——也完全不会读取任何控制字段。

第 (2) 款解释了组件为何能够读取它所声明的值:这些值位于其提供者的表中,因此一个除了 之外不读任何表的效应函数将无法使用它自己的共效应。它不得读取的是 之外的任何表,或任何控制字段——正是这一点使组件不能依据某个它未声明的纤维的生命周期状态进行分支。

这些规则是非确定性的:多个纤维可能持有与其目标视图不同的已提交视图,而该关系不对它们之间的顺序作任何承诺。它们也是响应式的

第 33 页

仅在于,没有任何规则提及调度器;这些步骤是规则应用的任意序列,因此,一个对所有这样的序列都证明成立的定理,对运行时可能采用的每一种调度策略都成立。

4.3 进行中的转换

本节在四种情形下扩展基础演算。第一种情形提供了第 3.2 节所需要、而第 4.2 节无法表达的东西:一个散布在某个区间上的停用,该区间可供其依赖者占据;其余三种情形则放弃了"转换是原子的、即时的、不会失败的"这一理想化假设——真实运行时中的转换三者皆不具备。被放弃的是"整个转换是一步"这一观念,而不是"一步是某条规则的一次应用";这四种情形共享同一个结构上的推论,此处一并说明:一个不是一步的转换,在其进行期间需要一个状态可供其占据,并且其可能运行的每一个方向各需要一个状态。

定义 49. 本节的生命周期状态将 替换为

其中 是剩余的效应迭代器(下文定义 51), 是迄今构建的累加器, 是已提交视图, 是结果:它由 承载时表示其停用所指向的结果,由 承载时表示其已到达的结果,即 或从第 4.3.4 节所提供的错误集 中取出的一个错误。

当纤维处于携带累加器与已提交视图的三个状态之一时,称该纤维已安装(installed);当它携带一个错误结果时,称其已失败(failed):

时,已安装的纤维 解析为 。定义 46 的静止(quiescence)在更宽的状态空间上解读为

第 4.1 节的定义原样承接到这个状态空间上,但有两点解读需要厘清。第一,第 4.2 节中的 在 O-Insert 的结论中解读为 ,在 O-Remove 的前提中解读为 。第二, 仍然只对 纤维的表取并集,因此,转换正朝任一方向进行的纤维只能通过其持有的 读取共效应,而自身不提供任何共效应;其转换已经写入的键,因此还不是依赖者可以据以激活的键。在两状态演算中这一区分是空洞的,因为那里的每一根已安装纤维都是

图 2 描绘了这些状态构成的生命周期,下面的四个小节给出其各条边上的规则。

L-Begin L-Iter L-Finish L-Divert L-Raise(携带错误) L-Leave L-Unload Inactive 未激活 Reloading(i, g, ω) 重载中 · 转换状态 Active(g, ω) 激活 Unloading(g, ω, ζ) 卸载中 · 转换状态
图 2|含进行中转换的生命周期(两个转换状态以轮廓线框出)。图中四个状态分别为 Inactive\mathsf{Inactive}(未激活)、Reloading(i,g,ω)\mathsf{Reloading}(i,g,\omega)(重载中)、Active(g,ω)\mathsf{Active}(g,\omega)(激活)与 Unloading(g,ω,ζ)\mathsf{Unloading}(g,\omega,\zeta)(卸载中),其中 Reloading\mathsf{Reloading}Unloading\mathsf{Unloading} 两个转换状态以轮廓线框出。转换边为:L-Begin(Inactive → Reloading)、L-Iter(Reloading 自环)、L-Finish(Reloading → Active)、L-Divert(Reloading → Unloading)、L-Raise(Reloading → Unloading,携带错误)、L-Leave(Active → Unloading)、L-Unload(Unloading → Inactive)。
第 34 页

4.3.1 撤回

第 3.2 节要求依赖者在它们的依赖之后激活,并要求依赖只有在它们的依赖者已经停用之后才能撤回自己的提供项。前半部分在基础演算中已经成立:一次激活要求 ,因此声明键 的纤维不可能在某个纤维正在积极提供 之前激活。后半部分才是实质性的,而且它所必须交付的远不止状态变更的一个次序。一个因其提供者即将消失而被拆除的组件,正在运行它自己的拆除代码,而这段代码可能需要那个正是正在被撤回的共效应;关闭一个连接池通常意味着把连接交还给提供它们的任何一方。后半部分必须交付的是:消费者在整个自身停用过程中仍然可以读取 ,并且提供者对 的撤回只在此之后才生效。基础演算根本无法交付这一点:它的 L-Unload 把移除提供项与运行逆变换合并在一步之内,在二者之间没有留下任何可供消费者的拆除过程占据的区间。

这一层把那一步拆分为两步,并用以下条件为后半部分把关。

定义 50. 当某个其他已安装纤维将一个键解析到纤维 时,称纤维 处被依赖:

L-Leave 记录停用的决定而不立即付诸行动,这使纤维停止提供其共效应,同时保持它自己的已提交视图以及所有其他纤维的已提交视图完好无损。L-Unload 应用累加器,丢弃已提交视图,并使纤维带着其所承载的结果进入 ;在第 4.3.4 节提供另一种情形之前,该结果恒为 。它是整个演算中唯一应用累加器的规则。

这一次序的两个半部分于是由该规则形式的不同部分承载:可见性这一半由已提交视图承载——L-Unload 将其作为最后一个动作丢弃;次序这一半由前提 承载——我们称之为守卫(guard),它将 的撤回扣住,直到每一个把 解析到 的消费者都已离开为止。定理 63 确立了这两点。

第 35 页

守卫是按绑定(binding)而非按纤维施加的: 检验的是某个已提交视图是否指名了 ,因此,一个未声明 的任何键的纤维不会构成障碍,一个在另一领域(第 3.2.3 节)中解析了 的某个键的纤维同样不会。在第 4.2 节的单一来源纪律下,按绑定的解读与更粗略的检验 相吻合——在那里,一个键至多只有一个可能的提供者。

这类守卫通常会死锁。使其不致死锁的,是 状态与 仅为 纤维之并这两者共同作用:一旦 L-Leave 已标记 的表便离开 ,于是任何目标视图都不能再指名 ,而每个已向 提交的消费者自身也已处于退出途中。定理 66 将这一点转化为守卫总会解除的断言。

该守卫沿共效应而非沿纤维树对停用进行排序:父纤维可以在其某个子纤维仍处于 状态时运行其逆变换,因为 只涉及已提交视图。因此,父纤维与子纤维之间的排序弱于定理 63 对提供者与其消费者所施加的排序;而效应在环境状态中相遇的父纤维与子纤维,则由定义 60 的独立性假设(independence hypothesis)支配。

4.3.2 迭代

一次激活可能依次执行多个效应,而停用必须恢复它们。我们用效应迭代器(effect iterator)来建模这样的激活,其每一次迭代都产出修改后的上下文、一个逆变换与一个续延(continuation):

定义 51. 将效应迭代器 与带见证的效应迭代器 定义为如下递归类型:

其中 产出三元组 ,分别表示:

  • 是新的上下文;
  • 是当前效应的逆函数;
  • 指示续延:
    • 表示迭代终止;
    • 提供下一次迭代。

该见证在定义 33 的 处解读,正如定义 37 解读 的见证那样:当 尊重 、且它产出的每个 都尊重 并满足上述条款时, 便属于 。三元组按分量比较—— 只与 比较, 时比较——而迭代器上的 是满足这些条款的最大关系。将 取为 上的相等,即可精确恢复该解读。

效应迭代器变换 通过递归调用将 扩展到迭代器结构上:

定义 52. 将效应迭代器变换 定义为:

第 36 页

在每次迭代中,逆变换 按应用顺序复合到 上,因此累加器 在被应用时自然地按后进先出(LIFO)顺序恢复效应。由于 一样落在同一个 中,迭代器本身就是一个效应,可以在任何效应可用的地方使用。组件的整个激活正是这样的一种使用,本节其余部分将对此加以形式化;实现还在每个变更点(mutation site)处接纳迭代器(第 5.1.1 节)。 续延使得任意两次连续迭代之间存在一个边界:在该边界处,上下文就是迄今各次迭代所造就的上下文,而累加器恰好恢复这些效应、不多不少。在这个意义上,效应迭代器是一种具体化的定界续延(delimited continuation)——即主流语言通过 yield 运算符暴露出来的结构 [43]——因此该模型可以直接映射到它们已经提供的生成器(generator)上。

在演算中,定义 44 的 自此之后在 处解读;将原子效应函数替换为迭代器,会把基础规则 L-Reload 分裂为一个轨迹所经过的"已开始"状态,并赋予纤维离开该状态的第二条出路。

L-Begin

L-Divert

L-Iter

L-Finish

每次迭代都将新产出的逆变换按 复合到累加器上(遵循定义 52),从而使累加器按后进先出顺序应用各逆变换。在任意两次连续迭代之间,如果目标视图已经改变,系统可以将该转换改道(divert),应用迄今累积的逆变换以恢复上下文。L-Divert 与其他所有停用一样经由 改道,而不是就地应用累加器;它在彼处遇到的守卫是空洞的——一个从未 过的纤维不提供任何东西,也不会出现在任何已提交视图中。它的两个分支中的第一个会中止纤维正在持有的那次迭代,而这只有迭代边界才能使之成为可能,因此一次改道所能落下的粒度就是迭代器的粒度;第二个分支则让该次迭代落地,第 4.3.3 节正是需要它的地方。

普通效应函数()是退化情形,其第一次迭代即产出 。这样的转换仍然会经过 状态,L-Divert 也仍然适用,但累加器是 ,且没有任何迭代运行过,因此不会恢复任何东西,该转换要么安装它的全部效应、要么一个也不安装。

第 37 页

4.3.3 异步

到目前为止的各层允许环境在一次迭代与下一次迭代之间移动,并假定每次迭代本身是瞬时完成的,其启动与落地合为一步。我们抽象地刻画非即时性:一次迭代产出一个类型为 的值,其中 是一个不透明的类型构造子,其定义性质在于:在提交与解析之间,外部状态可能发生变化。

在该模型下,一次迭代在一个状态上启动、在另一个状态上落地,而纤维在飞行期间处于 。该层所增添的是惯性:迭代一旦启动便必定落地,且其落地不可被拒绝。因此,一个在飞行期间转向的目标视图无法通过中止迭代来回应,只有 L-Divert 中令迭代落地的那一个分支仍然可用:迭代落地,其后纤维停用。因此,该层既不添加规则,也不添加规则所匹配的类型;在 的粒度上,惯性就是它的全部内容,其形式是对宿主可选取 L-Divert 的哪个分支的限制。

那个分支正是基础演算所无法表达的。在基础演算中,目标视图已经转向的转换会在发现它的同一步中被撤销;而在这里,飞行中的迭代必须首先落地,因此当逆变换运行时,纤维需要一个容身之处,唯一可靠的位置便是持有迭代所产生的逆变换的 。若改道经由 ,纤维便会在一步的时长内提供其共效应,并迫使它的依赖者针对一个已在离开的组件进行激活。这就是实现中重载与卸载相互链接的体现。

停用也可以直接链接回一次激活,这是通过复合(composite)而非规则实现的。L-Unload 对目标视图不携带任何前提,因此无论目标视图在纤维停用期间变成了什么,累加器都会运行,纤维变为 ,而 L-Begin 可以立即从该状态开始一次新的转换。

4.3.4 失败

到目前为止的每条规则都假定它所运行的效应会成功,而运行时做不到这一点。组件安装的效应会触及跟踪它们的上下文之外的事物,而所触及的事物可能拒绝:一个已被绑定的端口、一个不存在的文件、一个不应答的对端。失败的转换仍必须使纤维的效应得到恢复,而不是任其滞留。

为一个错误集合,并细化定义 51 的效应迭代器,使得迭代可以引发(raise)错误以取代产出三元组:

见证仅约束 情形,在模式不匹配处为空(vacuous)——引发没有任何需要撤销的东西——并且 所携带的 从此刻起按 解读。定义 52 的提升原样沿用,只是以引发的错误取代三元组进行传播,因此一个会引发错误的迭代器与普通迭代器一样,在任何可使用效应的地方都可用。该层添加一条规则,并使用了定义 49 的第二种结果,O-Remove 无需加宽(widening)即可接纳它。L-Iter、L-Finish 与 L-Divert 的前提在解读时,须在其所匹配的三元组外层包上 。引发是迭代所做出的行为,因此该规则是从 的退出。

第 38 页

L-Raise 先恢复、后记录。纤维以错误作为其结果转入 ,累积到失败迭代为止的累加器在那里被应用,纤维到达 且未安装任何东西,其所在状态与一次令其中止的 L-Divert 所产生的状态相比,仅差别在纤维所携带的结果上。像对待所有其他停用一样地对失败进行路由,使得每种结果都只能经由 L-Unload 到达——这正是定理 59 所依赖的唯一事实。L-Begin 以 为前提,因此生命周期不会从错误结果重新进入;这正是该结果的实质:它扣留一个其效应函数已在其所运行的状态上表现出不可靠(unsound)的纤维,而不是在未改变的环境中重试它。失败的纤维也不会阻碍任何事情:它处于 ,不携带已提交视图,也无法使 relied(被依赖)成立。

失败被记录在纤维上,而非传播给它的父纤维,因此转换失败的组件会使它的兄弟纤维继续运行——这正是插件宿主想要的行为,也是该结果按纤维(per-fiber)而非作为整个状态的性质来归属的原因。

4.4 元理论

第 4.3 节提供了十条规则:第 4.2 节的三个编排规则;用于激活的 L-Begin、L-Iter 与 L-Finish;用于激活可能提前结束的两种方式的 L-Divert 与 L-Raise;以及用于停用的 L-Leave 与 L-Unload。本节从这些规则的全局形式中读出可组合性的两个维度——一个纤维的保证无论其他纤维在期间做什么都成立——并补充只有整个系统才能被要求的东西:它总是达到其目标所要求的配置,且该配置正是静态组装会产生的那个。下面的每个性质都是关于步序列的性质,因此我们对步进行编号,并依据该编号来读取状态的各字段。

有两个约定从第 3.3.2 节带入本节。下文所有状态之间的等式都按定义 33 的观察等价 来解读,正如引理 38 解读第 3.1 节的(那些等式)一样;而效应函数被要求满足的见证条件正是定义 37 所给出的那个,对于迭代器按定义 51 给出的方式解读,对于登记型迭代(registering iteration)则按下面的 解读。

定义 53. 对步编号,使得 是前 步所到达的状态,并把在 处所采取的步记为

其中 是它所应用的规则——十条规则之一, 是该规则被应用处的名字。该序列始于满足 ,因此每个纤维都通过一次 O-Insert 而存在,无论该 O-Insert 是编排器的还是某次迭代所采取的(定义 47)。 的每个字段以上标携带该编号,因此 分别是 处的生命周期状态、已提交视图、表、累加器与剩余迭代器,而 本身的注册表与共效应上下文,即定义 45 的 在该处的取值。谓词以状态为参数、以其余一切为下标,因此 分别是定义 46、定义 49 与定义 50 的谓词在 处的取值。 的一个时段(episode)是使得 始终成立的下标最大区间 。它在 处开启,其中 ——空的 使开始时没有任何纤维处于已安装状态;它在 处关闭,此时 ,而最后一个时段不必关闭。

第 4.3 节的每条规则都以 的形状作结,其中前提从 计算出 ,在它们不计算任何东西处令 即为 ,而方括号编辑具名字段——

第 39 页

注册表。两半分别命名,且二者都是定义在整个 上的映射。在 处由一条作用于 的规则所采取的一步,其状态映射为

其中 所携带的迭代器与累加器,而编辑(edit) 是把该括号读作一个函数所得的结果,它将前提在 处计算出的值赋给括号所指名的字段。因此二者都由 连同 共同确定,并在每一个状态上都有定义——正是这一点使定理 61 与引理 71 得以在远离 处对它们求值。每一步都分解为

例如,在 L-Unload 处,;在 O-Remove 处,它则是删除操作 ——这正是分解式的后半部分被称为"编辑"而非"赋值"的原因。字段也沿着同一条接缝划分:表 ——一旦创建 的 O-Insert 将其置空,就没有任何 再写它——以及控制字段 连同 ——除经由定义 47 的原语外,没有任何 写它们。当两个状态除控制字段外在一切上一致时,记

关系 并非定义 33 中的 ,且二者互不细化(refine)对方,因为各自都会遗忘对方必须保留的内容。恢复的精确性(recovery exactness)是关于效应的论断,因此 精确地比较表与环境状态,而只遗忘注册表中关于"哪个纤维安装了它们"的记录。规则通过读取控制字段来决定自身是否适用,因此 必须保留它们;本节将 读作定义 33 与下列一致性的合取:注册表的定义域一致,且每条纤维的每个控制字段一致:

函数类型的字段(如 以及 内部的 )按定义 36 比较映射的方式比较;迭代器按定义 51 比较两个迭代器的方式比较;任何其他类型的字段则按相等比较。下面的结果在两种关系下都成立——每种关系对应状态的一半——引理 55 一次性为全部十条规则确立了 这一半。

表 1 将第 4.3 节的十条规则解读为这样的写操作。累加器、已提交视图与剩余迭代器都是 的组成成分,因此第三列也记录了针对它们的写操作;其中 指代第四列的迭代所产生的逆变换,而在 L-Divert 中止该迭代之处则为 。凡由迭代器构造的 注册一个纤维(定义 47)之处,该注册都会在其所抽取的名字处携带 O-Insert 行的写操作;累加器退役某个纤维的 L-Unload 则携带 O-Retire 行的写操作。下文中的每一个情形分析都是对表的一次查表,其中有五个查表出现得足够频繁,值得命名。

第 40 页
规则 被编辑的控制字段
O-Insert undefined
O-Retire 不受约束 不变
O-Remove undefined
L-Begin
L-Iter
L-Finish
L-Divert
L-Raise
L-Leave
L-Unload

表 1 | 各规则视为对其作用纤维 的写操作,其中 是作用于 的该规则。

引理 54. 将表 1 与定义 48 结合起来看,对每一步 以及 处出现的所有纤维

  1. 仅在 作用于 时成立,且该写操作位于 内部;
  2. 仅在 时产生,仅在 时消失,因此在 的一个时段内 关于 恒定;
  3. 仅在 时成立,且没有任何其他步骤把 作用于状态;
  4. ,且
  5. 的条目一同产生,此后永不再被写; 是单调的,只在 处被写,且只由 O-Retire 写。

证明. 设步骤 处应用规则 。由定义 53,它分解为 写表 1 第五列所指名的字段,且不写其他任何字段; 则是 的某个迭代的一次应用,或累加器 (后者是那些迭代所产生的逆变换的复合)。由定义 48,三者中的每一个都局限于 ,因此 之外不写 处出现的任何纤维的字段——此外还可能写注册所添加的条目,以及该注册的逆变换所写的 。因此,两半对写操作构成一个划分,而每一条款就是这一划分在某个字段上的解读。对第二、三列有一种解读被使用了两次: 是唯一不携带已提交视图的生命周期状态,L-Begin 是唯一一条离开它的规则,L-Unload 是唯一一条进入它的规则,而其余每一行都将其前提中的 原样带入结论。

(1) 不写任何表——第五列没有指名任何表; 也不为出现的 写任何 。因此 只可能在 处、且只在 内部发生变动。

(2) 的一个组成成分,而 只有 会写、且只在步骤所作用的纤维处写,因此由上述解读, 的一次 L-Begin 处产生,在 的一次 L-Unload 处消失。 的一个时段是 成立的一个区间,从而也是 在整个区间上都有定义的区间,因此两条规则都不会落在其内部。

(3) 就第四列而言,累加器只在 L-Unload 一处出现:其余规则都取正向映射 ,而任何 都不会把映射应用于状态。

(4) ;由上述解读,L-Begin 与 L-Unload 是仅有的两条其前提与结论在 是否为 上有所不同的规则。作用于某个 的步骤不写 ,而注册所添加的条目位于一个在 处并不存在的名字上。

第 41 页

(5) 第五列没有任何一行指名 ;它们随 O-Insert 所添加的条目一同产生——该条目由 O-Insert 的结论写入,注册所采取的 O-Insert 亦如此。只有 O-Retire 写 ,且写在 处,无论该 O-Retire 是由编排器所采取,还是作为某次注册的逆变换(定义 47)所采取;O-Insert 在一个尚未出现的名字上置 ,因此没有任何步骤会把某个 送回

还有三个查表说明规则看不见什么。其一是:规则只通过上述观察来读状态,因此整个演算可以下降到商

引理 55( 不变性)。 按上述解读设 。则第 4.3 节的一条规则在 处作用于 时适用,当且仅当它在 处作用于 时适用;两次应用所到达的状态仍由 相关联。

证明. 第 4.3 节的每条前提都属于四种类型之一,且每一种所读的都是该关系所保留的组成成分。将 与模式匹配的前提,以及 O-Remove 的前提 ,读的是控制字段。O-Insert 的前提 读的是 。提及 的前提读的是 内部的已提交视图以及 ——后者由定义 45 从 计算得出;而定义 33 只在两个共效应上下文的定义域一致时才将它们关联。其余前提读的是 。没有任何前提以超出 意义的方式读某个值 ,因此没有任何前提能把两个 -相关的状态区分开。

对于结论,由定义 53 有 所赋的值是它所匹配的前提的组成成分;由上一段以及定义 51(该定义在 -相关的状态下关联迭代器所产生的三元组)可知,这些值在两个状态下是相关的。而 尊重 :它要么是 ,要么是 的一次迭代(定义 51 要求它尊重 ),要么是 内部的累加器——由同一定义可知,它是若干各自尊重 的逆变换的复合。

状态所携带的名字由上述观察中的两个所读取: 与控制字段的下标索引;而抽取名字的规则会抽取任何尚未使用的名字(定义 47)。因此,在 意义下阅读下面的结果,同时也要求在重命名(renaming)意义下阅读它们——这正是第 4.1 节的纪律的具体兑现。

引理 56(等变性)。 是一个双射,并设 是携带注册表 的状态,其中出现在某个 中的每个名字都被替换为其像。则 是一个状态,凡 良构之处它都良构;且 带到 ,当且仅当 带到

证明. 前提只通过将某个名字与另一个名字比较来读取名字——无论是直接比较(如 O-Insert 的新鲜性 与 O-Remove 的 ),还是通过一张名字表(如 读取 )。双射保持每一种这样的比较。规则所写的唯一名字是 O-Insert 所置的 与 L-Begin 所置的 ——二者都取自其前提所读的内容——因此这些写操作与 可交换;效应函数根本不写任何名字,它只通过定义 47 的原语抽取一个名字,而定义 48 将该原语局限于它所添加的条目。良构性(定义 58)是四个把名字与名字相比较的条件。

因此,一个序列与其重命名按相同的顺序采取相同的规则,并到达仅相差 的状态。两个除了各自注册所抽取的名字外一致的序列因此被等同看待,下面的结果也是在使它们等同的重命名意义下阅读的。

第 42 页

第二个观察(lookup)是:一个被剥离至仅剩名字的条目,对规则而言是不可见的——正是这一点使定义 47 能够退役一个纤维,哪怕它恢复出的状态中已不再含有该纤维;也使引理 72 能够删除一个已删除时段所作的注册。

引理 57.(残留条目(vestigial entry)。)当 ,且不存在满足 时,称 处是残留的(vestigial);一个残留条目满足 。若 处是残留的,则对每条规则和每个

  1. 一条在 处作用于 时适用的规则,在 处作用于 时同样适用,且两次应用所到达的状态仅在 处的条目上不同,而该条目仍保持残留;
  2. 反之,一条在 处作用于 时适用的规则,在 处同样适用,除非它是抽取名字 或主张 的某个键的 O-Insert。

证明. 一个残留的 不向作用于 的规则之某前提所读取的任何观察作出贡献。它不处于 ,因此 不进入任何 也不是任何键的提供者,从而 都不受影响; 不成立,所以 不为 贡献任何析取项;没有任何 指名 ,所以 的 O-Remove 的前提 不受影响;而 只被作用于 本身的规则读取。第 (2) 款所排除的两条前提,正是删除()所放宽的那两条:缺席的名字是新鲜的,缺席的提供项与其他所有提供项都不相交。由引理 54,没有作用于 的规则写 的字段,因此该条目得以存续;又由定义 48,该步的状态映射被限定于 ,所以它使 保持为空。

简化生命周期状态以及与之匹配的规则,会得到一个子演算,而并非每条结果都能在简化之后存续。值得关注的情形是删去第 4.3.1 节——这正是第 4.3 节开头所作的划分,从元理论一侧读来即是:它的守卫正是确立定义 58 第 (3)、(4) 款的东西,而定理 63 依赖该守卫所创造的区间,因此没有守卫,这三者都会失效。另外三个小节所增添的内容则可以简化掉而不影响下文的结果,因为它们各自都只是向定义 49 所固定的那一个状态空间添加规则。

4.4.1 保持

定义 45 固定了注册表的形状,规则必须先对照它接受检验,下文的结果才能在其上展开。本小节指出规则所保持的不变量:其中第一款就是那个形状,其余各款则是那些结果所假定的内容。

定义 58. 当对所有的 与所有 ,下列条件成立时,称注册表 是良构的(well formed):

  1. 上全定义,且取值于

第 (1) 款正是定义 45 的树逐边读出所得:它使父指针落在注册表之内。该定义同样要求的无环性则无须设款,因为一个指针所指名的纤维,先于指名它的纤维被注册。

定理 59.(保持(Preservation)。)若 是良构的,则无论第 步应用哪条规则, 都是良构的。每一款都在 处由 处的全部四款推出。

证明. 设第 步作用于

(1)由表 1,只有 O-Insert 与 O-Remove 写某个 。O-Insert 以 为前提,这正是第 (1) 款对它添加的纤维的要求;它使所有其他 保持不变,

第 43 页

同时扩大 。O-Remove 有前提 ,因此存留下来的 不会指名它取走的纤维。

(2)O-Insert 的最后一条前提是 ,这正是第 (2) 款对它添加的纤维的要求;而由表 1,没有其他规则写某个 或扩大 。下文要用到两点推论:由定义 43 得 ,所以不同的表互不相交, 是一个函数;又 迫使 ,所以 至多有一个可能的提供者。

(3)由引理 54(2),唯一写某个 的规则是 L-Begin,其前提 使它在 上全定义且取值于 ——目标指名提供者。由表 1,唯一缩小 的规则是 O-Remove,其前提 给出 ,于是由 处的第 (4) 款,不存在这样的 :对某个 成立;而 自身不携带任何

(4)由引理 54(2) 与 (4),该款在 处只可能在如下情形失效:某个已安装者跌落、某个 被写入、或某个被某 指名的纤维离开了 。最后一种是 O-Remove,其所移除的纤维未安装,因而由 处的第 (4) 款,它不被任何已安装的 指名。第一种是 的 L-Unload,其前提 读出 ;它不为 写任何 ,并留下 ,因此该款对 也成立。第二种是 的 L-Begin,写 ,其值是 各键的提供者,因而在 处均为 ;该步不改变任何其他纤维的 ,所以它们在 处也仍然已安装。

L-Unload 的守卫正是承载第 (3)、(4) 两款的东西。O-Remove 的前提 只谈及父指针;使已提交视图不指名被移除纤维的,正是那个守卫——它在若干步之前、出于另一原因而被施加。由于失败同样经由 路由,这一论证无须针对错误结果重复。由此得出基础演算所不具备的两点:O-Remove 释放的名字可被 O-Insert 重新签发,因为没有陈旧的已提交视图会指名它;并且一个纤维一旦 即可被移除,无须另行检查是否有任何人依赖它。

4.4.2 时间可组合性

局部时间可组合性用一个累加器恢复一条效应序列(第 3.1.3 节)。注册表为每个纤维各持有一个累加器,而纤维彼此交错:在 将某个逆变换复合到 上的时刻与 运行的时刻之间,其他纤维已经移动了状态。 是否仍然撤销它当初被构造来撤销的东西,正是该保证的全局形式所断言的;而它所依赖的条件是:介于其间的各步与 可交换。

定义 60.,记 为包含 且对续延封闭的最小迭代器集合;并在一个迭代器处读出定义 17 的变换幺半群 ,取 中每个迭代器的前向映射与产出的逆变换作为其生成元:

在适用第 4.3.4 节之处,读出三元组周围的 ;并记 为:在由续延排序的链 上, 的上确界。当两个迭代器 按定义 19 的意义相互独立时——按这些变换幺半群读出,并把一次迭代的产出视为其逆变换连同其续延——称它们独立:

第 44 页

并对 对称地成立;其中 在映射上按定义 36 解读,在续延上按定义 51 解读,而在登记型迭代(定义 47)上则解读为它们所命名的组件的一致。一族迭代器 是两两独立的,当且仅当对每个 都独立;一个步骤序列是两两独立的,当 是两两独立的,其中 是该序列所曾持有的名字的集合——编排器插入的每个纤维对应一个名字,迭代注册的每个纤维也对应一个名字。

这个意义上的独立性正是轨迹理论(trace theory)所取为原始概念的东西:可交换的动作在序列上生成一个等价关系,在该等价关系下,重排两个相邻的独立动作会保持终点(endpoint)不变 [44];而引理 71 正是这些规则之下的这种重排。之所以用族(family)而不是集合,是为了让同一组件的两个名字保持在作用域内:此时条件要求该组件的效应函数与自身独立,这等价于要求 可交换。第一个条件是定理 61 所用到的,第二个条件是定理 73 额外需要的:重排两个纤维的步骤,会在另一个纤维移动过的状态上求值某个迭代器,而映射的可交换性本身并不说明该迭代器在那里产出相同的逆变换与相同的续延。检验第一个条件只需迭代本身即可,因为引理 18(1) 把交换性从生成元传递到它们生成的幺半群上。

在这些条件下,定理 7 的单累加器不变量在交错(interleaving)下依然成立,其形式正是时间可组合性的内容所在:运行一个逆变换会撤回该纤维的贡献,除此之外别无其他。

定理 61(恢复精确性)。 设步骤序列是两两独立的,设 的一个时段在 处开启,设 位于该时段内,并设 中作用纤维不是 的那些下标。则

也就是说,在 处应用 的累加器,所得到的状态——至多相差控制字段——与这些同样的步骤从 出发本会产生的状态相同。若把右边理解为 从未开始本会达到的状态,则还需额外假设:在 内没有任何 所注册的纤维执行步骤,因为 注册的纤维在 从未开始的场景下本不会出现在那里,也就不会执行该步骤。

证明. 归纳,遍及时段内满足 属于该时段的那些下标 。当 时, 处的步骤是 L-Begin——时段按定义 53 由此开启——故由表 1 得 ,下标集为空,结论即为 。每一步用到两个事实。由于 只写控制字段,有

又由于 中每个映射除注册所添加的控制字段外不写任何控制字段——依据定义 48 连同定义 47——因此每个这样的映射都把 相等的状态映到 相等的状态。设步骤 作用于 。由于该时段在 处都开启,引理 54(4) 排除了 的 L-Begin 与 L-Unload;而 O-Insert 与 O-Remove 所读取的 会被 否认,于是只剩两种情形。

第 45 页

当规则是 L-Iter、L-Finish 或着陆的 L-Divert 时,由表 1 得 ,且 ,其中 是该次迭代产出的逆变换。定义 51 的见证条件给出 ——当该迭代注册一个纤维时至多相差 (引理 57)——而由上面的等式, 保持 ,故

当规则是 L-Leave、L-Raise、中止的 L-Divert 或 的 O-Retire 时,由表 1 得 ,故同一等式在 下成立。无论哪种情形,归纳假设都在下标集不变的情况下继续成立,这正是定理 7 的运算一步一步进行的过程。

设步骤 作用于 。则由表 1 得 ,且 ——若规则为编排规则则 ——故由独立性得

这正是把 拼接在末尾的归纳假设。

推论 62(终结恢复)。 设步骤序列是两两独立的,并设 的一个时段在 处开启、在 处关闭,无论 到达何种结果。则,以 如定理 61 所设,

由 O-Remove 移除的纤维同样不会留下任何东西,其前提只允许

证明. 由引理 54(4),步骤 的 L-Unload,其 由引理 54(3) 为 ,故 ,定理 61 适用。命题陈述与 都不提及 ;而由表 1, 正是 L-Divert 与 L-Raise 所导致的状态唯一不同的字段。

上面的结果假定组件是两两独立的,而第 3.3.2 节正是兑现这一假定的地方:当组件执行的每个效应都是某个键的运算、且每个键都可交换时,由这些运算构造出的任意两个效应函数都是独立的(定理 42)。把该结果从效应函数推广到迭代器无需任何新东西——共效应介导的效应函数(定义 41)本就依据每个阶段所产生的结果来选择其后继,而这正是迭代器在其续延中所携带的内容。第 3.2 节的共效应运算是完全不需要任何假设的情形:组件在那里贡献的映射是集合运算与相应限制的复合,任意两个这样的映射只要触及不相交的键就可交换,而定义 58 第 (2) 款使不同纤维的提供项互不相交。

4.4.3 空间可组合性

局部空间可组合性把组件约束在其自身规范之内:只在依赖齐备之处激活它,并对照这些依赖对每一次上下文变化进行分类(第 3.2.2 节)。全局形式则增加了对其他纤维的量化:提供者只有在所有解析了某绑定的依赖者都停用之后才撤回该绑定,而转换据以安装其效应的解析在该转换之下不会偏移。共效应一侧的两个性质分别给出这两者,而它们被一并证明,因为它们是同一个不变量的两半,即引理 54(2) 所确立的 在一个时段内的固定性(fixity)。排序定理正是该固定性在时段中 处于 继而 的那一部分之上所换来的结果;相干定理则是它在 安装其效应的那部分之上所换来的结果。

定理 63(排序)。 纤维只在依赖齐备之处开始一次转换:

第 46 页

再设 的一个时段,满足 (其中 );设 为包含 的时段,并令 遍历 。则

  1. ,且若 闭合则

证明. 第一个断言来自 L-Begin 的前提 ,由定义 46,该前提给出 。(1) 即引理 54(2)。

对于 (2),位于 处的 L-Begin 写入 ,其值为提供者,故 ;位于 处的 L-Begin 留下 ,故 ,从而 ,两个时段均按定义 53 开启。设 闭合且假设 。则 ,故 ,且由 (1) 有 ;这即 ,而位于 处的 L-Unload 对此予以否定。因此

对于 (3), 处的提供者,故 。在 内没有作用于 的 L-Unload:当 闭合时,它落在 处(由 (2));当它不闭合时,引理 54(4) 使 根本没有 L-Unload。由于 ,表 1 因此使 L-Leave 成为 内唯一可作用于 的规则,且其 ;由引理 54(1), 在那里保持不变。

一个分布在多个步骤上的转换,若非如此,可能会安装针对在其下方已经变化的解析所计算的效应;两条前提阻止了这一点。L-Iter 与 L-Finish 携带前提 ,因此只有当其已提交视图仍是其目标视图时,转换才会继续;L-Divert 携带其否定,因此目标视图的任何变化都会使纤维脱离该转换。L-Raise 根本不以目标视图为条件——提升是迭代自身所做之事,而非环境所要求之事——并且它在任何情况下都会退出该转换。变化的两个方向不被区分:依赖已消失的组件与依赖已被替换的组件经由同一条路径离开,因为一个已变为 的目标视图与一个已变为其他某个纤维的目标视图,同样地不等于 。惯性是使这一点不至于成为对每一步的保证的东西。当目标视图转向时已在飞行中的迭代,无论如何都会按 L-Divert 落地,而该落地会安装一个基于不再成立的解析所计算的效应。因此,这些规则所交付的是一个析取,而第二个分支正是使第一个分支安全的原因。

定理 64.(解析相干性。)设 的一个时段 处开启,且 。则 在该时段的一个初始区间 上为 ,且该转换的每一次迭代都针对同一个解析 运行:

当纤维离开该区间(即 )时,下列情况恰好有一种成立:

  1. ,且该时段在某个 处闭合,满足 ,如推论 62 所述。

证明. 位于 处的 L-Begin 写入 ,且由表 1,它是进入该生命周期状态的唯一规则;其前提 与引理 54(4) 将其任何第二次应用置于该时段之外。因此 占据 的一个初始区间 ,且不会被重新进入。

第 47 页

第一个断言随后就是表 1 赋予 L-Iter 与 L-Finish 的前提 ,再结合引理 54(2) 的

对于该二分, 是一条其前提含 而其结论不含的规则,表 1 提供的候选为 L-Finish、L-Divert 与 L-Raise;前者落入 ,后两者落入 ,由此引理 54(4) 使 L-Unload 成为唯一出口,而推论 62 提供该等式。落地的 L-Divert 所贡献的迭代是 自身的迭代之一,因而属于累加器所撤回的映射之列。当 时,序列以转换仍在飞行中告终,此时只断言第一个主张。

4.4.4 进展性

一个将提供者的撤回推迟到其依赖者消失之后的守卫,只有在最终释放时才能使定理 63 成立。注册表各纤维上的一个关系承载着这一论证。

定义 65. 注册表名字上的优先关系为

可以提供 所声明的键。它只读取 ,而由引理 54(5),二者随纤维条目的出现而产生,且此后永不再被写入。

定理 66 与定理 73 是在 无环这一假设下确立的;这是一个假设,而非该定义所交付的结论——对于声明一个由自身提供的键的组件, 成立。 所排序的是两个纤维的激活而非它们的生命周期: 表示 必须先于 变为 ;而提供者比其消费者长寿则是定理 63(2)——一条关于带守卫演算的定理。

纤维的目标视图既回应创建它的纤维,也回应其提供者。创建者所写入的是 ,经由定义 47 的原语;且由引理 54(5), 是单调的。因此,创建者在其子纤维的整个存在期间至多只能使其目标视图转向一次。

进展性是一个关于某条规则可应用的断言,因此它是在宿主必须提供的规则之上表述的:L-Begin、L-Leave、L-Unload、落地规则 L-Iter、L-Finish 与 L-Raise,以及 L-Divert。它从不诉诸 L-Divert 的中止性替代分支,因此受第 4.3.3 节惯性约束的宿主同样被涵盖在内。

定理 66.(进展性。)假设 无环、对每个 ,且定义 60 的名字集合 有限;并设每一步都应用一条生命周期规则。记 为作用于 的步数,记

为其目标视图转向的次数。则

  1. (无死锁。) 蕴含某条生命周期规则在 处可应用;
  2. (终止。),且 均有限。

因此,每一条生命周期步骤的极大序列都以一个静止状态告终。

证明. 无死锁。设 ,则某条纤维 不满足定义 49 的静止之任一条款。对照表 1 阅读其此时可能所属的四种情形:

  • :L-Begin 可应用;
第 48 页
  • 且目标 :此时, 的值所选择的是 L-Iter、L-Finish 与 L-Raise 中的哪一个,就适用哪一个;
  • 且目标 :若 引发失败则适用 L-Raise,否则适用 L-Divert,使该次迭代落地而非中止它;
  • 且目标 :适用 L-Leave。

设没有任何纤维属于上述任一类型,则留下某个满足 。按如下方式构造 :给定处于 ,要么 ,此时 L-Unload 适用于 ,构造终止;要么存在 ,使得 。在后一种情形下

其中第二个隶属关系来自定理 63(3),运用于 所在的 的那个时段,故 。此外, 纤维位于定义 的并之外,因此 处未被提供,或由 之外的某个纤维提供。若 处于 ,则它必属于被排除的四种类型之一,因此它处于 ,构造得以继续。诸 -递增的,故由无环性可知它们彼此不同;而 有限,所以构造终止。

终止性。 两条断言界定了

(A) 在目标 恒等于 的极大区间上,至多有 步作用于 。读表 1 的 列:从 出发,纤维执行一次 L-Leave 与一次 L-Unload,然后——若 ——执行一次 L-Begin 与至多 次落地,若最后一次落地是 L-Raise,则还要再执行一次 L-Unload;从针对某个 出发,它以 L-Divert 代替 L-Leave;从任何其他状态出发,则执行该序列的一个后缀。区间内不再出现 L-Divert 或 L-Leave——L-Begin 所写入的 正是目标 本身——而在 处、 时的 处以及 处,没有任何规则适用。

(B) 若 且第 步作用于 ,则要么 ,要么第 步写入 。由定义 46, 的值是 以及 各键的提供者的表的函数;提供者满足 ,从而 ;而由引理 54(1),表只在作用于其所属纤维自身的步骤上改变。无环性给出第一种情形下 ,而引理 54(5) 的单调性将第二种情形限制在每个纤维至多一个 处。

由 (A),区间计数给出 的上界 ;由 (B), 的每一次转变要么消耗严格 -低于 的某个纤维的一步,要么就是 所允许的那一次转变,因此 。由于 无环且 有限,递归

是良基的,并定义出满足 ;因此 有限,且 。由式 (1),无法再扩展的序列是静止的。

的有限性是假设而非推导出来的,组件上的一个条件即可推出它。宿主所持有的组件是运行任何东西之前就已给出的有限多个程序;因此,若没有任何组件能够(无论多么间接地)注册某个注册了其自身实例的组件的纤维,则注册关系形成一棵深度有界的树,而 界定了其分支数。该假设所排除的,是一个无界地注册自身实例的组件。

第 49 页

目标记录的是提供纤维而非布尔值;在第 4.2 节的单源纪律(single-source discipline)下,两者驱动相同的转换,因为在那里一个键只有一个可能的提供者。该视角所带来的是上述结果的词汇:定理 63 与定理 64 都谈及纤维针对其激活所依据的解析(resolution);也正是这一点使这些结果在第 3.2.3 节的作用域化解析(scoped resolution)下依然成立——在该解析下,一个键在不同的领域中解析到不同的提供者,提供项不再强制该视角。实现承载了这一作用域,并将该视角保存在 fiber.committed 中(第 5.1.3 节)。

4.4.5 合流性

到目前为止的结果都是关于单个纤维的。刻画系统整体的性质是:其动态历史不留下任何痕迹——无论一个运行中的系统经历过怎样的激活与停用序列,它静止时所处的状态,正是同样的插入与退役序列——其中每个最终处于激活状态的组件都只加载一次、按依赖顺序加载,且从未被卸载——所会产生的那个状态。生命周期关系是合流的,它所收敛的范式(normal form)正是静态组装出来的那个状态。这正是变更传播(change propagation)为增量计算所确立的"与从头求值的一致性"在动态组合上的对应物 [45]

该断言只关乎 本身。编排步骤是输入;两条给定不同输入的序列落在不同的地方并无值得关注的原因;关键在于:生命周期规则——它在"哪个纤维下一步动作"以及" 纤维从哪个出口离开"上都是非确定的——是否可能产生分歧。

首先需要三条引理。第一条在不参照任何步骤序列的情况下确定最终处于 的纤维集合,正是这一点使它成为输入的函数而非调度(schedule)的函数。

定义 67. 当纤维未被退役、注册它的纤维受支持、且它声明的每个键都由某个受支持的纤维提供时,称该纤维在 处受支持(supported)。 上的支持关系(support relation)是这两条条款所读出的两个关系的并:

在该关系良基之处(引理 68),我们用 表示支持集(support set),即 处受支持的纤维:

其中 标记编排器插入的纤维,否则 是激活并注册 的纤维。这两条条款不读取 之外的任何字段。两半都将一个纤维与紧邻其下的一个纤维相关联——是父纤维(parent)而非祖先,是直接提供者而非传递性提供者,因为条款读出的正是这些;下文的结果需要序时取的是传递闭包,其极小元、极大元与线性化(linearization)与 相同。

条款引用了 本身,因此该定义是沿 的递归,而正是下面这条引理使它成为一个有解的定义。

引理 68.(支持是良基的。)设 无环,且 由某个步骤序列到达。则 是良基的,且 是定义 67 的唯一解,是仅关于 的函数。

第 50 页

证明. 中的名字按注册它们的那个步骤的下标排序,而定义 53 通过从空注册表开始序列来提供这种排序。 的父指针半边沿该下标递减:O-Insert 以 为前提,所以父指针指向一个更早注册的纤维,反复迭代它可在有限步内到达某个名字的全部祖先。因此一个环必须用到 ,而由于 是无环的,它必须把二者混合起来,这就需要某个 声明一个键,而 自身子树中的某个纤维可能提供该键。这样的纤维由 的某个后代的激活注册,因此在 的 L-Begin 之后的某一步注册;该 L-Begin 以 为前提,所以提供该键的纤维在此之前就已经是 ,而定义 58 的第 (2) 款使得该键没有第二个可能的提供者。因此,本会闭合该环的那个纤维永远不会被注册,该边也就不存在于 中。良基递归只有一个解,而各条款只读取这四个字段。

最后一个条款读取 ,即组件可能提供的键;而目标读取 ,即其纤维已安装的键;定义 43 仅通过 把二者联系起来。因此,支撑集一般会过近似 纤维,而弥合这一差距的条件如下。

定义 69. 当组件 的一次完成的激活已安装 的每一个键,从而在其每个 实例化纤维处都有 时,称该组件在其提供项上是完全的(total)。

与独立性(定义 60)一样,这是仅针对组件本身的条件,不涉及任何生命周期状态,也不涉及任何步骤;而独立性已经限定了它可能失败的程度:若某个组件只在另一组件的效应所达到的上下文状态处安装一个键,那么它的前向映射就不会与该组件的映射可交换,因此纤维所安装的键由它的组件决定,而非由调度决定。完全性(totality)额外保证的是:这个固定的集合是 的全部,而非它的一个真子集。

引理 70(静止时的支撑集)。 无环,设 成立,设 中没有纤维失败,并设 的每个组件在其提供项上都是完全的(定义 69)。则支撑集就是 纤维的集合:

证明. 为右端。由于没有纤维失败,定义 49 的静止性使得 成为仅有的状态,并给出

由定义 46,右端恰好当 且每个 都位于 中时成立;而由定义 69,。中间那条子句是目标不再承载的,而注册机制提供了它: 的纤维只由 的一次激活注册;若 ,则 不是 ,所以它的累加器已经运行并按定义 47 使 退役,从而得到 。因此 满足定义 67 的各条款,引理 68 表明它们只有一个解,所以

引理 71(对换)。 设各步骤两两独立且 良构,并设步骤 作用于不同的纤维

  1. 若两者都应用激活规则(即 L-Begin、L-Iter 或 L-Finish),且步骤 处可应用,则步骤 在步骤 产生的那个状态处可应用,且两种顺序到达相同的
第 51 页

2. 若步骤 处应用激活规则,步骤 处应用编排规则,且步骤 不注册 ,则对二者同样成立。

证明. 对于 (1),由表 1, 的步骤写入 ,并在 内部写入表 与效应部分。因此它不改动 ,且由定义 60 的第二个条件,也不改动 所产生的逆变换与续延(continuation),所以只需检查步骤 中提及 的那些前提。其退役半边不会失效,因为没有激活规则会写入 。其解析半边也不会变动:步骤 处可应用意味着每个 都在 中,而定义 58 的第 (2) 款使得提供这样的 的纤维成为唯一可能的提供者,所以 的任何写入都不会触及 的键。反向的同样论证表明步骤 可应用。最后,由定义 60 的第一个条件, 可交换,且两次编辑写入的是不同纤维的控制字段,因此两种顺序下的复合结果相同。

对于 (2),由表 1,编排步骤有 ,所以两个状态映射直接可交换;其 只在 处写入 ,激活步骤既不读也不写它们:后者的前提读取 ;对全新 的 O-Insert 不移动任何目标——新纤维不提供任何东西;而对 的 O-Retire 或 O-Remove 把 留在原处——前一种情形中 ,后一种情形中它的表不受影响。所以步骤 仍然可应用。反过来,编排步骤的每个前提要么在 处读取(步骤 不写它们),要么是 O-Insert 的两个前提之一——更小的注册表只会放宽它们——于是它在 处的可应用性给出它在 处的可应用性;此处正是步骤 不注册 这一点使得 处依然存在,而 O-Retire 与 O-Remove 要求它存在。

引理 72(删除)。 设步骤序列两两独立,设每个组件在其提供项上都是完全的(定义 69),设它到达一个没有任何纤维失败的静止状态 ,设 的一个闭合的时段,设序列中没有满足 的时段闭合,并设 期间注册的任何纤维都没有时段。记 为这些注册所抽取的名字。则删除 中作用于 的步骤,连同作用于 中某个名字的每个步骤,会留下一个步骤序列,它到达一个与 近似相等()、且在 之外与它 相等的状态。

证明. 被删除的步骤把状态留在它们找到它的地方。设 中作用于 之外纤维的步骤。推论 62 给出

其右端正是 的存活步骤独立产生的结果,,且它们的编辑写入的是删除所不触及的、 之外纤维的控制字段。由表 1, 的被删除步骤除 外不写任何字段;由于没有纤维失败,引理 54(4) 在 处把 恢复到 ——这正是它在 处所持有的值。

一个不变式贯穿后缀。记 为存活步骤在与 对应的位置所到达的状态。我们断言:对每个 中的每个名字在 处是残留的(vestigial),而在 中不存在;且两个状态在 之外每个名字的每个字段上都一致。在 处,这正是上一段连同定义 47 所给出的:定义 47 使 中的每个名字都被在 处运行的累加器退役,成为 并持有一张空表——按假设, 的纤维没有时段。归纳步是在 的每个名字处依次应用引理 57(1):作用于 之外的步骤在两个状态处有相同的前提,到达的状态再次 相等,并把 的条目留在残留状态。作用于 中某个名字的步骤属于被删除之列;引理 57(2) 说明了它为何必须被删除而非保留——对不存在的名字执行 O-Retire 或 O-Remove 没有可作用的纤维;再由 (1),这样的步骤不移动 之外的任何字段,所以删去它保持不变式。因此最终状态 相等,且在 之外相等。

第 52 页

没有存活的步骤会失去前提。作用于 的步骤只通过 读取 。前者在 声明了 所提供的一个键时依赖于 ,从而 ;也在 注册了 时依赖 ,而这使得 。在第一种情形中,按假设 的时段不闭合,所以它在 处是开放的;静止性给出 ,引理 70 把它的值置于 纤维之中,而 并非其中之一;由于一个键至多有一个可能的提供者, 的 L-Begin 处也没有提供 的任何键。后者仅通过 的值读取 ;删除该时段只会使 变为假,这放宽 L-Unload 上的守卫而非阻塞它。这样的步骤对 中某个名字的读取由不变式涵盖。两两独立是效应函数的性质,所以删除步骤会保持它。

定理 73(合流性)。 设一个步骤序列到达一个没有任何纤维失败的静止状态 ,设各步骤两两独立且每个组件在其提供项上都是完全的(定义 69),并设 如定义 67 所述。则

1.(规范形。)在归约撤回其条目的那些名字的范围内, 由一条从 出发的序列到达;该序列按原顺序采取相同的编排步骤——作用于编排器所插入的纤维的那些步骤先于每个生命周期步骤,其余每个步骤跟在注册其所作用纤维的那一步之后——并且对 的一个线性化 的枚举 ,按该顺序各取 的一个时段。

2.(合流性。)从 出发、采取相同编排步骤的任意两条这样的序列,在按引理 56 的方式重命名之后,所到达的状态由 相关联。

证明. 对于 (1),序列中的时段有两类:闭合的,以及在 处仍然开放的——由 与引理 70,后者是 中每个纤维各一个时段。

闭合的时段先处理,对它们的数目作归纳。在每一阶段,在时段仍然闭合的纤维中,挑选一个 -极大的纤维 的闭合时段;由引理 68 与 的有限性,这样的时段存在。引理 72 的三个假设随后均得到满足。由极大性,不存在满足 且有时段闭合的 。而且, 期间注册的任何纤维都没有时段:这样的纤维被在 处运行的累加器退役(定义 47),并由引理 54(5) 保持退役,所以它的目标视图为 ,引理 70 把它置于 之外,因此它在 处没有开放的时段;而 通过它的父指针把它关联到 ,所以由极大性它也没有闭合的时段。该引理连同它所注册的名字的那些步骤一起移除该时段,在那些名字的范围内把 留在原处。度量每次减一,因此最终不再有闭合的时段。

之外的纤维不采取任何生命周期步骤。由引理 70 与 ,它在 处没有开放的时段,而如今也不再有任何闭合的时段,所以它根本没有时段,自始至终都是 ;L-Begin 是唯一适用于它的规则,而应用它会打开一个时段。

编排步骤接下来处理。作用于编排器所插入的纤维的编排步骤,由引理 71(2) 越过另一纤维的一个生命周期步骤向前移动一位;该引理适用,是因为 中纤维的步骤不会注册这样的名字:注册抽取的是新名字,而这里的名字是原序列的某个 O-Insert 引入的。与同一纤维的生命周期步骤之间则无可交换: 的 O-Insert 已经先于 的每一个步骤,而 的 O-Retire 或 O-Remove 只应用于 之外,那里不采取生命周期步骤。依次把每一个移到最前面,会保持它们的相对顺序。作用于某个激活所注册的纤维的编排步骤不能移到最前面——其前提要求该纤维存在——所以它留在注册所放置它的位置;由上一段,它作用于 之外,因此由引理 71 的同一款,它与它和注册之间的所有步骤都可交换。

第 53 页

作归纳,把时段排序并使其连续。设 中是 -极小的。则 ,因为定义 67 把 中某个键的提供者与注册 的纤维都放入 ,而 把二者都置于 之下。所以 不读取任何其他纤维的字段;又因不再有编排步骤写 ,也不再有 之下的纤维会退役它, 是常数。作用于 的每个步骤都是激活步骤,没有时段闭合;其剩余的前提读取 ——由表 1,只有 写它们——因此每一步在每一个更早的状态处都可应用,引理 71 在不移动端点的情况下把它向前移动一位。每次应用都使 的某个步骤之前其他纤维的步骤数减一,因此 的时段成为一个位于开头的连续块。该论证在块之后的那个后缀上对 重复;那里 全程都是 且不再采取任何步骤,所以它也贡献一个常数的目标。这样产生的枚举由构造即线性化

对于 (2),由 (1),两条序列都归约到同一条规范序列,而两次归约在重命名的范围内作用于同一个 。定义 67 读取 ,其中后三个随纤维的条目只写一次(引理 54(5)),所以需要确认的是:相同的名字带着相同的 进入存在,且相同的名字被退役。插入是两条序列按假设共有的;注册它们也同样共有: 中一个纤维的激活在其每次迭代处注册迭代器在那里指名的组件,而定义 60 的第二个条件使该组件在交错之下保持不变,因此 -纤维之下的注册树是该纤维组件的函数;这些注册抽取的名字并不共有,正是在这里应用引理 56,用一双射匹配两棵树。而一次退役要么是编排步骤(共有),要么是累加器采取的 O-Retire——它退役的恰好是同一个激活所注册的名字。线性化 的两个枚举只差不可比较时段之间的对换;引理 71 再次使端点在这些对换下保持不变,所以两条规范序列一致。结合定理 66 的终止性,生命周期关系因此具有唯一的规范形(normal form)。

失败被排除在陈述之外,因为它是发散的一个真实来源,也不应把演算理解为否认它:一步是否引发(raise)取决于它所运行所对的状态,因此一种调度可能使一个纤维失败,而另一种调度却完成它,于是两个静止状态在那个纤维的生命周期状态上不同。由推论 62,它们在别的任何方面都不不同——推论 62 把失败纤维对状态的贡献置为零。

在第 4.2 节的基础演算中,同样的定理成立,证明除删去一款外不需要任何替换。L-Unload 在那里不携带守卫,所以引理 72 的最后一段是空泛的(vacuous);该引理的其余部分只援引 ,而基础演算原样提供它。

正是该定理授权我们把 Cordis 应用当作它是静态组装的那样来推理。一个添加组件、移除组件、替换提供者并撤销替换的编排器,保证会到达它若在一开始就把最终组合写下来本会得到的那个状态;而组件作者若想推理哪些共效应在作用域内,可以只针对静止状态进行推理。它也划定了该保证的范围:它说的是状态,而非系统沿途产生的发射(emission)——这正是第 6.1 节在系统边界内部追踪的获取(acquisition)与跨越边界的发射(emission)之间所作的区分。

第 54 页

5 实现与案例研究

本节介绍 Cordis,它将第 3 节的形式模型实现为一种实用的编程抽象。Cordis 是一个时空可组合性的元框架(meta-framework):与面向特定领域的应用框架(例如 Web 路由、ORM、UI 渲染)不同,它不规定任何具体场景;其唯一职责是提供普适的动态组合(dynamic composition)语义。该实现分为三层:(1) 核心库(第 5.1 节)直接实现效应系统与共效应系统;(2) 组件加载器(第 5.2 节)以配置协调(configuration reconciliation)与热模块替换(hot module replacement)扩展核心;(3) 诸如 Koishi(第 5.3 节)之类的应用框架在前两层之上构建领域特定功能。

5.1 核心库

表 2 概括了理论构造与其运行时对应物之间的对应关系。特别是,我们在本节通篇使用下文引入的运行时名称,而将理论符号保留给形式对应关系。我们还用 @@name 表示框架内部的符号键,因此 ctx[@@store] 中的方括号表示对上下文上不透明槽位的符号键访问,而非对字符串键映射的索引。

第 55 页
理论(第 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,拥有其被实例化时所处上下文的纤维
派生实现(定义 27) fiber.ctx,纤维运行所在的子上下文
(定义 44) fiber.state,生命周期状态;其 LOADING 为 ,FAILED 为
recover、累加器 fiber.dispose,累加器
(定义 44) fiber.committed,已提交视图
一个 Impl,其提供者纤维处于 ACTIVE
fiber.target,由 refresh(算法 5)重算,其中 为 INACTIVE
、惯性(第 4.3.3 节) fiber.inertia,进行中转换的句柄
O-Insert、O-Retire(定义 47) ctx.use 及其回调的逆(算法 4)
O-Remove 从运行时中丢弃的纤维,uid 被清除
L-Begin、L-Iter、L-Finish execute 的迭代循环(算法 1)
L-Divert 迭代边界处守卫失败(算法 1),或重载链入卸载
L-Leave refresh 将纤维标记为 UNLOADING(第 10 行)
L-Unload unload 及其惯性链式延续(算法 5)
L-Unload 上的守卫 unload 等待被通知的依赖者(第 25 行)
L-Raise 记录在纤维上的错误,其 target 置为

表 2 | 理论到实现的对应关系

本节余下部分自底向上地构建核心库。第 5.1.1 节实现可逆效应——这是使上下文发生变更的唯一原语;第 5.1.2 节在其之上实现响应式共效应;第 5.1.3 节将二者组合进组件生命周期;第 5.1.4 节则暴露建立在它们之上的上下文级操作。

第 56 页

5.1.1 效应跟踪

本节实现可逆效应(第 3.1 节)。Cordis 中每一次上下文变更都流经单一原语 ctx.effect:共效应提供、组件实例化以及所有其他变更上下文的操作,都归结为一次 ctx.effect 调用,因此任何经由上下文执行的操作都会被自动跟踪,并在组件卸载时得到恢复。在操作层面,ctx.effect(定义 52)的实现:它接受一个类型为 的回调,并将其提升为 ,从而产生一个释放闭包(dispose closure);该闭包一经调用,即恢复该效应。Cordis 通过这一操作同时接受 (特设多态,ad-hoc polymorphism);我们以迭代形式为代表,因为普通效应函数正是产出单个逆变换的退化迭代器。该操作不检查的,是 所携带的见证(witness):回调提供逆变换,而该逆变换能恢复其所伴随的效应——这是组件作者应尽的义务,而非运行时验证的性质。定理 61 正是演算诉诸该义务之处,而第 6.1 节界定了这一义务。

算法 1 展示了 ctx.effect 的构造。我们用 表示先运行 再运行 的释放器,用 表示空操作;因此,将每个新逆变换前置,即可得到后进先出(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 将回调作为效应迭代器(,定义 51)驱动,并把每一步产出的逆变换折叠为单个复合体。在每一步之前,它都查询调用方提供的守卫;一旦守卫触发,迭代即停止,只剩下迄今已累积的逆变换。这正是第 4.3.2 节的步边界中断: 续延(continuation)由迭代器的 done 标志连同守卫共同实现。

ctx.effectexecute 之上的薄封装,它增添了两点。第一,自销毁(self-disposal):守卫报告 armed 标志,返回的 disposearmed 翻转为 false,这一操作同时中止任何进行中的迭代,并使恢复至多触发一次。若触发两次,就会在一个没有任何效应应用产生过的状态上应用逆变换,此时没有任何东西约束它去还原任何内容。第二,父级复合:dispose 被前置到外层上下文的累加器

第 57 页

……所构造的逆 ctx.dispose,因此子效应的逆本身是作用于父纤维的效应,这正是 的递归结构。组件层级(第 5.1.3 节)复用了同一个 execute,只是其守卫测试的是 fiber.target 的稳定性,而非 armed。

5.1.2 共效应操作

本节实现响应式共效应(第 3.2 节)。所有共效应操作都作用于每个上下文携带的三个以符号为键的槽位:

  • @@store:值存储 ,从领域符号映射到类型化值;
  • @@isolate:领域表 ,从共效应键映射到领域符号;
  • @@intercept:拦截表 ,为每个键分配其元数据。

前两者组合成两层解析 ctx.get(key)(算法 2)先从 @@isolate 读取领域符号 ,再从 @@store 读取被绑定的值 这一层间接使得隔离可以把一个键重定向到独立的绑定;而 @@intercept 只在绑定被访问时才被查询,它调整的是绑定被使用的方式,而非它解析到什么。我们分两部分实现这些操作:(1)提供与通知,负责安装或撤回绑定并把变更传播给依赖者;(2)隔离与拦截,负责重塑一个键的解析方式。

提供与通知。 由于 具有类型 (第 3.1 节),共效应提供就是一次 ctx.effect 调用,并继承其自动跟踪与恢复。算法 2 实现 ctx.set(key, value),即具体的 :回调把值绑定到存储中领域符号 之下,返回的释放函数则将其移除。安装与移除都会调用 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 节展开。

第 58 页

算法 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

一个绑定只有在安装它的纤维处于 (激活)状态时才被算作对依赖者可用,因此 refresh 针对活跃提供者而非仅针对存储来解析每个已声明的键。这正是定义 46 的 provided by(由……提供)关系,也正是它使得撤回在发生前一步就对依赖者可见:已进入 (卸载中)状态的提供者已停止提供,因此其依赖者会在其绑定仍然全部就位时,重新计算出未满足的目标视图并开始自己的拆除。

隔离与拦截。 这两个操作在结构上做的是同一件事:各自派生一个子上下文,为 key 调整一张继承来的表,而父上下文保持不变,因此恢复是隐式的——丢弃子上下文即可,无需运行任何显式逆变换。ctx.isolate(key, realm) 用 realm(默认则为新生成的符号)覆盖领域映射 (实现 isolate,定义 29),因此两个对同一键赋予不同符号的上下文会解析到独立的绑定。ctx.intercept(key, metadata) 把 metadata 合并进拦截表 (实现 intercept,定义 31):按照该定义,新的元数据与上下文已为 key 携带的元数据合并,并优先于后者。

5.1.3 组件生命周期

组件通过 ctx.use 被实例化为一个纤维。本节为纤维(第 5.1 节引入)赋予操作语义,将其作为第 4.3.3 节的惯性状态机。以下算法由两个字段驱动:fiber.parent,即 fiber.ctx 的父上下文,它构成组件层次结构( 的递归结构,第 3.3.1 节);以及 fiber.inertia,即进行中的异步转换的句柄(空闲时为 null)。

算法 4 展示组件实例化。组件把共效应规范()与效应函数 component.apply 配对;实例化把组件的配置绑定进 fiber.apply(第 9 行),即配置应用后的效应函数(),生命周期随后运行它。回调函数(第 2 行)是在父纤维中被跟踪的效应:执行时,它通过调用 refresh(算法 5)启动子组件的生命周期;被恢复时,它把子组件的 target 强制设为 并触发卸载。这就是定义 47 的注册原语,其中 callback 作为其 O-Insert,callback 返回的闭包作为其 O-Retire:一次实例化就是父纤维的一个普通被跟踪效应,因此卸载父组件会级联到其子组件。

component.inject

算法 4 组件实例化

 1  function use(ctx, component, config)
第 59 页
 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;若该纤维尚未处于转换之中,则启动一个重载或卸载任务2reload 函数记录当前目标,并执行组件的效应函数 apply。完成后,它检查目标是否仍然匹配:若匹配,纤维进入 ACTIVE;若不匹配(无论新目标是 还是不同的提供者集合),它都链接到 unload。对称地,unload 按后进先出(LIFO)顺序恢复所有被跟踪的效应,然后要么进入 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

2 create_task 调度一个异步函数并发运行,并返回指向它的句柄(存储在 fiber.inertia 中)。我们显式写出它,是为了与语言无关:在急切调度(eager scheduling)下(例如 TypeScript 的 promise),该调用是隐式的,返回的 promise 即句柄;而在惰性调度(lazy scheduling)下(例如 Python 的协程、Rust 的 future),宿主必须派生(spawn)该任务,它才会推进。

第 60 页
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 组成一个元组,因此它是 (定义 46)的一个摘要。以提供者而非以值来标识一个绑定,这正是使一次与所记录目标的单一比较即告充分的原因:uid 是全新生成的、绝不复用,因此一个被替换的提供者不会被误认为它所替换的那个提供者——即使二者提供相等的值。由于 notify(第 5.1.2 节)在每次共效应变更时都会重新计算目标,一个纤维恰在其某个声明的键改由不同的纤维提供时重载。因此,一个就地覆盖自身绑定的提供者不会被观察到;想要让替换传播出去的组件,会撤回该绑定并重新安装它。

该算法在两个互补的层次上运作。在转换层次上,reloadunload 在完成时检查目标,使得转换之间可以进行惯性链接(inertial chaining)。在每个转换内部的迭代层次上,效应执行(算法 1)在每次迭代边界检查目标,使得单个转换内部可以进行部分回滚。这两种机制分别对应第 4.3.3 节的转换间链接,以及定理 64 所依据的转换内陈旧性检查(staleness check)。

有三行代码承载了定理 63 的共效应排序,而它们各自所处的位置,正是使该排序得以成立的原因。reload 在第 14 行提交解析得到的视图,而 unload 只有在每一个逆变换都运行完毕之后才丢弃它,因此一个纤维在其加载期间——包括它自身的拆除——始终读到相同的绑定。refresh 在第 10 行、转换任务创建之前,把纤维标记为 UNLOADING——这正是 L-Leave 步骤:纤维停止提供,依赖者在它的任何逆变换被调度之前,就针对这一点重新计算。随后 unload 在第 25 行等待每一个被通知的依赖者到达 INACTIVE——这正是 L-Unload 上的守卫;notify 只在依赖者声明的键解析到与提供者相同的领域符号时才接纳该依赖者,这即是守卫之要求在运行时的体现:依赖者必须是从该纤维处看到这个键,而不仅仅是声明它。该等待位于整个恢复过程之前,而不是位于某个被等待的逆变换内部,因为 fiber.dispose 会并发地启动一个纤维的各个效应,若把等待放进其中某一个效应内部,其余效应就会失去顺序。终止性由定理 66 保证:一个纤维只会等待那些已经不再可满足的依赖者,而一个本身也是提供者的依赖者,也会以同样的方式等待它自己的依赖者,因此提供者图是按需遍历的,而不是预先分析的。

第 61 页

5.1.4 上下文访问

第 5.1.2 节的共效应操作构成一个反射式 API:共效应通过 ctx.set(key, value) 写入、通过 ctx.get(key) 读取,二者都以名字为键。Cordis 在这一反射式 API 之上,叠加了第二种更为原生的扩展与消费上下文的方式:属性访问。组件可以把共效应作为属性 ctx[key] 来访问,仿佛它就是上下文的原生结构,而不必通过方法调用。在 TypeScript 中,Cordis 用一个 Proxy 实现这一点:其获取陷阱(get trap)中介每一次属性访问。算法 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) 是对存储的一次查询,返回被绑定的值或什么也不返回,并且从不失败;而代理则针对发起访问的纤维自身的视图进行解析,并在使用点强制执行共效应规范 。读取视图而非存储,也正是定理 63 所依据的:正是这一点,使得一个依赖对某个组件始终保持可读——即使该组件的拆除正是由该依赖的消失所触发的。

这种拒绝是在访问点执行的运行时检查。由于组件的共效应规范 是静态声明的,同样的违规在原则上可以在编译时检测出来:在执行之前,把每一个 ctx[key] 对照所声明的 进行解析即可;第 6.4 节讨论宿主语言的类型级依赖声明与编译期元编程如何恰好完成这一中介。

5.2 组件加载器

核心库为组件开发者提供了用于动态组合的命令式原语,如 ctx.effectctx.usectx.set。应用程序的编排器(orchestrator)则面临另一项关注点:他们把现成的组件装配进一个运行中的系统,并在其生命周期内调整组合。组件加载器通过引入一个声明式配置层来解决这一关注点:编排器把期望的组合指定为一个持久化数据结构,而加载器则把对该规范的变更翻译为相应的命令式纤维操作。

第 62 页

5.2.1 声明式配置

第 4 节把一个运行中的系统分解为若干纤维,其中每个纤维都是某一个组件的实例化。实例化所需的一切都可以声明,因此编排器可以把整个系统描述为一份声明式配置:一条持久记录,加载器把它实现为若干纤维,并与之保持同步。

**条目。**配置由若干条目(entry)组成。每个条目指定一个纤维并对其进行管理,且这种绑定是双向的:加载器通过调整纤维来响应条目字段的变化;而组件若修订自身配置或停用自身,其变化也会被写回它的条目。

定义 74. 一个条目声明单个纤维,并记录以下内容:

  • id——一个稳定标识符,当所在组的子列表发生变化时用作协调键;
  • url——要实例化的组件模块的 URL;
  • isolate——应用于条目上下文的隔离注解;
  • intercept——应用于条目上下文的拦截注解;
  • config——绑定进组件、用以构成其效应函数 apply 的配置;
  • disabled——该条目是否被管理性地关闭。

条目之所以能充当忠实的规格说明,是因为支撑一个纤维的正是条目所记录的内容。定义 67 的支撑集只读取 ,别无其他;而条目恰好提供这四者:disabled 给出 ,条目在树中的父节点给出 ,url 选出声明 的组件。支撑集不读取的那些字段正是纤维的运行时状态,实例化也同样不需要它们;引理 70 在"每个组件都安装其声明的每一个键"(定义 69)的限度内,把支撑集与静止状态(定义 49)中的 纤维等同起来。

这些条目构成一棵配置树,它是系统所加载内容的权威记录。一个条目可以是映射到单个纤维的叶子,也可以是其组件转而加载更多组件、从而使该条目成为分支节点。Cordis 为这种分组式与嵌套式加载提供了相应组件:@cordisjs/group 以子条目列表作为其配置并把它们作为子组加载;@cordisjs/include 则加载外部配置文件(YAML 或 JSON),并把其中的条目嫁接为嵌套子树。两者都是建立在定义 47(算法 4)的注册原语之上的普通组件,因此嵌套树仍在演算范围之内,下面的结果对它同样成立。

**协调。**当条目的记录发生变化时,加载器进行增量协调,而不是把纤维拆除后整体重建。以这种方式协调之所以可靠,其理由由元理论给出。

  • 定理 73 使静止状态单独成为最终配置的函数:无论加载器一路上执行了哪些实例化与退役,也无论其顺序如何,系统都会静止在"从零加载最终配置"所应到达之处。最终加载了哪些组件,只能依据各组件是否安装了其声明的每一个键(定义 69)从声明中读出;若某个组件声明了一个键、却仅在部分配置下安装它,加载器仍可对其进行协调,只不过此时已加载组件的集合也同样随这些配置而定。
  • 定理 66 证明系统确实会静止,因此一旦协调所对应的实例化与退役都已发出,协调即告完成。
  • 推论 62 把离开的纤维对状态的贡献置为零,因此重建一个条目会撤回其纤维所安装的内容,并让周围的纤维保持原样。
第 63 页
  • 定理 63 允许各条目一并实例化,无需编排器安排加载顺序:所声明的键尚未得到提供的纤维会停在它的 L-Begin 处等待,而提供者已离开的纤维则会在其之前被停用。因此,依赖约束的是纤维何时激活,而非其模块何时被获取并求值;于是加载器可以并发地加载模块——启动大型配置的耗时正耗费于此。

在条目所声明的纤维之上,加载器按条目的哪个字段发生了变化进行分派,并对每个字段应用扰动最小的操作。

  • id、url——重建该条目,因为条目的身份或其组件已经改变;
  • isolate——重新分配该条目的领域(算法 7);
  • intercept——就地更新,因为拦截元数据在读取时才被查阅,无需重载;
  • config——交给组件,由组件决定如何应用新载荷,通常是把新载荷与旧载荷做差异比较,仅在发生实质性变化时才重载。特别地,@cordisjs/group 条目的 config 就是其子条目列表,因此它按子条目 id 做带键的差异比较(keyed diff)来应用更新:创建、移除或更新每个子条目;由于更新一个存续的子条目会重新进入这同一个逐字段分派,组协调与条目更新会一同沿树向下递归;
  • disabled——置位时卸载纤维,清除时重载纤维。

**受管领域。**核心中的隔离在单个键上覆盖领域表 ,从而派生出一个子上下文(第 5.1.2 节);在上下文树保持静止的情况下这已经足够。然而条目可能在运行时被移动到别的组,因此加载器自行管理领域;isolate 字段在每个键上从两种作用域规则中选择其一。取值为 true 时要求一个局部领域:它对该条目私有,以其 id 为标签,条目无论移到何处都随身携带;取值为字符串时要求一个全局领域:所有命名该字符串的条目共享此领域,因此移动这样的条目,改变的是它与哪些条目共享绑定,而不是它属于哪个领域。一旦没有任何条目命名某个领域,该领域便被丢弃。

重新分配条目的领域,取决于哪些键改变了领域、条目自身是否就是某个发生变化的键上的提供者、以及需要通知哪些依赖者。中间那个问题是最难的:一个领域符号可能被若干纤维共享,而其中只有一个是提供者。加载器用定界符(delimiter)来回答:每个键一个符号 ,各上下文在它之下存储各自的标签。定界符写在某个上下文上并由其后代继承,因此当且仅当条目与提供者是在 的同一个 isolate 作用域内派生时,二者的标签才恰好一致——而正是在这种情况下, 处的绑定才属于条目自身、必须随它一起移动。

算法 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
第 64 页
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
16  function affected(fiber, 𝑘)
17    (𝑠1, 𝑠2, 𝑑1, 𝑑2) ← diff[𝑘]
18    return fiber.ctx[@@isolate][𝑘] ∈ {𝑠1, 𝑠2} and (fiber.ctx[𝛿𝑘] = 𝑑1) ≠ (𝑑2 = 𝑑1)
19  notify(entry.ctx, Δ, affected) ▷ 取代算法 3 中的领域测试

该测试依赖于分隔符的一个性质: 下的标签被写入条目的上下文,并由从它派生的每个上下文继承;在每次重分配时,该标签都会被重新抽取,因此,对于任意上下文

将该条件记为 ,其中 是它在提供者处的实例。重分配把满足 own 的上下文从 移到 ,其余上下文留在原处;而由上述循环可知,当且仅当提供者满足 own 时,绑定才被移到 。当依赖者在 处的自身领域恰好是绑定所在的领域时,依赖者就能看到该绑定。当 own 在依赖者与提供者上一致时,要么双方都移动,要么双方都不移动,因此依赖者在移动之后看到该绑定,当且仅当它在移动之前也看到了它。当 own 将二者区分开时,一侧移动而另一侧停留,于是依赖者会获得或失去该绑定。该不等式正是这种区分;而成员测试剔除的是那些在 任一领域中都不解析 的依赖者——移动的任何部分都不会触及它们。

5.2.2 热模块替换

热模块替换(hot module replacement,HMR)在模块层面应用可逆效应模式:当源文件发生变化时(通常发生在开发期间),系统在不重启进程的情况下就地替换受影响的模块。由于纤维已经界定了其组件的一切效应与共效应,一个本身即为组件的模块可以仅通过纤维操作完成替换:销毁旧纤维即可回收组件安装的所有内容,而从重载后的模块实例化的新纤维会将其重新安装。因此,与 Webpack [46] 或 Vite [47] 的 HMR 不同,HMR 不需要开发者标注的接受边界(acceptance boundary)。

@cordisjs/hmr 组件提供了 HMR 引擎,该引擎分三个阶段运行。

**阶段 1:模块分类。**引擎接收两个输入:暂存集(stashed set,即自上次重载以来内容发生变化的文件 URL 的集合)与外部集(externals set,即无法热替换、转而触发完全重启的模块的集合)。以 表示 直接导入的模块集合,引擎对变更的依赖子图进行分类,将每个模块标记为 accepted(接受)或 declined(拒绝):

算法 8 模块分类

 1  function classify(stashed, externals)
 2    accepted ← stashed
 3    declined ← externals
 4    pending ← ⌀
 5    for url in stashed do
第 65 页
 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)

以暂存文件的导入为种子,该不动点会在某个模块的任一导入被接受时接受该模块,并在其全部导入都被拒绝时拒绝该模块;任何因陷入导入环而悬而未决的模块默认被拒绝。

**阶段 2:过期条目检测。**利用 accepted 与 declined,引擎随后把组件条目筛选到其中的过期条目(stale entry)——即依赖树触及某个已变更模块的条目。引擎用 遍历每个条目的依赖树;该函数收集一个模块的传递导入,同时把 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,因此沿树上的每个过期模块都会在下一阶段失效。

第 66 页

**阶段 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⁴ 构建的开源聊天机器人应用框架。经过四年多的开发,它已积累了 4000 多个社区贡献的插件⁵,涵盖即时通讯(IM)适配器、数据库驱动程序,直至管理控制台与终端用户功能。其规模与多样性使其成为 Cordis 动态组合能力在生产环境中的代表性验证。

**元框架的表达力与通用性。**Koishi 以服务端机器人(server-side bot)的形式运行,其每一项功能都实现为基于第 5.1 节上下文原语的插件;Koishi 自身只贡献聊天机器人领域的词汇。同样的模型在一个完全不同的运行时中重现:Koishi 的 Web 控制台是第二个独立的 Cordis 应用,其插件组合的是浏览器及其用户界面的原语,而非服务端的原语。上述迥异的场景确立了第 3 节模型的两种性质。(1) 表达力:其原语足以承载一个完整的生产系统,宿主框架仅提供领域词汇。(2) 通用性:它固定了效应与共效应如何组合,同时把它们的含义留给各个应用自行解释,因此既不预设特定的领域,也不预设特定的运行时。

**无需认知开销的时间可组合性。**第 1.2.1 节所考察的插件系统无法在不重启扩展的情况下卸载单个扩展的效应。


脚注

³ 在 Node.js 上,这意味着要同时清除 ES 模块与 CommonJS 模块两套模块系统的缓存,因为经由 ES 加载器导入的模块可能同时出现在两者之中。

Koishi 目前使用 Cordis v3。本文介绍的是 Cordis v4,它细化了效应与共效应语义,并重新设计了加载器;两版共享同一核心组合模型。

Koishi 使用"插件"(plugin)一词指代本文将其形式化为"组件"(component)的概念。

第 67 页

宿主。Koishi 经常执行这一操作:编排器从控制台停用一个插件,其效应即被就地撤回;在开发期间,HMR 引擎会在保存时重新应用编辑过的插件,同时保留系统中其他位置的缓存状态与活动连接。Cordis 使这种移除对插件作者而言不仅可行,而且毫不费力。由于通过上下文执行的效应会被跟踪,其逆变换会自动复合(第 3.1 节),即使是缺乏经验的作者,也能在不编写卸载路径的情况下,获得插件上下文中介效应的有序清理。这实现了第 1.2.1 节所指出其缺失的关注局部性(locality of concern):原本依赖每位作者个人勤勉才能保证的正确性,如今由该抽象一次性承担。

跨开放生态系统的空间可组合性。 与第 1.2.1 节中插件间依赖基本缺失的插件系统相比,Koishi 的生态系统呈现出真正的依赖拓扑:IM 适配器提供对各消息平台的访问,数据库驱动提供持久化存储,功能插件将这些声明为共效应并加以访问。在运行时重新配置某个提供者——例如切换存储后端或重连适配器——只会重新激活那些已解析依赖发生变化的依赖者(第 3.2 节);依赖不可用的插件会保持不活跃,直到该依赖出现,而不会报错。案例分析所证实的是,这种组合在独立编写的代码之间依然成立:一个插件与其依赖通常由不同作者编写,他们除了连接彼此的共效应之外无需协调任何东西,因此响应式共效应使整个组装在由独立贡献者构成的开放生态系统中保持一致。

有效性威胁(Threats to validity)。 此处的证据取自单一宿主语言中的单一生态系统,因此无法将该范式的优点与其 TypeScript 实现的优点或 Koishi 特定领域的优点区分开来;而且它是观察性的,而非与替代架构进行的受控对比。因此,案例分析所确立的是一个存在性与采纳性(existence-and-adoption)的结果,而非定量结果;以基线来衡量该抽象的额外开销及其对开发者生产力的影响,仍属未来工作。

6 讨论

前几节给出的形式模型与实现引入了一种面向动态组合的编程范式。本节考察该范式如何推广到更广泛的工程关切,并讨论其中的设计张力与开放问题。

6.1 系统边界

第 3.1 节中的每个效应都携带一个逆变换,而该逆变换究竟意味着什么,由系统边界决定。边界将系统运行所面对的环境划分为两部分。(1)当系统能够独占式地修改某位置(location)并恢复到该修改之前的状态时,该位置位于边界之内,因此对其执行的操作会被记入 ,并可在之后被恢复。(2)当上述两种能力任一缺失时,该位置位于边界之外,因此对其执行的操作相当于 ,既不记录也不恢复。本节阐述该边界的性质及其对恢复的后果。

共效应带来的边界移动。 共效应通过具体化外部位置来移动边界:它将对该位置的每次访问都限定在它所提供的一组操作之内,并能为其每个操作提供逆变换,因此原本表现为 的操作转而会被记入 并被恢复。(第 68 页)

因此,边界是按位置而非按介质(medium)划分的,因为上述两种能力都是位置的性质,而具体化改变的是位置的访问方式,介质本身保持不变。例如,当只有系统自身写入某内存区域时,它位于边界之内;当其他进程也写入它时,它便位于边界之外。类似地,当只有系统能够到达某文件时——如私有路径下的临时文件——它位于边界之内;当它是其他程序可读写的路径时,则位于边界之外。移动边界本身就是一种权衡:一方面取决于环境是否为某位置提供可逆语义,另一方面取决于为每次访问提供这些语义的代价。我们在第 6.7 节讨论这一权衡所提示的协同设计。

获取与发射。 触及边界之外的操作通常分两个阶段进行。(1)在获取阶段,操作获得访问权并在边界内部安装一条记录:open 安装的描述符由 close 移除,malloc 保留的内存块由 free 释放,fork 启动的子进程由 kill 终止。该记录本身是具体化该位置的共效应的一部分,例如它所维护的映射中的一个条目,而安装该条目是一个可逆效应。这条记录同时还是数据得以离开的通道。(2)在发射阶段,操作通过该通道推送数据,正如 write 交给文件的字节或 send 放到网络上的数据报,这种推送相当于 ,将数据留在其他方可读可写之处。因此,这两个阶段落在边界的两侧:获取停留在边界之内,而发射跨越到边界之外。

扣留与补偿。 一个仍必须从发射中恢复的系统有两条可用途径。其一是扣留发射,直到产生它的状态确定会持久化为止,这正是回滚恢复(rollback-recovery)中的输出提交问题 [48]。其二是补偿 [49]:一种将状态恢复到应用程序所提供等价关系之下的动作,该等价关系比定义 33 的 更粗,例如删除已创建的文件或退还已收取的费用。这类动作与逆变换一样按后进先出(LIFO)的顺序复合,因此第 3.1 节的复合性质可迁移到它们之上。元理论则不然:定义 60 的可交换性是在 下证明的,必须针对更粗的等价关系重新建立。

6.2 服务复用

OSGi [50] 等动态组件平台围绕服务来组织组合:服务是提供者在某接口下发布、消费者绑定到其上的功能单元。Cordis 的共效应模型呼应了这一概念:服务对应于某个键背后的接口。提供服务(service)的组件是其提供者,注入服务的组件是其消费者。单个服务可以由多个提供者实现,而这种多重性可以两种形式实现。(1)独占绑定:多个实现共享一个接口,但同一时刻至多绑定一个;由编排器选择绑定哪个实现,而在它们之间切换需要卸载一个提供者并加载另一个,会瞬时扰动每个消费者的依赖。(2)服务代理:一个充当接口入口的中央服务,由底层提供者和消费者共同注入,从而多个提供者共存,代理在它们之间分发每个请求。与独占绑定相比,代理吸收了这种扰动:更新底层提供者时代理保持不变,因此消费者看不到其依赖的任何变化,也不会触发重载。

服务代理支撑三种能力:负载均衡、滚动更新与跨进程调用。

负载均衡。 当多个提供者共存时,代理按照可配置的策略(例如轮询、最少负载、按延迟加权)(第 69 页)

或消费者指定的显式目标在它们之间分发请求。由于提供者是普通组件,可以添加或移除它们以伸缩容量;每个提供者通过一个可逆效应向代理注册,因此卸载它会撤销注册,并自动将其从代理的路由集合中剔除。

滚动更新。 在运行时升级服务实现可归结为一次受控的提供者转换 [51, 52]。为执行该转换,新提供者作为额外的纤维被加载并向代理注册;一旦它变为激活(ACTIVE)状态,流量便从旧提供者逐渐迁移到新提供者(例如通过调整选择权重),旧提供者在不再承载进行中的请求后被卸载。这种提供者转换把传统上属于基础设施层面的操作(例如容器编排、蓝绿部署)变成了应用层的组合模式。

跨进程调用。 服务代理也可以跨越进程边界使用 [53]。每个进程承载自己的 Cordis 上下文及其本地提供者;一个协调组件将它们连接起来,把每个进程视为一个远程提供者。跨进程的服务访问由保持接口不变的 RPC 机制中介,使这种分布对消费者透明。一个需要注意的问题是:跨进程调用会带来延迟,并可能在半途失败,因此同步暴露它会阻塞调用方。因此,打算跨进程暴露的接口必须针对异步契约来设计。

6.3 访问控制与沙箱化

鉴于应用程序由独立组件组装而成,保障其安全需要两种互补机制:(1)约束组件可以访问哪些依赖;(2)将不可信代码与宿主环境沙箱化隔离。Cordis 通过依赖声明与拦截支持第一种机制;第二种机制则需要外部沙箱。

基于能力的访问控制。 依赖访问机制(第 5.1.4 节)已经构成了一种针对经代理中介属性的访问控制:组件只能访问它已声明的依赖;未声明的访问会引发错误。这在结构上类似于基于能力的安全模型 [54–56](capability-based security),其中权威来自对引用的持有,而非环境性权威(ambient authority)。inject 声明充当能力请求,上下文代理充当能力中介。由于这些请求是静态声明的,组件所需的经代理中介的完整能力集在它运行之前就已可知,这使得编排器可以在加载时审查和批准它们,而非在访问发生时才发现。

这种中介通过拦截机制推广到细粒度策略。访问控制元数据可以由上下文携带,或由组件声明(定义 30);当依赖被调用时,提供者会查阅它来决定某请求是否被允许。例如,文件系统依赖可以携带声明某组件可读写哪些路径的元数据,提供者会对每次调用对照元数据进行校验。由于这种拦截驻留在上下文上,而非任何一方的代码中,编排器可以调整它来约束任意组件对某依赖的访问,而无需修改提供者,例如授予社区组件只读的数据库访问权,而核心组件保留完整访问权。此外,由于拦截只影响依赖被调用的方式,而不影响依赖是否得到满足,它可以在运行时被安装、重新配置或移除,而不会触发任何重载或扰动依赖图。

第 70 页

不可信组件的沙箱化。 当组件的代码不可信时,语言层面的访问控制是不够的,因为能够访问宿主运行时的恶意组件可以直接触及底层对象,使这类检查形同虚设。沙箱化需要一条超出语言层面手段可达范围的执行边界,例如软件故障隔离 [57](software fault isolation)、独立的语言运行时、沙箱化进程或虚拟化容器 [58]。无论采用何种机制,不可信组件都在自己的沙箱化上下文中运行,并通过一座桥(bridge)到达宿主提供的依赖,这是对第 6.2 节跨进程调用的推广:同样的透明性论证使这种经桥访问与本地注入无法区分。在宿主一侧,桥是一个普通纤维,其能力可以被上述访问控制所削弱(attenuate)。

6.4 语言无关性与语言选择

尽管 Cordis 用 TypeScript 实现,上下文范式是与语言无关的:时空可组合性仅由其两个组合维度定义,因此可以在任何在这两个维度上都满足特定要求的语言中实现。我们依次分析各维度上的这些要求。

时间可组合性。 时间可组合性最基本的要求是闭包:一个可逆效应将动作与其逆变换配对,而该逆变换必须连同它所恢复的状态一起作为值被捕获,以便在拆除(teardown)时重放。除此之外,组件的代码及其加载的副作用必须能在运行时引入和收回。

语言如何满足这第二个要求取决于其执行模型。在托管运行时中,这采取程序化模块注册表的形式:已加载的模块可以从注册表中驱逐,并在不再被引用后被垃圾回收;例如 Node.js 就暴露了这样的注册表。[^6] 原生代码不暴露模块注册表,因此引入与收回采取显式动态链接与解链的形式(例如 Unix 上的 dlopen/dlclose,Windows 上的 LoadLibrary/FreeLibrary[59],即把目标代码加载进运行中的进程,之后再将之分离。WebAssembly 根据其嵌入者(embedder)选择其中一条路径:在托管嵌入者(如 JavaScript 宿主)下,模块实例由宿主的收集器回收;在原生嵌入者(如 Wasmtime)将其丢弃时被释放。在这些机制中,可逆效应模型把加载视为对上下文的一个效应,其逆变换撤销模块引入的符号、类型或处理程序的注册。

空间可组合性。 空间可组合性要求一种机制,让组件声明其依赖,并让运行时提供和注入这些依赖。这归结为一个依赖注入(DI)问题 [38],它在两个随语言而异的层面显现:依赖如何被类型化,以及依赖的访问如何被中介。

在类型层面,语言应提供一种方式,让开发者表达良类型的依赖访问。消费者通过从上下文读取键来获得共效应,因此上下文类型(第 3.2.1 节)必须记录每个键的共效应。Haskell 的类型类(typeclass)[60] 与 Rust 的 trait(特征)[61] 通过让提供者从其自身模块中以 instanceimpl 扩展上下文类型来实现这一点 [62]。TypeScript 的模块增强 [63] 同样让提供者模块将声明合并进上下文类型。

在运行时层面,依赖访问必须被动态中介:键背后的共效应会随着提供者的加载与卸载而变化,并且可能在不同……

[^6]: CommonJS 通过 require.cache 暴露模块缓存;ES 模块不提供公开的驱逐 API,尽管模块仍可通过引擎内部接口进行管理。

第 71 页

上下文。因此,语言需要一种对访问进行透明拦截的方式,使消费者的代码保持不变,例如通过 JavaScript 的 Proxy 对象 [64] 或 Python 的描述符协议(descriptor protocol,__get__[65]。若缺乏这样的原语,运行时反射 [66, 67] 可以动态地调解访问,但代价是类型安全性和开发者体验。

在这两个层面上,元编程设施同时提供类型化与调解。注解(annotations)[68] 与装饰器(decorators)将元数据附加到声明上,处理器将其展开为调解访问的访问器(accessor);编译期元编程(例如 Rust 过程宏、Scala 宏 [69]、Zig comptime)为每个依赖生成一个类型化声明以及这样一个访问器,从而无需通用的拦截原语。

6.5 相互依赖与组件粒度

在响应式共效应模型中,依赖环只会使涉及的组件永久保持非激活状态:给定两个组件 ,若 需要由 提供的键,而 需要由 提供的键,则二者的满足谓词都不可能为真。与并发系统中的死锁不同——死锁取决于调度,必须在发生时才能被检测到——这一条件仅凭依赖声明即可预测,因此运行时可以在组件加载时将其报告出来。

在实践中,大多数看似相互依赖的关系都可以分解为粒度更细的组件,从而消除环。考虑两个组件:一个服务器(提供网络接口)和一个访问控制器(实施授权策略)。这两个组件双向交互:访问控制器调解到达服务器的请求,而服务器暴露一个用于修改访问控制策略的端点。单体设计会让每个组件都依赖另一个。然而,这两个交互方向在逻辑上是相互独立的关注点。将它们分解可得到四个组件:server-core、access-control-core、request-mediation(依赖两个核心,以便对到达的请求应用访问控制)和 policy-management(依赖两个核心,以便通过服务器暴露策略修改)。通过这种方式,环被消除了,因为两个核心互不依赖;只有集成组件同时依赖二者。

这种分解原则上总是可行的,因为每一个双向交互都可以分解为独立的单向绑定,但它会增加组件的数量:在一般情况下,给定 个相互交互的组件,集成组件的数量可能随 呈二次方增长,因为每一对交互组件都可能需要为每个交互方向提供一个不同的组件。这不会影响正确性或运行时性能(组件是轻量的),而且更细的粒度可能是有益的:用户能够只加载他们需要的特定集成绑定,从而有效地提高系统的可组合性。然而,它可能影响开发者体验:更多的组件需要更多的配置、更多的命名,以及在理解依赖图时更多的认知开销。

缓解这种粒度成本是一个工程问题而非理论问题。实用的策略包括包打包(package bundling,即将相关的细粒度组件归并为一个可安装单元)、基于约定的接线(convention-based wiring,即自动连接名称或类型匹配某一模式的组件)以及脚手架工具(scaffold tooling,即根据声明式规范生成样板集成组件)。这些策略在保留无环模型的正式保证的同时,将编写负担降低到接近单体情形。

第 72 页

6.6 依赖类型化与版本管理

在形式模型中,依赖链接完全由键同一性确立:提供键 的组件满足任何在其依赖集中声明 的组件。类型族 保证单个编译单元内的类型级一致,但当组件被独立开发和构建时——这是组件生态系统中的常见情形——这一保证就会失效。这种失效导致两个不同的问题。

接口漂移(interface drift)。 提供者可能在各个版本之间修改与 关联的接口(增加字段、改变方法签名、更改行为契约),而针对较早接口编译的消费者仍继续声明相同的键 。该依赖在共效应层面得到满足(),但运行时值不再符合消费者的预期,从而导致类型错误、方法未找到(method-not-found)失败或静默的行为分歧 [70]

键冲突(key collision)。 两个独立开发的提供者可能使用相同的键名 来表示完全不相关的接口。由于仅凭键同一性就确立链接,期望某一提供者接口的消费者会在不做任何兼容性检查的情况下接受另一个提供者的值。与接口漂移不同——在接口漂移中提供者与消费者至少共享共同的谱系——键冲突在预期类型与实际类型之间没有任何关系,使得由此产生的失败不可预测且难以诊断。

这两个问题都指向同一个缺口:共效应模型只提供名义链接(按键名),而不提供版本化或结构化链接(按接口兼容性)[71]。我们讨论填补这一缺口的三种方法,从最依赖基础设施的到最与语言无关的。

键命名空间化(key namespacing)。 将键空间从 扩展为 (其中 标识定义接口的包),从构造上消除了键冲突:具有相同局部名称的独立开发的接口占据不同的键。这是最直接的解决方案,但耦合也最紧:它将包命名空间嵌入形式模型本身,使系统的键同一性依赖于外部的包注册表。

对等依赖(peer dependencies)。 一种耦合更轻的方式是通过宿主语言的包管理器声明版本约束 [72]。这是 Cordis 目前采用的方法。组件依赖在语义上就是对等依赖:组件不在内部捆绑其依赖,而是期望运行时上下文提供它们。支持对等依赖的包管理器(例如 npm)可以强制版本兼容性:如果提供某个键的包的版本落在消费者声明的对等范围之外,这种不兼容会在安装时被发现,而不是表现为运行时失败。然而,这种方法有两个局限:(1) 它依赖于提供者忠实地遵循语义化版本(semantic versioning),而这是一种无法强制执行的约定;(2) 包管理器通常将每个依赖解析为单一版本,这阻止了在同一应用程序内加载来自同一包的多个版本的组件。

结构化兼容(structural compatibility)。 一种完全与语言无关的方法将用兼容性谓词替换成员关系检查 ,该谓词验证提供者的实际接口在结构上包含消费者的预期。这类似于结构化子类型化 [73]:如果提供的接口是所需接口的子类型,则提供者满足消费者。挑战在于以与语言无关的方式定义该谓词:结构化兼容性对记录类型(宽度子类型化)是直截了当的,但对行为契约(例如前置/后置条件 [74]、效应规范 [22])则变得复杂,并且一旦参数多态引入有界量化 [75],就变得不可判定。

第 73 页

这三种方法针对问题的不同方面。设计一个统一的依赖模型,在保留共效应模型的动态组合保证的同时结合这些方法,仍然是一个开放问题。

6.7 与语言和操作系统的协同设计

第 6.4 节指出了宿主语言为上下文范式所必须提供的最低限度。本节讨论相反的问题:与这一范式协同设计的语言或操作系统,能在这最低限度之外提供什么。

与语言的协同设计。 围绕上下文范式设计的语言可以在两个方面优于库实现:它赋予上下文的语义,以及它赋予效应与共效应的原语。

这样的语言可以再次让上下文隐式化,同时保留第 3.3 节的上下文语义。命令式语言已经在隐式上下文中运行每一条语句,而那个单一的上下文既不跟踪效应,也不解析共效应。上下文范式则区分多个上下文:操作要么修改其运行所针对的上下文,要么从中派生出另一个上下文(定义 27)。就地实现(in-place realization)修改环境上下文,正如命令式语言所做的那样。派生实现(derived realization)则引入一个单独的上下文,语言必须为它提供一种构造。让上下文隐式化同时带来易用性(ergonomic)与安全性两方面的好处。

(1) 在库实现中,每个涉及效应或共效应的函数都将上下文作为普通参数或接收者,如第 5.1 节所述。当语言隐式提供上下文时,函数不再需要携带它。(2) 每个上下文都携带自己的生命周期状态和已提交视图(第 4.1 节)。库实现将上下文作为普通变量传递,因此组件可能通过闭包或全局变量错误地触及另一个组件的上下文。它在那里安装的效应会泄漏出其自身的生命周期,而它在那里读取的共效应也会逃逸出其依赖规范。让上下文隐式化可同时消除这两种问题。

这样的语言还可以让编译器了解效应与共效应。(1) 对于效应,效应迭代器(定义 51)在每一步都分配一个闭包,以保存逆变换以及它所恢复的状态。有了执行效应的语法,编译器可以为整个迭代生成单个状态机,并将这些逆变换保存在其帧(frame)中。(2) 对于共效应,共效应规范可以被纳入类型系统,这带来两个好处。首先,依赖环在编译期就被报告,而不是留给运行时(第 6.5 节)。其次,依赖可以按其类型的结构而非仅凭键同一性进行比较,正如行类型所做的那样 [28],这是对第 6.6 节的结构化兼容性的类型级支持。

与操作系统的协同设计。 第 1.2.3 节指出了一种动态组合的粗粒度替代方案:操作系统在进程粒度上提供时间可组合性,其上方的容器编排器在服务粒度上提供空间可组合性。与这一范式协同设计的操作系统将支持细粒度组合:让组件声明的共效应规范成为其可达范围的完整描述,并将其自身资源作为共效应提供。

这样的操作系统可以提供第 6.3 节推迟给语言外部机制的沙箱。它通过将组件限定在其声明的依赖范围内来实现这一点:在组件加载时提供这些依赖,并使其内部无法触及任何其他东西,正如 WebAssembly 模块在实例化时从它的宿主(embedder)处接收其导入一样 [76]。它

第 74 页

操作系统还可以把第 3.2.3 节的共效应隔离与拦截作为自身的能力来提供:为每个组件以不同的方式绑定键,并对其所供给的访问进行中介。这样的操作系统还可以把自身的资源作为共效应来提供。位于边界之外的资源之所以可逆,是因为运行时将每一次获取都记在发起获取的组件名下(第 6.1 节),而每个运行时各自保留一份记录。以共效应形式提供资源的操作系统只需保留一份这样的记录,因为它是资源的发放方,可以把资源归属到提出请求的组件。内存与文件描述符是最直接的候选,而且为了恢复而跟踪它们的工作已在内核接口层面完成 [77, 78]。此外,对于第 6.1 节只能拒绝或补偿的某些操作,操作系统可以使其可逆。以事务方式向持久存储执行写入的系统可以回滚该写入 [79],而建立在写时复制(copy-on-write)或不可变存储之上的系统则可以通过移动指针回到更早的状态 [80, 81]

7 相关工作

动态组合与若干成熟的研究领域相交叠。我们综述最相关的几条研究脉络,并逐一说明我们的贡献与它们之间的区别。

7.1 效应与共效应系统

第 2 节将效应与共效应作为我们工作的理论支柱作了回顾。我们首先定位如今在工业实践中常见的单子效应系统,然后综述三条把效应与共效应朝与 Cordis 相关的方向扩展的研究脉络:把代数效应重新诠释为能力(capability)、赋予效应可逆语义,以及在单一的分级纪律下统一效应与共效应。

单子效应系统(Monadic effect systems)。 有一类库把效应编码在既有通用语言的类型系统中,将效应表示为由运行时执行的单子值(monadic value)。Scala 中的 ZIO [82] 把计算建模为 ZIO[R,E,A],TypeScript 中的 Effect-TS [83] 则建模为 Effect<A,E,R>——一个其参数描述结果、类型化错误以及上下文必须提供的服务的泛型类型;fp-ts 库 [84] 通过基于 Reader 的单子变换器(monad transformer)编码同样的错误通道与需求通道。有两个特征将这些系统与 Cordis 区分开来。其一,这种跟踪是以单子嵌入为代价换来的:程序只有写在效应类型内部才能获得跟踪,而 Cordis 则是把效应跟踪作为覆盖在普通宿主代码之上的覆盖层。其二,需求通过解释来满足——即由已安装的、供给其操作的服务来满足;当该服务被撤回时,其操作所执行的效果仍然留存。Cordis 则相反,它为每个效应配对一个逆变换,并在提供者来来去去时重新解析需求(第 3.1 节、第 3.2 节)。

代数效应作为能力(Algebraic effects as capabilities)。 代数效应(第 2.1 节)使效应操作对类型系统可见。与我们的工作最接近的扩展是 Brachthäuser 等人的 Effekt 语言,它将效应类型重新诠释为能力 [85, 86]:效应类型表达的是计算需要从其上下文获得什么,而不是它可能产生什么副作用。这一视角与我们相同,都把上下文视为能力的中介者。Cordis 与 Effekt 在两个方面有所不同。(1)就目的而言,代数效应使效应可见是为了支持模块化解释,赋予同一个操作多种效应处理器语义;而 Cordis 使效应可见是为了支持跟踪与逆转,为每一个上下文变换配对一个逆变换。(2)就设定而言,Effekt 在类型层面静态地约束效应,默认采用基于作用域的推理——其中的能力是二等的、被限制在各自的词法作用域内,并通过装箱(boxing)恢复头等使用,即在类型中跟踪被捕获的能力以解除这一限制;而 Cordis 则在运行时约束效应,目标是在组件移除时完整地回收资源;第 6.7 节将讨论在这个意义上把上下文做成二等的语言会提供什么。

第 75 页

可逆效应语义(Reversible effect semantics)。 有一条平行的脉络赋予效应以可逆语义而非解释性语义。Heunen 等人 [87] 通过把 Hughes 的箭头(arrow)改造为 dagger 箭头与逆箭头,在可逆的框架中为副作用建模,从而刻画诸如序列化与可变存储这类其操作允许逆的效应。这是与我们的可逆效应最接近的形式化描述:两者都是为每个效应配对其撤销手段,而不是通过效应处理器来满足它。二者的区别在于可逆性所在的位置,以及它们对可逆性的要求程度。Heunen 等人工作在指称的、范畴论的框架中,在那里可逆性是一个全局性质:由于每个计算都是可逆的,可逆性由构造保证,逆是双侧的,并且可以从范畴结构中恢复出来。Cordis 在运行时跟踪逆变换,且对逆变换的要求更低:并不要求整个计算可逆,只要求每个原子效应允许一个单侧逆,该逆由调用者在应用点提供而非推导得出,任何复合效应的逆都可以通过复合由之推出(第 3.1 节)。

分级类型作为统一的效应与共效应(Graded types as unified effects and coeffects)。 Orchard 等人 [88] 提出把分级模态类型(graded modal type)作为同时涵盖效应推理(经由分级单子)与共效应推理(经由分级余单子)的总括性概念,并在 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 中,上下文是中介效应与共效应的 实体:激活运行组件的可逆效应,并由响应式共效应的满足所驱动(第 3.2 节),停用则将其全部逆转。COP 改变的是运行什么行为;Cordis 组合并逆转的是组件安装了什么效应与依赖。二者的区别是一种权衡。COP 把激活并入宿主语言的方法分派,以语言专用性为代价换来动态作用域的层范围;而 Cordis 作为与语言无关的覆盖层,在一个共享上下文上响应式地解析激活。

第 76 页

因此,Cordis 只能把 COP 的全局的、值驱动的部分表达为共效应:即在实现之间进行上下文相关的选择,而不能表达动态作用域的激活。

面向切面编程(Aspect-oriented programming)。 AOP [95, 96] 把横切关注点模块化为一个切面(aspect):一个对基程序中所选连接点进行量化的切入点(pointcut),以及在每个连接点处织入的通知(advice)。Cordis 解决的是同样的、否则会散布到各组件中的上下文行为问题,但其与切面类似的对应物是共效应:一个许多组件声明依赖的共享中介点,从而可以在不改动任何组件的情况下在那里重塑横切行为。这两种范式随后在两个轴向上有所不同。(1)声明与无感知:AOP 的切入点是无感知的、量化的,匹配任意代码本身并不知晓自己被通知的连接点;而 Cordis 把横切限定在各组件声明的共效应上,因此其触及范围恰好就是那层被声明的表面。这带来了确定性与可追溯性:应用编排器可以在配置层检查并管控什么横切了一个组件,而无需阅读或分析其源码;而 AOP 的关注点只有通过对其量化的切面才能解读。(2)生命周期集成:Cordis 中的横切变更由组件的效应承载,在组件卸载时被逆转,并响应式地传播给其依赖者,因此它是动态组合模型中的一步;动态 AOP 系统 [97, 98] 也可以在运行时织入与解织,但这是独立的操作,既不绑定组件的生命周期,也不会在被通知的代码之间触发重新解析。

7.3 时间可组合性

时间可组合性关注的是:在运行中的程序里替换或移除一个组件的同时,回收该组件所安装的效应。先前的各类方法按它们如何处理离开的组件的状态与效应而划分:把状态前向携带给后继版本、通过开发者编写的清理代码回收效应、在预先固定的作用域内自动逆转效应,或者从运行时通过拦截接口所积累的记录中回收资源。

有状态前向迁移(Stateful forward migration)。 有一大类系统通过在版本之间前向携带状态,在不停机的情况下替换运行中程序里的组件。它们都遵循同样的时机纪律:组件只有在到达安全的、无交互的点之后才可被替换。Kramer 与 Magee 把这一准则确立为静止(quiescence)[51],Vandewoude 等人后来将其放宽为干扰更小的宁静(tranquility)[52];我们的滚动更新模式(第 6.2 节)通过在卸载提供者之前排空在途请求来强制执行这一准则。动态软件更新(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.hotimport.meta.hot API 把状态前向传递。与 Cordis 的模块替换(第 5.2 节)相比,这些方法迁移内存状态的方式更为优雅:Cordis 逆转旧组件的被跟踪效应,并让新组件从全新状态重新应用其效应,因此组件自身的内存状态无法在一次……

第 77 页

……除非被置于生命周期更长的依赖之中,否则无法重载;而将 DSU 式的前向迁移(forward migration)叠加在可逆效应之上则是未来工作。不过,Cordis 的方法在两个方面更具一般性:它不需要 DSU 和热模块替换(HMR)所需的那种手写迁移函数,而且它支持完全卸载一个组件并回收其资源,而不仅仅是在原地更新一个组件。

开发者编写的恢复(Developer-authored recovery)。 第二族通过开发者手写的清理或补偿逻辑来恢复组件的效应。插件生命周期约定(例如 OSGi [50]、Eclipse 的扩展点、IntelliJ 和 VSCode)将清理委托给开发者编写的卸载回调;命令模式 [103] 将一个操作与其撤销方法封装在一起,用于撤销/重做栈;saga 模型 [49] 将长期事务结构化为一组步骤,每一步都配有一个补偿动作;代数效应处理器可以附加在拆除(teardown)时运行的终结器 [104];事件溯源 [105] 通过追加补偿事件来撤回状态,而根本不执行逆变换。在所有这些机制中,逆变换都是一项未强制执行的义务,与操作本身解耦,因此一个被遗忘的逆变换会悄然泄漏资源(如第 1.2.1 节的经验研究所记载)。React 的 useEffect 钩子 [106] 最接近在结构上把效应与其逆变换配对:它返回一个清理函数,运行时在每次重新执行之前以及组件卸载(unmount)时调用该函数。其不足之处在于可组合性:钩子只能在组件或其他钩子的顶层调用,绝不能出现在条件、循环或嵌套函数内部,而且其效应体既不能接受异步函数,也不能接受迭代器。因此,效应无法由其他效应组装而成,也无法与控制流交错,从而无从推导出复合逆变换。Cordis 的效应没有此类限制:它们是普通操作,可以自由组合并异步运行,而且只有每个原子效应才需要手写逆变换,任何复合效应的逆变换都由组合推导而来,因此组装已有效应完全不需要编写逆变换。这种将每个效应与其逆变换进行结构配对的机制,使完整恢复成为系统的不变式,而非开发者自律的问题。

静态作用域的逆转(Statically scoped reversal)。 第三族自动地、通过构造逆转效应,但将逆转限制在预先固定的作用域内。软件事务内存 [107, 108](源自硬件事务内存 [109])记录一份读写日志,使一组内存操作要么提交、要么中止,将内存回滚到事务之前的状态。可逆计算(reversible computing),从 Landauer 和 Bennett 的热力学分析 [110, 111] 到 Janus [112] 等可逆语言,更进一步使整个计算的每一步都全局可逆。可逆进程演算将回溯直接构建进语义本身:RCCS [113] 为每个进程携带一份记忆,并允许在其所导向的过去因果等价时将该步收回;Phillips 和 Ulidowski [114] 为 CCS、ACP 和 CSP 统一导出了可逆算子,同时保持它们的前向操作语义。它们的因果一致性判据是 Cordis 的恢复所遵循顺序的并发对应物——累加器按后进先出(LIFO)的顺序应用组件自身的逆变换,而第 4.3.1 节的守卫则将提供者的撤回推迟到其消费者停用之后(定理 63)。然而,其触及范围由语义固定:所执行的每个动作都保持可撤销;而 Cordis 组件为每个原子效应提供逆变换,其累加器将上下文带回到其组合开始之处。线性类型 [115]、RAII(资源获取即初始化)[4] 和 Rust 的所有权系统 [61] 将资源的释放绑定到词法区域。每一种都在静态上固定了逆转的作用域与触及范围;相比之下,Cordis 不预先固定任何此类作用域:它在组件的整个生命周期内逆转任意的上下文操作,并将词法资源管理视为互补手段,适用于单个组件内部的局部资源。

第 78 页

插入式回收(Interposed reclamation)。 第四族在组件本身不提供逆变换的情况下回收组件所获取的资源,方法是在运行时控制的接口处记录其获取行为。Nooks [77] 包装跨越 Linux 内核与其可加载扩展之间边界的每一次调用,使扩展所触及的内核对象都经过一个对象跟踪器,其记录告诉恢复管理器在扩展失败时应释放什么;影子驱动(shadow drivers)[78] 从另一侧截取同样的调用,记录决定驱动状态的请求与配置,以便重新启动的实例可以恢复到该状态。Akeso [116] 则通过编译器插桩获得记录,将内核执行划分为可嵌套的恢复域,记录其状态变化和跨线程依赖,并在回滚故障请求时连同依赖它的每一个域一起回滚。因此,回收来自运行时维护的记录,而非开发者记得要编写的清理代码,这使得该族成为可逆效应最接近的系统级先例。它在词汇和触及范围上与 Cordis 有所不同。平台固定了可以记录的内容——无论是按内核对象类型划分的释放代码、每类驱动一个影子,还是每个被插桩的分配器一个逆变换——因此组件只能持有平台已经知道如何释放的资源;而 Cordis 组件则引入自己的效应,并为每个原子效应提供一个逆变换(第 3.1 节)。同样,回收被一个已提交的请求或同一扩展的重启所限定,而 Cordis 在组件的整个生命周期内逆转,并将移除传播给其依赖者,后者依次释放它们自己的效应(第 3.2 节)。

7.4 空间可组合性

空间可组合性关注组件对其他组件的依赖如何被声明和绑定。先前的机制按绑定对变化的响应方式来划分:在初始化时一次性接线依赖、对整体组件的可用性作出反应、或者以单个值的粒度传播变化。

初始化时的依赖接线(Initialization-time dependency wiring)。 两种既有机制在初始化时将组件接线在一起。依赖注入框架 [38](例如 Spring [117]、Guice、Angular、Inversify)在初始化时将依赖注入组件,UI 框架上下文(例如 Vue.js 的 provide/inject 和 React 的 Context API)沿组件树传递依赖。有些支持动态作用域(例如 Spring 的 prototype/request 作用域、Angular 的分层注入器),但两者都不会响应式地重新解析:当提供者在运行时被替换或移除时,既有依赖者既不会被停用也不会被重新初始化,而且两者都不提供我们组件状态机所提供的那种生命周期管理。Cordis 的响应式共效应(第 3.2 节)提供了这一点:每当满足谓词(satisfaction predicate)发生变化时,通知机制就会触发生命周期转换。

可用性响应式组件模型(Availability-reactive component models)。 与我们的响应式共效应最接近的先例是对服务可用性作出反应。OSGi 的声明式服务(Declarative Services)和 iPOJO [118, 119] 让组件声明提供与所需的服务,运行时在服务出现和消失时自动激活和停用它们;iPOJO 的 Gravity 项目 [119] 明确以对不断变化的服务可用性进行自主运行时适配为目标,其 provide/require 模型直接预示了 Cordis 的 ctx.provide/ctx.get 模式。R-OSGi [53] 通过 RPC 将同样的抽象透明地扩展到分布式环境,将网络故障映射为服务撤回事件——这是第 6.2 节作为 Cordis 模型扩展所讨论的模式。所有这些系统都通过停用回调来恢复,这有两个方面的局限。首先,该回调是手写的,因此资源安全依赖于开发者自律,一个被遗漏的回调会悄然泄漏资源。其次,该回调是同步的:如果拆除需要与正在离开的依赖进行异步交换,这些框架不提供等待它的协议,迫使

第 79 页

对可能已经过时的引用进行阻塞等待。Cordis 的响应式共效应弥补了这两处空白:停用会撤销依赖者累积的效应,而其惯性的 状态(第 4.3.3 节)会在针对进一步变更采取行动之前,将异步拆除运行至完成。

值级响应性。 函数式响应式编程(functional reactive programming,FRP)[120] 及其现代形态(例如 SolidJS 中的信号 [121, 122]、Vue 的响应式系统、Angular Signals)以值级粒度传播变化:当某个信号发生变化时,派生计算会被同步地或在调度器(scheduler)[123] 的调度下重新求值。Cordis 的响应式共效应作用于组件粒度,增加了值级传播所无法建模的异步生命周期语义。在一致性方面,同样的粒度差异又以另一种方式起作用:在同一轮次(turn)内、按依赖图所确定的顺序进行传播,使 FRP 能够要求任何派生计算都不得读取更新输入与陈旧输入的混合体,这就是无毛刺性(glitch freedom)[124];而 Cordis 没有与轮次对应的概念——编排动作逐一到达——并且仅保证没有任何单个转换跨越其共效应的两次解析(定理 64)。两者互补而非相互竞争:Cordis 的共效应本身可以携带响应式值,组件仅在其实际消费的部分上更新,从而将组件级响应性细化为同时跨越两个层级的更细粒度的响应式共效应。

8 结论

我们通过将经典的效应与共效应概念提升为运行时机制,为动态组合提出了一个形式化基础。可逆效应解决了局部时间可组合性:每个上下文变换都携带一个由运行时跟踪的逆变换,且跟踪与恢复都保持复合,因此组件被移除时上下文得以恢复。响应式共效应解决了局部空间可组合性:每当上下文发生变化时,组件都会依据其共效应规范收到通知,每次变化被分类为激活、停用或中性,其中共效应隔离改变声明的键所解析到的内容,共效应拦截改变绑定的使用方式。我们将效应上下文与共效应上下文统一为单一的上下文类型,其中共效应上的观察等价为效应提供了独立性,从而构成了一种面向时空可组合性的编程范式。将这些机制组合为组件的概念,便得到动态组合演算,其元理论将时空可组合性从单个组件传递到由交错组件构成的整个系统。我们将这一范式实现为 Cordis 元框架:核心库提供效应跟踪与共效应解析,此外还有一个带配置协调与热模块替换的声明式组件加载器。Koishi 案例研究在一个拥有 4000 多个社区插件的生产系统中验证了 Cordis 的设计。

在人工策划的插件生态之外,未来验证的一个有吸引力的方向是自演化智能体框架(第 1.2.2 节),即 AI 智能体在几乎无需人工监督的情况下持续生成并替换自身的框架组件。在这样的场景中应用 Cordis,将验证快速组件替换下完全恢复的时间性保证,以及频繁拓扑变化下依赖协调的空间性保证。这种验证将证明该范式作为可恢复、可协调、持续自演化之基础,在智能体框架及其他自治系统中的适用性。

参考文献

本部分为参考文献,按原文保留:作者、标题、出处、链接等均不翻译,编号与原文一致,便于对照检索。本段共 124 条文献,编号 [1][124] 顺序完整、无重复、无遗漏。

[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. AddisonWesley, 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-longrunning-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. 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 contextdependence,” 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. (M. Elnozahy, L. Alvisi, Y.-M. Wang, and D. B. Johnson, “A Survey of RollbackRecovery 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 objectoriented 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.

附录 核心术语对照表

英文 中文 备注
temporal composability 时间可组合性
spatial composability 空间可组合性
spatiotemporal composability 时空可组合性
dynamic composition 动态组合
static composition 静态组合
component 组件
fiber 纤维 组件的运行时实例化(首次出现可注:即组件的实例化载体)
effect 效应
coeffect 共效应
revertible effects 可逆效应
reactive coeffects 响应式共效应
context 上下文
context type 上下文类型
effect context 效应上下文
coeffect context 共效应上下文
accumulator 累加器
inverse 逆变换(简称"逆")
twisted composition 扭转复合
twisted composition monoid 扭转复合幺半群
monoid 幺半群
registry 注册表 状态中按名存放纤维的结构
lifecycle 生命周期
lifecycle state 生命周期状态
transition 转换 状态机中的状态转换
activation / deactivate 激活 / 停用
teardown 拆除 组件销毁时的清理过程
withdrawal 撤回 提供项的撤回
provision 提供项 组件向环境提供的共效应键集合
installed / failed 已安装 / 已失败 纤维的状态
quiescence (quiet) 静止(quiet 译为"静止")
metatheory 元理论
preservation 保持 如 type preservation 译为"类型保持"
progress 进展性 如 progress and preservation 译为"进展性与保持"
confluence 合流性
observational equivalence 观察等价
independence of effects 效应的独立性
isolation 隔离
interception 拦截
realm 领域 realm table 译为"领域表"
effect iterator 效应迭代器
committed view 已提交视图
parent 父纤维 parent pointer 译为"父指针"
retirement flag 退役标志 O-Retire 译为"退役"
reload / unload 重载 / 卸载
iteration 迭代
asynchrony 异步
failure 失败
guard 守卫 规则前提中的守卫条件
inertia 惯性 fiber.inertia 译为"惯性句柄"
calculus 演算
base calculus 基础演算
typing context 类型上下文
reify 具体化 将上下文具体化为头等实体
first-class 头等
side effects 副作用
meta-framework 元框架
effect tracking 效应跟踪
coeffect resolution 共效应解析
core library 核心库
component loader 组件加载器
declarative 声明式
configuration reconciliation 配置协调
hot module replacement 热模块替换
plugin 插件
agent harness 智能体框架
extension host 扩展宿主
activate function 激活函数
deactivate hook 停用钩子
monoid homomorphism 幺半群同态
commutes / commutative diagram 可交换 / 交换图
proof 证明
theorem / lemma / definition 定理 / 引理 / 定义
proposition / corollary 命题 / 推论
remark / example 注记 / 例
equivalence relation 等价关系
quotient
partial function 偏函数
projection 投影
tuple 元组
unit 单位元
closure / associativity / identity 封闭性 / 结合律 / 恒等(性)
lift 提升
operational semantics 操作语义
soundness / completeness 可靠性 / 完备性
trace 轨迹
interleaved 交错的
episode 时段 纤维的一段活跃区间
monotone 单调的
LIFO 后进先出(LIFO)
key / binding 键 / 绑定
provider / consumer / dependent 提供者 / 消费者 / 依赖者
dependency 依赖
dependency topology 依赖拓扑
service 服务
multiplexing 复用
sandboxing 沙箱化
access control 访问控制
system boundary 系统边界
mutual dependencies 相互依赖
component granularity 组件粒度
dependency typing 依赖类型化
versioning 版本管理
co-design 协同设计
lexical scoping 词法作用域
module import resolution 模块导入解析
RAII RAII(资源获取即初始化)
store 存储 ctx[@@store] 中的 store
realm symbol 领域符号
proxy 代理
trap 陷阱(trap) get/set trap 译为"获取/设置陷阱"
disposer 释放器 运行逆变换的清理函数
callback 回调
refresh 刷新
target 目标 fiber.target
orchestration / orchestrator 编排 / 编排器
config 配置
metadata 元数据