rose-ash/plans/koka-on-sx.md

Koka-on-SX: Koka on the CEK/VM

Implement a Koka interpreter on SX. The unique angle: Koka's algebraic effects and handlers map directly onto SX's perform/cek-resume machinery — this is the language that will stress-test whether SX's effect system is principled enough, and expose any gaps. Every other language in the set works around effects ad-hoc; Koka makes them the primary abstraction.

End-state goal: core Koka programs running on the SX CEK evaluator, with algebraic effect handlers wired through perform/cek-resume. Not a full Koka compiler — no type inference, no row-polymorphic effect types, no LLVM backend — but a faithful runtime for idiomatic Koka programs.

What Koka adds that nothing else covers

• Structured effect declarations: effect state<s> { fun get() : s; fun set(s) : () } — named, typed effect operations, not just untyped perform tokens
• Resumable handlers: handler { return(x) -> x; get() -> resume(0); set(x) -> resume(()) } — multi-shot continuations, handlers as first-class values
• Effect polymorphism: functions declare their effect set (a -> <state<int>,console> b) — exposes whether SX can track which effects are in scope
• Tail-resumptive handlers: most practical handlers resume exactly once, which should be optimisable — tests whether the CEK machine can detect and collapse this
• Algebraic data types as the foundation: type maybe<a> { Nothing; Just(value: a) } — exercises the Phase 6 ADT primitive directly

Ground rules

