The evaluator: a CEK machine over computation closures

The evaluator is one abstract machine, core/src/evaluator/machine.rs. Its state is a focus and a stack: Machine { focus: Focus, stack: Vec<Frame> }, stepped against the store &mut Shell and the run’s &Mooring. Nothing else in the crate constructs a state or sees the stack; the module’s doors are evaluate(comp, env, …) — inject ⟨M, E⟩ over the empty stack and step until it is empty — apply(f, args, …), the same from a closed value meeting arguments, and its argument-free twin force(v, …). All return Settled<Value>.

What is in focus is a computation closure. Focus::Eval { comp, env } pairs a computation with the whole environment it was reached in: transient — never stored, sent, or kept alive by a binding — and so a type apart from Closure, the thunk value’s. Focus::Return(t) is a terminal meeting the frame above; Focus::Halt(Break) is a signal climbing the stack. A terminal has two shapes, Terminal::Value(v) and Terminal::Lambda { comp, env } — a λ is canonical at A → C and is never a value, so a Lam in focus returns as Lambda and the frame above decides: Apply consumes it by β, a computation-holed frame (Redirect, Unmask, Within, Grant, Try) passes it through, a value-holed frame (To, Capture, Guard, Cleanup, Audit, Gather) halts with the bare-lambda error — unreachable for a checked program, since the checker η-expands every arrow-typed computation into a thunked λ (SPEC §17.8). Decode has no frame: the kernel’s decode takes a value, so it closes and reads it inline in step_eval, and the checker reaches it through a bind over Capture rather than nesting the two.

One thunk value. Value::Thunk(Closure) is ⟨M, ρ|occ(M)⟩, built only by Closure::new, which restricts the environment to occ, read off the ThunkNode that owns M (Val::Thunk(Arc<ThunkNode>)) — occ(M) is computed once, by Node::new, where the node is built, not walked at every capture (a-closure-keeps-only-what-it-mentions). force of it puts its computation and environment in focus and pushes nothing, so force(thunk M) = M and a forced block’s cd persists exactly as a lambda’s does (scoping). A literal !{ … } takes that equation as a rule (U-β): Force(Val::Thunk(node)) puts node.shape() in focus under the current environment, closing nothing (Machine::force_val). Every form that suspends a command — if, case, try, ?, guard, within, grant — holds its arms as thunks and forces the one it chooses the same way: if true $aaah else $baaah runs $aaah, and case pushes an Apply with the variant’s payload before forcing the arm. Whether a thunk “is a lambda” is read off the body’s shape by Comp::arrow, never stored.

A list, record or map literal is a value closure too. form(val, env, sig) (core/src/evaluator/val.rs) is CBPV’s one-step rule for every value: a constant is itself, a name is lookup(name, env, sig), a variant forms its payload, thunk M is Closure::new, and a plain literal is List::literal or Map::literal — ⟨V, ρ|occ(V)⟩ — unless one of the names it directly mentions (through variant payloads and nested literals, never inside a thunk) is answered only by Σ: a Literal’s inspection reads ρ alone, with no Σ fallback, so that name could never be read back out, and form builds the literal eagerly instead, forming each element with sig. Inspecting a Literal’s element is the distributive law, one layer: a name is lent from ρ, a constant is built, and a nested literal or thunk closes over the same ρ — two refcount bumps, not a second restriction.

step is the tables. Machine::step dispatches on the focus: eval_rules has one match arm per CompKind (the ξ-rules: Return closes its value, Bind pushes To, App closes its arguments then pushes Apply and evaluates the head, Rec unfolds the n-ary group, Exec classifies the head through the lexical environment, Pipeline launches and joins its node, the seven handler forms close their operands, install, push their frame and force the body …); Assemble is the one rule that does O(data) work over what looks like value syntax: a list, record, or map literal with a spread or a computed key elaborates to it rather than to Return, and evaluator/assemble.rs builds the collection (evaluator) — a plain literal, with none of those, stays a Return and closes for free; step_return and step_halt have one arm per Frame — the two columns of the frame table. No arm calls another arm; no arm loops.

