# Ownership totality — authored own/borrow everywhere whitepaper **STATUS.** *Partially realised — the totality core shipped; the return-side soundness tail is still exploration.* The annotation-totality direction this whitepaper converged on **landed** via #55 (spec `../../docs/specs/0062-eliminate-implicit-mode.md`, commit `76b21c0`, 2026-06-02): `ParamMode::Implicit` is deleted, `ParamMode` is binary `{Own, Borrow}` (§3.3), every fn-type slot carries an explicit mode including value-type slots (§3.2 trivial-`own`, `(borrow Int)` an error), mode-polymorphism was not adopted (§4), and the one-time canonical-hash reset (§6) is done. Those current-state facts now live in the contract ledger (`../contracts/0008-memory-model.md`), per the honesty rule (`../contracts/0007-honesty-rule.md`) — read the contract, not this model, for what the compiler does today. What remains **exploration, not shipped**: the return-side soundness axis (§5.1–5.2 — the escape / return-provenance reachability pass). The cutover sidestepped it by *rejecting* `(ret (borrow T))` outright (spec 0062 "Out of scope") rather than verifying it; `escape.rs` is the older opt-only stack-promotion pass, not this check. Multi-return (§5.3) is likewise unbuilt. The §3.4 / §7-Q3 naming question is **resolved, not open**: the keywords stay the verbal `own`/`borrow` (user decision 2026-06-01, spec 0062 scope decision 1); the adjectival `owned`/`borrowed` was declined, so §3.4 is recorded rationale for a road not taken. The remaining §7 open questions are Q2 (scalar return-verification sequencing) and Q4 (multi-return adoption). *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 motivated it A user function whose return **type** was an RC-heap value (`Str`, or a boxed ADT) but whose signature omitted the ownership mode carried `ret_mode == ParamMode::Implicit` — the parser's silent default, which nothing inferred post-parse. Codegen read `Implicit` faithfully: the caller did **not** `dec` the returned slab, so the owned allocation leaked (`live = 1` under `AILANG_RC_STATS`). The #55 cutover removed this lane: `../contracts/0008-memory-model.md` now requires an explicit author-supplied `ret_mode`, and the `examples/rc_let_implicit_returning_app.ail` fixture asserts `live = 0` (the returned cell frees at the call site). The leak was the symptom. The cause was that an ownership default existed at all. ## 2. The principle: ownership is authored, never defaulted AILang's identity (`../../CLAUDE.md`): *local reasoning — "every definition carries its full type and effect set, so a signature can be trusted without reading the body"*; *mandatory mode and type annotations are kept*; *machine readability over human readability*. `Implicit` violates that identity head-on. Whether the caller becomes the owner of a value crossing a signature boundary — and must free it — is **not recoverable from the type alone**: a `Str`-returning `own` and a `Str`-returning `borrow` are indistinguishable by type; only the mode says who frees. The code made this concrete: the typechecker treated `Implicit ≡ Own`, yet codegen read `Implicit` separately and omitted the caller `dec`. The *same* fn-type was read two ways depending on whether one knew codegen's special-casing — exactly the trust break local reasoning exists to forbid. So the principle is: **ownership is authored, never defaulted.** This admits no half-application. A default cannot be partially removed: closing the Implicit lane on *returns* while leaving it open on *parameters* is the same default surviving on the input side; mandating a mode where it is meaningful (heap returns) while permitting it where it looks vacuous (a by-value `Int`) is a rule that forces truth in one direction and tolerates noise in the other. Totality is the only coherent stopping point: **`Implicit` is removed from the authorable surface, and every parameter and every return on every signature carries `own` or `borrow`.** There is no defaulted position anywhere. ## 3. The shape: totality with a binary mode ### 3.1 The polarity reframe (so the author needs no RC knowledge) The objection to totality is "now the author must know which types are heap." The reframe dissolves it: **`own` is the universal default; `borrow` is what implies aliasable (heap) data.** - `own` means "ownership is handed to the caller." For a fresh heap allocation, the caller now frees it. For a by-value `Int`, ownership of the copy is trivially the caller's — `own` is correct, just trivially true. - `borrow` means "this is a view into data owned upstream; the caller must not free it." You can only lend a view of something aliasable, which presupposes heap data. So `(borrow (con Int))` is an **error** — a value type has nothing to lend. The author's whole rule is then pure dataflow about their own body, with zero knowledge of the RC representation: **default to `own`; reach for `borrow` only when you are reading or passing through a value you were lent.** Every position has an answer — it is always either "I take it" (`own`) or "I lend/read it" (`borrow`); no position has `Implicit` as its uniquely-correct authored answer. ### 3.2 Value types: trivial-`own`, `borrow` is an error Every position carries a mode, including value-type positions — the surface stays uniform. Over a by-value type (`Int`, `Float`, `Bool`), `own` is trivially true and `borrow` is a `check` error. This is chosen over the alternative (value-type positions take no mode slot at all) deliberately: forbidding the slot would re-introduce exactly the RC-representation knowledge the polarity reframe removes (the author would have to know which types are heap to know which positions take a mode), and it would make the surface non-uniform. For an LLM author, uniform structure beats the saving of a trivially-true token: the model is not burdened by the token, it is burdened by a conditional rule. The mode on a value-type position therefore carries no runtime information (`live = 0` regardless); it is the forced, only-legal `own`. This is the price of uniformity, named honestly. ### 3.3 `ParamMode` is binary `ParamMode` becomes `{Own, Borrow}` — `Implicit` is deleted. Modes stay metadata fields on `Type::Fn` (`param_modes`, `ret_mode`), not new `Type` variants, preserving the 18a locality decision (modes belong to 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` — have a return whose ownership *is* the input's. Surely those need a mode variable (`id : (m a) -> (m a)`)? They do not, and the reasoning is load-bearing enough to state in full, because a reader will reach for mode-polymorphism on sight. ### 4.1 Totality does not require mode-polymorphism Every position — **including a position over a type variable** — takes a concrete authored `own`/`borrow`. `fst : forall a b. (borrow (Pair a b)) -> (borrow a)` is total and hole-free: the `(ret (borrow a))` is an honest fixed claim ("I return a borrowed view"). A type-variable position is therefore never a *hole* under fixed modes; it simply commits the function to one mode. What a mode variable would buy is not totality but the removal of *duplication* — one definition serving an `own`-instantiation and a `borrow`-instantiation at once. The two notions must not be conflated: "cannot express passthrough with one definition" is not "cannot express anything." ### 4.2 The reuse-across-modes need is confined to cut or better-split cases A single definition needs to serve both an `own`- and a `borrow`-instantiation only in two places: - **Higher-order routing combinators** (`compose`, `apply`, `id` as a function argument, `twice`/`iterate` over an endofunction). Here the seam modes must thread through, and one definition would have to cover every mode combination. But these are **point-free style** — cut by the language identity as human-attractive but LLM-neutral. The duality bites only in code AILang does not have. - **The consume-vs-preserve container duality** (`map`/`filter`/`find` applied to a container you discard vs. one you keep). This duality is real, but it is a **meaningful semantic distinction the author should state** — "do I destroy my input?" — not a routing detail to abstract behind a variable. Expressing it as two named functions (a borrow-reading variant and an owning-consuming variant) keeps the decision explicit; a mode variable would *hide* it. This is an argument against mode-polymorphism even where it technically applies. ### 4.3 The structural reason it does not bite AILang's iteration idiom is **named tail-recursion** (`tail-app`, e.g. `examples/bench_compute_collatz.ail`), not a passed-function combinator like `iterate f n`. Owning accumulation — state stepping, fixpoint normalisation, fold-like loops — is written as a function recurring on itself with accumulator parameters. The own/borrow clash at a higher-order slot needs a *reused function-argument combinator*, which the language does not reach for. A survey of the canonical higher-order functions confirms each has a single determinate mode slot: | HOF | Mode slot | Reuse-across-modes clash? | |---|---|---| | `map f xs` | `f : (borrow a) -> (own b)`, reads the list | no — owning-consume is a separate optimisation, and RC lets an owner lend to the borrow form | | `filter p xs` | `p : (borrow a) -> Bool`, consumes input | no | | `fold f acc xs` | `f : (own acc) (borrow a) -> (own acc)` | no — a borrow-accumulator is meaningless | | `find p xs` | `p : (borrow a) -> Bool`, returns `(borrow a)` view | no | | `any`/`all p xs` | `p : (borrow a) -> Bool` | no | | `zipWith f xs ys` | reads elements, builds fresh | no | | `id`/`compose`/`apply`/`const`/`flip` | passthrough/seam modes | point-free — cut | | `iterate`/`twice` | borrow-navigation (`twice tail`); owning goes via `tail-app` | no | ### 4.4 The authoring rule that replaces mode-polymorphism The discipline leans entirely on features the language already has: 1. **Named projection / view → `borrow`.** `fst`, `snd`, field accessors, `tail` return borrowed views. 2. **Owning extraction → `match`.** Taking a piece and discarding the rest is the primitive destructure: `match` transfers ownership of bound components and drops the rest. No named owning-projection is needed. 3. **Ownership recovery from a borrowed view → explicit `clone`.** `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: - **Totality** (every position carries an authored mode; no `Implicit`, no exemption). The *declaration* axis. It admits no holes. Because "remove a default" is an atomic cutover (you cannot half-remove `Implicit`), totality lands as one coherent step over the whole surface. - **Soundness / verification** (the authored `own`/`borrow` is checked against the body's actual ownership flow). The *correctness* axis. It *may* phase: a mandatory-but-unverified mode (require-and-trust) is a **soundness** gap, not a **totality** hole. The parameter side is already on the verification axis today: `consume-while-borrowed` rejects a consumed `borrow` param, `over-strict-mode` warns on a never-consumed `own` param, and the uniqueness pass computes per-param `consume_count`. So extending totality to *parameters* lands on already-verified ground and is **compiler-assisted** — the existing consume analysis can derive and 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 explicit modes on every position. Mechanical for a controlled single-author corpus, and compiler-assisted for parameters via the existing consume analysis; still large. - **Canonical-form / hash reset.** The hashable canonical JSON omits `param_modes` / `ret_mode` *while they are all `Implicit`* (`skip_serializing_if`, `crates/ailang-core/src/ast.rs`), precisely to keep pre-mode-annotation modules bit-identical. Remove `Implicit` and every signature carries explicit modes → **every module hash shifts**, once, across the whole corpus, and every hash-pin test resets. This is the one genuinely irreversible consequence and the one to sign off on deliberately. - **The dangerous failure mode motivates the verification axis.** Under require-and-trust, the asymmetry of wrong annotations matters: a wrong `borrow` (declared borrow, actually fresh) merely *leaks*; a wrong `own` (declared own, actually a borrowed alias) makes the caller `dec` data it does not own → **double-free / use-after-free**. Totality pushes authors toward `own` as the default — the more dangerous direction — so the return-side `own`-verification (the first-order "is this return actually fresh?" check) is the highest-value piece of the soundness axis. What is **not** a cost: mode-polymorphism. Dropping it (§4) removes mode variables, mode unification, and call-site instantiation from the scope entirely — a saving, not a debt. ## 7. Open questions 1. **Cutover shape.** `Implicit`-removal is atomic (you cannot half-remove a default), so the first shippable state carries uniform modes + full migration. Without mode-polymorphism the step is smaller than the original cluster, but is there any hole-free *smaller* increment, or is the cutover irreducibly one large step? (Working hypothesis: irreducible.) 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? §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.** §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); 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. --- *Cross-references:* memory model `../contracts/0008-memory-model.md` (current `param_modes`/`ret_mode` contract, the `over-strict-mode` / `consume-while-borrowed` machinery); RC + uniqueness whitepaper `0004-rc-uniqueness.md`; the fieldtest that surfaced the leak `../../docs/specs/0061-fieldtest-typed-mir.md`.