Spatiotemporal Composability & Cordis
A guided reading of Shi, Zhang & Cui, A Programming Paradigm for Spatiotemporal Composability (arXiv 2608.25512), paired with the Cordis v4 source and aimed at the Olai plugin-runtime question.
How to read this
The book follows the paper's order because the paper's order is a dependency order: each section is used by the next. Chapter 3 is a short primer on the notation the paper uses without introducing it — read it first if you have discrete maths and algorithms but no type theory. Chapters 4–7 are the theory, each opening with a running example and glossing every formula in plain words; 8–9 are the calculus and what it proves; 10–11 the code; 12 the honest edges; 13 what it means for Olai; 14 exercises. Appendix A is every symbol in one table. Formulas are typeset in Unicode the way the paper writes them, so you can grep the PDF for any symbol here.
Terms of art link out on their first use on each page — algebra and type-theory terms to the nLab, the rest to Wikipedia, MDN, Hackage, or the project's own site — marked with a small arrow. They are there for when a word is unfamiliar; nothing in the book depends on following them.
Colour coding of the side-cards:
A claim the paper proves or defines, with its number so you can find the proof.
My translation into things you already know. Not the paper's words.
Where the idea lands in cordis-for-olai.md or the spike (PR juspay/olai#472).
A limit, an unchecked obligation, or a place the theory stops.
Dynamic composition — plugins loaded and unloaded at runtime, agent harnesses rewriting their own parts — has two orthogonal problems. Temporal: when a component leaves, everything it did to the shared environment must be undone. Spatial: components depend on one another, and those dependencies appear, disappear and change identity while the system runs. Statically we solve these with lexical scoping (RAII, bracket) and module imports; dynamically neither reaches. The paper lifts effects (what a computation does to its environment) and coeffects (what it needs from it) from compile-time annotations to runtime mechanisms: every effect carries an inverse the runtime holds (revertible effects); every dependency is a declared spec against which each context change is classified activating / deactivating / neutral (reactive coeffects). Both act on one context type; routing every interaction through it is the context paradigm, and it buys an observational equivalence under which different components' effects commute. A small calculus (nine rules, fibers with a four-state lifecycle) proves the guarantees survive interleaving. Cordis is the TypeScript realization; Koishi (4000+ plugins) is the case study.