A rule cannot leave unlocated. Every rule returns Settled<Focus> (eval_rules, and step_return, step_halt, beta, apply_rule and force alike), so each raises with ? rather than by building a Focus::Halt of its own; step folds the Err into Focus::Halt once, and step_eval first stamps it with comp.span. There is exactly one exit, so a raising rule is stamped with the span of the node it is the rule for, and no arm can be written that skips the stamp. step_case and step_exec are rules under the same discipline. (Before this shape, a bare return in the Rec arm bypassed the stamp and cancelling a recursive definition rendered without a caret.)

Pushing is a type. Machine::reserve is the stack cap, checked before any effect, and returns the Slot that holds the stack’s only push; a rule cannot push without having asked. Frame::abandon is the one undo for the frames whose effect is only undone (Unmask, Within, Grant, and Audit on an escape), used by the rules and by the panic walk alike; on Gather it restores the cradle and stops the brood without waiting.

To holds its environment, which is what makes extent structural. M to x. N pushes To { bind, env: E } before M runs; when M returns a value, E[x ↦ v] is built from the frame’s own E, so x scopes over N and nothing else whatever M did. It is the only frame with syntax to close over, so the only one carrying an Env. Cleanup is the kernel’s to _ with a settled rest: it drops the cleanup’s value and resumes the outcome it holds (βguard-val). It also holds the cancel scope Guard displaced when it shielded the cleanup (Shell::shield), restored on pop and on abandon, so the finaliser and the re-halt run under the shield (a-cleanup-is-shielded-within-its-grace). Frames hold Arcs into the IR, never cloned IR, and undo tokens, never a Context clone: Redirect(Box<RedirectState>) tears down and settles its writes, the one interpreter of a redirect list (stdin, stdout, stderr open in that order; a write is observed when the body settles, carrying its target before and after), Within(WithinUndo) restores env overrides, the whole cwd cell and handlers, Grant pops the capability stack, Unmask restores the masked handler, Audit closes its trail scope and restores the capture policy; Try holds only its handler. Gather { brood, prev } holds the brood its body’s births enrol in and the cradle it displaced: on return it restores the cradle and settles the brood by exit_brood — the exit rule a worker’s base shares — and on a halt it restores the cradle and ends the brood within the cleanup grace (a-worker-ends-with-its-children). Frame is at most 128 bytes (asserted at compile time; Redirect and Unmask are boxed).

Capture holds the sink it replaced. cap M pushes a fresh buffer as shell.io.stdout and keeps the previous sink in the frame. A discarded statement writes to stdout, which is wherever the run’s stdout is, so inside a capture it is the buffer. On return the frame restores the sink and yields the buffer as Bytes, ignoring the body’s value (cap : F^w Unit → F Bytes); a buffer past SINK_BUFFER_CAP halts (capture_overflowed). On a halt it flushes what the body wrote to the sink it replaced (Shell::write_sink) and propagates the halt. Which computations a value demand wraps in it is decided by the checker, not here (graded-f).

a ? b ? c has no frame of its own: it elaborates to nested try (kernel _؟_, CK.Derived), right-associated so the last arm stays in tail position.

Tail calls push nothing. β binds the parameter into the closure’s environment and puts the body in focus; an Apply frame is pushed only when arguments remain (currying). So a call in tail position costs no frame, and depth is simply stack.len(). reserve is the cap — session.stack_limit, default 100 000 frames, the --recursion-limit knob — and every pushing rule calls it before any effect (sink swap, redirect entry, grant push), so a refused push leaks nothing; push itself cannot fail.

Recursion is rec, n-ary. Rec { group: Arc<GroupNode>, index } reads occ(g) off group — computed once, at the node’s build, over every member’s body — and restricts ρ to it: one restrict call, whose result every sibling’s thunk shares in this unfold. The member in focus binds to comp itself, Arc::cloned, not rebuilt; every other member’s thunk is a fresh Rec node over the same group (rec_node). The n bindings go into ρ|occ(g) with one Env::extend. A recursive reference forces its name, which re-enters Rec over the forced closure’s own environment — already ρ|occ(g), so restrict answers the identity and every later unfold shares that one root. Bodies are never rewritten; a group of one is Levy’s rec f. M, and binds its own member to the node already in focus, allocating nothing. Cancellation is polled here and at Bind, App, Exec advance and β, so let f = { !f }; !f is interruptible.

