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）可能性高；论文成型度高、metatheory 完整、有 production case study；最终 venue 待考
Section 数 8（含引言 / 预备 / 形式化 / calculus / 实现 / 讨论 / 相关 / 结论）
实现 Cordis 框架（TypeScript）——基于 github.com/cordiverse/cordis
案例 Koishi 聊天机器人框架（4000+ 插件，4 年生产）

章节结构

  1. Introduction（§1）——动机：插件系统、自演化 agent harness；定义时空可组合性。
  2. Preliminaries（§2）——Effect system（Moggi、Plotkin-Power algebraic effects + 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 rules）；transitions in progress（withdrawal / iteration / asynchrony / failure）；metatheory（preservation、temporal composability、spatial composability、progress、confluence）。
  5. Implementation & Case Study（§5）——core library、component loader、HMR 引擎；Koishi 案例。
  6. Discussion（§6）——system boundary、service multiplexing、access control、language independence、mutual dependencies、dependency typing & versioning、co-design with OS。
  7. Related Work（§7）——effect/coeffect systems、programming paradigms、temporal composability、spatial composability。
  8. Conclusion（§8）——总结 + future validation 方向（self-evolving agent harness）。

6 大贡献（§1.3）

  1. Revertible effects——effect 携带 inverse，runtime 追踪累加器。
  2. Reactive coeffects——声明式 specification + 变化时三态通知。
  3. Unified context type——effect context + coeeffect 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 终态正确

引用本页