一種時空可組合性的程式設計範式

摘要

現代軟體——從外掛系統到自我演化的代理支架——日益需要動態組合，但其形式基礎仍欠完備。我們識別出此問題的兩個正交維度：時間可組合性（temporal composability），即在移除元件時完全還原其副作用的能力；以及空間可組合性（spatial composability），即宣告並以反應式方式管理元件間依賴關係的能力。我們將經典的效果（effect）與共同效果（coeffect）概念提升至執行時期機制，以處理這兩個維度。具體而言，我們形式化了可還原效果（revertible effects），其中每一次上下文轉換皆伴隨一個逆變換，由執行時期持有，從而在單一元件內確立時間可組合性。我們形式化了反應式共同效果（reactive coeffects），其中每一次上下文變更皆根據元件的共同效果規格加以分類，以驅動其啟用與停用，從而在單一元件內確立空間可組合性。接著，我們將效果上下文與共同效果上下文統一為單一上下文型別，並透過該型別中介所有效果與共同效果，形成一種我們稱之為「上下文範式」（context paradigm）的規範；此中介導出一種觀察等價，在此等價之下，不同元件的效果得以交錯而不互相干擾。將這些機制組合為「元件」的概念後，我們提出一個動態組合的演算，其後設理論將時空可組合性從單一元件推展至整個交錯元件系統。我們在 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.