Skip to main content

Quantitative Types — Atkey QTT in Verum

Every binder in Verum can declare a quantity q ∈ {0, 1, ω} controlling how many times its body may use the bound variable. The three levels — erased (0), linear (1), unrestricted (ω) — give one type system that subsumes phantom indices, capability tracking, file-handle linearity, and zero-cost ghost state.

1. The three quantities​

Atkey 2018 / McBride 2016 Quantitative Type Theory partitions binders into three resource classes:

QuantitySurfaceUse countRuntime presenceUse case
Zero@quantity(0)exactly 0erasedphantom indices, ghost state, spec-only parameters
One@quantity(1)exactly 1runtime-presentfile handles, mutexes, capabilities, transactions
Many@quantity(omega)any (≥0)runtime-presentstandard functional-programming default

Verum's kernel default is Many — without an explicit quantity annotation a binder is unrestricted, so all existing code keeps working. Quantity is opt-in; users who don't need linearity pay zero ergonomic tax.

2. Surface forms​

2.1 @quantity(...) typed attribute​

The canonical form is the @quantity(...) attribute, attached before a parameter:

public fn consume_handle(@quantity(1) handle: FileHandle) -> Result<Bytes>;
public fn fixed_width(@quantity(0) width: Int, value: Int) -> Vec<Int>;
public fn read_freely(@quantity(omega) x: Int) -> Int;

Three surface shapes accepted by the @quantity attribute parser:

FormExampleLowering
Integer literal@quantity(0) / @quantity(1)Quantity.Zero / Quantity.One
Path identifier@quantity(omega), @quantity(linear), @quantity(erased)parsed via Quantity.parse
String literal@quantity("omega")parsed via Quantity.parse

Aliases recognised by Quantity.parse:

SpellingResolves to
0, Zero, zero, erasedQuantity.Zero
1, One, one, linearQuantity.One
omega, ω, Many, many, unrestrictedQuantity.Many

Unknown spellings (@quantity(2), @quantity(affine), @quantity(infinity)) are rejected at parse time — silent acceptance of a typo would be a soundness hole.

2.2 Reject paths​

InputOutcome
@quantity(2)rejected — 2 not in {0, 1, omega}
@quantity(affine)rejected — affine is a type-level modifier (see §6) but not a binder quantity in Atkey QTT
@quantity (no args)rejected — missing required argument
@quantity(0, 1)rejected — exactly one argument required
@inline(0)inert — from_attribute returns None because the attribute name is not quantity

Every rejection path above is covered by parser-test fixtures in the compiler's attribute-handling test suite, so adding a new alias (or accepting a new shape) requires both a code change and a companion test.

3. Worked examples​

3.1 File-handle linearity (q=1)​

@quantity(1)
public fn consume_file(@quantity(1) f: FileHandle) -> Bytes {
    let bytes = read_all(f);   // f used exactly once — VALID
    bytes
}

// REJECTED by V2 enforcement:
public fn double_use(@quantity(1) f: FileHandle) -> (Bytes, Bytes) {
    let a = read_all(f.clone());
    let b = read_all(f);          // E_LINEAR_DOUBLE_USE — f used twice
    (a, b)
}

// REJECTED by V2 enforcement:
public fn never_use(@quantity(1) f: FileHandle) -> Int {
    42                            // E_LINEAR_NEVER_USED — f never referenced
}

3.2 Phantom width (q=0)​

public fn fixed_width<@quantity(0) Width: Int>(buf: [Byte; Width]) -> Hash {
    // Width is a compile-time index — used in the type, never at runtime.
    // Erased entirely from the generated code.
    sha256_of(buf)
}

// REJECTED by V2 enforcement:
public fn leak_width<@quantity(0) Width: Int>(buf: [Byte; Width]) -> Int {
    Width                          // E_ERASED_AT_RUNTIME — Width has q=0
                                   // and cannot appear in a value-level
                                   // (computational) position.
}

3.3 Default (q=ω)​

// Unrestricted — equivalent to no annotation at all.
public fn add_self(@quantity(omega) x: Int) -> Int { x + x }

// Default (no annotation) is also q=ω. Existing functions stay legal:
public fn id<T>(x: T) -> T { x }    // x has implicit q=ω

3.4 Mixed quantities​

public fn protocol_step(
    @quantity(0) state_invariant: Int,        // erased
    @quantity(1) capability:      Capability, // linear
    @quantity(omega) message:     Message,    // unrestricted
) -> NewState {
    consume(capability);                       // linear: used once
    log(message);                              // ω: any count
    log(message);                              // (still legal)
    next(message)                              // (and again)
}

4. Enforcement: what happens today, and what is intended​

warning
What the compiler does with @quantity today

Checked against the shipped compiler. @quantity is not in the parser's attribute table, so every use of it — legal or not — is answered the same way and the check finishes:

fn consume(@quantity(1) handle: Int) -> Int { handle }
// warning<W0400>: unknown attribute `@quantity`
// …and the program runs, printing 3 for consume(3).
  • Placement is not checked. @quantity(1) on a function — an illegal placement by this page's own rules — draws the same warning, and nothing else.
  • The argument is not checked. @quantity(zzz_not_a_quantity) is accepted identically; no diagnostic names the spelling.
  • The bare forms do not parse. @1 gives error<E013>: invalid attribute: missing attribute name after @.
  • None of the three use-count diagnostics fires. A @quantity(1) parameter used twice, one used never, and a @quantity(0) parameter read at runtime each produce the W0400 warning and nothing more. That is consistent with the staging described below — stated here so a reader does not test it and conclude their annotation was accepted.

