spec: remove mut/var/assign — atomic cut (Approach A), grounding-check PASS
Removal milestone: Term::Mut + Term::Assign + the MutVar surface decl, one indivisible feature. loop/recur (shipped, closed) + let/if cover every shipped use; the construct fails the feature-acceptance criterion applied inverted (clause 2 redundant, clause 3 IS the iterated-mutable- state bug class). Approach A: no deprecation window, JSON tags fail closed as generic unknown-variant, codegen alloca machinery kept (loop reuses it) renamed binder_allocas, shared Term::Lam escape guard keeps its loop half. Decoupled from Stateful-islands. Grounding-check PASS — all 7 load-bearing assumptions ratified by currently-green tests. Roadmap: mut-removal as in-flight P0; the DESIGN.md/docs honesty-lint queued as a distinct P1 milestone (depends on the removal closing), its own brainstorm — no aspirational Wunschdenken / no post-mortem in DESIGN.md; reader sees the language as it IS now.
This commit is contained in:
@@ -35,6 +35,20 @@ work progresses.
|
||||
|
||||
## P0 — In flight
|
||||
|
||||
- [~] **\[milestone\]** Remove `mut` / `var` / `assign` — atomic
|
||||
hard-removal of the local-mutable-state construct (`Term::Mut` +
|
||||
`Term::Assign` + the `MutVar` surface decl; one indivisible
|
||||
feature). `loop`/`recur` (shipped, closed) + `let`/`if` cover
|
||||
every shipped use; the construct fails the feature-acceptance
|
||||
criterion applied inverted (clause 2 redundant, clause 3 IS the
|
||||
iterated-mutable-state bug class). Approach A: no deprecation
|
||||
window, JSON tags fail closed as generic unknown-variant, codegen
|
||||
alloca machinery kept (loop reuses it) + renamed `binder_allocas`,
|
||||
shared `Term::Lam` escape guard keeps its `loop` half. Explicitly
|
||||
decoupled from Stateful-islands (separate, deferred). Spec written
|
||||
+ grounding-check PASS; awaiting user spec review → planner.
|
||||
- context: `docs/specs/2026-05-18-remove-mut-var-assign.md`
|
||||
|
||||
- [x] **\[milestone\]** Prose `loop` binders — projection redesign —
|
||||
CLOSED 2026-05-18. Form-B prose now renders loop binders as a
|
||||
parenthesised init-list on the keyword (`loop(acc = 0, i = 1)
|
||||
@@ -73,6 +87,25 @@ work progresses.
|
||||
|
||||
## P1 — Next
|
||||
|
||||
- [ ] **\[milestone\]** DESIGN.md / docs honesty lint — sweep the
|
||||
canonical docs (above all `docs/DESIGN.md`) so they mirror ONLY
|
||||
the actual current state of development, correct and present-tense.
|
||||
Two banned failure modes: aspirational "foundation for / we'd
|
||||
like / planned" Wunschdenken (genuine forward intent belongs in
|
||||
*this* roadmap, never in DESIGN.md) and "this went wrong"
|
||||
post-mortem narrative (that lives in `docs/journals/`). Sole
|
||||
legitimate exception: a "reserved / unimplemented" claim that is
|
||||
explicitly AND correctly labelled as such (the effect-doc-honesty
|
||||
precedent — the discriminator is whether the doc asserts something
|
||||
exists/works that does not). A reader of DESIGN.md must see what
|
||||
the language IS now, not wishful thinking. Needs its own
|
||||
brainstorm (the Wunschdenken-vs-honest-reserved boundary is a
|
||||
design judgement, and the architect drift-checks against this
|
||||
file — its honesty is load-bearing).
|
||||
- depends on: Remove `mut` / `var` / `assign` (closes first)
|
||||
- context: 2026-05-18 user directive; reserved-vs-vapour
|
||||
precedent `docs/journals/2026-05-16-iter-effect-doc-honesty.md`
|
||||
|
||||
- [x] **\[milestone\]** Heap-`Str` ABI — runtime infrastructure for
|
||||
malloc-backed, refcounted `Str` values alongside the existing
|
||||
static `@.str_*` globals. Today the `Str` path is static-only
|
||||
|
||||
@@ -0,0 +1,246 @@
|
||||
# Remove `mut` / `var` / `assign` — Design Spec
|
||||
|
||||
**Date:** 2026-05-18
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
## Goal
|
||||
|
||||
Remove the local-mutable-state construct from AILang entirely. At
|
||||
the AST there are exactly two nodes — `Term::Mut` (the block, which
|
||||
declares the vars) and `Term::Assign` (the update); `var` is not a
|
||||
first-class `Term`, only the declaration syntax inside a `mut`
|
||||
block, and `Term::Assign` is statically illegal outside an enclosing
|
||||
`Term::Mut` (`mut-assign-out-of-scope`). The three keywords are one
|
||||
indivisible feature; the cut is atomic.
|
||||
|
||||
The feature-acceptance criterion, applied **inverted** (does the
|
||||
*removed* feature fail the gate?):
|
||||
|
||||
- **Clause 1** (an LLM author reaches for it): met — and per
|
||||
`docs/DESIGN.md` that counts *against*, not for, since clause 1 is
|
||||
satisfied by exactly the imperative constructs the core refuses.
|
||||
- **Clause 2** (removes redundancy / improves correctness):
|
||||
violated. Every one of the shipped `mut`-bearing fixtures is
|
||||
straight-line scalar mutation a `let`/`if` expresses; the
|
||||
iteration ones delegate to a tail-recursive helper. The construct
|
||||
*is* the redundancy. Proven executable below (`mut_counter.ail`
|
||||
before→after).
|
||||
- **Clause 3** (reintroduces no bug class the core exists to
|
||||
eliminate): violated. `Term::Mut` + `Term::Assign` is the
|
||||
iterated/sequenced mutable-state reasoning `docs/DESIGN.md`
|
||||
lines 99–108 name as the canonical clause-3 failure. Scalar
|
||||
sealing bounds the blast radius, not the reasoning burden — and
|
||||
nothing in-tree needs it.
|
||||
|
||||
`loop` / `recur` shipped and closed as a standalone milestone
|
||||
(2026-05-18) and is the surviving first-class iteration construct;
|
||||
`let` / `if` cover the straight-line cases. This milestone is
|
||||
explicitly **decoupled** from the open "Stateful islands" roadmap
|
||||
item, which is a separate, later, independent decision and is **not**
|
||||
in scope here.
|
||||
|
||||
## Architecture
|
||||
|
||||
Atomic hard-removal in one milestone, no deprecation window
|
||||
(Approach A). Surface, AST, checker, codegen, DESIGN.md, fixtures
|
||||
and the drift trio are all cut together so the schema is honest at
|
||||
every commit.
|
||||
|
||||
After removal the Form-A keywords `mut` / `var` / `assign` no longer
|
||||
lex; a JSON-AST carrying `{"t":"mut"}` or `{"t":"assign"}` fails
|
||||
closed as a generic serde unknown-variant error. There is **no**
|
||||
dedicated "construct removed" diagnostic — a tombstone diagnostic is
|
||||
permanent clutter for a language whose sole author is an LLM that
|
||||
simply stops emitting `mut` once `docs/DESIGN.md` no longer
|
||||
documents it (no-nostalgia).
|
||||
|
||||
One delicate interaction governs the whole milestone: **the codegen
|
||||
alloca machinery is shared with `loop`.** `loop-recur.3` lowered
|
||||
loop binders by reusing the mut.3 `pending_entry_allocas` mechanism
|
||||
and registering them in the existing `mut_var_allocas` map, and
|
||||
`loop-recur.tidy` widened the shared `Term::Lam` escape guard to
|
||||
cover both. The machinery therefore **survives** the cut (loop needs
|
||||
it); only its `mut` half is removed, and the now-misnamed
|
||||
`mut_var_allocas` is renamed `binder_allocas` for honesty (its
|
||||
"mut-var" name would otherwise be a lie in the source).
|
||||
|
||||
## Concrete code shapes
|
||||
|
||||
### The AILang program — inverted clause-1 faithfulness evidence
|
||||
|
||||
The headline is the proof that removal loses **no** expressivity:
|
||||
every shipped `mut` program rewrites to an observably identical
|
||||
`let`/`if` program. Two real fixtures, before → after:
|
||||
|
||||
`examples/mut_counter.ail` (the strongest evidence — the `mut` block
|
||||
computed *nothing*; the iteration was always the tail-recursive
|
||||
helper):
|
||||
|
||||
```clojure
|
||||
;; BEFORE — ships today (mut.3 fixture), prints 55
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(app print
|
||||
(mut
|
||||
(var sum (con Int) 0)
|
||||
(assign sum (app sum_helper 1 10 0))
|
||||
sum))))
|
||||
|
||||
;; AFTER — observably identical, prints 55
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(app print (app sum_helper 1 10 0))))
|
||||
;; sum_helper (tail-recursive accumulator) is unchanged.
|
||||
```
|
||||
|
||||
`examples/mut.ail` :: `mut_single_var` (the minimal scalar case):
|
||||
|
||||
```clojure
|
||||
;; BEFORE — value is 1
|
||||
(body
|
||||
(mut
|
||||
(var x (con Int) 0)
|
||||
(assign x (app + x 1))
|
||||
x))
|
||||
|
||||
;; AFTER — value is 1, faithful
|
||||
(body
|
||||
(let x 0 (app + x 1)))
|
||||
```
|
||||
|
||||
`mut.ail` :: `mut_nested_shadow` shows the rewrite also *exposes*
|
||||
the redundancy — the outer `var`+`assign` was dead code `mut`
|
||||
permitted (only the inner block is the body's value):
|
||||
|
||||
```clojure
|
||||
;; BEFORE — value 101 (outer x=10,x+1 discarded; inner x=100,x+1 returned)
|
||||
(body
|
||||
(mut (var x (con Int) 10) (assign x (app + x 1))
|
||||
(mut (var x (con Int) 100) (assign x (app + x 1)) x)))
|
||||
|
||||
;; AFTER — value 101, the dead outer state simply gone
|
||||
(body
|
||||
(let x 100 (app + x 1)))
|
||||
```
|
||||
|
||||
The must-fail side (the removal made executable): a module carrying
|
||||
`{"t":"mut"}` / a `.ail` with the `mut` keyword must now be
|
||||
rejected (serde unknown-variant / Form-A parse error). This is a new
|
||||
pin fixture, the clause-3 discriminator (the wrong code fails to
|
||||
typecheck, not merely advised against).
|
||||
|
||||
### Implementation shape (secondary — supporting, not the point)
|
||||
|
||||
| Site | Before | After |
|
||||
|---|---|---|
|
||||
| `ailang-core/src/ast.rs` (~529-638) | `Term::Mut { vars: Vec<MutVar>, body }`, `Term::Assign { name, value }`, `struct MutVar { name, ty, init }` | all three deleted; every exhaustive no-`_`-wildcard `Term` match across the 6 crates loses its `Mut`/`Assign` arms |
|
||||
| `ailang-surface` (`lex`/`parse`/`print`/`loader.rs`, `form_a.md`) | `mut`/`var`/`assign` keywords, `parse_mut`/`parse_assign`, print arms | deleted; the keywords no longer lex |
|
||||
| `ailang-check/src/lib.rs` | `Term::Mut`/`Term::Assign` synth arms; `mut_scope_stack` threaded through every synth caller; 4 variants `MutVarCapturedByLambda`, `UnsupportedMutVarType`[`mut-var-unsupported-type`], `MutAssignOutOfScope`[`mut-assign-out-of-scope`], `AssignTypeMismatch`[`assign-type-mismatch`] + their `code()`/`ctx()` arms; shared `Term::Lam` escape guard gate `!mut_scope_stack.is_empty() \|\| !loop_stack.is_empty()` | synth arms + `mut_scope_stack` + the 4 variants deleted; escape-guard gate simplifies to `!loop_stack.is_empty()`, the `mut_scope_stack` free-var pass removed — **the `loop_stack` half MUST survive byte-equivalent** (loop-binder-captured-by-lambda still rejected) |
|
||||
| `ailang-codegen` (`lib.rs` ~1779-1855, `escape.rs` ~193-417, `lambda.rs`) | `Term::Mut`/`Term::Assign` `lower_term` arms; `mut_var_allocas`/`pending_entry_allocas` save/restore | the two `lower_term` arms + the `mut`/`assign` escape arms deleted; the alloca machinery **kept** (loop reuses it) and `mut_var_allocas` renamed `binder_allocas`, doc-comments made truthful |
|
||||
| `docs/DESIGN.md` | `Term::Mut`/`Term::Assign` data-model entries (~2404-2422) + mut.1/mut.3/mut.4 prose (~2448-2458) + the symmetric lambda-capture note | the `mut` data-model + prose hard-deleted; the symmetric-rule note keeps only its `loop`-binder half; present-tense, zero nostalgia |
|
||||
| drift trio + `carve_out_inventory.rs` + roadmap | mut anchors in `design_schema_drift`/`spec_drift`/`schema_coverage`; mut carve-out fixtures counted in `EXPECTED` (18 post-loop-recur.tidy); roadmap "mut-local is the foundation for Stateful islands" sub-bullet | mut drift anchors removed in lockstep with the schema deletion; `EXPECTED` decremented by the mut carve-out count (exact integer = planner's to pin); the false foundation sub-bullet removed |
|
||||
|
||||
## Components
|
||||
|
||||
1. **AST** — delete the two variants and `MutVar`; sweep every
|
||||
exhaustive `Term` match (the same ~30-site no-wildcard pattern
|
||||
`loop-recur.1` swept additively, now in reverse).
|
||||
2. **Surface** — delete keyword lexing, the two parsers, the print
|
||||
arms, the loader handling, the `form_a.md` grammar lines.
|
||||
3. **Checker** — delete synth arms, `mut_scope_stack` threading,
|
||||
the 4 `CheckError` variants + registry/ctx arms; simplify the
|
||||
*shared* escape guard to `loop_stack`-only, preserving the
|
||||
loop-binder rejection exactly.
|
||||
4. **Codegen** — delete the two `lower_term` arms + `escape.rs`/
|
||||
`lambda.rs` `mut` handling; **keep** the alloca machinery
|
||||
(loop-carried), rename `mut_var_allocas` → `binder_allocas`.
|
||||
5. **Fixtures** — rewrite value-computing fixtures to `let`/`if`
|
||||
(`examples/mut.ail` 6 fns, `mut_counter.ail`, `mut_sum_floats.ail`,
|
||||
`fieldtest/mut-local_1..4`), repoint the e2e assertions
|
||||
(`mut_counter`→55, `mut_sum_floats`→55); **delete** the
|
||||
rejection-probe fixtures whose entire purpose is the removed
|
||||
mut-specific rejection (`fieldtest/mut-local_5_lambda_capture_probe.ail`,
|
||||
`mut-local_6_diag_probe.ail`, `examples/test_mut_var_captured_by_lambda.ail.json`)
|
||||
— no `let`/`if` equivalent exists for them.
|
||||
6. **DESIGN.md** — hard-delete the `mut` data-model + prose;
|
||||
present-tense; the file must read as the *current* language, with
|
||||
no trace of `mut`/`var`/`assign` and no post-mortem.
|
||||
7. **Drift trio + roadmap** — remove mut anchors in lockstep with
|
||||
the schema deletion (proves removal is matched by pin removal);
|
||||
decrement `carve_out_inventory` `EXPECTED`; delete the false
|
||||
Stateful-islands "foundation" sub-bullet.
|
||||
|
||||
## Data flow
|
||||
|
||||
Author writes `.ail` with `let`/`if`/`loop`/`recur` only → surface
|
||||
no longer lexes `mut`/`var`/`assign` (Form-A parse error on the
|
||||
keyword) → JSON-AST has no `"t":"mut"`/`"t":"assign"` (serde
|
||||
unknown-variant rejection, fail-closed) → checker/codegen never see
|
||||
the nodes. Non-`mut` modules are byte-stable end-to-end: removal is
|
||||
symmetric to the additive mut.1 introduction and serde is
|
||||
tag-based, so no canonical-JSON hash of any surviving module moves.
|
||||
`loop`/`recur` is unaffected — it shares the renamed alloca
|
||||
machinery, and its lowering is byte-identical (rename is
|
||||
representation-only).
|
||||
|
||||
## Error handling
|
||||
|
||||
The 4 `mut` `CheckError` variants are deleted. `{"t":"mut"}` /
|
||||
`{"t":"assign"}` produce the generic serde unknown-variant error —
|
||||
no dedicated diagnostic, no tombstone (fail-closed, no-nostalgia).
|
||||
`loop`/`recur`'s five `Recur*` codes and `LoopBinderCapturedByLambda`
|
||||
are byte-unchanged. The shared `Term::Lam` escape guard must keep
|
||||
rejecting a lambda that captures a `loop` binder — this is a
|
||||
non-regression pin, since the guard is the exact code being
|
||||
simplified.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
- **Behaviour-preservation (inverted clause-1, executable):** the
|
||||
rewritten fixtures' e2e value assertions stay green —
|
||||
`mut_counter`→`55`, `mut_sum_floats`→`55` — proving the `let`/`if`
|
||||
rewrite is faithful.
|
||||
- **loop/recur non-regression:** the full `loop_recur_*` /
|
||||
`loop_sum_to*` fixture suite byte-identical (the shared
|
||||
alloca-machinery rename must not move loop codegen); the
|
||||
`loop-binder-captured-by-lambda` rejection still fires
|
||||
point-exactly (shared escape guard, loop half survives);
|
||||
`tail-app`/`tail-do` byte-frozen.
|
||||
- **Schema honesty:** drift trio (`design_schema_drift`,
|
||||
`spec_drift`, `schema_coverage`) + `carve_out_inventory` green at
|
||||
the new `EXPECTED` — proving the schema-region deletion is
|
||||
matched by the drift-anchor deletion.
|
||||
- **Removal made executable:** a new must-fail pin — a `.ail` with
|
||||
the `mut` keyword and a module with `{"t":"mut"}` are now rejected
|
||||
(Form-A parse error / serde unknown-variant).
|
||||
- **Round-trip invariant:** all surviving non-`mut` modules
|
||||
`ail parse|render|parse` byte-identical; pre-existing hash pins
|
||||
byte-stable.
|
||||
- `cargo test --workspace` green.
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
- `mut`/`var`/`assign` do not lex in Form A; `{"t":"mut"}` /
|
||||
`{"t":"assign"}` are rejected as unknown serde variants; no
|
||||
`Term::Mut`/`Term::Assign`/`MutVar` symbol remains in any crate.
|
||||
- The 4 `mut` `CheckError` variants are gone; `loop`/`recur`'s
|
||||
codes and the loop-binder escape-guard behaviour are
|
||||
byte-unchanged (non-regression pinned).
|
||||
- Every value-computing fixture is rewritten faithfully and still
|
||||
produces its original value (`mut_counter`/`mut_sum_floats`
|
||||
print 55); the three rejection-probe fixtures are deleted.
|
||||
- `docs/DESIGN.md` is present-tense and contains zero
|
||||
`mut`/`var`/`assign` mention and zero nostalgia/aspiration; the
|
||||
drift trio + `carve_out_inventory` are green at the new
|
||||
`EXPECTED`.
|
||||
- The Roundtrip Invariant holds byte-identically for all surviving
|
||||
modules; the `loop`/`recur` e2e (`55` / `500000500000` /
|
||||
infinite-compiles) stay green.
|
||||
- `cargo test --workspace` green; milestone-close `audit` bench
|
||||
baseline pristine (pure removal, no hot-path touched — any
|
||||
non-pristine result is a defect, not a ratifiable delta).
|
||||
Reference in New Issue
Block a user