# 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:

```nix
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:

```nix
{ _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