时空可组合性的编程范式

摘要

现代软件——从插件系统到自我演化的智能体框架——日益需要动态组合，但其形式基础仍不完善。我们识别出该问题的两个正交维度：时间可组合性，即完全撤销组件副作用的能力；以及空间可组合性，即声明并反应式管理组件间依赖的能力。我们通过将经典效应与协效应概念提升为运行时机制来解决这两个维度。具体而言，我们形式化了可逆效应，其中每个上下文变换都携带一个由运行时持有的逆变换，从而在单个组件局部建立时间可组合性。我们形式化了反应式协效应，其中每个上下文变化都根据组件的协效应规格进行分类，以驱动其激活与停用，从而在单个组件局部建立空间可组合性。随后，我们将效应上下文与协效应上下文统一为单一的上下文类型，并通过该类型协调所有效应与协效应，由此得出我们称之为上下文范式的一种规约；这种协调引发一种观测等价性，在此等价性下，不同组件的效应相互交织而互不干扰。我们将这些机制组合为组件概念，给出一个动态组合演算，其元理论将时空可组合性从单一组件推广到整个交织组件系统。我们在Cordis中实现了这些思想，这是一个时空可组合性的元框架，提供包含效应追踪与协效应解析的核心库，以及一个具有配置协调和热模块替换的声明式组件加载器。

English

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.