diff --git a/design/models/0009-explicit-rc.md b/design/models/0009-explicit-rc.md new file mode 100644 index 0000000..2e52b37 --- /dev/null +++ b/design/models/0009-explicit-rc.md @@ -0,0 +1,392 @@ +# Explicit RC — refcounting as an opt-in, not the floor + +**STATUS.** *Design exploration — NOT current state, NOT an approved +milestone.* Nothing here is shipped. The canonical memory model today is +universal reference counting with static uniqueness inference +(`../contracts/0008-memory-model.md`, `0004-rc-uniqueness.md`): every ADT +and closure is RC-heap-allocated, and a uniqueness pass elides inc/dec +where it can prove a reference unique. This whitepaper records a possible +direction — make RC an **authored opt-in** rather than the universal +floor — and isolates the genuinely-open questions in §8. The honesty +rule (`../contracts/0007-honesty-rule.md`) governs the contract ledger, +not this exploratory model; this file exists precisely to fix a future +shape before committing it. If adopted, it revises the floor recorded in +`0004-rc-uniqueness.md` and the codegen contract in +`../contracts/0008-memory-model.md`, and lands as one or more specs under +`../../docs/specs/`. + +This is the **runtime-axis dual** of ownership totality +(`0008-ownership-totality.md`). That whitepaper makes the *annotation* +total — every position carries `own`/`borrow`, no `Implicit`. This one +asks the question totality makes askable: once ownership is authored on +every position, does the *runtime discipline* still have to be universal +RC, or can it follow the annotation — affine values drop deterministically +with no refcount, and RC narrows to the positions that actually declare +sharing? The two compose: 0008 makes ownership total in the type; 0009 +makes the runtime mechanism track the type. + +--- + +## 1. The pain that motivates it + +Memory management is the project's dominant maintenance cost. Across the +last ~200 commits, roughly a third touch the RC / ownership / drop +machinery. The notable fact about every leak and refcount bug in that +history is **where it was not**: not one was a defect in the RC runtime +itself (`ailang_rc_alloc`, `inc`, `dec`, free-on-zero — the header-at-`ptr +- 8` layout in `runtime/rc.c` is small and correct). Every bug lived in +the *static inference that decides where to place inc/dec/drop*: + +- **#43 A2a** — cross-module ownership modes lost because the uniqueness + pass ran per-module and missed a type-scoped signature + (`RawBuf.get`), defaulting a `borrow` argument to `Consume` and + suppressing a scope-close drop. +- **#43 A2b** — the uniqueness side table is keyed by `(def_name, + binder_name)`; a shadow-rebind (`let buf … let buf …`) collapsed the + keys, so codegen read a sibling binding's `consume_count`. The repair + was a whole desugar alpha-rename pass (`docs/specs/0056`, plan 0111). +- **#47 / #49** — loop-carried owned values (a `RawBuf` accumulator, a + `Str` threaded through `recur`) leaked because the codegen predicate + `is_rc_heap_allocated` had no arm for that term shape. +- **`449df13`** — `Subst::apply` silently rebuilt every `Type::Fn` with + `param_modes: vec![]`, dropping the modes; the typed-MIR drop path + then could not see ownership and leaked. + +The codegen-side complexity map quantifies it: roughly **22 +independent conditions** — spread across `uniqueness.rs`, +`linearity.rs` (2149 lines), `escape.rs`, `drop.rs`, `match_lower.rs`, +`lower_to_mir.rs` and the substitution/monomorphisation passes — must +all agree for a single drop to be placed correctly. + +The diagnosis is not "RC is slow" or "RC is wrong." It is that **three +memory disciplines run in parallel and the bugs live at their seams**: + +1. **Affine ownership** via `own`/`borrow` modes (the Rust-shaped part); +2. **Universal reference counting** underneath *everything*; +3. **A uniqueness inference** that exists only to reconcile (1) with (2) + — to prove references unique so it can *elide* the RC traffic that + (2) would otherwise emit. + +Discipline (3) is pure overhead in the literal sense: it is machinery +whose entire job is to remove the runtime mechanism of (2) wherever it +can. The corpus is overwhelmingly single-owner functional code — lists, +trees, `RawBuf` fills — so the inference is mostly *succeeding* at +proving uniqueness and stripping the RC. We pay enormous static-analysis +complexity to delete a mechanism we mostly never needed, and the bugs +are in the deletion logic. + +## 2. The principle: RC is authored, never universal + +0008's principle is "ownership is authored, never defaulted." The dual +on the runtime axis is: **the refcount is authored, never universal.** + +A heap value is one of two things, and the author says which: + +- **owned / `box`** — a *unique* heap allocation. Exactly one live owner + at any program point. No refcount. Freed deterministically when the + owner's lexical scope ends or the owner is moved-and-consumed. This is + Rust's `Box` — affine, single-owner, drop-at-scope. +- **shared / `rc`** — a *refcounted* heap allocation. Multiple owners + may coexist; each is created by an explicit, source-visible `share`, + each contributes one to the count, and the count is decremented at + each owner's scope-end with free-on-zero. This is Rust's `Rc`. + +The default is `box`. `rc` appears only where an author declares genuine +sharing. Refcounting stops being the floor and becomes a *named, +visible, rare* construct — the dual of how 0008 makes `Implicit` +unrepresentable. + +This admits no half-application, exactly as totality does not (0008 §2): +a value's heap discipline must be readable from its type, or the trust +break local reasoning forbids has merely moved from "which mode?" to +"counted or not?". + +## 3. Why affine drop is sound here without a cycle collector + +The move is only legal because AILang has already legislated the +preconditions. `../contracts/0015-language-constraints.md` binds four +constraints — strict evaluation, no recursive value bindings, no shared +mutable refs, ADTs acyclic by construction — whose stated purpose is to +make the reference graph a **DAG**. Today those constraints justify +"RC without a cycle collector." They justify something stronger that the +universal-RC framing leaves on the table: + +> A DAG of single-owner values needs no refcount at all. Deterministic +> drop at end-of-owner-scope frees every node exactly once, in +> reverse-construction order, with no count to maintain. + +Refcounting earns its keep on exactly one thing: **a node with more than +one owner** (so that no single scope-end may free it). The DAG +constraint plus AILang's *linear-by-default with explicit `clone`* +(`0004-rc-uniqueness.md` §2) already forces every act of sharing to be +written. So the set of values that genuinely need a count is precisely +the set the author already had to mark. Making that set the `rc` set is +not a new burden — it is naming a partition the language already draws. + +The cycle question does not reappear: an `rc` value is still acyclic by +construction (constraints 1–4 are unchanged), so no `rc` graph can leak +via a cycle. `rc` buys *sharing*, not *cycles* — the cycle-collector +backstop stays unnecessary for the same reason it is unnecessary today. + +## 4. Worked surface + +The author-facing surface barely changes; the change is what the +compiler must do underneath. (Form-A keywords `box` / `rc` / `share` +below are illustrative; the real spelling is an open question, §8 Q4, +and should align with 0008 §3.4's adjectival argument — likely `owned` +heap vs `shared` heap.) + +### 4.1 The linear majority — no RC at all + +```lisp +(data List + (ctor Nil) + (ctor Cons (con Int) (box List))) ; unique tail — affine, refcount-free + +(fn map_inc + (type (fn-type (params (own (box List))) (ret (box List)))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) (term-ctor List Nil)) + (case (pat-ctor Cons h t) + (term-ctor List Cons (app + h 1) (app map_inc t)))))) +``` + +Count the occurrences of `rc`: zero. For the entire list / tree / +`RawBuf` corpus the author writes `box`, and `box` carries no count. The +inc/dec inference, the `reuse-as` hint, the `over-strict-mode` lint, and +the escape-analysis-to-reclaim-stack all have nothing to do here, because +"this allocation is not shared" is a *type fact*, not an inference +result. + +### 4.2 Genuine sharing — the one place `rc` and `share` appear + +```lisp +(fn two_views + (type (fn-type (params (own (rc List))) (ret (con Pair)))) + (params shared_tail) + (body + (let a (term-ctor List Cons 1 (share shared_tail)) ; +1 owner, visible + (let b (term-ctor List Cons 2 (share shared_tail)) ; +1 owner, visible + (term-ctor Pair MkPair a b))))) ; a, b, shared_tail + ; drop at scope-end → dec +``` + +Forget a `share` and use `shared_tail` twice and it is a **use-after-move +error on that line** — the affine/linearity check (`linearity.rs`, which +already exists) catches it locally — not a silent leak surfacing three +passes later in codegen. The failure class moves from "the compiler +placed a drop wrong" to "the author did not declare sharing," and the +latter is local and checkable. + +### 4.3 In-place mutation: unique-by-type replaces unique-by-inference + +`RawBuf` is the language's only mutation, and the case where explicit +ownership pays the most. Its `set` is `own RawBuf → own RawBuf` and its +doc states the current semantics exactly: + +> *Under uniqueness in-place; under shared copy-on-write (Issue #22).* + +i.e. whether a write reuses the slab or copies is decided by the +uniqueness *inference* — the fragile part (A2a, A2b, the loop arm). With +`box`: + +```lisp +(fn set ; HYPOTHETICAL + (type (forall (vars a) + (fn-type (params (box (con RawBuf a)) (own (con Int)) (own a)) + (ret (box (con RawBuf a)))))) + (params b i v) (intrinsic)) +``` + +A `box` is unique *by type*, so the write is in-place **unconditionally** +— no proof, no copy-on-write branch, no refcount check at the write site. +There is no shared case for a `box`; an author who wanted sharing wrote +`rc`, and `set` on an `rc` is a type error ("cannot mutate a shared +buffer") rather than a silent COW branch. + +**This is consume-and-return, not mutable aliasing.** `set` *consumes* +its buffer (a move); the old binding is dead afterward and never +observable, so semantically a new value is produced and "immutable once +constructed" (constraint 3) holds for every individual value — the +in-place slab reuse is an optimisation under the hood, never a +language-visible write through a live alias. A `&mut`-style mutable-borrow +mode is therefore **out of scope by principle, not preference**: a mutable +borrow *is* a mutable alias, which constraint 3 forbids, and it is the one +genuinely hard part of Rust's borrow checker (aliased-mutation policing) +that AILang's identity removes the pressure for. In-place update rides +*uniqueness/linearity* (now: *type*), exactly as 0008 §8 records, not +exclusive borrows. + +The shadow-rebind idiom (`let buf … let buf …`) may stay verbatim, and +A2b still cannot recur — not because the rebind is gone, but because there +is **no uniqueness side table to collapse**. Codegen reads no per-name +`consume_count` to decide in-place vs. drop; drop is placed at the +lexical scope of the move-checked binding. The alpha-rename pass `C′` +(spec 0056) was load-bearing only for disambiguating side-table keys; +absent the side table it is at most optional scoping hygiene. + +## 5. What this removes from the compiler, and what stays + +**Removed** — from author code *and* from the compiler: + +- The **uniqueness-elision inference** (`uniqueness.rs`'s `consume_count` + dataflow) — its entire job was to strip universal RC; with no universal + RC there is nothing to strip. A `box` is non-shared by type; an `rc` is + counted by type. +- The **`is_rc_heap_allocated` term-shape predicate** with its + Ctor/Lam/Own-App/Loop arms — the thing that kept missing cases (#47). + "Does this need a drop?" becomes a *type* question (`box`/`rc`), total + and arm-free, not a term-shape guess. +- The **`over-strict-mode` lint** and its `suppress` mechanism — there is + no over-strict `own` to warn about once `box` carries no count. +- **`reuse-as`** as a distinct hint — a unique `box` is reusable in place + because it is the sole owner; reuse is a property of the owner, not an + author annotation the inference must verify. +- The **escape-analysis-to-reclaim-stack** pass (`escape.rs`) — an owned + `box` already *is* "not shared," so stack-promotion of non-escaping + allocations is a plain liveness question, not a clawback from a + universal-RC default. + +**Kept** (and made more prominent): + +- The **affine / linearity check** (`linearity.rs`) — use-after-move, + consume-while-borrowed. This is the load-bearing safety pass and it + already exists; it becomes *the* mechanism rather than a diagnostic + layered over an inference. +- **`own` / `borrow`** — unchanged, call-scoped, no lifetime variables + (0008 §8). +- **`clone` / `share`** — but now type-distinguished: `share` on an `rc` + is a cheap inc; "clone" of a `box` is a genuine copy. The two meanings + the single `Term::Clone` conflates today are split by the type. + +The net is **fewer moving parts than today**, not more: the borrow check +stays (we pay it already), and the universal-RC + elision-inference + +escape-clawback triad collapses into one type-directed rule. + +## 6. Relation to ownership totality (0008) and to Rust + +0008 and this whitepaper are two cuts of the same object and are most +coherent adopted together: + +| Axis | 0008 (totality) | 0009 (explicit RC) | +|---|---|---| +| What it totalises | the *annotation* (`own`/`borrow` everywhere) | the *runtime discipline* (counted vs. affine) | +| Removes | `Implicit` default | universal-RC default | +| Default | `own` (trivially true on value types) | `box` (affine, no count) | +| The opt-in | `borrow` (a lent view) | `rc` (a shared, counted value) | +| Soundness pass | return-provenance / escape (0008 §5.2) | the same affine check, now load-bearing | + +0008 §5.1 already takes **regime A** — borrows may not escape into an +escaping heap structure; a field of a returned box is necessarily owned. +That decision is exactly what makes `box` drop transitively sound here: +under regime A, dropping an owned box recursively frees owned children +with no borrowed member to mis-free. The two designs share one +substrate. + +This is **not** a rebuild of Rust, for the reasons 0008 §8 already lays +out and this proposal sharpens: no lifetime variables (point-free is +cut, §4.4 there), no `&mut` / shared-XOR-mutable (§4.3 here, constraint +3), no elision (totality is the opposite of Rust's lifetime elision). +What this adds to 0008 is the one further Rust correspondence 0008 left +implicit: `box` ≈ `Box`, `rc` ≈ `Rc`, and **the default is `Box`, not +`Rc`** — which is the entire point. Today AILang's default is +effectively `Rc` everywhere with a pass trying to downgrade it to `Box`; +the proposal flips the default to `Box` and makes `Rc` the marked case, +which is both what Rust does and what the corpus's actual sharing +profile wants. + +## 7. Feature-acceptance check + +`../contracts/0004-feature-acceptance.md`: a feature ships only if an LLM +author reaches for it unprompted *and* it measurably improves +correctness or removes redundancy. + +- **Reached for unprompted.** The `Box`/`Rc` distinction is core Rust + vocabulary; an LLM author trained on Rust produces `Box` for unique + ownership and `Rc` only for sharing without prompting. The construct is + LLM-native in the strongest sense — it is what the model already + expects, and the *current* implicit-universal-RC model is the surprise. +- **Correctness.** It deletes the inference layer that produced ~⅓ of + recent commits and the three named leak clusters; "is this shared?" + becomes a checked type fact rather than a dataflow result codegen + re-reads out of band. +- **Redundancy.** It removes universal refcount traffic (inc/dec the + uniqueness pass mostly elides anyway) and the `reuse-as` / + `over-strict` / escape-clawback machinery that exists to claw back what + universal RC over-charges. + +Both clauses are met. The cost (below) is real but is implementation +effort and one irreversible hash reset, not a design objection — and per +the design-rationale rule effort is at most a tiebreaker. + +## 8. Costs, consequences, open questions + +Named honestly: + +- **Memory-model swap + hash reset.** This revises the canonical floor + (`0004-rc-uniqueness.md`) and the codegen contract + (`../contracts/0008-memory-model.md`). As in 0008 §6, removing a + serialisation default (here: the RC-everywhere assumption baked into + layout and drop emission) shifts module hashes once across the corpus + and resets every hash-pin test. This is the one genuinely irreversible + step and the one to sign off on deliberately. The hash-pin blast radius + spans every `crates/*/tests/` hash-pin file, not only the AST-home + crate. + +- **Closures are the hard case.** A closure captures an environment; + capture-by-move (`box`) vs. capture-by-share (`rc`) is a real authored + decision, and the capture set is where single-ownership is least + obvious. Today captures are conservatively `Consume` + (`uniqueness.rs`, "Lam captures are conservatively Consume" — + unsound-but-safe). The explicit model must make `move`/`share` on + captures authored and checked. This is the closure-chain benchmark + that already measures widest against the RC target + (`0004-rc-uniqueness.md`). **Open (Q1):** what does the capture surface + look like, and does the affine check cover capture-by-move without new + machinery? + +- **`clone` semantics split.** `Term::Clone` today is "RC inc." Under the + split, `share` on an `rc` is the inc; cloning a `box` is a genuine + (structural) copy. **Open (Q2):** is a structural deep-copy of a `box` + a primitive, or is it only ever "promote to `rc` then `share`"? The + latter keeps one sharing mechanism; the former allows owned duplication + without ever introducing a count. + +- **Coupling to 0008's return-side pass.** 0008 §5.2 shows that for a + *compound* `box` return, the flat ownership claim is sound only if a + reachability pass proves nothing borrowed is reachable. That pass is + the same one this proposal relies on for transitive `box` drop. **Open + (Q3):** does `box`-drop soundness require 0008's escape analysis to + land first, making 0009 strictly downstream of 0008's verification + axis? (Working hypothesis: yes for compound returns; scalar `box` + drop is independent.) + +- **Keyword spelling.** **Open (Q4):** `box`/`rc`/`share` vs. the + adjectival `owned`/`shared` that 0008 §3.4 argues for on + position-neutrality grounds. The choice should land *before* the hash + reset, since renaming a keyword post-cutover is a second irreversible + step (0008 §7 Q3 makes the identical argument for `own`/`borrow`). + +- **Sharing-heavy workloads.** The proposal bets the corpus is + overwhelmingly single-owner. **Open (Q5):** is there a real workload + class (memoised DAGs, hash-consed terms, shared dictionaries) where + `rc` would be pervasive rather than rare? If so, the ergonomics of + pervasive `share` need a second look — though even then the + *correctness* argument (sharing is checked, not inferred) stands. + +**Resolved by the shape above** (not open): the default is `box`, not +`rc` (§2); affine drop is sound under the existing DAG constraints (§3); +no `&mut` / mutable-borrow mode, in-place rides consume-and-return (§4.3); +the uniqueness-elision inference, `is_rc_heap_allocated`, `over-strict`, +`reuse-as`, and escape-clawback are removed, the affine check stays (§5). + +--- + +*Cross-references:* ownership totality (the annotation-axis dual) +`0008-ownership-totality.md`; current memory model +`../contracts/0008-memory-model.md`; RC + uniqueness floor this revises +`0004-rc-uniqueness.md`; the language constraints that make affine drop +sound `../contracts/0015-language-constraints.md`; feature-acceptance +gate `../contracts/0004-feature-acceptance.md`.