coeffect-systemreactivedependency-injectiondynamic-compositiontype-theory

Reactive Coeffects (反应式上涵)

在 Spatiotemporal Composability (时空可组合性 范式中，组件声明它对环境的需求 (coeffect specification)；每当 context 变化（依赖出现、消失、改换身份），runtime 把变化通知给声明该依赖的组件，并按 activating / deactivating / neutral 三态分类。Shi, Zhang & Cui (2026) Section 3.2 的核心构造。

形式化定义

Coeffect Context

\Sigma = K \xrightarrow{\mathrm{fin}} V_k 键 K 到值类型 V_k 的有限偏函数——coeffect 表的并，即当前所有 active fiber 安装的依赖集合。Component 持有： - specification d \subseteq K：声明的依赖键。 - provision p \subseteq K：可提供的键。 ### Specification 与 Notification Definition 24 对每个 k，附带一组操作 \mathcal{A}_k（含 forward map + yielded inverse）。值 v \in V_k 配等价关系 \simeq_k（"观测等价"），由操作确定。 Definition 25 组件声明 specification d : \mathcal{D}_\Sigma，是 key 的多集（带 allow-optional 标记）。 Definition 26 通知——给定旧/新 coeffect 状态 \sigma, \sigma'，对每个声明的 key k \in d，判定： - activating：\sigma \not\models d 且 \sigma' \models d（新依赖就绪） - deactivating：\sigma \models d 且 \sigma' \not\models d（依赖消失） - neutral：其余（依赖提供方变了但仍满足） ### Satisfaction Predicate \sigma \models d \;:\Longleftrightarrow\; \forall k \in d.\, k \in \mathrm{dom}(\sigma)

Isolation 与 Interception

  • Isolation（Definition 28）：每个 fiber 的 context 可声明 isolate: { key: realm } 映射——同一 key 在不同 realm 由不同 fiber 提供，互不干扰。
  • Interception（Definition 30）：coeffect 携带 metadata，consumer 调用时 provider 查 metadata 决定请求是否允许（capability-based 访问控制）。

与 classical coeffect 体系的关系

Classical coeffect (Petricek, Uustalu-Vene) Reactive coeffect
描述 类型 / 类型上下文标注 运行时 specification + 通知
推理时机 编译期 运行时
依赖变化 编译期 fixed 三态通知（activating / deactivating / neutral）
隔离 词法作用域 Realm table（runtime override）
拦截 编译期类型检查 Provider 查 context metadata

运行时三态

  • activating：dependency 出现 → 组件从 Inactive 转 Reloading → Active。
  • deactivating：dependency 消失 → 组件转 Unloading → 等 relied_n(γ) 守卫释放 → L-Unload（累加器撤销 effect）→ Inactive。
  • neutral：provider 换了但语义等价（idempotent set 注册）→ 不触发 reload。

relied_n(γ)（Definition 50）：\exists m, k.\, m \neq n \wedge \mathrm{installed}_m(\gamma) \wedge \omega_m(k) = n——n 还有别的已安装 fiber 仍把它当 provider，则 n 不能立即撤销。

在 Cordis 中的实现

class MyConsumer extends Context {
  // 声明依赖
  inject = ['db', 'logger']
  constructor(ctx: Context) {
    super(ctx, 'my-consumer')
    // ctx['db'] 走 Algorithm 6：沿 fiber 链向上 walk 找 committed view
    // 命中 → 返回；inject 但未 commit → INACTIVE_ACCESS
    // 走到 root 仍未声明 → UNDECLARED_ACCESS
  }
}

Algorithm 6 Proxy 解析——resolve(ctx, key)：

  1. 当前 fiber 命中 committed view → 返回。
  2. 命中 inject 但未 commit → 抛 INACTIVE_ACCESS。
  3. 走到 root 仍无声明 → 抛 UNDECLARED_ACCESS。
  4. 否则向 parent.fiber 走一步。

案例：Koishi 切换数据库 backend

Koishi 切换数据库后端时：所有声明 inject = ['db'] 的 plugin 自动重新激活；未声明 db 的 plugin 保持不变。plugin 作者之间不需协调——只需对 coeffect key 名字达成一致。

与 quant 系统的潜在接口

  • 因子 / datafeed 切换：把数据源声明为 coeffect key，切换时只有声明该 key 的策略重激活。
  • 风险模型版本切换：将 risk-model 版本作为 realm，调用方透明切换。
  • Agent-trading 工具依赖：模型生成的 tool 之间用 coeffect key 协调，无需中心编排器。

详见 Spatiotemporal Composability (时空可组合性 页中标注的迁移接口。

引用本页