programming-paradigmeffect-systemcoeffect-systemcontextdynamic-composition

Context Paradigm (上下文范式)

把 effect context 与 coeffect context 统一为单一上下文类型，是 Shi, Zhang & Cui (2026) Section 3.3 提出的编程范式：所有 effect 与 coeffect 都经由显式 context 参数传递，每条 effect 携带 inverse、每个 coeffect 有声明 specification；组合性与可逆性从开发者纪律升格为结构性保证。Cordis 框架 即此范式的实现。

统一类型的构造

Unified Context

\Gamma \text{ 同时携带 } \partial\Gamma \text{ (effect 部分) 与 } \Sigma \text{ (coeffect 部分)} Definition 32 一个 context \gamma 包含： - state projection \sigma_\gamma——键值表形式的 coeffect 部分。 - accumulator——effect 部分的 LIFO 累加器（见 Revertible Effects (可撤销效应)）。 ### Observational Equivalence 两个 context state \gamma, \gamma' 等价，当且仅当： \gamma \simeq \gamma' \;:\Longleftrightarrow\; \sigma_\gamma \simeq_{\sigma} \sigma_{\gamma'}

其中 coeffect 投影的等价逐键由 \simeq_k 决定（Definition 33）。heap 布局、生成的名字等"无键绑定的部分"被遗忘——这是为什么 Theorem 7 能"up to \simeq"读。

Lemma 35：indistinguishability \approx_{\mathcal{A}} 是 \mathcal{A} 上最粗等价——所有操作 respect 的等价都包含其中。

Independence 供应

Theorem 42：若两个 effect 函数 e_1, e_2 涉及的 key 上操作可交换（Definition 39），则 e_1, e_2 独立——这是 Revertible Effects (可撤销效应) 累加器能任意顺序撤销所需的结构性条件。

"独立" = transformation 复合 monoid commutation + 各自 outcome 不被对方扰动。

与既有范式的比较（Section 3.3.3）

显式 state threading（pure FP） 隐式 mutation（imperative/OOP） Context Paradigm
Effect 表示 State monad 等显式 threading 隐式（useEffect 等隐藏 runtime state） 显式 context 参数 + tracked inverse
Coeffect 表示 Reader monad 等 Service locator（Spring getBean） 显式 inject + proxy 调解
推理性 强（types reflect effects） 弱（必须读实现传递闭包） 强（context 类型记录 key → 操作）
人体工学 差（每个函数都要 thread state） 好（直接调用） 好（Proxy 透明）
可逆性 需手动实现 需手动管理 结构保证（自动 LIFO 撤销）
依赖变化 编译期 fixed ad hoc 检测 三态 reactive 通知

React useEffect 的对照

// React: 注册 effect 但 target 和注册机制不显式
useEffect(() => {
  const conn = openConnection(url)
  return () => conn.close()  // inverse 手写
}, [url])
  • 副作用目标（DOM 节点、订阅）不作为参数出现。
  • 撤销是手写、隐式于 hook 闭包。
// Cordis: 显式 + runtime 追踪
ctx.effect(() => {
  const conn = openConnection(url)
  ctx.set('db', conn)
  return () => conn.close()  // runtime 自动 LIFO 调用
})
  • inverse 显式返回；runtime 追踪累加器。
  • 卸载时结构性撤销，无需开发者纪律。

范式带来的结构性保证

正确性目标 在 Context Paradigm 中的来源
卸载时 effect 完整撤销 Revertible effects + 累加器
依赖变化时一致性重 wiring Reactive coeffects + 三态通知
死锁避免 Theorem 66：relied_n(γ) 守卫必定释放
调度无关性 Confluence（Theorem 65）
跨作者独立组件协调 coeffect key 作为唯一定约

量化迁移提示

  • 任何有副作用的子模块（开仓、下单、订阅 feed、写缓存）都可用 (f, g) pair 建模。
  • 任何跨子模块依赖（数据源、配置、风险模型）都可用 coeffect key 声明。
  • 这套范式自动获得"安全卸载 + 一致重 wiring"两条结构性保证——对长寿命、模块化、自动演化的策略系统有直接借鉴价值。

引用本页