diff --git a/sx/sx/plans/foundations.sx b/sx/sx/plans/foundations.sx index a13a239..224ed93 100644 --- a/sx/sx/plans/foundations.sx +++ b/sx/sx/plans/foundations.sx @@ -213,178 +213,346 @@ ;; Digging deeper: what's next ;; ----------------------------------------------------------------------- - (h2 :class "text-xl font-bold mt-12 mb-4" "Digging Deeper") - - (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" "Step 1: Serializable CEK state") - - (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 "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)")) - - (h3 :class "text-lg font-semibold mt-8 mb-3" "Step 2: CEK stepping debugger") - - (p (code "cek-step") " is pure data\u2192data. A debugger is just a UI over it:") - - (~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 "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 "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 "This requires solving Step 1 (serialization) first. " - "Content-addressing is serialization + hashing.") - - (h3 :class "text-lg font-semibold mt-8 mb-3" "Step 4: Concurrent CEK") - - (p "Multiple CEK machines running in parallel, communicating via channels:") - - (~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 "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 - ;; ----------------------------------------------------------------------- - - (h2 :class "text-xl font-bold mt-12 mb-4" "The Three-Axis Model") - - (p "The deepest primitive is not a single thing. " - "It's a point in a three-dimensional space:") - - (~docs/code :code - (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. SX's current position:") + (h2 :class "text-xl font-bold mt-12 mb-4" "Progress") (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 pb-2 font-semibold" "Next"))) + (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 pb-2 font-semibold" "Status"))) (tbody - (tr (td :class "pr-4 py-1" "Depth") - (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 (+ async I/O)") - (td "Concurrent CEK (Art DAG integration)")) - (tr (td :class "pr-4 py-1" "Linearity") - (td :class "pr-4" "Unrestricted") - (td "Affine (resource safety)"))))) + (tr (td :class "pr-4 py-1" "1") + (td :class "pr-4" "Serializable CEK state") + (td :class "text-emerald-600 font-semibold" "\u2714 Done \u2014 freeze-scope, freeze-signal, freeze-to-sx, thaw-from-sx")) + (tr (td :class "pr-4 py-1" "2") + (td :class "pr-4" "CEK stepping debugger") + (td :class "text-emerald-600 font-semibold" "\u2714 Done \u2014 live island with reactive code view, DOM preview")) + (tr (td :class "pr-4 py-1" "3") + (td :class "pr-4" "Content-addressed computation") + (td :class "text-emerald-600 font-semibold" "\u2714 Done \u2014 content-hash, freeze-to-cid, thaw-from-cid")) + (tr (td :class "pr-4 py-1" "4") + (td :class "pr-4" "Concurrent CEK") + (td :class "text-amber-600 font-semibold" "Spec complete \u2014 implementation next")) + (tr (td :class "pr-4 py-1" "5") + (td :class "pr-4" "Linear effects") + (td :class "text-stone-400" "Future"))))) ;; ----------------------------------------------------------------------- - ;; The Curry-Howard correspondence + ;; Step 4: Concurrent CEK \u2014 deep spec ;; ----------------------------------------------------------------------- - (h2 :class "text-xl font-bold mt-12 mb-4" "The Curry\u2013Howard Correspondence") + (h2 :class "text-xl font-bold mt-12 mb-4" "Step 4: Concurrent CEK") - (p "At the deepest level, computation and logic are the same thing:") + (p "Multiple CEK machines running concurrently. The machines are independent \u2014 " + "each has its own C, E, K registers. Communication is via typed channels. " + "The host provides the concurrency mechanism (Web Workers, forkIO, tokio::spawn). " + "The spec defines the coordination primitives.") + + (h3 :class "text-lg font-semibold mt-8 mb-3" "4.1 Spawn") + + (p "The fundamental primitive. Create a new CEK machine from a thunk, " + "run it concurrently, return a signal that resolves with the result:") + + (~docs/code :code + (str "(let ((result (spawn (fn () (* 6 7))))) +" + " ;; result is a signal \u2014 nil until the computation completes +" + " (effect (fn () +" + " (when (deref result) +" + " (log (str \"answer: \" (deref result)))))) +" + " ;; => \"answer: 42\" (eventually)")) + + (p "Implementation: the host freezes the thunk\u2019s CEK state, ships it to a worker, " + "the worker thaws and runs, posts back the result, the signal resolves. " + "The reactive system propagates the change \u2014 any island deref\u2019ing the signal re-renders.") + + (p "The default implementation is synchronous (no actual concurrency). " + "The host overrides " (code "spawn-impl") " for real concurrency:") + + (~docs/code :code + (str ";; Host-provided spawn (Web Worker) +" + "(set! spawn-impl +" + " (fn (thunk result-sig) +" + " (let ((frozen (freeze-to-sx \"spawn\"))) +" + " (worker-post frozen) +" + " (worker-on-message +" + " (fn (val) (reset! result-sig val))))))")) + + (h3 :class "text-lg font-semibold mt-8 mb-3" "4.2 Channels") + + (p "Typed communication pipes between concurrent computations. " + "Send is non-blocking. Receive suspends via " (code "shift") " until data arrives:") + + (~docs/code :code + (str ";; Create a channel +" + "(make-channel \"results\") +" + " +" + ";; Producer (in spawned computation) +" + "(spawn (fn () +" + " (channel-send \"results\" (expensive-computation)))) +" + " +" + ";; Consumer (in main thread) +" + "(let ((val (channel-receive \"results\"))) +" + " ;; val is a signal if no data yet, or the value if buffered +" + " (when (signal? val) +" + " ;; Reactive: re-renders when data arrives +" + " (div \"Waiting...\" (deref val))))")) + + (p "Channels are named and registered globally. Multiple producers and consumers " + "can share a channel. The buffer stores values until a consumer reads them. " + "When a consumer arrives and the buffer is empty, a signal is returned " + "that resolves when a producer sends.") + + (p "Channel semantics:") + + (ul :class "list-disc pl-6 mb-4 space-y-1" + (li (strong "Unbuffered") " \u2014 send blocks until a receiver is ready (rendezvous)") + (li (strong "Buffered") " \u2014 send succeeds immediately, values queue (current default)") + (li (strong "Broadcast") " \u2014 every receiver gets every value (pub/sub)") + (li (strong "Select") " \u2014 wait on multiple channels, take the first that has data")) + + (h3 :class "text-lg font-semibold mt-8 mb-3" "4.3 Fork / Join") + + (p "Spawn multiple computations, collect all results. " + "The spec primitive, not a library pattern:") + + (~docs/code :code + (str ";; Fork: run N computations concurrently +" + "(let ((results (fork-join (list +" + " (fn () (fetch-user 1)) +" + " (fn () (fetch-user 2)) +" + " (fn () (fetch-user 3)))))) +" + " ;; results is a list of signals +" + " ;; All resolve when all computations complete +" + " (div +" + " (map (fn (r) (div (deref r))) results)))")) + + (p "Fork/join composes with the reactive system. Each result signal drives " + "a reactive DOM node. Results appear as they complete, not all-or-nothing.") + + (h3 :class "text-lg font-semibold mt-8 mb-3" "4.4 Scheduler") + + (p "The scheduler decides which CEK machine steps next. " + "Different strategies for different use cases:") + + (ul :class "list-disc pl-6 mb-4 space-y-1" + (li (strong "Round-robin") " \u2014 fair, each machine gets equal time") + (li (strong "Priority") " \u2014 UI-facing computations step first") + (li (strong "Work-stealing") " \u2014 idle workers steal from busy ones") + (li (strong "Cooperative") " \u2014 machines yield explicitly via " (code "yield!")) + (li (strong "DAG-ordered") " \u2014 step machines whose inputs are ready (Art DAG)")) + + (~docs/code :code + (str ";; Cooperative scheduling +" + "(spawn (fn () +" + " (for-each (fn (item) +" + " (process item) +" + " (yield!) ;; let other machines run +" + " ) items))) +" + " +" + ";; DAG scheduling +" + "(dag-execute +" + " {:nodes {:a (fn () (load-image \"input.jpg\")) +" + " :b (fn (a) (resize a 512 512)) +" + " :c (fn (a) (blur a 3)) +" + " :d (fn (b c) (composite b c))} +" + " :edges {[:a] [:b :c] +" + " [:b :c] [:d]}})")) + + (h3 :class "text-lg font-semibold mt-8 mb-3" "4.5 Content-addressed concurrency") + + (p "Concurrent computation + content addressing = verifiable parallel execution:") + + (ul :class "list-disc pl-6 mb-4 space-y-1" + (li "Each spawned computation\u2019s initial state has a CID") + (li "Each result has a CID") + (li "The mapping input-CID \u2192 output-CID is a proof of computation") + (li "Memoize: if input-CID was computed before, return cached output-CID") + (li "Distribute: send input-CID to whichever worker has the data") + (li "Verify: any machine can re-run from input-CID and check output-CID matches")) + + (~docs/code :code + (str ";; Content-addressed spawn +" + "(let ((input-cid (freeze-to-cid \"job\"))) +" + " ;; Check cache first +" + " (or (result-cache-get input-cid) +" + " ;; Not cached \u2014 compute and cache +" + " (let ((result (spawn (fn () (expensive-work))))) +" + " (effect (fn () +" + " (when (deref result) +" + " (result-cache-put input-cid +" + " (freeze-to-cid \"result\"))))) +" + " result)))")) + + (h3 :class "text-lg font-semibold mt-8 mb-3" "4.6 Host mapping") + + (p "Each host implements concurrency differently. The spec is the same:") (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" "Logic") - (th :class "text-left pr-4 pb-2 font-semibold" "Computation") - (th :class "text-left pb-2 font-semibold" "SX"))) + (th :class "text-left pr-4 pb-2 font-semibold" "Primitive") + (th :class "text-left pr-4 pb-2 font-semibold" "JavaScript") + (th :class "text-left pr-4 pb-2 font-semibold" "Python") + (th :class "text-left pr-4 pb-2 font-semibold" "Haskell") + (th :class "text-left pb-2 font-semibold" "Rust/WASM"))) (tbody - (tr (td :class "pr-4 py-1" "Proposition") - (td :class "pr-4" "Type") - (td "Effect signature")) - (tr (td :class "pr-4 py-1" "Proof") - (td :class "pr-4" "Program") - (td "Implementation")) - (tr (td :class "pr-4 py-1" "Proof normalization") - (td :class "pr-4" "Evaluation") - (td "CEK transitions")) - (tr (td :class "pr-4 py-1" "Hypothesis") - (td :class "pr-4" "Variable binding") - (td "Environment (E register)")) - (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" "Double negation (\u00ac\u00acA)") - (td :class "pr-4" "Continuation") - (td "shift/reset, deref-as-shift"))))) + (tr (td :class "pr-4 py-1 font-mono" "spawn") + (td :class "pr-4" "Web Worker") + (td :class "pr-4" "asyncio.create_task") + (td :class "pr-4" "forkIO") + (td "tokio::spawn")) + (tr (td :class "pr-4 py-1 font-mono" "channel") + (td :class "pr-4" "MessageChannel") + (td :class "pr-4" "asyncio.Queue") + (td :class "pr-4" "TChan (STM)") + (td "mpsc::channel")) + (tr (td :class "pr-4 py-1 font-mono" "yield!") + (td :class "pr-4" "setTimeout(0)") + (td :class "pr-4" "await asyncio.sleep(0)") + (td :class "pr-4" "threadDelay 0") + (td "tokio::task::yield_now")) + (tr (td :class "pr-4 py-1 font-mono" "freeze/thaw") + (td :class "pr-4" "postMessage + JSON") + (td :class "pr-4" "pickle / SX text") + (td :class "pr-4" "Serialise + SX text") + (td "serde + SX text")) + (tr (td :class "pr-4 py-1 font-mono" "select") + (td :class "pr-4" "Promise.race") + (td :class "pr-4" "asyncio.wait FIRST_COMPLETED") + (td :class "pr-4" "STM orElse") + (td "tokio::select!"))))) - (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. " - "A handler is a proof that the effect can be realized. " - "Evaluation is proof normalization \u2014 the systematic simplification of a proof to its normal form.") + (h3 :class "text-lg font-semibold mt-8 mb-3" "4.7 Roadmap") - (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.") + (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" "Phase") + (th :class "text-left pr-4 pb-2 font-semibold" "What") + (th :class "text-left pr-4 pb-2 font-semibold" "Host") + (th :class "text-left pb-2 font-semibold" "Validates"))) + (tbody + (tr (td :class "pr-4 py-1" "4a") + (td :class "pr-4" "spawn + Web Worker") + (td :class "pr-4" "JavaScript") + (td "Freeze/thaw across execution contexts")) + (tr (td :class "pr-4 py-1" "4b") + (td :class "pr-4" "Channels (buffered)") + (td :class "pr-4" "JavaScript") + (td "Cross-worker communication")) + (tr (td :class "pr-4 py-1" "4c") + (td :class "pr-4" "Fork/join + DAG scheduler") + (td :class "pr-4" "JavaScript") + (td "Art DAG integration path")) + (tr (td :class "pr-4 py-1" "4d") + (td :class "pr-4" "Haskell bootstrapper") + (td :class "pr-4" "Haskell") + (td "Spec portability, native concurrency")) + (tr (td :class "pr-4 py-1" "4e") + (td :class "pr-4" "Rust/WASM bootstrapper") + (td :class "pr-4" "Rust") + (td "Browser performance, WASM target")) + (tr (td :class "pr-4 py-1" "4f") + (td :class "pr-4" "Content-addressed spawn") + (td :class "pr-4" "Any") + (td "Memoization, distribution, verification")) + (tr (td :class "pr-4 py-1" "4g") + (td :class "pr-4" "IPFS-backed content store") + (td :class "pr-4" "Any") + (td "Global content addressing, peer-to-peer")) + (tr (td :class "pr-4 py-1" "4h") + (td :class "pr-4" "Select + broadcast channels") + (td :class "pr-4" "Any") + (td "Complex coordination patterns")) + (tr (td :class "pr-4 py-1" "4i") + (td :class "pr-4" "Linear channels") + (td :class "pr-4" "Any") + (td "Resource safety, exactly-once delivery"))))) + + (p "Each phase is independently valuable. Phase 4a (Web Worker spawn) is the immediate next build. " + "Phase 4d (Haskell) proves the spec is truly host-independent. " + "Phase 4e (Rust/WASM) proves it can be fast. " + "Phase 4g (IPFS) makes it distributed.") ;; ----------------------------------------------------------------------- - ;; Summary + ;; Step 5: Linear effects (future) ;; ----------------------------------------------------------------------- - (h2 :class "text-xl font-bold mt-12 mb-4" "Summary") + (h2 :class "text-xl font-bold mt-12 mb-4" "Step 5: Linear Effects") - (p "The depth axis is complete. Every layer from patterns down to raw CEK " - "is specced, bootstrapped, and tested. 89 tests across three suites.") - - (p "The next moves are lateral, not downward:") + (p "Constrain the continuation: a handler " (em "must") " resume exactly once. " + "No dropping (resource leak), no duplicating (nondeterminism). " + "This is the linearity axis from the three-axis model.") (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.")) + (li (strong "Affine channels") " \u2014 send at most once. Prevents duplicate messages.") + (li (strong "Linear scopes") " \u2014 a freeze scope that must be thawed. Prevents orphaned state.") + (li (strong "Session types") " \u2014 a protocol that must complete. Prevents half-open connections.") + (li (strong "Resource handles") " \u2014 a file/DB handle that must be closed. Prevents leaks.")) - (p "Each step is independently valuable. The foundation is built. " - "Now we find out what it can carry.") + (p "Linear effects connect SX to Rust\u2019s ownership model. " + "Affine types (use at most once) are the practical sweet spot. " + "Full linearity (use exactly once) is for protocols and resources.") - (p :class "text-stone-500 text-sm italic mt-12" + (p "This is the furthest horizon. The infrastructure \u2014 freeze scopes, channels, " + "content addressing \u2014 must be solid first. Linearity is a discipline on top, " + "not a prerequisite beneath.") + + (p :class "text-stone-500 text-sm italic mt-12" "The floor is thought itself. We can't go deeper, because there's no one left to dig.")))