coop/rose-ash
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Update foundations plan: all five layers complete, reframe next steps

Browse Source 
The depth axis is done — CEK (Layer 0) through patterns (Layer 4) are
all specced, bootstrapped, and tested. Rewrite the plan to reflect
reality and reframe the next steps as validation (serialization,
stepping debugger, content-addressed computation) before building
superstructure (concurrent CEK, linear effects).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This commit is contained in:
giles
2026-03-14 13:20:07 +00:00
parent 48d493e9cc
commit b3cba5e281
1 changed files with 170 additions and 441 deletions
Download Patch File Download Diff File Expand all files Collapse all files

611
sx/sx/plans/foundations.sx
View File

@@ -21,16 +21,50 @@
"No layer can be decomposed without the layer beneath it.")
(~docs/code :code
(str "Layer 0: CEK machine (expression + environment + continuation)\n"
"Layer 1: Continuations (shift / reset \u2014 delimited capture)\n"
"Layer 2: Algebraic effects (operations + handlers)\n"
"Layer 3: Scoped effects (+ region delimitation)\n"
"Layer 4: SX patterns (spread, provide, island, lake, signal, collect)"))
(str "Layer 0: CEK machine (expression + environment + continuation) \u2714 DONE\n"
"Layer 1: Continuations (shift / reset \u2014 delimited capture) \u2714 DONE\n"
"Layer 2: Algebraic effects (operations + handlers) \u2714 DONE\n"
"Layer 3: Scoped effects (+ region delimitation) \u2714 DONE\n"
"Layer 4: SX patterns (spread, provide, island, lake, signal) \u2714 DONE"))
(p "SX currently has layers 0, 1, and 4. "
"Layer 3 is the scoped-effects plan (provide/context/emit!). "
"Layer 2 falls out of layers 1 and 3 and doesn't need its own representation. "
"This document is about layers 0 through 2 \u2014 the machinery beneath scoped effects.")
(p "All five layers are implemented. The entire hierarchy from patterns down to raw CEK "
"is specced in " (code ".sx") " files and bootstrapped to Python and JavaScript. "
"No hand-written evaluation logic remains.")
;; -----------------------------------------------------------------------
;; What we built (status)
;; -----------------------------------------------------------------------
(h2 :class "text-xl font-bold mt-12 mb-4" "What We Built")
(div :class "overflow-x-auto mb-6"
(table :class "min-w-full text-sm"
(thead (tr
(th :class "text-left pr-4 pb-2 font-semibold" "Layer")
(th :class "text-left pr-4 pb-2 font-semibold" "Spec files")
(th :class "text-left pr-4 pb-2 font-semibold" "What it provides")
(th :class "text-left pb-2 font-semibold" "Tests")))
(tbody
(tr (td :class "pr-4 py-1" "0 \u2014 CEK")
(td :class "pr-4 font-mono text-xs" "cek.sx, frames.sx")
(td :class "pr-4" "Explicit step function, 20+ frame types, cek-call dispatch, CEK-native HO forms")
(td "43 CEK + 26 reactive"))
(tr (td :class "pr-4 py-1" "1 \u2014 Continuations")
(td :class "pr-4 font-mono text-xs" "continuations.sx, callcc.sx")
(td :class "pr-4" "shift/reset (delimited), call/cc (full), ReactiveResetFrame + DerefFrame")
(td "Continuation tests"))
(tr (td :class "pr-4 py-1" "2 \u2014 Effect signatures")
(td :class "pr-4 font-mono text-xs" "boundary.sx, eval.sx")
(td :class "pr-4" ":effects annotations on define, boundary enforcement at startup")
(td "Boundary validation"))
(tr (td :class "pr-4 py-1" "3 \u2014 Scoped effects")
(td :class "pr-4 font-mono text-xs" "eval.sx, adapters")
(td :class "pr-4" "scope/provide/context/emit!/emitted, scope-push!/scope-pop!")
(td "Scope integration"))
(tr (td :class "pr-4 py-1" "4 \u2014 Patterns")
(td :class "pr-4 font-mono text-xs" "signals.sx, adapter-dom.sx, engine.sx")
(td :class "pr-4" "signal/deref/computed/effect/batch, island/lake, spread/collect")
(td "20 signal + 26 CEK reactive")))))
;; -----------------------------------------------------------------------
;; Layer 0: The CEK machine
@@ -65,36 +99,35 @@
(p "Three things, all necessary, none decomposable further.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "CEK in eval.sx")
(h3 :class "text-lg font-semibold mt-8 mb-3" "CEK in SX")
(p "SX already implements CEK. It just doesn't name it:")
(p "The CEK machine is the default evaluator on both client (JS) and server (Python). "
"Every " (code "eval-expr") " call goes through " (code "cek-run") ". "
"The spec lives in two files:")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li (code "frames.sx") " \u2014 20+ frame types (IfFrame, ArgFrame, MapFrame, ReactiveResetFrame, ...)")
(li (code "cek.sx") " \u2014 step function, run loop, special form handlers, HO form handlers, cek-call"))
(p (code "cek-call") " is the universal function dispatch. "
"It replaces the old " (code "invoke") " shim \u2014 SX lambdas go through " (code "cek-run") ", "
"native callables through " (code "apply") ". One calling convention, bootstrapped identically to every host.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "CEK-native higher-order forms")
(p "All higher-order forms step element-by-element through the CEK machine:")
(~docs/code :code
(str ";; eval-expr IS the CEK transition function\n"
";; C = expr, E = env, K = implicit (call stack / trampoline)\n"
"(define eval-expr\n"
" (fn (expr env)\n"
" (cond\n"
" (number? expr) expr ;; literal: C \u2192 value, K unchanged\n"
" (string? expr) expr\n"
" (symbol? expr) (env-get env expr) ;; variable: C + E \u2192 value\n"
" (list? expr) ;; compound: modify K (push frame)\n"
" (let ((head (first expr)))\n"
" ...))))\n"
(str ";; map pushes a MapFrame, calls f on each element via continue-with-call\n"
"(map (fn (x) (* 2 (deref counter))) items)\n"
"\n"
";; The trampoline IS the K register made explicit:\n"
";; instead of growing the call stack, thunks are continuations\n"
"(define trampoline\n"
" (fn (val)\n"
" (let loop ((v val))\n"
" (if (thunk? v)\n"
" (loop (eval-expr (thunk-expr v) (thunk-env v)))\n"
" v))))"))
";; deref inside the callback goes through CEK's DerefFrame\n"
";; \u2192 reactive-shift-deref fires if inside a reactive-reset boundary\n"
";; \u2192 the continuation from deref to the MapFrame is captured as a subscriber"))
(p "The trampoline is the K register. Thunks are suspended continuations. "
"Tail-call optimization is replacing K instead of extending it. "
"SX's evaluation model is already a CEK machine \u2014 the plan is to make this explicit, "
"not to build something new.")
(p "This means " (code "deref") " works inside " (code "map") ", " (code "filter") ", "
(code "reduce") ", " (code "for-each") ", " (code "some") ", " (code "every?") " callbacks. "
"The HO forms don't escape to tree-walk \u2014 the CEK machine processes every step.")
;; -----------------------------------------------------------------------
;; Layer 1: Delimited continuations
@@ -116,15 +149,25 @@
(code "shift") " says: \"give me everything between here and that boundary as a callable function.\" "
"The captured continuation " (em "is") " a slice of the K register.")
(p "This is already specced in SX (continuations.sx). What it gives us beyond CEK:")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Deref as shift")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li (strong "Suspendable computation") " \u2014 capture where you are, resume later")
(li (strong "Backtracking") " \u2014 capture a choice point, try alternatives")
(li (strong "Coroutines") " \u2014 two computations yielding to each other")
(li (strong "Async as a library") " \u2014 async/await is shift/reset with a scheduler"))
(p "The reactive payoff. " (code "deref") " inside a " (code "reactive-reset") " boundary "
"is shift/reset applied to signals:")
(h3 :class "text-lg font-semibold mt-8 mb-3" "The Filinski Embedding")
(~docs/code :code
(str ";; User writes:\n"
"(div :class (str \"count-\" (deref counter))\n"
" (str \"Value: \" (deref counter)))\n"
"\n"
";; CEK sees (deref counter) \u2192 signal? \u2192 reactive-reset on stack?\n"
";; Yes: capture (str \"count-\" [HOLE]) as continuation\n"
";; Register as subscriber. Return current value.\n"
";; When counter changes: re-invoke continuation \u2192 update DOM."))
(p "No explicit " (code "effect()") " wrapping needed. "
"The continuation capture IS the subscription mechanism.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "The Filinski embedding")
(p "Filinski (1994) proved that " (code "shift/reset") " can encode "
(em "any") " monadic effect. State, exceptions, nondeterminism, I/O, "
@@ -132,78 +175,6 @@
"This means layer 1 is already computationally complete for effects. "
"Everything above is structure, not power.")
(p "This is the key insight: "
(strong "layers 2\u20134 add no computational power. ") "They add " (em "structure") " \u2014 "
"they make effects composable, nameable, handleable. "
"But anything you can do with scoped effects, "
"you can do with raw shift/reset. You'd just hate writing it.")
;; -----------------------------------------------------------------------
;; Layer 2: Algebraic effects
;; -----------------------------------------------------------------------
(h2 :class "text-xl font-bold mt-12 mb-4" "Layer 2: Algebraic Effects")
(p "Plotkin & Pretnar (2009) observed that most effects have algebraic structure: "
"an operation (\"perform this effect\") and a handler (\"here's what that effect means\"). "
"The handler receives the operation's argument and a continuation to resume the program.")
(~docs/code :code
(str ";; Pseudocode \u2014 algebraic effect style\n"
"(handle\n"
" (fn () (+ 1 (perform :ask \"what number?\")))\n"
" {:ask (fn (prompt resume)\n"
" (resume 41))})\n"
";; => 42"))
(p (code "perform") " is shift. " (code "handle") " is reset. "
"But with names and types. The handler pattern gives you:")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li (strong "Named effects") " \u2014 not just \"capture here\" but \"I need state / logging / auth\"")
(li (strong "Composable handlers") " \u2014 stack handlers, each handling different effects")
(li (strong "Effect signatures") " \u2014 a function declares what effects it needs; "
"the type system ensures all effects are handled"))
(p "Plotkin & Power (2003) proved that this captures: "
"state, exceptions, nondeterminism, I/O, cooperative concurrency, "
"probability, and backtracking. All as instances of one algebraic structure.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "What algebraic effects cannot express")
(p "Standard algebraic effects have a limitation: their operations are " (em "first-order") ". "
"An operation takes a value and produces a value. But some effects need operations that "
"take " (em "computations") " as arguments:")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li (code "catch") " \u2014 takes a computation that might throw, runs it with a handler")
(li (code "local") " \u2014 takes a computation, runs it with modified state")
(li (code "once") " \u2014 takes a nondeterministic computation, commits to its first result")
(li (code "scope") " \u2014 takes a computation, runs it within a delimited region"))
(p "These are " (strong "higher-order effects") ". They need computations as arguments, "
"not just values. This is precisely what the scoped-effects plan addresses.")
;; -----------------------------------------------------------------------
;; Layer 3: Scoped effects (the bridge)
;; -----------------------------------------------------------------------
(h2 :class "text-xl font-bold mt-12 mb-4" "Layer 3: Scoped and Higher-Order Effects")
(p "Wu, Schrijvers, and Hinze (2014) introduced " (em "scoped effects") " \u2014 "
"algebraic effects extended with operations that delimit regions. "
"Pirog, Polesiuk, and Sieczkowski (2018) proved these are "
(strong "strictly more expressive") " than standard algebraic effects.")
(p "Bach Poulsen and van der Rest (2023) generalized further with "
(em "hefty algebras") " \u2014 a framework that captures " (em "all") " known higher-order effects, "
"with scoped effects as a special case. This is the current state of the art.")
(p "SX's " (code "provide") " is a scoped effect. It creates a region (the body), "
"makes a value available within it (context), and collects contributions from within it (emit/emitted). "
"This is why it can express things that plain algebraic effects can't: "
"the region boundary is part of the effect, not an accident of the call stack.")
;; -----------------------------------------------------------------------
;; The floor proof
;; -----------------------------------------------------------------------
@@ -228,85 +199,96 @@
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li (strong "C without E") " = combinatory logic. Turing-complete but inhumane. "
"No named bindings \u2014 everything via S, K, I combinators. "
"Proves you can drop E in theory, but the resulting system "
"can't express abstraction (which is what E provides).")
"No named bindings \u2014 everything via S, K, I combinators.")
(li (strong "C without K") " = single expression evaluation. "
"You can compute one thing but can't compose it with anything. "
"Technically you can encode K into C (CPS transform), "
"but this transforms the expression to include the continuation explicitly \u2014 "
"K hasn't been removed, just moved into C.")
"You can compute one thing but can't compose it with anything.")
(li (strong "E without C") " = a phone book with no one to call.")
(li (strong "K without C") " = a to-do list with nothing on it."))
(p "You can " (em "encode") " any register into another (CPS eliminates K, "
"De Bruijn indices eliminate E), but encoding isn't elimination. "
"The information is still there, just hidden in a different representation. "
"Three independent concerns; three registers.")
"The information is still there, just hidden in a different representation.")
;; -----------------------------------------------------------------------
;; Open questions
;; Digging deeper: what's next
;; -----------------------------------------------------------------------
(h2 :class "text-xl font-bold mt-12 mb-4" "Open Questions")
(h2 :class "text-xl font-bold mt-12 mb-4" "Digging Deeper")
(p "The hierarchy above is well-established for " (em "sequential") " computation. "
"But there are orthogonal axes where the story is incomplete:")
(p "The hierarchy is built. Now we test whether the floor is solid. "
"Each step below validates the foundation before superstructure is added.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Concurrency")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Step 1: Serializable CEK state")
(p "Scoped effects assume tree-shaped execution: one thing happens, then the next. "
"But real computation forks:")
(p (code "make-cek-state") " already returns a plain dict. Can we serialize it, "
"ship it to another machine, and resume?")
(~docs/code :code
(str ";; Freeze a computation mid-flight\n"
"(let ((state (make-cek-state expr env (list))))\n"
" ;; Step a few times\n"
" (let ((state2 (cek-step (cek-step state))))\n"
" ;; Serialize to JSON\n"
" (json-serialize state2)\n"
" ;; Ship to worker, persist to disk, or content-address as CID\n"
" ))"))
(p "If this works, every SX computation is a value. "
"If it breaks, the state representation needs fixing " (em "before") " we build channels and fork/join on top.")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li "Video processing \u2014 pipeline stages run in parallel, frames are processed concurrently")
(li "CI/CD \u2014 test suites fork, builds parallelize, deployment is staged")
(li "Web rendering \u2014 async I/O, streaming SSE, suspense boundaries")
(li "Art DAG \u2014 the entire engine is a DAG of dependent transforms"))
(li "Can environments serialize? (They're dicts with parent chains \u2014 cycles?)")
(li "Can continuations serialize? (Frames are dicts, but closures inside them?)")
(li "Can native functions serialize? (No \u2014 need a registry mapping names to functions)")
(li "What about signals? (Dict with mutable subscribers list \u2014 serialize the value, not the graph)"))
(p "The \u03c0-calculus (Milner 1999) handles concurrency well but not effects. "
"Effect systems handle effects well but not concurrency. "
"Combining them is an open problem. "
"Brachth\u00e4user, Schuster, and Ostermann (2020) have partial results for "
"algebraic effects with multi-shot handlers (where the continuation can be invoked "
"on multiple concurrent threads), but a full synthesis doesn't exist yet.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Step 2: CEK stepping debugger")
(p "For SX, this matters because the Art DAG is fundamentally a concurrent execution engine. "
"If SX ever specifies DAG execution natively, it'll need something beyond scoped effects.")
(p (code "cek-step") " is pure data\u2192data. A debugger is just a UI over it:")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Linearity")
(~docs/code :code
(str ";; The debugger is an island that renders CEK state\n"
"(defisland ~debugger (&key expr)\n"
" (let ((state (signal (make-cek-state (parse expr) env (list)))))\n"
" (div\n"
" (button :on-click (fn () (swap! state cek-step)) \"Step\")\n"
" (pre (str \"C: \" (inspect (get (deref state) \"control\"))))\n"
" (pre (str \"K: \" (len (get (deref state) \"kont\")) \" frames\")))))"))
(p "Can an effect handler be invoked more than once? Must a scope be entered? "
"Must every emitted value be consumed?")
(p "This is a live island. Each click of Step calls " (code "cek-step") " on the state signal. "
"The deref-as-shift mechanism updates the DOM. No framework, no virtual DOM, no diffing.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Step 3: Content-addressed computation")
(p "Hash a CEK state \u2192 CID. This is where SX meets the Art DAG:")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li (strong "Unrestricted") " \u2014 use as many times as you want (current SX)")
(li (strong "Affine") " \u2014 use at most once (Rust's ownership model)")
(li (strong "Linear") " \u2014 use exactly once (quantum no-cloning, exactly-once delivery)"))
(li "A CID identifies a computation in progress, not just a value")
(li "Two machines given the same CID produce the same result (deterministic)")
(li "Memoize: if you've already run this state, return the cached result")
(li "Distribute: ship the CID to whichever machine has the data it needs")
(li "Verify: re-run from the CID, check the result matches"))
(p "Linear types constrain the continuation: if a handler is linear, "
"it " (em "must") " resume the computation exactly once. No dropping (resource leak), "
"no duplicating (nondeterminism). This connects to:")
(p "This requires solving Step 1 (serialization) first. "
"Content-addressing is serialization + hashing.")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li "Resource management \u2014 file handles that " (em "must") " be closed")
(li "Protocol correctness \u2014 a session type that must complete")
(li "Transaction semantics \u2014 exactly-once commit/rollback")
(li "Quantum computing \u2014 no-cloning theorem as a type constraint"))
(h3 :class "text-lg font-semibold mt-8 mb-3" "Step 4: Concurrent CEK")
(p "Benton (1994) established the connection between linear logic and computation. "
"Adding linear effects to SX would constrain what handlers can do, "
"enabling stronger guarantees about resource safety. "
"This is orthogonal to depth \u2014 it's about " (em "discipline") ", not " (em "power") ".")
(p "Multiple CEK machines running in parallel, communicating via channels:")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Higher-order effects beyond hefty algebras")
(~docs/code :code
(str ";; Fork: two CEK states from one\n"
"(let ((left (make-cek-state expr-a env (list)))\n"
" (right (make-cek-state expr-b env (list))))\n"
" ;; Interleave steps\n"
" (scheduler (list left right)))"))
(p "Nobody has proved that hefty algebras capture " (em "all possible") " higher-order effects. "
"The hierarchy might continue. This is active research with no clear terminus. "
"The question \"is there a structured effect that no framework can express?\" "
"is analogous to G\u00f6del's incompleteness \u2014 it may be that every effect framework "
"has blind spots, and the only \"complete\" system is raw continuations (layer 1), "
"which are universal but unstructured.")
(p "The Art DAG is the natural first consumer. Its execution model is already "
"a DAG of dependent computations. CEK states as DAG nodes. "
"Channels as edges. The scheduler is the DAG executor.")
(p "This is where scoped effects meet the \u03c0-calculus. "
"But it depends on Steps 1\u20133 being solid.")
;; -----------------------------------------------------------------------
;; The three-axis model
@@ -318,242 +300,29 @@
"It's a point in a three-dimensional space:")
(~docs/code :code
(str "depth: CEK \u2192 continuations \u2192 algebraic effects \u2192 scoped effects\n"
"topology: sequential \u2192 concurrent \u2192 distributed\n"
"linearity: unrestricted \u2192 affine \u2192 linear"))
(str "depth: CEK \u2192 continuations \u2192 algebraic effects \u2192 scoped effects [all done]\n"
"topology: sequential \u2192 concurrent \u2192 distributed [sequential done]\n"
"linearity: unrestricted \u2192 affine \u2192 linear [unrestricted done]"))
(p "Each axis is independent. You can have:")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li "Scoped effects + sequential + unrestricted \u2014 " (strong "SX today"))
(li "Scoped effects + concurrent + unrestricted \u2014 the Art DAG integration")
(li "Scoped effects + sequential + linear \u2014 resource-safe SX")
(li "Algebraic effects + concurrent + linear \u2014 something like Rust + Tokio + effect handlers")
(li "CEK + distributed + unrestricted \u2014 raw Erlang/BEAM"))
(p "SX's current position and trajectory:")
(p "Each axis is independent. SX's current position:")
(div :class "overflow-x-auto mb-6"
(table :class "min-w-full text-sm"
(thead (tr
(th :class "text-left pr-4 pb-2 font-semibold" "Axis")
(th :class "text-left pr-4 pb-2 font-semibold" "Current")
(th :class "text-left pr-4 pb-2 font-semibold" "Next")
(th :class "text-left pb-2 font-semibold" "Eventual")))
(th :class "text-left pb-2 font-semibold" "Next")))
(tbody
(tr (td :class "pr-4 py-1" "Depth")
(td :class "pr-4" "Layer 4 (patterns) + Layer 1 (continuations)")
(td :class "pr-4" "Layer 3 (scoped effects)")
(td "Layer 0 (explicit CEK)"))
(td :class "pr-4" "All layers (0\u20134) implemented")
(td "Validate via serialization + stepping"))
(tr (td :class "pr-4 py-1" "Topology")
(td :class "pr-4" "Sequential")
(td :class "pr-4" "Async I/O (partial concurrency)")
(td "DAG execution (Art DAG)"))
(td :class "pr-4" "Sequential (+ async I/O)")
(td "Concurrent CEK (Art DAG integration)"))
(tr (td :class "pr-4 py-1" "Linearity")
(td :class "pr-4" "Unrestricted")
(td :class "pr-4" "Unrestricted")
(td "Affine (resource safety)")))))
;; -----------------------------------------------------------------------
;; What explicit CEK gives SX
;; -----------------------------------------------------------------------
(h2 :class "text-xl font-bold mt-12 mb-4" "What Explicit CEK Gives SX")
(p "Making the CEK machine explicit in the spec (rather than implicit in eval-expr) enables:")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Stepping")
(p "A CEK machine transitions one step at a time. "
"If the transition function is explicit, you can:")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li "Single-step through evaluation (debugger)")
(li "Pause and serialize mid-evaluation (suspend to disk, resume on another machine)")
(li "Instrument each step (profiling, tracing, time-travel debugging)")
(li "Interleave steps from multiple computations (cooperative scheduling without OS threads)"))
(h3 :class "text-lg font-semibold mt-8 mb-3" "Serializable computation")
(p "If C, E, and K are all data structures (not host stack frames), "
"the entire computation state is serializable:")
(~docs/code :code
(str ";; Freeze a computation mid-flight\n"
"(let ((state (capture-cek)))\n"
" (send-to-worker state) ;; ship to another machine\n"
" ;; or: (store state) ;; persist to disk\n"
" ;; or: (fork state) ;; run the same computation twice\n"
" )"))
(p "This connects to content-addressed computation: "
"a CID identifying a CEK state is a pointer to a computation in progress. "
"Resume it anywhere. Verify it. Cache it. Share it.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Formal verification")
(p "An explicit CEK machine is a state machine. State machines are verifiable. "
"You can prove properties about all possible execution paths: "
"termination, resource bounds, effect safety. "
"The theorem prover (prove.sx) could verify CEK transitions directly.")
;; -----------------------------------------------------------------------
;; SX's existing layers
;; -----------------------------------------------------------------------
(h2 :class "text-xl font-bold mt-12 mb-4" "SX's Existing Layers")
(p "SX already has most of the hierarchy, specced or planned:")
(div :class "overflow-x-auto mb-6"
(table :class "min-w-full text-sm"
(thead (tr
(th :class "text-left pr-4 pb-2 font-semibold" "Layer")
(th :class "text-left pr-4 pb-2 font-semibold" "SX has")
(th :class "text-left pr-4 pb-2 font-semibold" "Where")
(th :class "text-left pb-2 font-semibold" "Status")))
(tbody
(tr (td :class "pr-4 py-1" "0 \u2014 CEK")
(td :class "pr-4" "eval-expr + trampoline")
(td :class "pr-4" "eval.sx")
(td "Implicit. Works, but CEK is hidden in the host call stack."))
(tr (td :class "pr-4 py-1" "1 \u2014 Continuations")
(td :class "pr-4" "shift / reset")
(td :class "pr-4" "continuations.sx")
(td "Specced. Bootstraps to Python and JavaScript."))
(tr (td :class "pr-4 py-1" "2 \u2014 Algebraic effects")
(td :class "pr-4" "\u2014")
(td :class "pr-4" "\u2014")
(td "Falls out of layers 1 + 3. No dedicated spec needed."))
(tr (td :class "pr-4 py-1" "3 \u2014 Scoped effects")
(td :class "pr-4" "provide / context / emit!")
(td :class "pr-4" "scoped-effects plan")
(td "Planned. Implements over eval.sx + adapters."))
(tr (td :class "pr-4 py-1" "4 \u2014 Patterns")
(td :class "pr-4" "spread, collect, island, lake, signal, store")
(td :class "pr-4" "various .sx files")
(td "Implemented. Will be redefined in terms of layer 3.")))))
;; -----------------------------------------------------------------------
;; Implementation path
;; -----------------------------------------------------------------------
(h2 :class "text-xl font-bold mt-12 mb-4" "Implementation Path")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 1: Scoped effects (Layer 3)")
(p "This is the scoped-effects plan. Immediate next step.")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li "Spec " (code "provide") ", " (code "context") ", " (code "emit!") ", " (code "emitted") " in eval.sx")
(li "Implement in all adapters (HTML, DOM, SX wire, async)")
(li "Redefine spread, collect, and reactive-spread as instances")
(li "Prove existing tests still pass"))
(h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 2: Effect signatures (Layer 2)")
(p "Add optional effect annotations to function definitions:")
(~docs/code :code
(str ";; Declare what effects a function uses\n"
"(define fetch-user :effects [io auth]\n"
" (fn (id) ...))\n"
"\n"
";; Pure function \u2014 no effects\n"
"(define add :effects []\n"
" (fn (a b) (+ a b)))\n"
"\n"
";; Scoped effect \u2014 uses context + emit\n"
"(define themed-heading :effects [context]\n"
" (fn (text)\n"
" (h1 :style (str \"color:\" (get (context \"theme\") :primary))\n"
" text)))"))
(p "Effect signatures are checked at registration time. "
"A function that declares " (code ":effects []") " cannot call " (code "emit!") " or " (code "context") ". "
"This is layer 2 \u2014 algebraic effect structure \u2014 applied as a type discipline.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 3: Explicit CEK (Layer 0)")
(p "Refactor eval.sx to expose the CEK registers as data:")
(~docs/code :code
(str ";; The CEK state is a value\n"
"(define-record CEK\n"
" :control expr ;; the expression\n"
" :env env ;; the bindings\n"
" :kont kont) ;; the continuation stack\n"
"\n"
";; One step\n"
"(define step :effects []\n"
" (fn (cek)\n"
" (case (type-of (get cek :control))\n"
" :literal (apply-kont (get cek :kont) (get cek :control))\n"
" :symbol (apply-kont (get cek :kont)\n"
" (env-get (get cek :env) (get cek :control)))\n"
" :list (let ((head (first (get cek :control))))\n"
" ...))))\n"
"\n"
";; Run to completion\n"
"(define run :effects []\n"
" (fn (cek)\n"
" (if (final? cek)\n"
" (get cek :control)\n"
" (run (step cek)))))"))
(p "This makes computation " (em "inspectable") ". A CEK state can be:")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li "Serialized to a CID (content-addressed frozen computation)")
(li "Single-stepped by a debugger")
(li "Forked (run the same state with different inputs)")
(li "Migrated (ship to another machine, resume there)")
(li "Verified (prove properties about all reachable states)"))
(h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 4: Concurrent effects (topology axis)")
(p "Extend the CEK machine to support multiple concurrent computations:")
(~docs/code :code
(str ";; Fork: create two CEK states from one\n"
"(define fork :effects [concurrency]\n"
" (fn (cek)\n"
" (list (step cek) (step cek))))\n"
"\n"
";; Join: merge results from two computations\n"
"(define join :effects [concurrency]\n"
" (fn (cek-a cek-b combine)\n"
" (combine (run cek-a) (run cek-b))))\n"
"\n"
";; Channel: typed communication between concurrent computations\n"
"(define channel :effects [concurrency]\n"
" (fn (name)\n"
" {:send (fn (v) (emit! name v))\n"
" :recv (fn () (shift k (handle-recv name k)))}))"))
(p "This is where scoped effects meet the \u03c0-calculus. "
"The Art DAG is the natural first consumer \u2014 "
"its execution model is already a DAG of dependent computations.")
(h3 :class "text-lg font-semibold mt-8 mb-3" "Phase 5: Linear effects (linearity axis)")
(p "Add resource-safety constraints:")
(~docs/code :code
(str ";; Linear scope: must be entered, must complete\n"
"(define-linear open-file :effects [io linear]\n"
" (fn (path)\n"
" (provide \"file\" (fs-open path)\n"
" ;; body MUST consume the file handle exactly once\n"
" ;; compiler error if handle is dropped or duplicated\n"
" (yield (file-read (context \"file\")))\n"
" ;; cleanup runs unconditionally\n"
" )))"))
(p "This is the furthest horizon. "
"Linear effects connect SX to session types, protocol verification, "
"and the kind of safety guarantees that Rust provides at the type level.")
;; -----------------------------------------------------------------------
;; The Curry-Howard correspondence
;; -----------------------------------------------------------------------
@@ -584,21 +353,9 @@
(tr (td :class "pr-4 py-1" "Implication (A \u2192 B)")
(td :class "pr-4" "Function type")
(td "Lambda"))
(tr (td :class "pr-4 py-1" "Conjunction (A \u2227 B)")
(td :class "pr-4" "Product type")
(td "Dict / record"))
(tr (td :class "pr-4 py-1" "Disjunction (A \u2228 B)")
(td :class "pr-4" "Sum type / union")
(td "Case dispatch"))
(tr (td :class "pr-4 py-1" "Universal (\u2200x.P)")
(td :class "pr-4" "Polymorphism")
(td "Generic components"))
(tr (td :class "pr-4 py-1" "Existential (\u2203x.P)")
(td :class "pr-4" "Abstract type")
(td "Opaque scope"))
(tr (td :class "pr-4 py-1" "Double negation (\u00ac\u00acA)")
(td :class "pr-4" "Continuation")
(td "shift/reset")))))
(td "shift/reset, deref-as-shift")))))
(p "A program is a proof that a computation is possible. "
"An effect signature is a proposition about what the program does to the world. "
@@ -607,8 +364,7 @@
(p "This is why CEK is the floor: it " (em "is") " logic. "
"Expression = proposition, environment = hypotheses, continuation = proof context. "
"You can't go beneath logic and still be doing computation. "
"The Curry\u2013Howard correspondence is not a metaphor. It's an isomorphism.")
"You can't go beneath logic and still be doing computation.")
;; -----------------------------------------------------------------------
;; Summary
@@ -616,46 +372,19 @@
(h2 :class "text-xl font-bold mt-12 mb-4" "Summary")
(p "The path from where SX stands to the computational floor:")
(p "The depth axis is complete. Every layer from patterns down to raw CEK "
"is specced, bootstrapped, and tested. 89 tests across three suites.")
(div :class "overflow-x-auto mb-6"
(table :class "min-w-full text-sm"
(thead (tr
(th :class "text-left pr-4 pb-2 font-semibold" "Step")
(th :class "text-left pr-4 pb-2 font-semibold" "What")
(th :class "text-left pr-4 pb-2 font-semibold" "Enables")
(th :class "text-left pb-2 font-semibold" "Depends on")))
(tbody
(tr (td :class "pr-4 py-1" "1")
(td :class "pr-4" "Scoped effects")
(td :class "pr-4" "Unify spread/collect/island/lake/context")
(td "eval.sx + adapters"))
(tr (td :class "pr-4 py-1" "2")
(td :class "pr-4" "Effect signatures")
(td :class "pr-4" "Static effect checking, pure/IO boundary")
(td "types.sx + scoped effects"))
(tr (td :class "pr-4 py-1" "3")
(td :class "pr-4" "Explicit CEK")
(td :class "pr-4" "Stepping, serialization, migration, verification")
(td "eval.sx refactor"))
(tr (td :class "pr-4 py-1" "4")
(td :class "pr-4" "Concurrent effects")
(td :class "pr-4" "DAG execution, parallel pipelines")
(td "CEK + channels"))
(tr (td :class "pr-4 py-1" "5")
(td :class "pr-4" "Linear effects")
(td :class "pr-4" "Resource safety, protocol verification")
(td "Effect signatures + linear types")))))
(p "The next moves are lateral, not downward:")
(p "Each step is independently valuable. The first is immediate. "
"The last may be years out or may never arrive. "
"The hierarchy exists whether we traverse it or not \u2014 "
"it's the structure of computation itself, "
"and SX is better for knowing where it sits within it.")
(ul :class "list-disc pl-6 mb-4 space-y-1"
(li (strong "Validate the floor") " \u2014 serialize CEK state, build a stepping debugger, "
"content-address computations. These test whether the foundation holds weight.")
(li (strong "Topology") " \u2014 concurrent CEK for the Art DAG. Multiple machines, channels, scheduling.")
(li (strong "Linearity") " \u2014 resource safety. Affine continuations that must be resumed exactly once."))
(p "Each step is independently valuable. The foundation is built. "
"Now we find out what it can carry.")
(p :class "text-stone-500 text-sm italic mt-12"
"The true foundation of any language is not its syntax or its runtime "
"but the mathematical structure it participates in. "
"SX is an s-expression language, which makes it a notation for the lambda calculus, "
"which is a notation for logic, which is the structure of thought. "
"The floor is thought itself. We can't go deeper, because there's no one left to dig.")))