Design + ops scaffolding for the next phase of work, none of it touching
substrate or guest code.
lib-guest.md: rewrites Architectural framing as a 5-layer stack
(substrate → lib/guest → languages → shared/ → applications),
recursive dependency-direction rule, scaled two-consumer rule. Adds
Phase B (long-running stratification) with sub-layer matrix
(core/typed/relational/effects/layout/lazy/oo), language profiles, and
the long-running-discipline section. Preserves existing Phase A
progress log and rules.
ocaml-on-sx.md: scope reduced to substrate validation + HM + reference
oracle. Phases 1-5 + minimal stdlib slice + vendored testsuite slice.
Dream carved out into dream-on-sx.md; Phase 8 (ReasonML) deferred.
Records lib-guest sequencing dependency.
datalog-on-sx.md: adds Phase 4 built-in predicates + body arithmetic,
Phase 6 magic sets, safety analysis in Phase 3, Non-goals section.
New chisel plans (forward-looking, not yet launchable):
kernel-on-sx.md — first-class everything, env-as-value endgame
idris-on-sx.md — dependent types, evidence chisel
probabilistic-on-sx.md — weighted nondeterminism + traces
maude-on-sx.md — rewriting as primitive
linear-on-sx.md — resource model, artdag-relevant
Loop briefings (4 active, 1 cold):
minikanren-loop.md, ocaml-loop.md, datalog-loop.md, elm-loop.md, koka-loop.md
Restore scripts mirror the loop pattern:
restore-{minikanren,ocaml,datalog,jit-perf,lib-guest}.sh
Each captures worktree state, plan progress, MCP health, tmux status.
Includes the .mcp.json absolute-path patch instruction (fresh worktrees
have no _build/, so the relative mcp_tree path fails on first launch).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
8.5 KiB
koka-on-sx loop agent (single agent, queue-driven)
Role: iterates plans/koka-on-sx.md forever. Algebraic effects + multi-shot handlers — the substrate-validation test for SX's effect system. Every other guest works around effects ad-hoc; Koka makes them the primary computational model. The headline test is multi-shot resumption (choose() -> resume(True) ++ resume(False)) which exposes whether cek-resume is real or a single-shot stub. One feature per commit.
description: koka-on-sx queue loop
subagent_type: general-purpose
run_in_background: true
isolation: worktree
DO NOT START WITHOUT THE PREREQUISITES
This loop must not start until both of the following are true:
- lib-guest Steps 3, 4, 6 are
[done]— Koka's tokenizer consumeslib/guest/lex.sx, its parser consumeslib/guest/pratt.sx, its pattern matcher consumeslib/guest/match.sx. - ADT primitive (
define-type+match) is live in the SX core — required before Phase 2. Track viaplans/sx-improvements.mdPhase 3 (Steps 5–8) or its successor.
Pre-flight check:
ls /root/rose-ash/lib/guest/lex.sx /root/rose-ash/lib/guest/pratt.sx /root/rose-ash/lib/guest/match.sx
printf '(epoch 1)\n(define-type test-adt (A) (B v))\n(epoch 2)\n(match (A) ((A) "ok") (_ "no"))\n' \
| /root/rose-ash/hosts/ocaml/_build/default/bin/sx_server.exe 2>&1 | tail -3
If any lib-guest file is missing OR define-type/match errors instead of returning "ok", stop and report. Do not start.
Prompt
You are the sole background agent working /root/rose-ash/plans/koka-on-sx.md. You run in an isolated git worktree on branch loops/koka. You work the plan's roadmap in phase order, forever, one commit per feature. Push to origin/loops/koka after every commit.
Restart baseline — check before iterating
- Read
plans/koka-on-sx.md— Roadmap + Progress log + Blockers tell you where you are. - Run the pre-flight check above. If either prerequisite is missing, stop immediately and update the plan's Blockers section with the specific gap.
ls lib/koka/— pick up from the most advanced file that exists. If the directory does not exist, you are at Phase 1.- If
lib/koka/tests/*.sxexist, run them via the epoch protocol againstsx_server.exe. They must be green before new work.
The queue
Phase order per plans/koka-on-sx.md:
- Phase 1 — tokenizer + parser (consuming
lib/guest/lex.sx+lib/guest/pratt.sx) - Phase 2 — ADT definitions + match (consuming
lib/guest/match.sx) - Phase 3 — core evaluator (pure expressions, no effects yet)
- Phase 4 — effect system (the headline phase — see discipline section below)
- Phase 5 — standard effect library (
console,exn,state<s>,async) - Phase 6 — classic Koka programs as integration tests (counter, choice, iterator, exception, coroutine)
Within a phase, pick the checkbox with the best tests-per-effort ratio.
Every iteration: implement → test → commit → tick [ ] in plan → append Progress log → push → next.
Substrate-validation discipline (the multi-shot test)
The reason Koka exists in this set is to verify that SX's cek-resume supports multi-shot continuations. The Phase 4 commit that lands choose() -> resume(True) ++ resume(False) returning [True, True, False, True] is the single most important commit in this whole plan. Everything before it is scaffolding; everything after it is filling out the language.
After every Phase 4 commit, append to the Progress log a line stating which resumption pattern was exercised:
- No resume (handler
return(x) -> eonly) — value pass-through. - Tail resumption (
op() -> resume(v)) — handler resumes exactly once, in tail position. Should be optimisable; verify no extra allocation. - Single resume not in tail (
op() -> let x = resume(v) in compute(x)) — handler resumes once, then does work after. - Multi-shot (
choose() -> resume(True) ++ resume(False)) — handler resumes the same continuation twice. - Zero resume (handler returns without calling resume) — abort/escape semantics.
A handler that compiles but does the wrong thing under multi-shot is a substrate bug, not a Koka bug. Open a Blockers entry, do not fix the substrate from this loop.
Ground rules (hard)
- Scope: only
lib/koka/**andplans/koka-on-sx.md. Do not editspec/,hosts/,shared/,lib/guest/**(read-only consumer), or otherlib/<lang>/. - Consume
lib/guest/wherever it covers a need (lex, pratt, match). Hand-rolling defeats the validation goal. - Do not patch the substrate from this loop. If
cek-resumeis misbehaving, write the failing test, open a Blockers entry, stop. The fix lives inspec/evaluator.sxand is not your scope. - Effect types are deferred entirely. Track effects at runtime only — an unhandled effect at the top level raises a runtime error, not a type error. No row polymorphism.
- NEVER call
sx_build. 600s watchdog will kill you. Ifsx_server.exeis broken, add a Blockers entry and stop. - SX files:
sx-treeMCP tools ONLY.sx_validateafter every edit. NeverEdit/Read/Writeon.sx. - Worktree: commit, then push to
origin/loops/koka. Never touchmain. Never push toarchitecture. - Commit granularity: one feature per commit. Short factual messages:
koka: state effect handler + 4 tests. - Plan file: update Progress log + tick boxes every commit.
- If blocked for two iterations on the same issue, add to Blockers and move on.
Koka-specific gotchas
- Effects are dynamically scoped, not lexically. When an effect operation
op()fires inside a function called from inside a handler, the call-time handler stack matters, not the definition-time environment. This is the opposite of normal lexical scope. SX'sperform/cek-resumeis dynamically scoped by construction — that's why the mapping works. - Handler installation is
with handler { body }, not a function call. The handler is installed for the dynamic extent ofbody. Implement as awith-handlerevaluator form, not as a lambda taking a body argument — the body must run inside the handler frame, not be passed into a handler-creating call. resumeis bound by the handler clause, not globally. Each operation clauseop(args) -> bodyexposesresumeas a callable insidebody.resume(v)continues the suspended computation withvas the value of the originalop()call. Implement by capturing the continuation at theperformpoint and binding it toresumein the clause's env.return(x) -> eis the value clause. When the handled body finishes without firing the effect, its value is bound toxin this clause and the result ise. If absent, default isreturn(x) -> x. This is not the same as a normal function return.- Tail-resumptive handlers should be optimisable. Most practical handlers (
state.get() -> resume(s),console.println(s) -> { print(s); resume(()) }) resume exactly once in tail position. The CEK should be able to detect this and skip the continuation capture entirely. If you discover the optimisation is missing, that's substrate work — open a Blockers entry, do not implement here. type maybe<a> { Nothing; Just(value: a) }. Map directly to SX(define-type maybe (Nothing) (Just value)). Polymorphism erased at runtime — the type parameter is for documentation/future inference, not for evaluation.- Pipe
|>is reverse application.x |> f |> g=g(f(x)). Parse as left-associative infix at low precedence. - No type inference, no exhaustiveness checking. Phase 2 match falls back to runtime
match-failureexception on no clause hit. Don't try to verify exhaustiveness statically.
General gotchas (all loops)
- SX
do= R7RS iteration. Usebeginfor multi-expr sequences. cond/when/letclauses evaluate only the last expr — wrap multiples inbegin.env-bind!creates a binding;env-set!mutates an existing one (walks scope chain).sx_validateafter every structural edit.list?returns false on raw JS Arrays — host data must be SX-converted.- Shell heredoc
||gets eaten — escape or usecase.
Style
- No comments in
.sxunless non-obvious. - No new planning docs — update
plans/koka-on-sx.mdinline. - Short, factual commit messages (
koka: multi-shot choose + 3 tests). - One feature per iteration. Commit. Log. Push. Next.
Go. Run the pre-flight check. If lib-guest or the ADT primitive is not in place, stop and report. Otherwise read the plan, find the first unchecked [ ], implement it.