AILang/docs/specs/0034-loop-recur.md

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<LoopBinder>, body: Box<Term> }
• Term::Recur { args: Vec<Term> }
• 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 (con Int) 0) (i (con 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 (con 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<LoopBinder>, body: Box<Term> }   // "t":"loop"
Term::Recur { args: Vec<Term> }                              // "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/0032-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/0031-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/0033-llm-surface-discipline.md §6.2 — the principles entry this milestone discharges.