• Scope: only touch lib/koka/** and plans/koka-on-sx.md. Do not edit spec/, hosts/, shared/, or other lib/<lang>/.
• Shared-file issues go under "Blockers" below with a minimal repro; do not fix here.
• SX files: use sx-tree MCP tools only.
• Architecture: Koka source → Koka AST → interpret directly via CEK. No separate Koka evaluator — host the semantics in SX, run on the existing CEK machine.
• Effect types: defer type inference entirely. Track effects at runtime only — an unhandled effect at the top level raises a runtime error, not a type error.
• Commits: one feature per commit. Keep ## Progress log updated and tick boxes.

Architecture

Koka source text
    │
    ▼
lib/koka/tokenizer.sx   — keywords, operators, indent-sensitivity, type-level syntax
    │
    ▼
lib/koka/parser.sx      — Koka AST: fun, val, effect, handler, with, match, resume,
    │                     return clause, ADT definitions, basic type expressions
    ▼
lib/koka/eval.sx        — Koka AST → CEK evaluation via SX primitives:
    │                     ADT (define-type/match from Phase 6)
    │                     Effects (perform/cek-resume from spec/evaluator.sx)
    │                     Coroutines optional (Phase 4 primitives)
    ▼
SX CEK evaluator (both JS and OCaml hosts)

Key semantic mappings:

Koka construct	SX mapping
fun f(x) body	(define (f x) body)
val x = expr	(let ((x expr)) ...)
effect E { fun op() : t }	register effect tag E/op in effect env
op() inside handler scope	(perform (list "E" "op" args))
handler { return(x)->e; op()->resume(v) }	(guard ...) + cek-resume
with handler { body }	install handler for duration of body
match x { Nothing -> e1; Just(v) -> e2 }	SX (match x ...) via Phase 6 ADT
type maybe<a> { Nothing; Just(value:a) }	(define-type maybe (Nothing) (Just value))
resume(v) in handler	(cek-resume k v) where k is captured continuation
return(x) -> expr	final-value clause when no effect fires

Koka semantics in brief

Effects and handlers

effect console
  fun println(s : string) : ()

fun greet(name : string) : <console> ()
  println("Hello, " ++ name)

fun main()
  with handler
    return(x) -> x
    println(s) -> { print-string(s ++ "\n"); resume(()) }
  greet("world")

• effect console declares an effect with one operation println
• greet uses console — any call to println inside will look up the nearest enclosing handler
• with handler { ... } installs a handler; resume(()) continues the suspended computation

Multi-shot resumption

effect choice
  fun choose() : bool

fun xor(p : bool, q : bool) : <choice> bool
  val a = choose()
  val b = choose()
  (a || b) && !(a && b)

fun all-results()
  with handler
    return(x) -> [x]
    choose() -> resume(True) ++ resume(False)
  xor(True, False)
// => [True, True, False, True]

This is the test that exposes whether cek-resume supports multi-shot (calling the same continuation twice). SX's delimited continuations do support this — Koka will verify it end-to-end.

Roadmap

Phase 1 — Tokenizer + parser (core expressions)

• Tokenizer: keywords (fun, val, effect, handler, with, match, return, resume, type, alias, if, then, else, fn), operators (++, ->, |>, :, <, >, ,), identifiers, numbers, strings, booleans
• Parser — expressions: - literals: int, float, bool (True/False), string - val x = e bindings - fun f(x, y) body definitions - if c then e1 else e2 - match x { Pat -> e; ... } - lambda fn(x) -> e - function application f(x, y) - infix operators: ++, +, -, *, /, ==, !=, <, >, &&, || - pipe |>: x |> f = f(x)
• Tests: lib/koka/tests/parse.sx — 40+ parse round-trip tests

Phase 2 — ADT definitions + match

• Parser: type name<a> { Ctor1; Ctor2(field: t); ... } declarations
• Eval: map to SX define-type + match (requires Phase 6 primitives)
• Built-in: maybe<a> (Nothing / Just), result<a,e> (Ok / Error), list<a> (Nil / Cons)
• Tests: ADT construction, matching, nested patterns — 25+ tests

Phase 3 — Core evaluator

• koka-eval entry: walks Koka AST, evaluates in SX env
• Arithmetic, string ++, comparison, boolean ops
• val/let binding
• Function definitions and application (first-class functions)
• if/then/else
• match with constructor, literal, variable, wildcard patterns
• Basic list ops: map, filter, foldl, length, head, tail
• Tests: lib/koka/tests/eval.sx — 40+ tests, pure expressions only

Phase 4 — Effect system

• Effect declaration: (koka-declare-effect! "console" (list "println")) registers operations in a global effect registry
• Effect operation call: when println(s) is evaluated inside a handler scope, emit (perform (list :effect "console" :op "println" :args (list s)))
• Handler installation: with handler { return(x)->e; println(s)->resume(v) } installs a guard-like frame that catches perform signals matching the effect, binds arguments, and exposes resume as a callable that invokes cek-resume
• resume(v): calls (cek-resume captured-k v) where captured-k is the continuation captured at the perform point
• return(x) -> e clause: handles the normal return value when no effect fires
• Tests: lib/koka/tests/effects.sx — 30+ tests: - basic handler (state, console, exception) - unhandled effect → runtime error - nested handlers (inner shadows outer) - multi-shot resumption (choice effect — the key test) - tail-resumptive handler (resumes exactly once — verify no extra allocation)

Phase 5 — Standard effect library

• console effect: println, print, readline (mock)
• exn effect: throw, catch wrappers
• state<s> effect: get, set, modify
• async effect: await mapped to SX perform IO suspension
• Tests: programs using each stdlib effect — 20+ tests

Phase 6 — Classic Koka programs as integration tests

• counter.koka — stateful counter via state effect
• choice.koka — multi-shot choice generating all results
• iterator.koka — yield-based iteration via a custom effect
• exception.koka — structured exception handling
• coroutine.koka — producer/consumer via two interleaved effects
• Each as a self-contained test in lib/koka/tests/programs.sx

Key blockers / dependencies

• Phase 6 ADT primitive (define-type/match) — required before Phase 2. Track: plans/agent-briefings/primitives-loop.md Phase 6.
• Multi-shot continuations — cek-resume must support calling the same continuation multiple times. Verify with: (let ((k #f)) (perform 'x) ...) called twice. This should already work given the multi-shot delimited continuation work.
• Effect handler stack — SX's guard is not quite the right primitive for deep-handler semantics. May need (with-handler effect-tag handler-fn body) as a new evaluator form, or can be emulated via guard + perform reshaping.

Comparison to other languages in the set

Language	Effect model
Lua	none (errors only)
Prolog	none (cuts only)
Erlang	message-passing (not algebraic)
Haskell	IO monad (monadic, not algebraic)
JS	promise/async-await (one-shot)
Ruby	exceptions + fibers
Koka	algebraic effects + multi-shot handlers

Koka is the only language that uses SX's effect system as its primary computational model. It will expose whether perform/cek-resume is sufficient or needs typed effect tagging, scoping rules, and a handler stack distinct from guard.

Progress log

Newest first.

• (none yet)

Blockers

• ADT primitive (Phase 6 of primitives-loop) must land before Phase 2 starts.