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

Deep concurrent CEK spec in foundations plan
Some checks failed
Build and Deploy / build-and-deploy (push) Has been cancelled
Details

Browse Source 
Steps 1-3 marked done. Step 4 (Concurrent CEK) fully specced:

4.1 Spawn — freeze thunk, run on worker, resolve signal
4.2 Channels — buffered, unbuffered, broadcast, select
4.3 Fork/Join — spawn N, collect results as signals
4.4 Scheduler — round-robin, priority, work-stealing, DAG-ordered
4.5 Content-addressed concurrency — memoize, distribute, verify
4.6 Host mapping — JS/Python/Haskell/Rust primitives table
4.7 Roadmap — 9 phases from Web Worker spawn to linear channels

Step 5 (Linear Effects) outlined: affine channels, linear scopes,
session types, resource handles.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This commit is contained in:
giles
2026-03-15 00:50:47 +00:00
parent e2940e1c5f
commit b3a7df45e6
1 changed files with 316 additions and 148 deletions
Download Patch File Download Diff File Expand all files Collapse all files

462
sx/sx/plans/foundations.sx
View File

@@ -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 "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.")))