# Linear


Graded linear resource tracking: acquire/consume/release with usage enforcement.

Each resource gets a capability token at acquire time. The graded handler
covers linear (exactly once), affine (at most once via release), exact(n),
and unlimited usage through a single maxUses parameter.

Quick start:

```nix
let comp = bind (linear.acquireLinear "secret") (token:
  bind (linear.consume token) (val:
    pure val));
in linear.run comp
```

For composition with other handlers, use handler/return/initialState with
`adaptHandlers`.

## `acquire`

_acquire: take a graded linear resource and obtain a capability token; `maxUses` (or null) sets the linearity bound enforced by the handler._

```
acquire : { resource : a, maxUses : Int | null } -> Computation Token
```

Acquire a graded linear resource. Returns a capability token.

The token wraps the resource with an ID for tracking. The handler
maintains a resource map in its state, counting each consume call
against the maxUses bound.

- `maxUses = 1` — Linear: exactly one consume required
- `maxUses = n` — Exact: exactly n consumes required
- `maxUses = null` — Unlimited: any number of consumes allowed

Tokens should be consumed exactly maxUses times, or explicitly
released. At handler exit, the return clause (finalizer) checks:
released → always OK, `maxUses = null` → always OK,
otherwise → `currentUses` must equal `maxUses`.

## `acquireExact`

_acquireExact: acquire a resource that must be consumed exactly `n` times; encodes graded linearity beyond pure linear/affine._

```
acquireExact : a -> Int -> Computation Token
```

Acquire a resource that must be consumed exactly n times.

## `acquireLinear`

_acquireLinear: acquire a strictly linear resource (maxUses = 1); the finalizer fails unless exactly one consume happens before scope exit._

```
acquireLinear : a -> Computation Token
```

Acquire a linear resource (exactly one consume required).

## `acquireUnlimited`

_acquireUnlimited: acquire a resource with `maxUses = null`; the finalizer never reports usage mismatches for unlimited tokens._

```
acquireUnlimited : a -> Computation Token
```

Acquire an unlimited resource (any number of consumes allowed).

## `consume`

_consume: spend a use of a capability token and return the wrapped resource; aborts with `LinearityError` on use-after-release or bound-exceeded._

```
consume : Token -> Computation a
```

Consume a capability token, returning the wrapped resource value.

Increments the token's usage counter. Aborts with `LinearityError` if:
- Token was already released (`"consume-after-release"`)
- Usage would exceed maxUses bound (`"exceeded-bound"`)

The returned value is the original resource passed to acquire.

## `handler`

_linear.handler: interprets linearAcquire/linearConsume/linearRelease over a `{ nextId, resources }` state; emits tagged LinearityError on misuse._

Graded linear resource handler. Interprets linearAcquire, linearConsume,
and linearRelease effects. Tracks resource usage in handler state.

Use with `trampoline.handle`:

```nix
handle {
  handlers = linear.handler;
  return = linear.return;
  state = linear.initialState;
} comp
```

Or use the convenience: `linear.run comp`

- `linearAcquire`: creates token, adds resource entry to state
- `linearConsume`: increments usage counter, returns resource value
- `linearRelease`: marks resource as released (finalizer skips it)

## `initialState`

_linear.initialState: `{ nextId = 0; resources = {}; }`; monotonic ID counter plus an empty resource map indexed by stringified ID._

Initial handler state for the linear resource handler.

```nix
{ nextId = 0; resources = {}; }
```

- `nextId`: monotonic counter for generating unique resource IDs.
- `resources`: map from ID (string) to resource tracking entry.

## `release`

_release: drop a capability token without consuming it; the finalizer then skips it (affine usage). Aborts on double-release._

```
release : Token -> Computation null
```

Explicitly release a capability token without consuming it.

Marks the resource as released. The finalizer skips released resources,
so this allows affine usage (acquire then drop). Aborts with
`LinearityError` on double-release.

## `return`

_linear.return: finalizer checking every non-released, finite-bound resource was consumed exactly `maxUses` times; wraps mismatches in LinearityError._

```
return : a -> State -> { value : a | LinearityError, state : State }
```

Finalizer return clause for the linear handler.

Checks each resource in handler state:
- `released` → OK (explicitly dropped)
- `maxUses = null` → OK (unlimited)
- otherwise → `currentUses` must equal `maxUses`

On violation, wraps the original value in a `LinearityError` with
details of each mismatched resource. On success, passes through
unchanged. Runs on both normal return and abort paths.

## `run`

_linear.run: convenience wrapper bundling handler, return, and initialState; runs a computation under the graded linear discipline._

```
run : Computation a -> { value : a | LinearityError, state : State }
```

Run a computation with the graded linear handler.

Bundles handler, return clause, and initial state into one call.
To compose with other handlers, use handler/return/initialState
separately with `adaptHandlers`.

```nix
let
  comp = bind (acquireLinear "secret") (token:
    bind (consume token) (val:
      pure "got:${val}"));
in linear.run comp
# => { value = "got:secret"; state = { nextId = 1; resources = { ... }; }; }
```