spec: loop-recur — standalone strict iteration construct
Brainstorm milestone spec for first-class additive Term::Loop / Term::Recur (Approach A). De-bundled from the reverted Iteration-discipline milestone: no structural-guardedness checker, no Diverge effect — the half-enforced-dichotomy failure that sank the original bundle is explicitly out of scope. recur has no non-tail spelling (structural jump, by-construction stack safety). verify_tail_positions left byte-unchanged; new private verify_loop_body pass owns recur-tail-position checking. Feature acceptance: all 3 clauses pass. Grounding-check Step 7.5: PASS, 9 ratified load-bearing assumptions. User-approved.
This commit is contained in:
@@ -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<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 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<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/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.
|
||||
Reference in New Issue
Block a user