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:

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:

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.

{ 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.

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