The type-system side is real and separate: verum_types carries a Quantity and a QTT usage walk, and inference does read the attribute. What is missing is the front-end registration that would make @quantity a checked surface. Everything below describes the intended discipline.

The intended discipline is advisory at the binder level and enforced at the surface level:

  • The full grammar from §3 — bare @0 / @1 / @ω, the @quantity(...) long form, and every legal-vs-illegal placement — is parsed by the front-end, validated, and surfaced through diagnostics on illegal forms.
  • The annotation is preserved through to the IR, so quantitative information is available to downstream consumers (kernel, codegen) even when the body-level linearity walk does not yet run.
  • verum check src/ accepts every legal @quantity(...) annotation on parameter positions and rejects illegal placements.

The body-level use-count diagnostics (E_LINEAR_DOUBLE_USE, E_LINEAR_NEVER_USED, E_ERASED_AT_RUNTIME) are computed by a linearity-tracking pass that walks the function body after type checking. The walk follows McBride 2016 §3 — counting syntactic occurrences of each bound variable, summing along structural rules, and demanding that pattern matches consume the linear binder exactly once along every path. The pass is staged behind the surface discipline so that programs annotated with @quantity(...) remain valid through the rollout.

5. Interaction with other type-system features​

5.1 Refinement subtypes​

Quantity composes with refinement subtypes orthogonally — the quantity tracks use count while the refinement tracks value predicate. Both can decorate the same binder:

public fn read_bounded(@quantity(1) buf: Vec<Byte>{len(it) <= 4096}) -> Bytes;

The kernel's K-Refine rule (§7.3) and the linearity-tracking pass (§4.2 above) operate on the same AST node without interaction.

5.2 Refinement of the linear capability​

A q=1 capability with a refinement narrows the use site even further:

public fn debit_account(
    @quantity(1) tx: Transaction{state == Open},
    amount: Int,
) -> Transaction{state == Closed};

The linear discipline ensures the transaction is consumed exactly once (no double-spend); the refinement ensures the state is Open on entry and Closed on exit. Verum's combination delivers what F* / Liquid Haskell each do separately.

5.3 CBGR memory safety​

Quantitative types complement CBGR (§15.1) at a different layer: CBGR enforces temporal memory safety (no use-after-free); quantity enforces resource discipline (use exactly once). A function can take both a CBGR reference and a linear value:

public fn write_through(
    @quantity(1) handle: FileHandle,
    buf: &checked [u8],
) -> Result<()>;

5.4 Effect / context system​

Quantity is independent of the using [...] context system. A linear binder can come from a context-bound function call:

public fn dispense(@quantity(1) cap: SerialCap) -> Bytes
    using [Logger]
{
    log("dispensing");
    consume(cap)
}

The runtime context graph is entirely separate from the binder- linearity graph.

6. Difference from affine / linear type-level modifiers​

Verum has two linearity-related surfaces, easy to confuse:

SurfaceLayerGranularityWhat it tracks
affine type Foo { ... } (or linear)type declarationper-typethe values of type Foo are at-most-once / exactly-once consumable
fn f(@quantity(1) x: T)per-binderper-parameterthis specific binding of x is exactly-once

The type-level modifier (affine type Foo or linear type Foo) constrains the type's destruction contract — every value of an type affine carries the same "at most once" rule across its lifetime.

The binder-level quantity (@quantity(N) per this page) constrains this specific use site — different parameters of the same function can have different quantities even if their types are identical.

The two surfaces are orthogonal — a function can take an affine- typed argument with q=ω (the function uses the value freely; the caller still has to satisfy the at-most-once-globally rule) or a non-affine type with q=1 (this specific occurrence in this function is linear; other call sites of values of that type are not constrained).

7. CLI workflow​

verum check src/                     # parses + validates every @quantity(...)
verum verify src/                    # body-level linearity diagnostics
verum audit --epsilon                # @enact (Actic) is independent of quantity

verum audit --kernel-rules enumerates the kernel rules currently in force; the linearity rule (K-Quant) joins that list once the body- level pass enables it for a module.

8. Reading list​

  • Atkey, R. 2018. Syntax and Semantics of Quantitative Type Theory. LICS 2018. — the QTT calculus Verum's surface follows.
  • McBride, C. 2016. I Got Plenty o' Nuttin'. — the operational treatment of q ∈ {0, 1, ω} plus pattern-binding rules used by V2 enforcement.
  • Atkey & Krishnaswami 2015. Combining Linearity and Dependency. — interaction with dependent types.
  • Mai, Y. 2017. On Strict Linearity. — the linearity discipline (q=1 strictly, no relaxation to affine) Verum adopts by default.

9. Further Verum reading​

  • Trusted kernel — the kernel-level invariant layer that V2 quantity-checking will integrate with.
  • Refinement reflection — refinement subtypes pair orthogonally with quantity.
  • CBGR — runtime memory safety; complements quantity at a different layer.
  • — the normative source for this page.