From fda9b78e9fb26aa44ef72923a1b4dcb76e6b89c7 Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 15 May 2026 13:37:16 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20iteration-discipline=20milestone=20?= =?UTF-8?q?=E2=80=94=20structural=20recursion=20+=20named=20loop/recur;=20?= =?UTF-8?q?tail-app=20retired?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit User-approved 2026-05-15 (read, probed via the sma_factory.myc streaming analysis, no D1/D2 change requested, proceed-by-/boss). Grounding-check PASS holds: spec bytes unchanged since the Step 7.5 dispatch (the non-load-bearing "34 vs 36 tail-app sites" wording left as attested rather than re-grounding for a count the agent ruled non-defect; the 21-fixture migration unit is exact). Three ordered iterations: it.1 loop/recur additive, it.2 guardedness checker + Diverge effect, it.3 tail-app/tail-do retirement + corpus migration. --- docs/specs/2026-05-15-iteration-discipline.md | 437 ++++++++++++++++++ 1 file changed, 437 insertions(+) create mode 100644 docs/specs/2026-05-15-iteration-discipline.md diff --git a/docs/specs/2026-05-15-iteration-discipline.md b/docs/specs/2026-05-15-iteration-discipline.md new file mode 100644 index 0000000..578463d --- /dev/null +++ b/docs/specs/2026-05-15-iteration-discipline.md @@ -0,0 +1,437 @@ +# Iteration discipline — Design Spec + +**Date:** 2026-05-15 +**Status:** Draft — awaiting user spec review +**Authors:** Brummel (orchestrator) + Claude + +## Goal + +Give AILang exactly two iteration forms and remove the third: + +1. **Structural recursion** — a recursive call permitted *iff* it is + structurally guarded (recurses on a constructor-smaller component + of an algebraic argument). Under Decision 10 (ADTs are acyclic by + construction) such recursion is **total by construction**: it + terminates because the value it descends cannot be infinite. It + stays a plain call, pure, effect-free, and is the most LLM-natural + correct iteration pattern (tree / list / AST / JSON + match-and-recurse — saturated in every FP corpus). + +2. **Named `(loop …)` + `recur`** — the single explicit backward + jump, lexically scoped to an enclosing named loop. Every + repetition that is *not* structurally decreasing (accumulator + loops that are not structural, counted iteration, state machines, + streaming) is expressed here, and only here. + +3. **`tail-app` / `tail-do` — retired.** The marked-tail-call concept + (`Term::App { tail: bool }`, `Term::Do { tail: bool }`, the two + surface keywords, `musttail` lowering, `verify_tail_positions`'s + old role, `CheckError::TailCallNotInTailPosition`, Decision 8) is + removed. A call is either structural recursion (a plain call, + checked total) or it is `loop`/`recur`. No marked-tail-call + concept survives. + +This discharges fieldtest finding **F1** (mut-local's own stated +motivation — "removes friction from accumulators that today need +tail-recursive helpers" — was structurally unmet, because without a +loop the only iteration mechanism *remained* the tail-recursive +helper). It closes the "forgot to mark a recursive call as tail → +silent stack overflow" trap **completely**: a non-structural +recursion-by-call is now a named compile error, not a runtime crash. +It unifies with Decision 10: acyclic *values* and an acyclic +*implicit call graph* — the only cycle anywhere in a program is an +explicit, named, typed `loop`. Fieldtest finding **F4** (DESIGN.md +never named the tail-rec fallback) is absorbed: there is no tail-rec +fallback to document anymore. + +## Architecture + +Three coupled mechanisms, shipped as three ordered iterations. The +ordering is forced by a codegen invariant, not by convenience: + +- The codegen block-termination invariant (`emit_call` / + `emit_indirect_call` / `lower_effect_op` set + `self.block_terminated = true` only on `tail: true`; + `match_lower.rs` pre-tail-call shallow-dec and the + `lib.rs:1238–1577` branch-termination bookkeeping depend on it) + means `tail: true` currently *owns* the "this block ends with a + self-terminating control transfer" seam. `recur` is precisely a + self-terminating backward control transfer. So `recur` must occupy + that seam **before** `tail` can vacate it. + +Iteration order: + +- **it.1 — `loop`/`recur`, additive.** New `Term::Loop` / + `Term::Recur` AST + schema/canonical + Form-A surface + round-trip + fixture + checker (scope + tail-position rules for `recur`) + + codegen (loop-header block with phi binders; `recur` = backward + branch occupying a *new* block-termination seam, *alongside* the + still-present `tail` seam). Nothing is removed. End state: a + working `loop`/`recur` and `tail-app` coexist. + +- **it.2 — structural-guardedness checker + `Diverge` effect.** The + recursion-guardedness analysis + `CheckError::NonStructuralRecursion`; + and the first real implementation of the Decision-3 `Diverge` + effect (any `FnDef` whose body contains a `Term::Loop`, or calls a + `Diverge` callee, must declare `Diverge`). End state: structural + recursion is pure+total; non-structural recursion-by-call is a + compile error directing the author to `loop`; `loop`-bearing + functions carry `!Diverge`. `tail-app` still exists but is now + redundant with structural recursion. + +- **it.3 — retire `tail-app`/`tail-do` + migrate corpus.** Remove the + `tail` fields, the two keywords, the `musttail` lowering, + `verify_tail_positions`'s old role, `TailCallNotInTailPosition`, + Decision 8; rework the codegen block-termination invariant so the + seam is solely `recur`'s; migrate all 21 `.ail` fixtures / 34 + `(tail-app …)` sites. Destructive; last; depends on it.1 (loop + occupies the seam) and it.2 (the structural fixtures are *proven* + total before their redundant tail marker is stripped). + +First-iteration planner scope: **it.1** in full. + +## Components + +Per-construct touch-point set follows the mut-local milestone +template (`docs/specs/2026-05-15-mut-local.md` §Components): AST+serde +→ schema-drift + DESIGN.md §Data-model anchor → Form-A surface +parse+print → round-trip fixture → check arm + diagnostics → codegen +lower + escape → e2e example. + +### it.1 — `loop` / `recur` + +- **AST (`crates/ailang-core/src/ast.rs`).** + `Term::Loop { binders: Vec, body: Box }`; + `Term::Recur { args: Vec }`; + `struct LoopBinder { name: String, #[serde(rename="type")] ty: + Type, init: Box }`. Serde round-trip unit tests alongside + the existing `Term::Mut` ones (ast.rs ~899–940). New variants + require new anchors in `crates/ailang-core/tests/design_schema_drift.rs` + (`Term::Loop → "loop"`, `Term::Recur → "recur"`) **and** matching + §"Data model" entries in `docs/DESIGN.md` in the same iteration, or + the drift test fails. +- **Form-A surface.** No lexer change — `loop` / `recur` are + head-idents exactly as `mut` / `var` / `assign` are (confirmed: + mut.1 needed no `lex.rs` change). `crates/ailang-surface/src/parse.rs`: + EBNF block, dispatch arm, `parse_loop` / `parse_recur`, keyword + list. `crates/ailang-surface/src/print.rs`: `Term::Loop` / + `Term::Recur` arms. `crates/ailang-prose/src/lib.rs`: read + + rebuild arms (the prose projection is a lockstep member with + parse/print/serde). +- **Round-trip.** New `examples/loop_*.ail` fixture(s) — + auto-discovered by `crates/ailang-surface/tests/round_trip.rs` + (globs `examples/*.ail`); this is the round-trip gate. +- **Check (`crates/ailang-check/src/lib.rs`).** `Term::Loop` typed by + typing each binder's `init`, binding `name:ty` in a fresh frame, + typing `body` (the loop's type is the body's type, and every + `recur` site must unify with the binder vector). `Term::Recur` + arity + per-position type must match the lexically-enclosing + `Term::Loop`'s binders. New diagnostics: `RecurOutsideLoop` (a + `recur` with no enclosing `loop`), `RecurArityMismatch`, + `RecurTypeMismatch`. `recur` must be in **tail position** of the + enclosing loop body — `verify_tail_positions` is repurposed: from + it.1 on, the tail-position pass also enforces "every `recur` is in + tail position of its enclosing loop"; the diagnostic for a + mis-placed `recur` is `RecurNotInTailPosition` (it.3 removes the + old `tail-app`-flavoured role of the same pass — see it.3). The + Term-walker arms (desugar, lift, mono, the + `MutVarCapturedByLambda`-style free-var helpers) all gain + `Term::Loop`/`Term::Recur` cases (~25 walker sites, mirroring the + mut.1 blast radius). +- **Codegen (`crates/ailang-codegen/src/lib.rs`, + `escape.rs`).** `Term::Loop` → an LLVM loop-header basic block with + one `phi` per binder (entry edge = `init`, back edge = `recur` + args); body lowered with the header in scope. `Term::Recur` → + evaluate args, emit the back-edge `br` to the header, set + `self.block_terminated = true`. This is a **new** block-termination + seam, added *alongside* the existing `tail: true` seam (no existing + codegen path is modified in it.1). `escape.rs` gains `Term::Loop`/ + `Term::Recur` escape-walk arms. +- **e2e.** `examples/loop_counter.ail` (accumulator counter that + today would be a `tail-app` helper) runs and prints the same value + the equivalent tail-rec helper would. + +### it.2 — guardedness checker + `Diverge` + +- **Structural-guardedness analysis (`crates/ailang-check`).** A new + pass over each self- or mutually-recursive `FnDef` / `LetRec` + clause. No annotation — the structural argument position is found + by analysis (see Design decision **D1** for why implicit, not an + explicit `{struct}` marker). For each recursive call, the argument + in the candidate structural position must be a *proper constructor + sub-component* of the function's value at that position, established + by `match`-pattern destructuring of that parameter. Accumulator + arguments (any non-structural position) are unconstrained. + Mutual recursion uses the conservative same-ADT-family rule (D1). + Failure → `CheckError::NonStructuralRecursion` naming the + unguarded call and directing the author to `(loop …)` / `recur`. + **Transitional grandfather (it.2-only):** a recursive call that is + not structurally guarded but *is* marked `tail: true` is exempt + from the rejection. During the it.2→it.3 window a marked tail call + is precisely the author's explicit "this is intended iteration, not + accidental unbounded recursion" assertion — its original Decision-8 + purpose — so grandfathering it keeps the it.1/it.2-additive vs + it.3-destructive split honest: the 21 corpus fixtures still + type-check through it.2 unchanged. it.3 removes the `tail` field + **and** this exemption in the same destructive step, by which point + every previously-exempt site has been migrated to `loop` or to a + now-checked structural plain call. +- **`Diverge` effect (first implementation; Decision 3 was a + placeholder).** The `FnDef` effect-collection site (where raised + effects are reconciled with the declared `Type::Fn.effects` row) + gains: if the body syntactically contains a `Term::Loop`, OR calls + a function whose declared effect set contains `"Diverge"`, then + `"Diverge"` must be in the declared row, else + `CheckError::UndeclaredEffect` (existing diagnostic, existing + machinery — `Diverge` rides the same `Vec` effect row as + `IO`). Structural recursion contributes **no** effect. See **D2**. +- **DESIGN.md.** Decision 3 amended: `Diverge` is no longer "wired up + in the MVP only nominally" — it is the effect of `loop`-bearing + code. §"Feature-acceptance criterion" already carries the canonical + worked example (the iteration story) from the 2026-05-15 edit; this + iteration makes the prose match the implementation. + +### it.3 — retire `tail-app` / `tail-do` + +- **Remove.** `Term::App.tail`, `Term::Do.tail`, `is_false`; + `tail-app` / `tail-do` dispatch + `parse_tail_app` / + `parse_tail_do` + the keyword-list entries + the `print.rs` + `(tail-app …)`/`(tail-do …)` arms + the prose `"tail "` projection; + `verify_tail_positions`'s tail-app role (the pass keeps only the + `recur`-in-tail-position role from it.1); `CheckError:: + TailCallNotInTailPosition`; the `musttail` lowering in `emit_call` + / `emit_indirect_call` and the `tail call` hint in + `lower_effect_op`. DESIGN.md Decision 8 rewritten as *superseded* + (kept as a tombstone explaining why explicit tail calls were + retired — the schema-drift anchors and EBNF/jsonc blocks updated in + lockstep); the Decision-3 `Diverge` line and the EBNF + `tail-app-term` production removed. +- **Codegen block-termination rework.** The `block_terminated = true` + seam, currently set by `tail: true` and consumed by + `match_lower.rs:658–913` + `lib.rs:1238–1577`, becomes solely + `recur`'s (and the ordinary fall-through `ret`). This is the only + non-mechanical part of it.3 and the reason it.1 ships the new seam + first. +- **Corpus migration (21 fixtures / 34 sites).** + Accumulator-shaped recursions + (`bench_compute_collatz`, `bench_compute_intsum`, + `bench_latency_explicit`/`_implicit`, `bench_list_sum*`, + `rc_tail_sum_explicit_leak`, `mut_counter`, `mut_sum_floats`, + `floats_1_newton_sqrt`, `forma_1_factorial`, …) → `(loop …)` / + `recur`. Structurally-decreasing recursions (`list_map_poly`, + `sort`, `std_list`, `floats_2_average_int_list`) → plain calls + (now total-checked by it.2). Each migrated fixture must still `ail + check` clean and `ail run` to byte-identical stdout (behavioural + pin). Bench fixtures migrate too; the milestone-close audit + re-ratifies `bench/baseline*` if loop-header codegen diverges from + the retired `musttail` self-call (expected equivalent-or-better: a + header block + phi is at least as good as a `musttail` self-call, + and removes the call-frame entirely). + +## Data flow + +`.ail` source → `ailang_surface::parse` → JSON-AST (`Term::Loop` / +`Term::Recur` are first-class canonical nodes, hashable, round-trip +gated) → `ailang-check`: + +1. typecheck (binders typed; `recur` unified with enclosing loop) → +2. tail-position pass (`recur`-in-tail-position; from it.3 this is + the pass's *only* job) → +3. structural-guardedness pass (it.2) — rejects non-structural + recursion-by-call → +4. effect reconciliation (it.2) — `loop`-bearing or `Diverge`-calling + ⇒ `Diverge` in declared row. + +→ desugar / lift / mono (walker arms thread `Term::Loop`/`Recur` +unchanged) → `ailang-codegen` (`Term::Loop` = header block + phi; +`Term::Recur` = back-edge `br` + block-terminate) → LLVM text → +`clang -O2`. + +The acyclic-call-graph invariant: after it.2, the only back-edge in +generated IR comes from a `Term::Recur` to its lexically-paired +`Term::Loop` header. Every other call is forward and (for recursive +defs) structurally decreasing — i.e. statically known to bottom out. + +## Error handling + +New `CheckError` variants (bracket-`[code]:`-free Display body, per +the 2026-05-15 F2 bugfix convention — the CLI formatter prepends the +`[code]`; the Display string must not embed it): + +- `NonStructuralRecursion` — "recursive call to `f` is not on a + structurally-smaller argument; express this iteration as `(loop …)` + / `recur`". Carries the call site and the offending argument. +- `RecurOutsideLoop` — a `recur` with no lexically-enclosing `loop`. +- `RecurArityMismatch` — `recur` arg count ≠ enclosing loop binder + count. +- `RecurTypeMismatch` — `recur` arg type ≠ corresponding binder type. +- `RecurNotInTailPosition` — `recur` not in tail position of the + enclosing loop body. (Replaces the role of the retired + `TailCallNotInTailPosition`.) + +`UndeclaredEffect` (existing) is reused for the +`Diverge`-not-declared case — no new variant; `Diverge` is just +another effect-row string. + +it.3 removes `TailCallNotInTailPosition` and its `code()`/`ctx()` +arms; the schema-drift / diagnostic-doc lists update in lockstep. + +## Testing strategy + +- **it.1:** serde round-trip unit tests for `Term::Loop`/`Recur`; + `round_trip.rs` auto-picks new `examples/loop_*.ail`; check-side + pins for `RecurOutsideLoop` / `RecurArityMismatch` / + `RecurTypeMismatch` / `RecurNotInTailPosition` (negative fixtures, + carve-out inventory extended); a positive nested-loop + + loop-inside-lambda fixture (mirrors the mut.3 lambda-boundary + concern — loop allocas/phi must scope to the closure's own header); + e2e `examples/loop_counter.ail` runs and prints the expected value. +- **it.2:** positive pins — structural list/tree/JSON walks check + clean and stay `Diverge`-free; accumulator-over-structural (foldl + shape) checks clean as structural (D1); negative pins — + non-structural recursion-by-call fires `NonStructuralRecursion`; + a `loop`-bearing fn without `!Diverge` in its row fires + `UndeclaredEffect`; mutual same-family recursion passes, mutual + cross-family fails. The mut-local e2e fixtures + (`mut_counter`/`mut_sum_floats`) are *not* migrated yet in it.2 ( + they still use `tail-app`); they migrate in it.3. +- **it.3:** every one of the 21 migrated fixtures keeps a + before/after stdout-equality pin; `cargo test --workspace` green; + `design_schema_drift.rs` green with `tail` anchors removed and + `loop`/`recur` anchors present; milestone-close `audit` runs + `bench/` (re-ratify baseline only if loop codegen measurably + differs from the retired `musttail` path, with the regression + ratified as a known accepted delta the way mut.4-tidy ratified the + typecheck-surface tax). + +## Design decisions & rejected alternatives + +**D1 — Structural guardedness is inferred, not annotated; the +accumulator-carrying walk is structural; mutual recursion uses the +conservative same-family rule.** + +- *Inferred, not annotated.* No `{struct n}`-style marker. Rationale + (clause 1 + clause 2): an LLM author does not annotate the + decreasing argument — there is no FP-corpus precedent for it + outside Coq/Agda, which are not in the LLM-natural distribution; a + required annotation would be exactly the redundancy the language + exists to remove (clause 2), and the analysis is local and cheap + (walk `match`-pattern bindings of one parameter). *Rejected:* + explicit decreasing-argument annotation — rejected because it + fails clause 1 (LLM would not write it unprompted) and adds + redundancy (clause 2), not because it is more work. +- *Accumulator-carrying structural walk = structural recursion + (plain, pure, total).* Only the structural argument must decrease; + accumulator positions are free. Forced by coherence with D2: a + `foldl`/`sum`-with-accumulator over a list is the single most + LLM-natural iteration shape in the entire FP corpus; classifying it + as non-structural would push the whole functional-iteration corpus + through `loop`/`recur` and `!Diverge` — self-defeating. The + accumulator is not the recursion's well-founded measure; the + structural argument is, and Decision 10's acyclicity bounds the + depth regardless of accumulator growth. *This resolves the + load-bearing open question (2) from the roadmap entry.* +- *Mutual recursion = conservative same-ADT-family rule.* A + mutually-recursive group is total iff there is a single ADT family + F such that every member has a structural parameter of a type in F + and every recursive call (self or cross-group) passes, at the + callee's structural position, a proper sub-term of the caller's + structural parameter. *Rejected for this milestone:* a general + lexicographic / size-measure ordering — deferred, named in the + spec as out of scope. The same-family rule covers tree/forest, + even/odd-over-Nat, and the mutual JSON walk (the LLM-natural set); + anything outside it must use `loop`/`recur`. This is a deliberate, + recorded conservative scope cut, not an oversight. *This resolves + the load-bearing open question (1) from the roadmap entry.* + +**D2 — `loop`/`recur` carries the `Diverge` effect; structural +recursion stays pure+total. (The genuine fork.)** + +- *Chosen (Option B):* non-structural recursion-by-call is a hard + compile error (`NonStructuralRecursion`); the only way to write an + unbounded cyclic computation is `loop`/`recur`; and any `FnDef` + whose body contains a `Term::Loop` (or calls a `Diverge` callee) + must declare `Diverge` in its effect row. This is the first real + implementation of the Decision-3 `Diverge` placeholder. + - *Rationale, from the language:* local reasoning — "every + definition carries its full type and effect set, so a signature + can be trusted without reading the body" — is AILang's + load-bearing pillar after machine-readability. "Can this function + fail to terminate?" is precisely a body-fact the effect row + exists to lift to the signature. `!IO` already does this for + observable effects; `!Diverge` for non-termination is the same + move, and `loop` is the first construct that gives a *free + syntactic hook* (no termination prover needed — the check is + "does the body contain a `Term::Loop`"). It also makes clause 3 + self-reinforcing: structural recursion stays pure and total, so + an LLM author who wants a clean (`!IO`-free, `!Diverge`-free) + signature is *structurally pulled* toward structural recursion + and pays `!Diverge` only when genuinely writing an unbounded + loop. That behavioral nudge is the milestone's reason to exist. +- *Rejected (Option A):* `loop`/`recur` effect-free; `Diverge` + deleted from DESIGN.md entirely; non-termination simply localized + to the `loop` keyword with no signature consequence. Rejected + because it discards local reasoning about termination at exactly + the moment `loop` makes it free to provide — a caller could no + longer tell from a signature whether a callee may spin, violating + the local-reasoning pillar. Effort is not the reason; the + local-reasoning contract is. +- *Conservativeness note:* every `loop`-bearing fn gets `!Diverge` + even if its `recur` happens to be structurally bounded. This is a + sound over-approximation and intentional: proving a general + `loop` terminates is the totality analysis we deliberately do not + build. The author who wants the pure+total guarantee writes + structural recursion; the author who reaches for `loop` is + telling the compiler "termination is mine to argue", and the + signature says so. +- *Transitional note:* the "hard compile error" lands in it.2 with a + single, deliberately temporary exemption — a still-`tail: + true`-marked recursive call is grandfathered until it.3 removes the + `tail` field and the exemption together. See it.2 Components + ("Transitional grandfather"). This is what lets it.1/it.2 stay + additive and confines all corpus breakage to the one destructive + iteration (it.3). + +**D3 — `loop` is Clojure-shaped (named binders + positional +`recur`), `recur` is tail-position-only and lexically scoped.** +`recur` re-enters the lexically-enclosing `loop` only (never an +implicit fn head — Clojure permits the implicit form; AILang does +not, for the same no-outward-inference reason that originally +motivated explicit `tail-app`: the jump target must be syntactically +present, not inferred from call position). Tail-position-only keeps +the back-edge the *last* thing a loop iteration does, which is what +makes the phi-node codegen well-defined and the construct a true +constant-stack loop. + +**D4 — One milestone, three ordered iterations; the order is forced +by the codegen block-termination seam, not by convenience.** See +Architecture. Recording it here so a future reader does not +"optimise" the order and break the seam handover. + +## Acceptance criteria + +- it.1: `examples/loop_counter.ail` builds and runs to the expected + value; `loop`/`recur` round-trips (parse→print→parse idempotent, + JSON-AST hashable); all five new `Recur*` diagnostics fire on + their negative fixtures; `tail-app` still works unchanged; + `cargo test --workspace` green. +- it.2: a structural list/tree/JSON walk and a foldl-shaped + accumulator walk both check clean with **no** `Diverge` in their + effect row; a non-structural recursion-by-call fires + `NonStructuralRecursion`; a `loop`-bearing fn missing `!Diverge` + fires `UndeclaredEffect`; mutual same-family recursion passes, + cross-family fails; DESIGN.md Decision 3 + §Feature-acceptance + prose match the implementation; `cargo test --workspace` green. +- it.3: `Term::App.tail` / `Term::Do.tail` / both keywords / + `musttail` lowering / `verify_tail_positions`' tail-app role / + `TailCallNotInTailPosition` / Decision 8 all removed; + `design_schema_drift.rs` green with `loop`/`recur` anchors and no + `tail` anchors; all 21 migrated fixtures `ail check` clean and + `ail run` to byte-identical pre-migration stdout; milestone-close + `audit` clean (bench baseline pristine or regression ratified); + `cargo test --workspace` green. +- Milestone: the language has exactly two iteration forms; the only + back-edge in any generated program is an explicit, named, typed, + `!Diverge`-surfaced `loop`; F1 and F4 are discharged; the feature + passes all three feature-acceptance clauses (recorded above and in + DESIGN.md §"Feature-acceptance criterion").