# Prose `loop` binders — projection redesign — Design Spec **Date:** 2026-05-18 **Status:** Draft — awaiting user spec review **Authors:** Brummel (orchestrator) + Claude ## Goal The Form-B prose projection of `Term::Loop` currently renders the binder-with-initial-value list as bare `name = init;` statements *inside* the `loop { … }` body block: ```rust loop { acc = 0; i = 1; if i > n { acc } else { recur(acc + i, i + 1) } } ``` A reader (LLM or human) decodes `loop { x = 0; … }` with the C/Rust mental model: *re-assign `x = 0` on every iteration, then run the rest*. That reading is wrong. The binders are **loop entry state**, bound once on entry and thereafter re-bound **only** by `recur`; they are not body statements and do not re-run per iteration. Prose exists as the reading/diffing surface. AILang's load-bearing doctrine is "the signature tells the truth without reading the body"; the dual obligation is that *when the body is read, the projection must not lie about it*. The current projection lies. This milestone replaces it. The fix is a single change to one render arm in `ailang-prose`. The `loop`-recur AST, Form-A surface, canonical JSON-AST, typechecker and codegen are **unchanged**. This is a projection-only milestone, one iteration. ## Architecture `ailang-prose` is a one-way, deliberately lossy projection (`docs/PROSE_ROUNDTRIP.md`). There is **no Form-B parser**: edited prose is re-integrated by an LLM mediator (`ail merge-prose`), and that mediator is fed `ailang_surface::print` (Form-A) as the original module — *not* the prose. Consequently the `loop` prose rendering feeds nothing back: it is read by humans/LLMs in step 2 of the prose cycle and nowhere else. The byte-isomorphic round-trip invariant in this project is **Form-A ↔ JSON-AST** (surface crate, gated by the cross-form-identity preflight). Prose is not on that path. This milestone therefore has **zero** interaction with the round-trip invariant — stated explicitly here so milestone-close audit does not chase a phantom risk. The only contract the change must preserve is *projection determinism* (same module → same prose bytes), which any pure printer change preserves trivially, plus the snapshot-test discipline in `crates/ailang-prose/tests/snapshot.rs` (a renderer change requires a deliberate, diff-visible snapshot update — exactly the RED→GREEN of this milestone). The chosen rendering is a parenthesised init-list on the `loop` keyword, positionally isomorphic to `recur`'s argument list: ```rust loop(acc = 0, i = 1) { if i > n { acc } else { recur(acc + i, i + 1) } } ``` Rationale (semantic, not effort): - The body block `{ … }` now contains exactly the loop body — the binders are physically outside it, killing the "re-init every iteration" misreading at the syntax level. - `loop(acc = 0, i = 1)` and `recur(acc + i, i + 1)` are the same positional shape. The binder list *is* the parameter list that `recur` re-supplies; making them visually isomorphic teaches the correct model ("`recur` re-binds these, positionally") instead of obscuring it. - Types are stripped (`acc = 0`, not `acc: Int = 0`), consistent with the standing prose rule that `(con T)` is dropped everywhere — `let`, `mut`/`var`, and fn parameters all render type-free in prose because the type is re-derivable. Rejected alternatives: - **`loop with acc = 0, i = 1 { … }`** — `with` already denotes the effect set in prose (`fn main() -> Unit with IO`). Overloading one token with two unrelated meanings reduces readability; rejected on the token-collision ground, not on effort. - **`loop { initially acc = 0, i = 1; }`** — stays inside the braces (still visually conflated) and invents an `initially` keyword; weaker than the chosen form on the exact axis at issue. ## Concrete code shapes ### The AILang program (primary — clause-1 evidence) This milestone changes **no** authoring surface, so there is no new construct an LLM author reaches for. The clause-1 artefact is the existing, unchanged Form-A program and its projection. The program (`examples/loop_sum_to_run.ail`, verbatim, unchanged by this milestone): ```lisp (module loop_sum_to_run (fn main (doc "loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55.") (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body (app print (app sum_to 10)))) (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))))))) ``` Its prose projection, **before** (current, misleading): ```rust // module loop_sum_to_run /// loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55. fn main() -> Unit with IO { print(sum_to(10)) } fn sum_to(n: Int) -> Int { loop { acc = 0; i = 1; if i > n { acc } else { recur(acc + i, i + 1) } } } ``` **After** (this milestone): ```rust // module loop_sum_to_run /// loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55. fn main() -> Unit with IO { print(sum_to(10)) } fn sum_to(n: Int) -> Int { loop(acc = 0, i = 1) { if i > n { acc } else { recur(acc + i, i + 1) } } } ``` The empty-binder loop (`examples/loop_forever_build.ail`'s `(loop (i (con Int) 0) (recur (app + i 1)))` has one binder; a genuinely binder-less `(loop )` is also legal) renders `loop() { … }` — parentheses are always emitted, for regularity and symmetry with `recur()` (which already renders the no-arg form with empty parens). Single-binder example (`examples/loop_forever_build.ail`): ```rust fn spin(n: Int) -> Int { loop(i = 0) { recur(i + 1) } } ``` ### Implementation shape (secondary — supporting, not the point) One arm in `crates/ailang-prose/src/lib.rs`, the `Term::Loop` case of `write_term` (currently lib.rs:938–954). Before: ```rust Term::Loop { binders, body } => { // loop-recur iter 1: minimal-correctness Form-B render. // Prose surface for loop is not yet designed; render the // shape so a reader sees it without overcommitting. out.push_str("loop {\n"); for b in binders { indent(out, level + 1); out.push_str(&b.name); out.push_str(" = "); write_term(out, &b.init, level + 1, owning_module); out.push_str(";\n"); } indent(out, level + 1); write_term(out, body, level + 1, owning_module); out.push('\n'); indent(out, level); out.push('}'); } ``` After: ```rust Term::Loop { binders, body } => { out.push_str("loop("); for (i, b) in binders.iter().enumerate() { if i > 0 { out.push_str(", "); } out.push_str(&b.name); out.push_str(" = "); write_term(out, &b.init, level, owning_module); } out.push_str(") {\n"); indent(out, level + 1); write_term(out, body, level + 1, owning_module); out.push('\n'); indent(out, level); out.push('}'); } ``` The init expressions render at `level` (they are on the keyword line, not inside the indented block) — mirrors how `recur`'s args already render at the call-site level (lib.rs:956–965). The doc comment that says "Prose surface for loop is not yet designed" is removed (it is now designed). `Term::Recur` is **unchanged**: it already renders `recur(a, b)` correctly and is now visibly isomorphic to the loop head. The two non-render `Term::Loop` sites — `count_free_var` (lib.rs:~1167) and `subst_var_with_term` (lib.rs:~1341) — are **not touched**; they implement shadowing/substitution semantics, not rendering. ## Components - `crates/ailang-prose/src/lib.rs` — rewrite the `Term::Loop` arm of `write_term`. ~12 LOC in one arm. No signature change, no new function, no new dependency. - `examples/loop_sum_to_run.prose.txt` (new) and `examples/loop_forever_build.prose.txt` (new) — committed snapshot expectations carrying the Option-A bytes. - `crates/ailang-prose/tests/snapshot.rs` — two `#[test]` functions (`snapshot_loop_sum_to_run`, `snapshot_loop_forever_build`) invoking the existing `check_snapshot` harness. These cover the two structurally distinct cases: multi-binder + non-recur exit, and single-binder + recur-only (no exit). ## Data flow `examples/.ail` → `ailang_surface::load_module` → `ailang_prose::module_to_prose` → byte-compare against committed `examples/.prose.txt`. Unchanged harness; this milestone only adds two stems to the set and changes the bytes the renderer produces for `Term::Loop`. No runtime, codegen, typecheck, or schema data path is touched. ## Error handling None applicable. Prose rendering is total over a well-formed AST (the AST is already validated by `load_module` before reaching the renderer). The change introduces no new failure mode and no new diagnostic. The empty-binder case is handled by the loop emitting `loop() { … }` (the `for` loop body simply does not execute; the `(` / `)` are emitted unconditionally). ## Testing strategy RED-first, via the existing snapshot harness: 1. **RED.** Author `examples/loop_sum_to_run.prose.txt` and `examples/loop_forever_build.prose.txt` with the **desired** Option-A bytes, plus the two `#[test]` functions. Against the current renderer these fail (it emits the old `loop { acc = 0; … }` shape), pinning the symptom. 2. **GREEN.** Apply the `write_term` `Term::Loop` rewrite. Both snapshots pass. 3. **No-regression.** The full `crates/ailang-prose` test suite stays green — no other fixture contains `Term::Loop`, so no other snapshot changes (confirmed: no existing `examples/*.prose.txt` contains `loop`). 4. **Determinism** is covered structurally — the renderer is a pure function of the AST; the snapshot equality check *is* the determinism assertion. Explicitly **out of scope for test coverage** (because untouched): the Form-A ↔ JSON-AST cross-form-identity preflight and the `merge-prose` cycle. The spec asserts these are not on the changed path; no new test is added there because nothing there changes. Multi-line wrapping of a long binder list is **out of scope**: single-line comma-separated, consistent with how `recur` args and fn-call args already render. If a future fixture needs wrapping it is a separate, separately-motivated change. ## Acceptance criteria - `cargo test -p ailang-prose` green, including the two new `snapshot_loop_*` tests. - `ail prose examples/loop_sum_to_run.ail` emits the **After** block above byte-for-byte (binders on the `loop(...)` keyword line; the `{ … }` body contains no `name = init;` lines). - `ail prose examples/loop_forever_build.ail` emits `loop(i = 0) {` with `recur(i + 1)` as the body. - No diff in any other `examples/*.prose.txt`. - No change to `examples/*.ail`, `*.ail.json` build artefacts, typecheck, codegen, runtime, or `docs/DESIGN.md` (the loop/recur semantics are unchanged; only their reading projection changes). - `docs/PROSE_ROUNDTRIP.md` unchanged (the cycle it documents is untouched; prose remains a lossy one-way projection). ### Feature-acceptance criterion (DESIGN.md gate) This is a projection change, not an authoring feature, so clause 1 ("an LLM author naturally produces code that uses it") is evaluated against the *reading* surface, not a new construct: the program is unchanged; the deliverable is its honest projection. The three clauses: 1. **Naturally used:** the prose surface is the LLM/human reading and diffing surface for every module containing a loop — it is used by construction, not opt-in. 2. **Measurably improves correctness / removes redundancy:** yes — it removes a projection that actively implies wrong (re-init- every-iteration) loop semantics. A reading surface that lies about the body it projects is a correctness defect in that surface; the fix is the removal of that defect. 3. **Reintroduces no eliminated bug class:** none. Prose has no parser and relaxes no semantic constraint; the Form-A surface, typechecker, codegen, and round-trip invariant are untouched. Passes on all three.