diff --git a/design/models/0008-ownership-totality.md b/design/models/0008-ownership-totality.md index be3dd91..8d9a4c8 100644 --- a/design/models/0008-ownership-totality.md +++ b/design/models/0008-ownership-totality.md @@ -12,6 +12,12 @@ shape before committing it. When a direction here is chosen, it becomes one or more specs under `docs/specs/`, and the current-state facts migrate into the contract ledger. +*Refined 2026-06-01 by design discussion: §3.4 (the keywords are +adjectival, not verbal), §4.4 (the no-mode-polymorphism result is +contingent on the point-free cut), §5.1–5.3 (compound returns are an +ownership tree; multi-return is the ownership-honest return path), and +the sharpened §7 questions, and §8 (relation to Rust).* + --- ## 1. The leak that motivates it @@ -110,6 +116,53 @@ metadata fields on `Type::Fn` (`param_modes`, `ret_mode`), not new fn-parameter positions, not to types in general). There is **no** mode variable and **no** third polymorphic axis — see §4. +### 3.4 The keywords are adjectival, not verbal + +`own` and `borrow` are *acquisition verbs* — they name what the +receiver at a position does. On a parameter the receiver is the callee +and the verb reads natively: `borrow param` = "I borrow this, the +caller keeps it"; `own param` = "I take ownership." On a *return* the +receiver flips to the caller, and the same verb reads backwards from the +author's viewpoint: `own ret` means "I *hand* ownership away," `borrow +ret` means "I *lend* a view" — the author is the lender, not the +borrower. The same word names opposite roles on the two sides. §3.1's +own text shows the seam: it glosses `own` as "ownership is handed to the +caller" (the return reading) but states the authoring rule as "reach for +`borrow` only when reading a value you were lent" (the param reading). +The polarity reframe unifies the *bit* (transfer vs. alias) but not the +*verb*. + +The fix is to name the mode adjectivally — as a property of the value +the receiver holds, not an act of acquisition. `owned` / `borrowed` +(past participles, i.e. adjectives) are position-independent because an +adjective describes the thing, not the directed act: `(param (owned +Str))` and `(ret (owned Str))` both read as "an owned Str"; `(ret +(borrowed Str))` reads as "returns a borrowed Str" — the idiomatic form, +where the bare imperative `borrow` does not. The deep invariant §3 wants +to unify (transfer vs. alias is a property of the value) was always +position-independent; only the verb form obscured it, so the participle +*strengthens* the uniformity argument rather than breaking it. §3.2's +value-type rule is unaffected: `(borrowed (con Int))` is as plainly an +error as `(borrow (con Int))`. And the Rust-familiarity that the +feature-acceptance gate rewards is preserved — the idiomatic English is +already "returns a *borrowed* str / an *owned* String," never "returns +*borrow* str." + +This is not merely aesthetic. §6 names a wrong `own` (declared own, +actually an alias) as the double-free — the dangerous direction, and the +one totality pushes authors toward. If `own` on a return connotes "I +take ownership" to an author when it means "I give ownership away," the +verb form is a mis-annotation pump pointed straight at the double-free. +The choice carries a safety stake, not only a readability one. + +A corroborating code smell: `ret_mode` today has the *type* `ParamMode` +(`crates/ailang-core/src/ast.rs`). A return mode is not a param mode — a +param mode is a *demand on the caller* (contravariant), a return mode is +a *promise to the caller* (covariant): the same two-element lattice read +in opposite variance. That is why one verb fits both badly. The shared +type wants a position-neutral name (`Ownership`, `TransferMode`) rather +than the param-centric one. The naming question is tracked in §7 Q3. + ## 4. Fixed modes suffice — why there is no mode-polymorphism A natural objection: passthrough functions — `id`, projections, `apply` @@ -190,6 +243,22 @@ The discipline leans entirely on features the language already has: `ParamMode` stays binary; "every position carries a concrete `own`/`borrow`" holds literally, with no third-axis footnote. +One honesty caveat on §4 as a whole: "fixed modes suffice" is +*contingent on the point-free cut*, not independent of it. §4.2 already +says the duality "bites only in code AILang does not have" — the +load-bearing word is *have*. If AILang ever un-cut higher-order routing +combinators (`compose`, `apply`, `id`-as-argument — the HOFs that +control *neither* end of their seam and merely wire two black-box +functions whose modes come from the caller), the reuse-across-modes +clash returns and the mode-variable question reopens. The honest +statement is "*given* the point-free cut, fixed modes suffice" — a +dependency, not a standalone theorem. The structural discriminator that +makes today's HOFs safe is that each (`map`, `fold`, `find`, +`map_first`) controls *both* ends of its seam — it reads the element out +of the container it owns and builds the result — so the seam mode is +determinate per definition; only the wire-two-black-boxes kind needs a +mode variable, and that kind *is* point-free. + ## 5. Two orthogonal axes: totality vs soundness These must not be conflated: @@ -215,6 +284,100 @@ propose each parameter's correct mode. The *return* side is the half with no verification yet; it needs new return-provenance ("escape") analysis. +### 5.1 Compound returns: ownership is a tree, `ret_mode` is flat + +The orthogonality above is clean for a *scalar* return. It frays for a +*compound* one. A returned `(Pair a b)` is a single heap node, and +`ret_mode == Own` says the caller owns the *box* — but the two fields +carry their own ownership. A function returning a Pair of {a fresh +`Str`, a view into a borrowed argument} has an owned box, an owned field +0, and a *borrowed* field 1. A single top-level `Own` directs the caller +to recursively `dec` the whole box, whose drop decs field 1 → **dec of +borrowed data → use-after-free.** Ownership is a property of every heap +node in the type tree; one bit at the root cannot describe the interior. +This is not return-specific — a `Pair`-typed *parameter* has the same +interior that the flat `param_modes` entry does not cover; it is +sharpest on returns because returns escape. + +There are two regimes, and the choice decides whether a flat `ret_mode` +is enough: + +- **(A) Borrows may not escape into an escaping heap structure.** Then + every field of a returned box is necessarily owned, ownership is + transitive from the root, and the flat `ret_mode` is sufficient *and + sound* — precisely because the mixed case is forbidden at + construction. The price: to return a view as part of a structure, you + must `clone` it to owned first. This is Rust's "cannot return a struct + borrowing a local," minus lifetime variables. +- **(B) Borrows may escape, tracked per field.** Then the mode + annotation becomes a *tree mirroring the type tree*, and to verify a + borrowed field you must name *what it borrows from* — i.e. lifetime + parameters. That is a different, much larger language, and it fails + the "no human-hostile complexity without enough correctness gain" + gate. + +AILang takes (A). §3.1's own gloss ("a view into data owned upstream") +already points there: for an escaping box field, "upstream" is gone once +the caller holds the box, so the borrow concept is ill-defined. + +### 5.2 For compound returns, verification is constitutive, not phased + +This is where §5's "two orthogonal axes" claim needs a caveat. The flat +`ret_mode == Own` on a Pair *means* "the caller may recursively free" +only if it is guaranteed that nothing borrowed is reachable from the +box. That guarantee **is** the escape analysis. So the return-side pass +is not the first-order "is this return fresh?" of §5/§6 — it is "is +*everything reachable from this return* owned?", and it is not a +*separable, deferrable* axis: it is what makes the flat `ret_mode` a +sound representation at all. For compound returns, representation and +verification are a *coupled pair*. This pushes §7 Q2 from "should +return-verification land with the cutover" to "*must*, for any cutover +that lets `Own` stand on a boxed return" — an unverified `Own` on a +mixed Pair is not merely untrusted, it is unsound by construction. + +### 5.3 Multi-return is the ownership-honest return path + +An *unboxed multi-return* (several results handed back in registers, no +heap node) dissolves the tree problem for the return case. With no box +there is no "owned box / borrowed field" interior: each returned value +is its own top-level position with its own mode — `ret_mode` becomes a +`Vec`, symmetric with `param_modes`. A `(owned Str, borrowed +Str)` multi-return is flat and sound *without* the reachability pass, +because the borrow flows *alongside* the owned value, not *inside* it +(it aliases an argument the caller still holds); only the scalar +return-provenance check applies, per position, never the reachability +check. The boxed Pair forces homogenisation toward owned (regime A's +mandatory `clone`); multi-return does not, because no shared box forces +the values to share a fate. So on the ownership axis multi-return is +strictly the *simpler* side. + +Multi-return does **not** subsume the tuple. They answer orthogonal +questions: multi-return is an ABI for one position; a `data` aggregate +is a *value* with a *type*, and only a typed value can be a list +element, a constructor field, instantiate `forall a`, or be held across +iterations. The moment aggregation is structural or durable, the box is +required. The two compose: a multi-return *position* may itself be a +Pair, which then takes the transitive treatment while its siblings stay +flat — orthogonal layers, not competitors. + +The boundary between them is a meaningful authored decision, not a +routing detail — symmetric with the §4.2 consume/preserve split. Boxing +*is* the ownership commit: "do I box these?" = "do I commit them to one +owned aggregate that outlives the call?", and under regime A that is +exactly the point a borrowed member must `clone` to owned. Multi-return += results not yet committed, each keeping its mode; `data`-boxing = +commit to a single owned aggregate. + +Whether AILang *adds* multi-return is a feature-gate question separate +from totality, but the gate's answer leans yes: the present idiom +"allocate a Pair, then `match` it apart at the call site" is a +measurable redundancy (a heap alloc + dec for a value that never lived +as an aggregate), and multi-return is the only ownership-honest way to +return heterogeneous modes. It never removes the need for the boxed +aggregate; it shrinks what the return-side escape pass must cover (only +boxed returns need the reachability check of §5.2), which is an argument +to weigh it *before* fixing the escape-analysis scope. + ## 6. Costs and consequences (named honestly) - **Total migration.** Every signature in the corpus and prelude gains @@ -257,15 +420,86 @@ scope entirely — a saving, not a debt. 2. **Verification sequencing.** Is require-and-trust an acceptable interim on the soundness axis, given the double-free risk of a wrong `own`? Or should return-side `own`-verification land *with* the - totality cutover rather than after it? + totality cutover rather than after it? §5.2 partly forces this: for + *compound* returns, verification is constitutive of the flat + `ret_mode`'s meaning, so "with the cutover" is mandatory wherever + `Own` may stand on a boxed return — the open part is only the + *scalar* return. -3. **Naming.** If this lands, the glossary should pin the vocabulary - (mode, `own`/`borrow`, trivial-`own`, the projection/extraction/clone - rule) before drift sets in. +3. **Naming.** §3.4 argues the keywords should be adjectival + (`owned`/`borrowed`), not the acquisition verbs (`own`/`borrow`) that + read backwards on returns, and that the shared `ParamMode` type wants + a position-neutral name (`Ownership`). Open: adopt the participle + form, or keep the bare Rust-familiar verbs? Either way the choice + should land *before* the cutover — the §6 hash reset is the one + irreversible step, and renaming the keyword post-cutover would be a + second one. The glossary should then pin the vocabulary (mode, the + chosen keywords, trivial-`own`, the projection/extraction/clone rule) + before drift sets in. + +4. **Multi-return adoption.** Should AILang add unboxed multi-return + alongside boxed aggregates (§5.3)? It is the ownership-honest return + path (flat per-position modes, no reachability pass) and removes the + allocate-then-immediately-`match` redundancy, but it is a second + return mechanism with its own surface syntax and a `Vec` `ret_mode`. + Its scope interacts with the cutover: adopting it shrinks what the + return-side escape pass must cover, so it is worth deciding *before* + fixing the escape-analysis scope. **Resolved by the converged shape above** (no longer open): re-scope to totality (§2), value-type mode policy → trivial-`own` (§3.2), -mode-polymorphism → not adopted; fixed modes suffice (§4). +mode-polymorphism → not adopted; fixed modes suffice (§4); +compound-return ownership → regime A, a flat `ret_mode` + transitivity +rather than a per-field mode tree (§5.1); multi-return does not subsume +the boxed tuple (§5.3). + +## 8. Relation to Rust (and why this is not a rebuild) + +The vocabulary here is Rust's, and pretending otherwise would violate +the honesty rule: `own`/`borrow` ≈ move/borrow, a borrowed return ≈ +`&T`, regime A (§5.1) ≈ Rust's "cannot return a struct borrowing a +local," the unboxed heterogeneous product (§5.3) ≈ a Rust tuple, +ownership recovery via `clone` ≈ `.clone()`, RC ≈ `Rc`/`Arc`. An LLM +author reaches for these *because* it has read Rust; inventing fresh +names for the same concepts would be vanity and worse for the author. + +But adopting the vocabulary is not rebuilding the language. The bulk of +Rust's complexity is machinery AILang's identity removes the pressure +for, and the removals are principled, not effort-driven: + +- **No lifetime/mode polymorphism.** Rust's lifetime *variables* — with + their variance, subtyping, `for<'a>` (HRTB), reborrowing, NLL — exist + largely so a human can write one reusable generic abstraction across + many lifetime instantiations. That is the exact analogue of the + mode-polymorphism §4 declines, and for the same reason: AILang cut + point-free (§4.4), so the pressure that forces Rust to carry lifetime + variables evaporates. "Rust without lifetimes" is something Rust + itself cannot be, because its human audience demands the combinator + style AILang forbids. +- **No `&mut`, no shared-XOR-mutable.** The genuinely hard part of + Rust's borrow checker — policing aliased mutation — is out of scope: + the memory model has no shared mutable references + (`../contracts/0008-memory-model.md`), and `borrow` is a read-only + view. In-place update rides *uniqueness/linearity* (update iff + statically unique — the Clean/linear-types lineage), not exclusive + borrows. AILang draws its mutation-safety from a different tradition + than its borrow vocabulary; see `0004-rc-uniqueness.md`. +- **No elision; the opposite of Rust on defaults.** Rust *has* lifetime + elision — a default that omits annotations for human convenience. + §2's totality is the opposite stance: nothing is defaulted, because a + default is the trust break local reasoning forbids. On the default + question AILang is *stricter* than Rust, not a copy of it. + +So this is not "Rust" but the *fixed-mode, monomorphic, +read-only-borrow, elision-free fragment* of Rust's ownership +vocabulary, with mutation-safety from the uniqueness tradition and RC as +the floor (`0004-rc-uniqueness.md`) — a hybrid none of the source +languages is. The transferable parts (ownership is binary +transfer-vs-alias; borrows must not escape; recovering a view costs a +`clone`) are not Rust inventions but the physics of refcount-free +memory, which one adopts rather than rebuilds. One would be rebuilding +Rust only by *also* taking the lifetime apparatus — and §2, §3.4, and §4 +are jointly the argument for why this does not. ---