本文介绍了一种时空可组合性的编程范式，以应对现代软件系统中动态组合的挑战。它确定了两个正交维度：时间可组合性，确保组件移除时其效果能够完全且安全地逆转；以及空间可组合性，管理组件间结构化的依赖解析。以 Visual Studio Code 为案例研究，作者展示了当前插件系统的局限性，其中动态卸载和扩展间依赖支持不足。他们提出了一个基于可逆效应和反应性共效应的形式化基础，统一为单一上下文类型，并提出了一个具有操作语义的动态组合演算。这些思想在 Cordis 中实现，这是一个提供效应跟踪、共效应解析和热模块替换的元框架。论文总结道，这一范式实现了细粒度、安全的动态组合，克服了粗粒度进程或容器重启的成本，并适用于自修改代理框架及其他动态架构。
This article introduces a programming paradigm for spatiotemporal composability, addressing the challenges of dynamic composition in modern software systems. It identifies two orthogonal dimensions: temporal composability, which ensures complete and safe reversal of a component's effects upon removal, and spatial composability, which manages structured dependency resolution among components. Using Visual Studio Code as a case study, the authors demonstrate limitations in current plugin systems, where dynamic unloading and inter-extension dependencies are poorly supported. They propose a formal foundation based on revertible effects and reactive coeffects, unified into a single context type, and present a calculus for dynamic composition with operational semantics. The ideas are implemented in Cordis, a meta-framework providing effect tracking, coeffect resolution, and hot module replacement. The paper concludes that this paradigm enables fine-grained, safe dynamic composition, overcoming the costs of coarse-grained process or container restarts, and is applicable to self-modifying agent harnesses and other dynamic architectures.
核心贡献 · Key contributions
提出了一种时空可组合性的编程范式，将可逆效应与反应性共效应统一为单一上下文类型。 Introduces a programming paradigm for spatiotemporal composability, unifying revertible effects and reactive coeffects into a single context type.
形式化了带有显式逆的可逆效应，使得组件移除时能够完全且安全地逆转其效应。 Formalizes revertible effects with explicit inverses, enabling complete and safe reversal of component effects upon removal.
将反应性共效应形式化为依赖规范，对上下文变化进行分类以驱动激活与停用。 Formalizes reactive coeffects as dependency specifications, classifying context changes to drive activation and deactivation.
提供了具有操作语义的动态组合演算，确保交错组件间的可组合性。 Provides a calculus of dynamic composition with operational semantics, ensuring composability across interleaved components.
在 Cordis 中实现了该范式，这是一个具有效应追踪、共效应解析和热模块替换的元框架。 Implements the paradigm in Cordis, a meta-framework with effect tracking, coeffect resolution, and hot module replacement.
展示了当前插件系统（如 VSCode）的局限性，并说明了该范式在自修改智能体框架中的适用性。 Demonstrates limitations of current plugin systems (e.g., VSCode) and applicability to self-modifying agent harnesses.
局限 · Limitations
形式模型假设效应是可逆的，但对于 I/O 或外部副作用等不可逆操作可能不成立。 The formal model assumes effects are revertible, which may not hold for irreversible operations like I/O or external side effects.
任意顺序逆转需要效应独立性，这在实践中可能难以保证。 Independence of effects is required for arbitrary-order reversal, which may be difficult to guarantee in practice.
实现 Cordis 是一个元框架，其性能开销和可扩展性尚未评估。 The implementation Cordis is a meta-framework; its performance overhead and scalability are not evaluated.
该范式依赖运行时追踪，可能引入复杂性和静态系统中不存在的潜在运行时错误。 The paradigm relies on runtime tracking, which may introduce complexity and potential runtime errors not present in static systems.
案例研究集中于 VSCode，对其他插件系统或动态架构的适用性可能有所不同。 The case study focuses on VSCode; applicability to other plugin systems or dynamic architectures may vary.
论文章节 · Sections（共 61）
1 引言1 Introduction
1.1 可组合性的维度1.1 Dimensions of Composability
1.2.1 插件系统1.2.1 Plugin Systems
1.2.2 自进化智能体利用1.2.2 Self-Evolving Agent Harnesses
1.2.3 粗粒度变通方案1.2.3 The Coarse-Grained Workaround
1.3 贡献1.3 Contributions
2 预备知识2 Preliminaries
2.1 效应2.1 Effects
2.2 余效应2.2 Coeffects
2.3 与动态可组合性的关系2.3 Relationship to Dynamic Composability
3 可逆效应与反应性共效应3 Revertible Effects and Reactive Coeffects
3.1 可逆效应3.1 Revertible Effects
3.1.1 效应上下文3.1.1 Effect Context
3.1.2 可逆效应函数3.1.2 Revertible Effect Functions
3.1.3 效应的独立性3.1.3 Independence of Effects
3.2 反应式协效应3.2 Reactive Coeffects
3.2.1 余效应上下文3.2.1 Coeffect Context
3.2.2 规范与通知3.2.2 Specification and Notification
3.2.3 隔离与拦截3.2.3 Isolation and Interception
3.3 上下文范式3.3 The Context Paradigm
3.3.1 统一上下文3.3.1 Unified Context
3.3.2 观测等价性3.3.2 Observational Equivalence
3.3.3 情境范式定位3.3.3 Situating the Context Paradigm
4 动态组合的演算4 A Calculus of Dynamic Composition
4.1 组件与纤维4.1 Components and Fibers
4.2 基础演算4.2 The Base Calculus
4.3 进行中的转换4.3 Transitions in Progress
4.3.1 撤回4.3.1 Withdrawal
4.3.2 迭代4.3.2 Iteration
4.3.3 异步性4.3.3 Asynchrony
4.3.4 失败4.3.4 Failure
4.4 元理论4.4 Metatheory
4.4.1 保持性4.4.1 Preservation
4.4.2 时间组合性4.4.2 Temporal Composability
4.4.3 空间可组合性4.4.3 Spatial Composability
4.4.4 进展4.4.4 Progress
4.4.5 汇合性4.4.5 Confluence
5 实现与案例研究5 Implementation and Case Study
5.1 核心库5.1 Core Library
5.1.1 效果追踪5.1.1 Effect Tracking
5.1.2 余效应操作5.1.2 Coeffect Operations
5.1.3 组件生命周期5.1.3 Component Lifecycle
5.1.4 上下文访问5.1.4 Context Access
5.2 组件加载器5.2 Component Loader
5.2.1 声明式配置5.2.1 Declarative Configuration
5.2.2 热模块替换5.2.2 Hot Module Replacement
5.3 案例研究：Koishi5.3 Case Study: Koishi
6 讨论6 Discussion
6.1 系统边界6.1 System Boundary
6.2 服务多路复用6.2 Service Multiplexing
6.3 访问控制与沙箱6.3 Access Control and Sandboxing
6.4 语言独立性与选择6.4 Language Independence and Selection
6.5 相互依赖与组件粒度6.5 Mutual Dependencies and Component Granularity
6.6 依赖类型与版本管理6.6 Dependency Typing and Versioning
6.7 与语言和操作系统的协同设计6.7 Co-Design with Languages and Operating Systems