Linear and affine

Linear and affine — the dyadic discipline

What / why / where. Ephapax has two ways to introduce a binding — affine (let) and linear (let!) — and the choice is made per-binding, not per-type or per-function. Affine values may be used at most once; linear values must be used exactly once. The discipline is enforced by the typechecker via the BindingForm tag in src/ephapax-typing/src/lib.rs. This page explains what the two forms mean operationally, why per-binding selection is unusual, and how Ephapax compares to Rust's ownership and Linear Haskell's linear arrows.

If you want the proof-side picture instead, jump to Region-calculus (which proves no-escape + no-GC over a linear-aware region context) or Proof status (splitLinearCoverage, no_consumption_at_true_linear, the substitution lemma).

---

The two forms, operationally

A binding form determines two things at once: how many times the variable may be referenced, and what happens if a code path doesn't use it.

Form	How many uses	If unused	Implicit drop
let x = e	0 or 1	OK	yes
let! x = e	exactly 1	type error	no

Affine let is the more permissive form: not using it is fine, using it once is fine, using it twice is rejected. The "drop" at end-of-scope is implicit and free (for region-allocated values, the region exit bulk-frees them; see Region-calculus).

Linear let! is the stricter form: every code path through the binding's scope must consume it exactly once. The typechecker tracks usage with a used: bool flag on each context entry and verifies, at every control-flow merge and at every region exit, that no let! binding remains unconsumed.

Function parameters are treated by a third rule: a parameter of linear type behaves like let!, a parameter of non-linear type behaves like let. See the demands_consumption method on CtxEntry.

fn example() -> i32 {
    let! x = 42;       // linear: must be used exactly once
    x                  // OK: x consumed exactly once
}

(from conformance/valid/linear_consumed.eph)

---

What goes wrong if you break the rule

conformance/invalid/ has one .eph source per error code; each is the smallest program that exercises the rule.

let! never used — error E001, linear_not_consumed.eph:

fn example() -> i32 {
    let! x = 42;
    // x is never used — linear violation
    0
}

let! used twice — error E002, linear_used_twice.eph:

fn example() -> i32 {
    let! x = 42;
    let a = x;     // first use — consumes x
    let b = x;     // second use — ERROR
    a + b
}

Branches disagree — error in the "branches consume different linear resources" family, branch_inconsistent.eph:

fn example(cond: bool) -> i32 {
    let! x = 42;
    if cond { x } else { 0 }   // one branch consumes x, other doesn't
}

The third case is the subtle one: a linear discipline must be path-sensitive. Ephapax requires both arms of a conditional to agree on which linear bindings they consumed. See What can go wrong for the full failure-mode catalogue.

For the contrast, conformance/valid/dyadic_mix.eph mixes both forms in a single function: linear let! for the database connection and transaction (must be consumed), affine let for the intermediate query results (can be dropped if unused).

---

How the checker enforces it

The discipline lives entirely in two data structures in ephapax-typing/src/lib.rs:

pub enum BindingForm {
    Let,        // let:    use at most once, implicit drop OK
    LetBang,    // let!:   use exactly once, no implicit drop
    Param,      // fn arg: linear iff type is linear
}

struct CtxEntry {
    ty: Ty,
    used: bool,
    binding_form: BindingForm,
    region: Option<RegionName>,   // see Region-calculus
}

Three rules are checked:

1. At every variable reference, if the binding is in a form that demands exactly-once consumption and its used flag is already set, the typechecker rejects (E002). Otherwise the flag is set and the reference is allowed.

2. At every region exit, every entry whose region == current_region and whose demands_consumption() is true must have used == true, else E001 / E004.

3. At every branch merge (if/match), the two arms' contexts must agree on which linear bindings they consumed.

The Idris2 frontend in idris2/src/Ephapax/Affine/Typecheck.idr does the same job with a Mode = Affine | Linear mode parameter and a used: Bool field on Entry. The two checkers are kept in step by conformance/ — every valid/invalid program must round-trip through both.

---

Why per-binding, not per-type?

Most substructural type systems put the discipline on the type or on the function arrow:

• Rust says: every value is affine. Drop exists because Rust has no way to express "must be consumed". You cannot have a Rust value that the compiler refuses to let you implicitly drop.

• Linear Haskell puts a multiplicity on the function arrow: f :: a %1-> b takes its argument linearly. The argument's type doesn't change; the function's signature does. Two functions with the same domain can disagree on whether they treat that domain linearly.

• Idris 2 QTT puts a quantity (0, 1, or ω) on each binder. This is strictly more expressive than let/let! but also strictly more annotation-heavy: every function signature carries quantities on every argument.

Ephapax takes a middle path. The discipline rides on the binding form, not the type or the arrow. The same value 42 : i32 can be bound affinely (let x = 42) in one place and linearly (let! x = 42) in another. The signature of a function does not have to commit to a discipline — the caller chooses at the call site, depending on whether they intend the returned value to be droppable.

The practical consequence: you can write a Db.connect that returns a connection handle, and the caller decides — by writing let! — that this particular connection must be closed before end-of-scope. Linear Haskell would force the discipline into Db.connect's arrow type. Rust would have no way to express it.

See docs/specs/LANGUAGE-COMPARISON.adoc for the full feature matrix, and Comparison to other languages for the wiki-friendly summary.

---

Cross-references

• Region calculus — how the discipline interacts with scoped allocation
• What can go wrong — full failure-mode catalogue
• Comparison to other languages — how this compares to Rust, Linear Haskell, Idris 2, ATS, …
• Glossary — definitions of "affine", "linear", "borrow", "second-class", "well-formed CNF"
• Proof status — what's mechanically verified about the discipline in Coq + Idris 2