diff --git a/docs/roadmap.md b/docs/roadmap.md index 2086198..e1c093f 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -40,10 +40,17 @@ clean. Pick the next milestone from P2.)_ ## P1 — Next -- [ ] **\[milestone\]** Iteration discipline — structural recursion + +- [~] **\[milestone\]** Iteration discipline — structural recursion + named `loop`/`recur`; recursion-by-call restricted; `tail-app` - retired. The iteration story of the language, decided in principle - 2026-05-15. Two constructs survive, one is removed: + retired. Spec `docs/specs/2026-05-15-iteration-discipline.md` + (approved fda9b78; scope-corrected 2018178/10a0595). **Status + 2026-05-15: it.1 SHIPPED (96db54d — loop/recur additive), it.2 + SHIPPED (a4be1e5 — guardedness checker + first real Diverge + effect), it.3 BLOCKED on a surfaced fundamental design fork (see + "The blocking fork" below — needs a user design decision + a new + iteration it.2b before it.3 can re-dispatch).** The iteration + story of the language, decided in principle 2026-05-15. Two + constructs survive, one is removed: - **Structural recursion stays — and becomes total-by-construction.** A recursive call is permitted iff it is structurally guarded: each recursive call is on a constructor-smaller component of an @@ -85,30 +92,90 @@ clean. Pick the next milestone from P2.)_ LLM-natural *and* their bug class is closed by construction; a bare `while` is exactly what clause 3 rejects). - **The open spec question (the real brainstorm work).** Not "whether" - but the precise definition of "structurally smaller" / the - guardedness check. Two hard points: (1) *mutual* structural - recursion (needs a measure / size over the ADT, not just a - one-argument syntactic decrease); (2) the accumulator-carrying - structural walk — `foldl`-shaped, simultaneously structural *and* - tail-shaped — the spec must decide whether it counts as structural - recursion (a plain call) or must be expressed as `loop`/`recur`. - This is the load-bearing spec decision; brainstorm + grounding-check - own it. + **Original open spec questions — RESOLVED in it.2 (a4be1e5).** + (1) *mutual* structural recursion → the conservative same-ADT-family + rule (connected-components union-find over the type-reference + graph; admits tree/forest, even/odd-over-Nat, mutual JSON; a + general size-measure ordering stays out of scope). (2) the + `foldl`-shaped accumulator-carrying structural walk → **counts as + structural recursion** (plain, pure, total — only the structural + argument must decrease; accumulator positions are unconstrained). + Both shipped and pinned. + + **The blocking fork (it.3-surfaced 2026-05-15 — needs a USER + design decision; touches the purity pillar the user co-designed).** + The milestone's totality thesis recognised exactly ONE + total-by-construction recursion scheme: structural-over-an-acyclic- + ADT (Decision 10). The it.3 mandated corpus sweep proved this is + *incomplete*. Six corpus fixtures contain the single most + LLM-natural tree-builder shape: + `build(d: Int) = if d==0 then Leaf else Node(1, build(d-1), build(d-1))`. + It is provably terminating, but: **not** ADT-structural (`d` is + `Int`, no constructor-smaller component) and **not** `loop`/`recur`- + able (it is *branching/double* recursion; `recur` is a single + tail-position back-edge — a balanced-tree build is not a tail + loop; the only `loop` form is a hand-rolled explicit-stack + worklist, which no LLM writes). So the milestone *as-specified* + makes a trivially-total, maximally-natural function + **inexpressible** — failing its own feature-acceptance criterion + (clause 1: the LLM reaches for `build(d-1),build(d-1)`; clause 2: + the milestone would *remove* expressivity). This is a real + design-thesis gap, not a migration nuisance: there is a SECOND + canonical total-by-construction scheme the design overlooked — + **well-founded recursion on a strictly-decreasing non-negative + integer measure** (`f(0)=base; f(n)=…f(n-1)…`, branching allowed). + + **Decision the user must make** (it trades against the purity + pillar — Int ≠ ℕ; AILang has no `Nat`/refinement types, so + Int-bounded recursion is total only for *non-negative entry*): + - **A1 (RECOMMENDED).** Make the totality story a *trichotomy*: + ADT-structural | Int-bounded-well-founded | explicit `loop`/`recur`. + Accept Int-bounded recursion (recursive call on `p - ` + with a non-recursing base guard, branching allowed) as a + *second total-by-construction class*, with one documented + obligation: non-negative entry (a negative seed diverges — the + same precondition class as array-bounds the language already + lives with). Restores the entire `f(n-1)` recursion family (the + second-most-common shape in any corpus); keeps all 6 fixtures + verbatim; the trichotomy is *more* complete, not less principled. + Rationale is the language's own gate: a milestone that makes + `build(d)` inexpressible cannot pass the feature-acceptance + criterion. *Why this is a user call:* it concedes "total by + construction, sign nothing" → "total by construction modulo one + documented non-negative-entry obligation" — a dilution of a + purity pillar the user personally weighted in the original + Socratic design dialogue. + - **A2.** Introduce a `Nat` type; accept Int-bounded recursion + only on `Nat` — preserves zero-precondition purity, but `Nat` + is its own sub-milestone and an LLM writes `depth: Int` unless + the prelude makes `Nat` the natural default (clause-1 friction). + - **A3 / B / C (not recommended).** Strict-dichotomy + + explicit-worklist (fails clause 1 — no LLM hand-rolls a stack + for tree-build); a narrow carve-out predicate (the patch smell); + reshaping the LLM-natural fixtures (forbidden — + `feedback_dont_adapt_tests_to_bugs`). + + **If A1 (or A2): new iteration it.2b** — additive widening of the + it.2 guardedness checker to also accept Int-bounded (incl. + branching) recursion as total; no removal. After it.2b the 6 + fixtures check clean with zero migration; it.3 then re-dispatches + from c992eb9 (the `bench/it3-oracle/` 40-fixture behavioural + oracle is preserved and reused; nothing in it.3 was destructive). + The it.3 RC-RSS/18g.1 load-bearing risk (Task 5.5/5b) is still + UNTESTED — must not be treated as resolved by the milestone-close + audit. **Relation to Stateful islands.** This entry owns the iteration story and *supersedes* the "while-loops legal" scope bullet of the Stateful-islands milestone below. The genuinely-escaping mutable-state path (`ref a` / `MutArray a` / `Stateful a b` / - `pipe`) is unaffected and stays in Stateful-islands — that is the - deliberately-fenced streaming escape hatch for *escaping* state, - not the default iteration story, and F1 no longer motivates it. + `pipe`) is unaffected and stays in Stateful-islands. - - context: 2026-05-15 chat — design convergence from the - mut-local fieldtest (F1) through the fenced-`while` / - `!Mut`-visibility dead end to the structural-recursion + - named-loop synthesis. Pending brainstorm produces - `docs/specs/-iteration-discipline.md`. + - context: spec `docs/specs/2026-05-15-iteration-discipline.md`; + per-iter journals 2026-05-15-iter-it.1 (shipped), -it.2 + (shipped), -it.3 (BLOCKED — the design fork above). Next action + is a USER decision on the blocking fork (A1 recommended), then + iteration it.2b, then it.3 re-dispatch from c992eb9. - [x] **\[milestone\]** Heap-`Str` ABI — runtime infrastructure for malloc-backed, refcounted `Str` values alongside the existing