AI 中文总结
该研究针对软件动态组合的时空可组合性问题，提出上下文范式，实现可撤销效应与反应式余效应，开发元框架Cordis，将时空可组合性扩展至整个组件系统。
AI 中文摘要
现代软件——从插件系统到自进化智能体管控系统——日益需要动态组合，但其形式基础仍未充分发展。我们确定了该问题的两个正交维度：时间可组合性，即移除组件时完全撤销其副作用的能力；空间可组合性，即声明并反应式管理组件间依赖关系的能力。我们通过将经典的效应与余效应概念提升为运行时机制来解决这两个维度问题。具体而言，我们将可撤销效应形式化，其中每个上下文转换都带有运行时保存的逆操作，建立单个组件局部的时间可组合性；我们将反应式余效应形式化，其中每个上下文变化都根据组件的余效应规范进行分类，以驱动其激活与停用，建立单个组件局部的空间可组合性。随后，我们将效应上下文与余效应上下文统一为单一上下文类型，并通过该类型介导所有效应与余效应，得到一种名为上下文范式的规范；该介导诱导出一种观测等价性，据此不同组件的效应可交错而互不干扰。将这些机制结合为组件概念，我们提出一种动态组合演算，其元理论将时空可组合性从单个组件扩展至由交错组件构成的整个系统。我们在Cordis中实现了这些思路，Cordis是一个时空可组合性元框架，提供带有效应跟踪与余效应解析的核心库，以及带有配置协调与热模块替换的声明式组件加载器。
英文摘要
Modern software -- from plugin systems to self-evolving agent harnesses -- increasingly requires dynamic composition, yet its formal foundations remain underdeveloped. We identify two orthogonal dimensions of the problem: temporal composability, the ability to completely revert a component's side effects upon removal, and spatial composability, the ability to declare and reactively manage inter-component dependencies. We address the two dimensions by lifting classical effect and coeffect concepts to runtime mechanisms. In particular, we formalize revertible effects, in which every context transformation carries an inverse that the runtime holds, establishing temporal composability local to one component. We formalize reactive coeffects, in which every context change is classified against a component's coeffect specification to drive its activation and deactivation, establishing spatial composability local to one component. We then unify the effect context and the coeffect context into a single context type and mediate every effect and coeffect through it, yielding a discipline we call the context paradigm; the mediation induces an observational equivalence up to which the effects of distinct components interleave without disturbing one another. Combining these mechanisms into the notion of a component, we give a calculus of dynamic composition whose metatheory carries spatiotemporal composability from a single component to a whole system of interleaved components. We implement these ideas in Cordis, a meta-framework of spatiotemporal composability that provides a core library with effect tracking and coeffect resolution, as well as a declarative component loader with configuration reconciliation and hot module replacement.
Comments92 pages, 1 figure, 2 tables
