paperprogramming-languagestype-theoryeffect-systemcoeffect-systemdynamic-compositioncordis

Shi, Zhang & Cui (2026) — A Programming Paradigm for Spatiotemporal Composability

大白话：这是一篇 88 页的编程语言 / 类型论论文，把经典的 effect（效应）与 coeffect（上涵）体系从「编译期结构」提升为运行时机制，提出时空可组合性 (spatiotemporal composability) 范式，并实现为 Cordis 框架 元框架。已在 Koishi 聊天机器人框架（4000+ 社区插件）生产环境验证。

论文信息

项 内容
标题 A Programming Paradigm for Spatiotemporal Composability
作者 Yifan Shi (PKU), Wei Zhang (PKU), Tianyi Cui (DeepSeek-AI)
页数 88
公开状态 内部/工作论文（PDF 头部无 arXiv id / DOI；获取自作者本人）
venue 推断：投 PL 会议（ICFP / POPL / OOPSLA）可能性高；论文成型度高、元理论完整、有生产案例研究；最终 venue 待考
章节数 8（含引言 / 预备 / 形式化 / calculus / 实现 / 讨论 / 相关 / 结论）
实现 Cordis 框架（TypeScript）——基于 github.com/cordiverse/cordis
案例 Koishi 聊天机器人框架（4000+ 插件，4 年生产）

章节结构

  1. Introduction（§1）——动机：插件系统、自演化 agent harness；定义时空可组合性。
  2. Preliminaries（§2）——Effect system（Moggi、Plotkin-Power 代数效应 + handlers）、Coeffect system（Petricek comonadic、graded coeffects）。
  3. Revertible Effects & Reactive Coeffects（§3）——核心形式化：effect context / track / independence；coeffect context / specification / notification / isolation / interception；context paradigm。
  4. A Calculus of Dynamic Composition（§4）——Component 与 fiber；base calculus（5 条规则）；进展中的转换（withdrawal / iteration / asynchrony / failure）；元理论（preservation、temporal composability、spatial composability、progress、confluence）。
  5. Implementation & Case Study（§5）——核心库、组件加载器、HMR 引擎；Koishi 案例。
  6. Discussion（§6）——系统边界、服务复用、访问控制、语言无关性、相互依赖、依赖类型与版本管理、与操作系统协同设计。
  7. Related Work（§7）——effect/coeffect 体系、编程范式、temporal composability、spatial composability。
  8. Conclusion（§8）——总结 + 未来验证方向（self-evolving agent harness）。

6 大贡献（§1.3）

  1. Revertible effects（可撤销效应）——效应携带逆操作，运行时追踪累加器。
  2. Reactive coeffects（反应式上涵）——声明式 specification + 变化时三态通知。
  3. Unified context type（统一上下文类型）——effect context + coeffect context 合二为一。
  4. Calculus of dynamic composition（动态组合演算）——组件形式化 + 操作语义 + 全局可组合性元理论。
  5. Cordis——元框架实现。
  6. Koishi case study（案例研究）——4000+ 插件的四年生产验证。

关键定理

编号 名称 含义
Theorem 4 pr1 ∘ track = f ∘ pr1 effect 正确传递 state 投影
Theorem 5 track 是 monoid homomorphism inverse 复合的结构性
Theorem 7 Soundness invariant 累加器恢复到初始 state
Theorem 16 LIFO 累加器 累加器按 LIFO 撤销
Theorem 40 distinct-key independence 不同 key 上的操作独立
Theorem 42 commutative-key independence 同一 key 上操作可交换 ⟹ 独立
Theorem 63 coeffect 排序 依赖者先激活，后撤销
Theorem 64 no transition straddles 单次 transition 不跨两个 resolution
Theorem 65 confluence 不同调度顺序都归到同一 quiescent state
Theorem 66 guard release relied 守卫必定释放（无死锁）
Theorem 73 quiescent is function of final config 增量 reconciliation 终态正确

引用本页