Linear

Linear type constructors: structural guards for capability tokens.

Pure type predicates that check token structure without consuming. Usage enforcement is in effects/linear.nix (separate concerns).

Linear(T) — exactly one consume required Affine(T) — at most one consume (release allowed) Graded(n, T) — exactly n consumes (generalizes Linear/Affine)

See Orchard et al. (2019) for graded modal types.

Affine

Affine: structural type constructor for capability tokens that may be consumed at most once; identical shape to Linear, release is permitted.

Affine : Type -> Type

Affine type: capability token that may be consumed at most once.

Structurally identical to Linear(T). The name communicates that the resource may be explicitly released (dropped) via effects/linear.release without consuming it — "at most once" vs Linear's "exactly once."

The structural guard is the same: both check for a valid capability token with inner type T. The usage distinction (exactly-once vs at-most-once) is enforced by the effect handler, not the type system.

Operations:

• .check v — pure guard: is v a valid affine token wrapping T?
• .validate v — effectful: sends typeCheck for blame tracking
• .innerType — the wrapped type T

Graded

Graded: structural type constructor for capability tokens with declared usage multiplicity; generalises Linear/Affine via the maxUses parameter.

Graded : { maxUses : Int | null, innerType : Type } -> Type

Graded type: capability token with usage multiplicity annotation.

Generalizes Linear and Affine via a maxUses parameter:

Graded { maxUses = 1; innerType = T; }    # ≡ Linear(T)
Graded { maxUses = null; innerType = T; }  # ≡ Unlimited(T)
Graded { maxUses = n; innerType = T; }     # ≡ Exact(n, T)

The structural guard is the same as Linear and Affine — token structure with inner type check. The maxUses appears in the type name for documentation but is NOT checked by the guard (the grade lives in handler state, not the token).

The name uses ω for null (unlimited): Graded(1, Int), Graded(5, String), Graded(ω, Bool)

From Orchard et al. (2019) "Quantitative Program Reasoning with Graded Modal Types" — semiring-indexed usage annotations where + models branching, × models sequencing, 1 = linear, ω = unlimited.

Operations:

• .check v — pure guard: is v a valid graded token wrapping T?
• .validate v — effectful: sends typeCheck for blame tracking
• .innerType — the wrapped type T
• .maxUses — the declared usage multiplicity

Linear

Linear: structural type constructor for capability tokens that must be consumed exactly once; checks token shape, leaves usage tracking to the linear effect handler.

Linear : Type -> Type

Linear type: capability token that must be consumed exactly once.

Creates a type whose check verifies the capability token structure:

{ _linear = true, id = Int, resource = innerType }

Pure structural guard — checking does not consume the token. effects/linear.nix tracks consumption separately.

Adequacy invariant:

Linear(T).check v ⟺ all typeCheck effects in Linear(T).validate v pass

Holds by construction via mkType's auto-derived validate.

Operations:

• .check v — pure guard: is v a valid linear token wrapping T?
• .validate v — effectful: sends typeCheck for blame tracking
• .innerType — the wrapped type T