The environment is a map, and it is not the store. Env (core/src/types/env.rs) is ρ alone: a sorted array of at most SMALL (8) bindings, a persistent hash map past it, chosen by size and invisible to its readers. bind/extend produce a fresh environment that disturbs none a closure captured; clone is O(1); restrict narrows it to a closure’s names, identity when nothing is dropped. Σ — the language natives and the frozen prelude — is Signature (core/src/types/signature.rs), one per shell, never part of any environment; crate::types::lookup(name, env, sig) reads ρ, then Σ’s prelude, then Σ’s natives, and every rule that resolves a name (Val::Variable in form, Exec’s bare-head lookup in command_call::resolve) goes through it. The store is everything else on Shell: sig, sinks, the dynamic Context (grants, handlers, env overrides, cwd, args, modules, hooks), the trail, workers, leases. Context is read in O(1) by capability checks and command dispatch and changed only by frames holding their own undo; neither it nor Σ is ever part of a closure (shell-state).

The top level is a sequence of phrases (core/src/evaluator.rs, run_phrases). A Toplevel is Phrase::{Define, Run}; each phrase is a closed computation over the session environment shell.env, and a Define extends that environment for every phrase after it, in this run and every later one — installed as it lands, so a use in the next phrase sees it, and a run that halts has installed exactly the Defines that ran. A block is a right-nested Bind chain, a; b being a to _. b, so a let inside a block scopes over the rest of the block by structure. run_phrases takes a Mode — Session, Local, Module, Prelude — which alone decides leases.

Boundaries. Three things start a fresh machine over the empty stack: a run-door phrase, a worker thread (a spawn or watch), and a pipeline stage thread (runtime/pipeline/thread.rs). The spawn form pushes no frame: its rule forms the operands and births the worker in one step (spawn_form). A gather is a frame like any handler’s, not a boundary: its body runs on the same machine, and only the births inside it start machines of their own. A native that applies a user function — the collection combinators, hook dispatch — runs a nested machine on the host stack through machine::apply; NESTED_MACHINE_LIMIT (calibrated by nested_machines_fit_a_worker_stack on a 2 MiB thread, a quarter of the 8 MiB Shell::spawn_thread gives a worker) caps that nesting with a clean error. No native reads a lexical environment: help and explain reflect on the session.

Pipes are nodes between machines ([[internals/pipeline-execution|pipeline execution]]). A multi-stage pipeline is a configuration: an external stage is a process in the pipeline’s group, and a ral-written stage is a thread (launch_thread_stage via Shell::spawn_thread) whose shell starts from the parent’s session and runs machine::evaluate(comp, env, …) — the stage’s subterm under the node’s own environment — over the empty stack. The parent’s Pipeline rule holds a PipeNode — the process group and the running stages, which it launches and joins (collect, then finish) in one step: no frame, because nothing runs beneath the node; the outcome climbs the parent’s frames like any other rule’s terminal. No frame ever crosses: not to a stage, whose stack is empty by construction, nor to a sealed child engine, which receives the engine seed’s env, context and terms (core/src/seed.rs) — one environment, ρ alone, interned by its allocation’s identity; Σ never crosses, so the receiver answers a decoded closure’s Σ names from its own.

Panics and cancellation. evaluate/apply wrap the step loop in catch_unwind; on a panic every frame is abandoned top-down — sinks restored, redirects torn down, trail scopes closed, undo applied — and the run door restores its checkpoint (env, context), so a panic commits nothing. The depth counter is lowered on both paths.

See also cbpv, scoping, control-operators, the-evaluator-steps-closures; code maps evaluator, shell-state, runtime. The formal account is docs/SPEC.md §17.8. The Agda kernel (dev/agda) is a substitution-based CK machine and stays one: a closure machine is a refinement to be proved against it, not its foundation.