AILang/design/models/0008-ownership-totality.md

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<ParamMode>, 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.