時空間合成可能性のためのプログラミングパラダイム

要旨

現代のソフトウェアは、プラグインシステムから自己進化型エージェントハーネスに至るまで、動的合成をますます必要としているが、その形式的基盤は未発達なままである。我々はこの問題の直交する二つの次元を特定する。すなわち、時間的コンポーザビリティ（コンポーネントの除去時にその副作用を完全に取り消す能力）と、空間的コンポーザビリティ（コンポーネント間の依存関係を宣言し、リアクティブに管理する能力）である。我々は、古典的なエフェクト概念とコエフェクト概念をランタイム機構へと持ち上げることにより、これら二つの次元に対処する。具体的には、可逆エフェクトを形式化する。可逆エフェクトでは、すべての文脈変換がランタイムの保持する逆変換を伴い、単一コンポーネントに局所的な時間的コンポーザビリティを確立する。さらに、リアクティブコエフェクトを形式化する。リアクティブコエフェクトでは、すべての文脈変化がコンポーネントのコエフェクト仕様に照らして分類され、その活性化と非活性化が駆動され、単一コンポーネントに局所的な空間的コンポーザビリティが確立される。次に、エフェクト文脈とコエフェクト文脈を単一の文脈型へと統合し、あらゆるエフェクトとコエフェクトをその文脈型を通じて仲介する。これにより、我々が「文脈パラダイム」と呼ぶ体系が得られる。この仲介は観察的等価性を誘導し、その等価性のもとで、異なるコンポーネントのエフェクトは互いに干渉することなくインターリーブされる。これらの機構をコンポーネントの概念へと統合することで、我々は動的合成の計算体系を与える。そのメタ理論は、時空間的コンポーザビリティを単一コンポーネントから、インターリーブされたコンポーネント群からなるシステム全体へと伝搬させる。我々はこれらのアイデアを、時空間的コンポーザビリティのメタフレームワークであるCordisに実装する。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.