diff --git a/docs/specs/2026-05-17-loop-recur.md b/docs/specs/2026-05-17-loop-recur.md new file mode 100644 index 0000000..9234b8b --- /dev/null +++ b/docs/specs/2026-05-17-loop-recur.md @@ -0,0 +1,316 @@ +# Standalone `loop` / `recur` — Design Spec + +**Date:** 2026-05-17 +**Status:** Draft — awaiting user spec review +**Authors:** Brummel (orchestrator) + Claude + +## Goal + +Add `loop` / `recur` to AILang as a **standalone, strictly additive** +iteration surface that lowers to the same back-edge `tail-app` +already produces, with one closed rule: `recur` is valid only in +tail position of its enclosing `loop`; anything else is a compile +error. + +This is **not** the reverted Iteration-discipline milestone. That +milestone bundled `loop`/`recur` (it.1) with a structural-recursion +guardedness checker + the `Diverge` effect (it.2) and a destructive +`tail-app` retirement + total-by-construction thesis (it.3); the +bundle was reverted on 2026-05-16 because the totality dichotomy +made the maximally-LLM-natural `build(d:Int)=Node(1,build(d-1), +build(d-1))` inexpressible, and because — per the revert spec — +"`loop`/`recur` (it.1) was never run through the feature-acceptance +gate for LLM-naturalness in its own right; it rode in on the +thesis." This spec does exactly that gate, standalone. + +**Deliberate boundaries (in scope by their absence):** + +- **No totality claim.** A `loop` with no non-`recur` exit branch + is legal and runs forever, exactly like `while(true)`. `loop`/ + `recur` asserts nothing about termination. This is the precise + difference from the reverted milestone. +- **No guardedness pass.** `verify_structural_recursion`, + `term_contains_loop`, the `NonStructuralRecursion` diagnostic are + **not** part of this milestone. +- **No `Diverge` effect.** No effect is raised by `loop`/`recur`. + `Diverge` stays reserved-and-unimplemented exactly as today. +- **`tail-app` untouched.** `tail-app` / `tail-do` and + `verify_tail_positions`' tail-app role are byte-unchanged. + `loop`/`recur` coexists with them; mutual recursion and tail + calls into a *different* function (which `recur` cannot express) + continue to go through `tail-app`. No retirement, now or implied. + +## Feature-acceptance verdict (the gate the revert spec demanded) + +- **Clause 1 (an LLM author produces it).** Satisfied and + non-discriminating — the criterion itself states an LLM reaches + for every construct native to its imperative training + distribution. The evidence is the worked `.ail` in §"Concrete + code shapes", not a prose assertion. +- **Clause 2 (measurably improves correctness OR removes + redundancy).** Passes on both arms. *Correctness:* today + stack-safety hinges on an author-asserted tail mark on a + hand-written self-recursive helper; a forgotten/incorrect mark + silently degrades to a stack-growing call — correct on small + input, overflow on deep input, an input-size-dependent silent + failure. Strict `recur` turns a non-tail back-jump into a compile + error: an entire silent-failure class becomes a compile-time + diagnostic. *Redundancy:* removes the separate helper fn, the + invented name, and the explicit threading of all loop state as + parameters. +- **Clause 3 (reintroduces no bug class a core constraint + eliminates).** `recur` rebinds loop parameters to *new values* + per iteration — not mutation, no aliasing, no cycle; Decision 10 + intact. `tail-app` and Decision 8 byte-unchanged. Approach A + keeps `loop`/`recur` a first-class node, so the round-trip + invariant holds and pre-existing canonical-JSON hashes stay + bit-stable (additive, skip-serialized). The clause-3 failure that + sank the *bundle* was it.2's half-enforced totality dichotomy (a + checker that rejected bare non-structural recursion while + grandfathering `tail`-marked calls — not a stable additive + stopping point). Strict standalone `loop`/`recur` has no such + disease: its only rule is closed and complete ("`recur` must be + in tail position"), rejects no pre-existing code, grandfathers + nothing, and depends on no future destructive iteration. + +## Architecture + +Three strictly-additive AST nodes, mirroring the *shape* the +reverted it.1 used, **minus** every it.2 / it.3 element: + +- `Term::Loop { binders: Vec, body: Box }` +- `Term::Recur { args: Vec }` +- `struct LoopBinder { name: String, ty: Type, init: Term }` + +Form-A surface: `(loop (NAME TYPE INIT) ... BODY)` and +`(recur ARG ...)`. The binder triple deliberately mirrors mut's +`(var NAME TYPE INIT)` — same author-facing shape, no new form +vocabulary. `loop` is an expression; its value is `body`'s value +on the iteration that exits via a non-`recur` branch. `recur` +re-enters the lexically innermost enclosing `loop`, rebinding its +binders positionally; `recur` itself has no value type (it does +not fall through — it transfers control), so its synthesised type +is a fresh metavar that unifies with whatever sibling branch the +enclosing `if`/`match` requires (this resolves the same open risk +it.1 recorded: `recur` appears in `if` branches that must unify +with the sibling type). + +## Concrete code shapes + +### The AILang program (clause-1 evidence — the headline) + +What an LLM author writes for "sum 1..n" **with** `loop`/`recur`: + +``` +(fn sum_to + (type (fn-type (params (con Int)) (ret (con Int)))) + (params n) + (body + (loop (acc Int 0) (i Int 1) + (if (app > i n) + acc + (recur (app + acc i) (app + i 1)))))) +``` + +What the same author must write **today** (status quo it replaces) +— a separate helper, three threaded params, and a self-call that +*must* be tail-marked or it silently overflows on large `n`: + +``` +(fn sum_to_go + (type (fn-type (params (con Int) (con Int) (con Int)) (ret (con Int)))) + (params acc i n) + (body (if (app > i n) + acc + (app sum_to_go (app + acc i) (app + i 1) n)))) +(fn sum_to + (type (fn-type (params (con Int)) (ret (con Int)))) + (params n) + (body (app sum_to_go 0 1 n))) +``` + +The clause-2 improvement is visible in the diff between the two: +one construct vs. helper+threading, and a structurally-guaranteed +back-jump vs. an author-asserted mark. + +### Must-fail fixture (clause-3 discriminator — correct behaviour +is rejection) + +`recur` outside tail position must fail to typecheck: + +``` +(fn bad_recur + (type (fn-type (params (con Int)) (ret (con Int)))) + (params n) + (body + (loop (i Int 0) + (app + 1 (recur (app + i 1)))))) ; recur is an argument to +, + ; NOT tail → RecurNotInTailPosition +``` + +Expected: `ail check` exits 1 with diagnostic code +`recur-not-in-tail-position`. The other three negatives +(`recur` with wrong arity / wrong arg type / outside any `loop`) +each fire their own code. + +### Implementation shape (secondary — supporting, not the point) + +Before → after, load-bearing changes only; exact bytes/lines are +the planner's job. + +`crates/ailang-core/src/ast.rs` — `Term` enum gains two variants; +serde skip-serializes nothing new on *existing* variants, and the +new variants are absent from every pre-existing fixture, so their +canonical JSON is unchanged (additive-extension pattern, same as +mut.1 / iter13a / iter18e): + +``` +// before: Term has no Loop/Recur +// after: +Term::Loop { binders: Vec, body: Box } // "t":"loop" +Term::Recur { args: Vec } // "t":"recur" +struct LoopBinder { name: String, #[serde(rename="type")] ty: Type, init: Term } +``` + +`crates/ailang-check/src/lib.rs` — a **new private** pass +`verify_loop_body` checks `recur`-in-tail-position; the existing +`pub fn verify_tail_positions` signature and its `tail-app` role +are **unchanged** (the reverted it.1 wrongly repurposed it; here it +is left alone and a sibling pass is added instead): + +``` +// before: verify_tail_positions only (tail-app role) +// after: verify_tail_positions UNCHANGED +// + fn verify_loop_body(...) // new, private; recur tail-position only +``` + +`crates/ailang-codegen/src/lib.rs` — a loop-header basic block, +one `phi` per binder seeded from the binder inits, and `recur` +lowered to a back-edge `br` updating the phis. The existing +tail-driven `block_terminated` seam is **extended** with a parallel +setter for the back-edge (it.1's shape) — `tail-app`'s use of the +seam is unchanged. + +## Components + +1. **Surface** (`crates/ailang-surface`): `parse_loop`, + `parse_recur`, print arms, keyword entries, EBNF block; + `crates/ailang-core/specs/form_a.md` grammar entries. +2. **Core** (`crates/ailang-core`): the two `Term` variants + + `LoopBinder`, additive serde, serde round-trip unit tests; + schema-drift / schema-coverage / spec-drift / carve-out-inventory + anchors extended with the `Term::Loop → "loop"` / + `Term::Recur → "recur"` entries (the planner re-derives the exact + `EXPECTED` carve-out delta from the current tree — no count is + hard-coded here). +3. **Prose** (`crates/ailang-prose`): read + rebuild arms for both + variants (lockstep with free-var / subst walkers). +4. **Check** (`crates/ailang-check`): `Term::Loop` binder typing; + `Term::Recur` positional arity + per-arg type unification against + the enclosing loop's binder types via a `loop_stack`-style frame + threaded exactly as mut.2's `mut_scope_stack`; the new private + `verify_loop_body` for tail-position. Four `CheckError` variants + (see §Error handling). No guardedness pass. +5. **Codegen** (`crates/ailang-codegen`): loop-header block, per- + binder `phi`, `recur` back-edge `br`, the parallel + `block_terminated` setter, lambda-boundary loop-frame + save/restore (mirroring mut.3's lambda-boundary handling). +6. **Walkers**: additive `Term::Loop`/`Term::Recur` arms in + `desugar.rs`, `lift.rs`, `mono.rs`, `linearity.rs`, + `uniqueness.rs`, `reuse_shape.rs`, `pre_desugar_validation.rs`, + and the `builtins.rs` test helpers (~25 sites — the it.1 blast + radius, additive). + +## Data flow + +`.ail` → `ailang_surface::parse` (`Term::Loop` / `Term::Recur` +nodes created) → typecheck (binder typing → `recur` arity/type +unification → `verify_loop_body` tail-position check) → +desugar / lift / mono (additive walker arms, no rewrite of +loop/recur) → `ailang-codegen` (loop-header + per-binder phi + +back-edge br) → LLVM text → `clang -O2`. The `tail-app` path runs +alongside, byte-unchanged; there is no interaction between the two +back-edge mechanisms. + +## Error handling + +Four `CheckError` variants, all from the reverted it.1, **none** +from it.2: + +- `RecurOutsideLoop` — `recur` with no enclosing `loop`. +- `RecurArityMismatch` — `recur` arg count ≠ enclosing loop's + binder count. +- `RecurTypeMismatch` — a `recur` arg's type ≠ the corresponding + binder's type. +- `RecurNotInTailPosition` — `recur` appears anywhere other than + the tail position of its enclosing `loop` body. + +Bracket-`[code]`-free `Display` (the F2 convention, consistent with +the mut-* variants). Each gets a `code()` arm; `ctx()` arms only +where a dedicated context string adds value (arity/type variants), +otherwise the catch-all — the planner determines the exact split +from the current `lib.rs` ctx structure. Explicitly **excluded**: +`NonStructuralRecursion` (that was the it.2 totality enforcement). +`UndeclaredEffect` is unchanged — `loop`/`recur` raises no effect. + +## Testing strategy + +- **Positive E2E.** A `sum_to`-class fixture builds and runs to the + correct printed value; plus a deep-`n` variant that, under the + status-quo hand-written form with a *forgotten* tail mark, would + overflow — here safe by construction (this is the clause-2 + correctness claim made executable). +- **Negative fixtures.** Four `.ail.json` fixtures, one per + `CheckError` code, each asserting `ail check` exits 1 with exactly + that code (`.contains(code)`, non-vacuous). The + `RecurNotInTailPosition` fixture is the §"Concrete code shapes" + must-fail program. +- **Round-trip.** Every new fixture passes the existing + text→AST→JSON→AST→text byte-isomorphism gate + (`ailang-surface/tests/round_trip.rs`) — this is the concrete + proof Approach A preserves the Roundtrip Invariant (a desugaring + approach would fail exactly here, which is why it was rejected). +- **Hash stability.** A pin asserting a representative pre-existing + fixture's canonical-JSON bytes / content hash are unchanged by + the schema extension (same pattern as the mut.1 / iter13a / + iter18e hash pins). +- **Schema-drift.** `design_schema_drift.rs` / `schema_coverage.rs` + / `spec_drift.rs` / `carve_out_inventory.rs` green with the new + anchors. +- **`tail-app` non-regression.** Existing `tail-app` IR-snapshot + and e2e fixtures byte-identical (proves coexistence, not + replacement). +- **Full suite.** `cargo test --workspace` green. + +## Acceptance criteria + +- `loop` / `recur` parse, print, and round-trip; `Term::Loop` / + `Term::Recur` / `LoopBinder` exist as additive nodes with + canonical JSON `"t":"loop"` / `"t":"recur"`. +- The four `Recur*` codes fire point-exactly on their negative + fixtures; `recur` outside tail position is a compile error. +- An infinite `loop` (no non-`recur` exit) typechecks and compiles + (no termination claim is made or enforced). +- `tail-app` / `tail-do` / `verify_tail_positions` / Decision 8 are + byte-unchanged; no `Diverge`, no `verify_structural_recursion`, + no `NonStructuralRecursion`. +- Pre-existing canonical-JSON hashes are bit-stable; the Roundtrip + Invariant holds for loop/recur-bearing modules. +- `cargo test --workspace` green; milestone-close `audit` bench + baseline pristine (additive surface; any non-pristine result is a + defect, not a ratifiable delta — though a check-time feature tax, + as seen with mut-*, may be ratified with a paired baseline update + if localised and non-hot-path). + +## Cross-references + +- `docs/DESIGN.md` — Decision 8 (verified tail calls; unchanged), + Roundtrip Invariant, Feature-acceptance criterion, §"Data model". +- `docs/specs/2026-05-16-iteration-discipline-revert.md` — why the + bundle was reverted; this spec is the de-bundled, gate-passed + re-attempt of its it.1 core only. +- `docs/specs/2026-05-15-iteration-discipline.md` — superseded + bundle spec; its it.1 surface is the *shape* reference (its it.2 / + it.3 content is explicitly out of scope here). +- `docs/specs/2026-05-17-llm-surface-discipline.md` §6.2 — the + principles entry this milestone discharges.