diff --git a/sx/sx/plans/foundations.sx b/sx/sx/plans/foundations.sx index e987eb2..a13a239 100644 --- a/sx/sx/plans/foundations.sx +++ b/sx/sx/plans/foundations.sx @@ -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.")))