Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

docs(design): add the ownership-totality whitepaper (model 0008)

Browse Source 
Exploratory model that converges the direction sparked by the
typed-MIR fieldtest Implicit-return leak (spec 0061). It is not
current state and not an approved milestone — the surface still
defaults ParamMode::Implicit; the file fixes a future shape before
committing it to specs.

The converged shape:

- Ownership is authored, never defaulted. Implicit is removed from
  the authorable surface; every parameter and return carries
  own/borrow. A default cannot be half-removed, so totality is the
  only coherent stopping point.
- Value types take trivial-own; borrow over a value type is an
  error. The surface stays uniform so the author needs no knowledge
  of which types are heap.
- No mode-polymorphism. A type-variable position is never a hole
  under fixed modes — it takes a concrete own/borrow. Mode variables
  would only remove duplication, and the reuse-across-modes need is
  confined to point-free combinators (cut by the language identity)
  and the consume-vs-preserve container duality (better expressed as
  two named functions). Structurally, AILang iterates via tail-app,
  not passed-function combinators, so the higher-order own/borrow
  clash does not arise. ParamMode stays binary {Own, Borrow}.

Left open: cutover shape, verification sequencing, glossary naming.
The one irreversible consequence — a corpus-wide module-hash reset
once Implicit stops eliding the mode fields from canonical JSON — is
named for deliberate sign-off.
This commit is contained in:
Brummel
2026-06-01 10:53:41 +02:00
parent 7a99c5dbfa
commit 768189abce
1 changed files with 277 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
design/models/0008-ownership-totality.md
+277
View File
@@ -0,0 +1,277 @@
# Ownership totality — authored own/borrow everywhere whitepaper
**STATUS.** *Design exploration — NOT current state, NOT an approved
milestone.* Nothing here is shipped; the present surface still has
`ParamMode::Implicit` as the parser default on both parameters and
returns. This whitepaper records the **converged shape** of a possible
direction — the points the design discussion has settled — and isolates
the genuinely-open questions in §7. 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. 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.
---
## 1. The leak that motivates it
A user function whose return **type** is an RC-heap value (`Str`, or a
boxed ADT) but whose signature omits the ownership mode carries
`ret_mode == ParamMode::Implicit` — the parser's silent default, which
nothing infers post-parse. Codegen reads `Implicit` faithfully: the
caller does **not** `dec` the returned slab, so the owned allocation
leaks (`live = 1` under `AILANG_RC_STATS`). This is documented
intentional behaviour today: `../contracts/0008-memory-model.md` states
`ret_mode` is author-required and never inferred, and the
`examples/rc_let_implicit_returning_app.ail` fixture asserts `live = 1`
as correct under the Implicit back-compat lane.
The leak is the symptom. The cause is that an ownership default exists
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 makes this concrete: the typechecker
already treats `Implicit ≡ Own` (`ParamMode::mode_eq`,
`crates/ailang-core/src/ast.rs`), yet codegen reads `Implicit`
separately and omits the caller `dec`. The *same* fn-type is read two
ways depending on whether one knows 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.
## 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.
## 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.
## 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?
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.
**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).
---
*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`.