Capabilities

March makes side effects visible in your types — zero runtime overhead, enforced at compile time. This guide explains what capabilities are, when to reach for each kind, when to leave them alone, and how they compose.

The problem they solve

In most languages, a function’s signature tells you what data flows in and out. It says nothing about what the function does to the world:

# Does this read a file? Call the network? Write to a database?
# You have to read the implementation to find out.
def compute_price(product_id: str) -> float:
    ...

That invisibility causes three recurring problems:

Accidental effects. A function you thought was pure secretly calls a logger, which opens a file, which fails in a read-only sandbox. You find out at runtime.

Unclear contracts. “Does this library ever write files?” requires reading all the source. No amount of documentation fully substitutes for a machine-checked declaration.

Audit blind spots. Answering “which modules talk to the network?” in a large codebase means grepping and hoping — unless the compiler tracks it.

March’s capability system addresses all three. Effects appear in the type, and the compiler traces them through the call graph — with one honesty caveat worth stating up front: the absence of a capability declaration is a machine-verified, build-breaking guarantee wherever Cap(X) flows through a signature (a function/actor/extern parameter, or a transitive use of another module that requires one) — that surface is enforced as a hard error. A module that calls an IO builtin directly in a function body, without ever threading a Cap(X) through any signature, is instead flagged with a warning-level hint: informative, but --check still exits 0. See “What the compiler tells you,” below, for both sides of that line, live-verified.

mod Price do
  -- No `needs`, and every parameter here is an ordinary value — no `Cap(X)`
  -- anywhere in the signature. This module cannot be forced to declare a
  -- capability it doesn't have, and calling into it can never trigger a
  -- signature-level cap error.
  fn compute(base : Float, discount : Float) : Float do
    base * (1.0 - discount)
  end
end

Which tool do I need?

IO permission caps

Every module that touches external resources declares needs:

mod Server do
  needs IO.Network

  fn listen(cap : Cap(IO.Network), port : Int) : () do
    ...
  end
end

The compiler enforces this transitively when the capability flows through a signature: Server.listen takes Cap(IO.Network) as a parameter, so any module that uses Server and calls listen must itself declare needs IO.Network (directly or via a broader ancestor, e.g. needs IO), or the build fails with a clear message telling you which import requires which cap — e.g. a Caller module useing Server without needs IO.Network gets module `Caller` imports `Server` which requires `Cap(IO.Network)`, but `IO.Network` is not declared in `needs`.. This is a hard compile error for the signature/use/extern surface — see “What the compiler tells you,” below, for the separate, weaker case where a module reaches for an IO builtin directly in a function body without ever putting Cap(X) in a signature.

Capability hierarchy

Cap(IO) is the root. Sub-capabilities narrow what is allowed:

IO
├── IO.Console          — stdout/stderr (println, print)
├── IO.FileSystem
│   ├── IO.FileRead     — read files, list directories
│   └── IO.FileWrite    — write, delete, rename files/dirs
├── IO.Network
│   ├── IO.NetConnect   — outbound TCP, WebSocket
│   │   ├── IO.NetConnect.TLS  — encrypted transport (tls_connect, tls_accept, …)
│   │   └── IO.Database — database connections (declaration-only; child of NetConnect)
│   └── IO.NetListen    — bind + listen on a port
├── IO.Process          — env vars, child processes, process exit
├── IO.Clock            — wall clock, monotonic time
├── IO.Random           — CSPRNG (random_bytes, uuid_v4)
├── IO.Signal           — OS-signal watchers (Signal.watch/unwatch/raise)
├── IO.Spawn            — task spawning (task_spawn, task_spawn_link, …)
├── IO.Mut              — shared mutable state (Vault tables)
├── IO.Telemetry        — telemetry/observability emission (declaration-only)
└── IO.Foreign          — calling unverified C (extern blocks)
    └── IO.Foreign.Blocking — blocking extern (spawns OS thread)

A module that declares needs IO can pass Cap(IO) to any function that requires a narrower cap. Use cap_narrow to produce a sub-capability — it’s free, compile-time only:

fn start(cap : Cap(IO)) : () do
  let net_cap  : Cap(IO.Network)        = cap_narrow(cap)
  let tls_cap  : Cap(IO.NetConnect.TLS) = cap_narrow(cap)
  Server.listen(net_cap, 8080)
end

Choosing the right level

Use the narrowest capability that accurately describes what the code actually does. Narrower declarations make stronger claims; the compiler verifies them.

In libraries, prefer narrow caps. A library that only reads config files should declare needs IO.FileRead, not needs IO. Callers can then hand it a read-only view, statically proving it cannot secretly write.

In entry points, needs IO is fine. The interesting precision lives in the libraries. Application main modules compose everything; they don’t need to obsess over narrowing.

What the compiler tells you

There are two severities, and which one you get depends on where the uncovered capability shows up — this honest distinction matters, so it’s stated explicitly rather than glossed over.

Signature, transitive use, or extern — a build-breaking ERROR (--check exits 1). If Cap(X) appears in a function/actor/extern parameter, or you use a module that itself needs a capability you haven’t declared, there is no way to ship without fixing it:

$ march --check caller.march   # `use`s a module needing Cap(IO.Network), no `needs IO.Network` of its own
-- ERROR --
module `Caller` imports `Server` which requires `Cap(IO.Network)`, but `IO.Network` is not declared in `needs`.
help: add `needs IO.Network` to the module body.
$ echo $?
1

A direct body call to an IO builtin, with no Cap(X) anywhere in a signature — a WARNING (--check exits 0). The compiler still tells you exactly what’s missing and how to fix it — this is genuinely useful, actionable feedback — but it does not fail the build:

$ march --check reader.march   # fn slurp(path) : Result(String, String) do file_read(path) end — no needs
-- HINT --    call to `file_read` requires `needs IO.FileRead` — add `needs IO.FileRead` to module `Reader`
-- WARNING -- function body calls a builtin that requires `Cap(IO.FileRead)` but `Reader` does not declare `needs IO.FileRead`.
$ echo $?
0

Follow the hint either way — it’s always correct, and cleaning up the warning keeps a module’s needs list an accurate account of what it does. But don’t rely on the warning to block a merge or a release: it won’t. If you need “this module absolutely cannot read files” as a hard, CI-enforced guarantee, thread Cap(IO.FileRead) through the relevant signatures so the violation lands on the ERROR side of this line, not the WARNING side.

When not to use IO caps

Pure functions need nothing. If a function hashes a string, parses JSON, sorts a list, or formats a number, write no needs. The absence of needs is a machine-verified guarantee of the ERROR-level kind above only for the signature/use/extern surface — the compiler cannot force you to declare a capability that never appears in a signature and is never transitively required by an import, so this guarantee is strongest when the functions in question actually take Cap(X) parameters (or use something that does). A module with no needs that calls IO builtins purely in function bodies will typecheck (--check exits 0) with only advisory warnings, not a rejection — see above.

Don’t over-narrow to look principled. Declaring needs IO.FileRead when your function also writes is a lie the compiler will catch. If a function reads and writes, needs IO.FileSystem is correct even if it feels “less precise.” Accurate beats narrow-but-wrong.

Don’t use IO caps for pure domain concepts. A function that validates an email address or checks a constraint has no business with capabilities. Capabilities exist for external state, not for logic.

Don’t use capabilities for per-value guarantees. Cap(IO.FileRead) proves a module is allowed to read files; it says nothing about whether a specific string value came from a trusted source. For per-value guarantees, use an opaque refined type.

Small scripts: just use needs IO. For a 50-line script you’ll run once, fine-grained capability declarations add more friction than value. Use needs IO at the top and move on. The value of narrow caps emerges in larger codebases with multiple contributors over time.

Specific IO capabilities

IO.Mut — shared mutable state

IO.Mut covers Vault tables — process-global shared mutable hash maps. A module with no needs IO.Mut is statically proven never to touch shared mutable state:

mod Cache do
  needs IO.Mut

  fn store(key : String, val : Int) : () do
    let tbl = Vault.new("app_cache")
    Vault.set(tbl, key, val)
  end
end

This is especially useful for library code that should have no hidden state.

IO.NetConnect.TLS — encrypted transport only

IO.NetConnect.TLS is a child of IO.NetConnect. Declaring it (without IO.NetConnect) proves the module uses only encrypted connections — no plaintext TCP. Declaring needs IO.NetConnect covers both.

mod HttpsClient do
  needs IO.NetConnect.TLS  -- plaintext TCP is statically excluded

  fn fetch(fd, h, host) do
    tls_connect(fd, h, host)
  end
end

IO.Telemetry — observability annotation

IO.Telemetry is declaration-only: the compiler accepts it as a semantic annotation but does not scan for specific builtins. Use it to make telemetry visible in a module’s surface contract so callers know this module emits observability data:

mod Metrics do
  needs IO.Telemetry

  fn record_request(duration : Int) : () do
    ...
  end
end

IO.Foreign — calling unverified C

IO.Foreign is a meta-capability triggered by the presence of an extern block — not by any specific builtin call. C code bypasses every March type guarantee, so the compiler requires you to acknowledge this explicitly.

mod Bindings do
  needs IO.Foreign
  needs IO.FileSystem  -- the specific cap the C code uses

  extern "libc": Cap(IO.FileSystem) do
    fn read(fd : Int, buf : String, n : Int) : Int
  end
end

The blocking modifier spawns an OS thread. Declare both caps when any extern function is blocking:

mod Bindings do
  needs IO.Foreign
  needs IO.Foreign.Blocking
  needs IO.FileSystem

  extern "libc": Cap(IO.FileSystem) do
    blocking fn slow_read(fd : Int) : Int
  end
end

needs IO.Foreign alone subsumes IO.Foreign.Blocking (parent covers child), so one declaration suppresses both warnings if you prefer coarser annotations.

Behavioral module caps — cap no_panic, cap no_alloc, cap no_extern, cap pure, cap deterministic

Beyond IO permission caps and proof caps, March has five behavioral capability declarations that trigger static analysis passes rather than IO-permission accounting. They share only the cap keyword with needs/Cap(X) — a module can declare cap no_panic and separately declare needs IO.Network, and the two mechanisms never interact. Each lives as a bare cap <name> statement in the module body.

cap no_panic — guaranteed panic-free

mod SafeMath do
  cap no_panic

  fn divide(a : {v : Int | v >= 0}, d : {v : Int | v > 0}) : Int do
    a / d
  end
end

A module with cap no_panic must not contain any expression that can panic at runtime. The compiler enforces this with three sub-checks:

1. Panic-surface ban — bans direct and transitive calls to a fixed panic surface: explicit panic/todo/unreachable, the prelude partial functions (unwrap, expect, head, tail, last), and dotted stdlib partials (List.nth, Option.unwrap, Result.unwrap, Array.get, …). Transitive means a local helper that calls one of these makes every local caller of that helper panicky too.
2. Division safety — proves every integer divisor is non-zero via the Z3 SMT solver. Both literal divisors (a / 0 → immediate error) and variable divisors are handled:
   • Variable with an Int refinement {v | pred}: Z3 discharges pred ⊢ v ≠ 0; fast syntactic short-circuit for common patterns (v > 0, v >= 1, v != 0, v < 0).
   • Let-bound variable: Z3 discharges var = rhs ⊢ var ≠ 0 with param assumptions injected.
   • No refinement or unsupported expression: conservative error.
3. Non-exhaustive match ban — inside a cap no_panic module, a match that doesn’t cover every constructor is an ERROR, not just the ordinary non-blocking exhaustiveness warning every other module gets: an uncaught pattern is a runtime panic (“no matching clause”), and cap no_panic exists precisely to rule that class of failure out.

When Z3 is absent, cap no_panic is still conservatively enforced — unverifiable divisions are treated as errors.

Use Math.checked_div / Math.checked_mod when you cannot prove the divisor non-zero statically; they return Option(Int) instead of panicking.

cap no_alloc — no heap allocation

mod RealTimeDSP do
  cap no_alloc

  fn mix(a : Float, b : Float, gain : Float) : Float do
    (a + b) * gain
  end
end

cap no_alloc walks every function body and flags heap-allocating expressions:

Nullary constructors (None, True, False, custom zero-arg tags) and unit () are safe — they compile to immediate integer tags with no heap allocation.

The check recurses into sub-expressions inside if, match, let, blocks, etc.

cap no_extern — no foreign calls

mod NoFFIService do
  cap no_extern
  needs IO.Network

  fn ping(_cap : Cap(IO.Network), host : String) : Int do
    string_length(host)
  end
end

A module with cap no_extern may not contain an extern block and may not declare needs IO.Foreign — either one is an immediate error. Useful for a module that must stay pure C-free code, e.g. because it needs to run somewhere extern’s FFI trust boundary isn’t available.

cap pure — no side effects at all

mod PureMath do
  cap pure

  fn add(a : Int, b : Int) : Int do
    a + b
  end
end

A module with cap pure bans every call to a builtin that performs any side effect — file IO, network IO, spawning, sending, vault access, console output, randomness, the clock — as well as spawn/send/exit. The banned set is derived from the same authoritative builtin-to-capability table (builtin_cap_table) the ordinary IO-cap body-scan check consults, so it stays in sync with the real builtin surface — a module declaring cap pure and calling file_write is rejected:

$ march --check leaky_pure.march   # cap pure; fn write(...) : Result(Unit, String) do file_write(path, contents) end
-- ERROR -- `write` in `mod LeakyPure` (declared `cap pure`) calls `file_write`, which has side effects.
$ echo $?
1

cap deterministic — no clock, no randomness

mod DeterministicSim do
  cap deterministic

  fn checksum(bytes : String) : Int do
    string_length(bytes)
  end
end

cap deterministic is strictly weaker than cap pure: it bans only the two nondeterminism sources — wall-clock/monotonic-clock reads and random-number generation — so a cap deterministic module may still perform ordinary IO such as file_read, as long as it never touches the clock or an RNG:

$ march --check clock_leak.march   # cap deterministic; calls unix_time_ms(())
-- ERROR -- `now` in `mod DetLeak` (declared `cap deterministic`) calls `unix_time_ms`, which is non-deterministic.
$ echo $?
1

Choosing among the five

All five declarations can coexist in the same module. Each is checked by its own independent pass, and none of them subsumes or implies any other.

Capability inference hints

If you call a function that requires a needs X declaration but your module doesn’t have one, the compiler emits a hint (not an error) pointing to the call site:

hint: this call uses IO.FileRead but mod Config does not declare `needs IO.FileRead`.
hint: add `needs IO.FileRead` to the module body.

This is informational, and it is not necessarily backed by a type error — do not assume one is coming. The type checker enforces needs as a hard error only when Cap(X) reaches a signature, a transitive use, or an extern block (see “What the compiler tells you,” above). A hint attached to a plain body call to an IO builtin, with no Cap(X) in any signature, can appear on a program that otherwise checks clean — the hint is the whole story in that case, not a preview of a rejection.

Putting it together

Here’s how capability declarations compose across a small web application. Reading the needs list of each module answers “what does this module do to the world?” without opening the implementation:

mod AppConfig do
  -- Note: named `AppConfig`, not `Config` — `Config` is already a stdlib
  -- module (`stdlib/config.march`), and a user module of the same name
  -- would collide with it once this file joins a real multi-file build.
  needs IO.FileRead          -- reads one config file, nothing else

  type AppConfig = AppConfig

  fn load(path : String) : AppConfig do ... end
end

mod Metrics do
  needs IO.Telemetry         -- makes observability a visible architectural concern

  fn record(event : String, duration : Int) : () do ... end
end

mod Api do
  -- Likewise `WebServer`/`ConnCtx` here, not `HttpServer`/`Conn` — those
  -- names are already taken by stdlib's `HttpServer` module.
  use WebServer

  needs IO.NetListen         -- binds a port
  needs IO.NetConnect.TLS    -- outbound HTTPS only — no plaintext TCP
  needs IO.Mut               -- session vault

  fn start(io : Cap(IO.NetListen), tls : Cap(IO.NetConnect.TLS),
           mut : Cap(IO.Mut)) : () do
    WebServer.new()
    |> WebServer.plug(fn conn -> handle(conn, tls, mut))
    |> WebServer.run(io, 8080)
  end
end

mod Main do
  use AppConfig
  use Api

  needs IO

  -- The initial Cap(IO) is provided implicitly by the runtime to `main()` —
  -- there is no `root_cap()` call in user code.
  fn main(cap : Cap(IO)) : () do
    let config  = AppConfig.load("/etc/myapp/config.toml")
    let io_cap  : Cap(IO.NetListen)      = cap_narrow(cap)
    let tls_cap : Cap(IO.NetConnect.TLS) = cap_narrow(cap)
    let mut_cap : Cap(IO.Mut)            = cap_narrow(cap)
    Api.start(io_cap, tls_cap, mut_cap)
  end
end

AppConfig is provably read-only. Api cannot read files and cannot use plaintext TCP. If AppConfig.load ever called a network function, the build would fail until needs IO.NetConnect was added — no audit needed.

Runtime behaviour

All Cap(X) values are runtime-erased. They compile to null in LLVM IR and to VUnit in the interpreter. No allocation, no indirection, no overhead. Enforcement is purely at compile time.

Hot-deploy authorization — node-local admission control

When using forge deploy hot to upgrade a running application, the node has a second opportunity to enforce capability discipline at deployment time — after signature verification, before the new code is loaded.

This section covers the node-side policy gate. There is also a client-side monotonicity gate — a deploy that widens a function’s authority beyond the running version aborts unless you pass --grant-cap. Both gates, with a full worked example (a console-only handler that gains file_write, and how each gate responds), are in the Hot Code Reload guide → Capability-safe deploys.

How it works

A hot deploy activates only the functions that changed (each is sent as a separate signed activation message). For each activated function, forge deploy hot embeds that function’s own inferred IO capabilities — the capabilities its own body actually requires — in the message. Admission is checked per activated function, not over the whole artifact. (This granularity matters: --hot-reload links the entire standard library, so a whole-artifact capability set would be dominated by the stdlib’s footprint and identical for every app — useless for a policy. Gating on the changed function’s own caps is what makes the policy discriminating.) The trust boundary is: the base server binary is trusted — the operator built and started it, with a policy — and each hot-patched function is what the gate governs.

The receiving node, for each activated function:

1. Recomputes the capability set — normalizes the function’s declared caps and hashes them with BLAKE3, reproducing the digest that was signed during the deploy.
2. Tamper-checks — compares its computed digest to the signed value; a mismatch (ERR cap_tamper) aborts before dlopen. The tamper check is unconditional even when the function declares no capabilities: a genuinely cap-free function has the fixed digest blake3(""), so a stripped capability field on a signed message is detected rather than silently admitted.
3. Applies the deployment policy — if MARCH_DEPLOY_POLICY is set (a file path), the node verifies that every capability the activated function declares is subsumed by a capability listed in the policy; a capability outside policy (ERR cap_policy <cap>) aborts.

Configuring the policy

Set the MARCH_DEPLOY_POLICY environment variable to a file path:

export MARCH_DEPLOY_POLICY=/etc/march/deploy-policy.txt

The policy file is line-delimited. Each non-empty, non-comment line is a permitted capability path:

# /etc/march/deploy-policy.txt
IO
IO.FileRead
IO.NetConnect.TLS
IO.Clock

An empty policy file or absent MARCH_DEPLOY_POLICY ⇒ permissive (all activations admitted). This is the default for backward compatibility. A policy constrains what hot-patched functions may do; it does not retroactively constrain the trusted base binary the operator already deployed.

Threat model and scope

The policy is authorization on a self-reported manifest — a defense-in-depth layer, not a sandbox. A party with the signing key can lie about what capabilities the code uses. The node admission gate proves:

• The artifact was signed by the expected entity (Phase 4 ed25519 signature).
• The declared capability set has not been tampered with in transit (BLAKE3 tamper-check).
• The declared capabilities are within a static policy envelope (subsumption check).

It does not prove that the code actually uses only those capabilities — only that the manifest claims it does, and the claim is signed and untampered. Runtime enforcement via cap no_panic, cap no_alloc, FFI sandboxing, or OS-level confinement can provide stronger guarantees. For most deployments, the combination of compile-time capability verification + signed manifests + policy gates is sufficient.

Proof caps — encoding initialization order

IO caps control which resources a module may touch. Proof caps control when dependent code may run. They’re separate concerns.

The problem they solve

Some operations must happen before others:

-- What stops someone calling this before run_migrations?
fn query(sql : String) : List(Row) do ... end

A proof cap makes “migrations have run” part of the type:

mod Db do
  proof cap Migrated
  needs IO

  fn run_migrations(cap : Cap(IO)) : Cap(Db.Migrated) do
    -- do the real migration work using the IO capability, then mint the proof.
    -- `mint_cap` is the sanctioned way to construct a proof cap; it typechecks
    -- ONLY here — inside a public `fn` of the declaring module. Runtime-erased.
    mint_cap(cap)
  end

  fn query(m : Cap(Db.Migrated), sql : String) : List(Row) do
    -- cannot be called without migration proof
    ...
  end
end

Cap(Db.Migrated) is unforgeable — every claim below is compiler-enforced:

• cap_narrow cannot produce it — enforced, not merely “not in the IO hierarchy”: cap_narrow’s result may never be a nominal proof cap in any expression position (it only attenuates IO caps).
• The runtime-provided Cap(IO) in main() cannot produce it — the only mint is mint_cap, and mint_cap is gated.
• Only public (fn) functions of mod Db can mint_cap it — private (pfn) functions may pass it through but cannot construct one.
• External code can pass it through, but cannot construct one — and no polymorphic launder through a nested unannotated helper can erase the cap type either (the deeper forge, closed by the nested-module soundness fix).

Any module that accepts Cap(Db.Migrated) must declare needs Db.Migrated. Forgery is a compile error:

mod Sys do
  mod Db do
    proof cap Migrated
  end

  mod App do
    needs IO
    needs Db.Migrated

    -- ERROR: only public functions of `Db` can construct `Cap(Db.Migrated)`.
    -- `mint_cap` outside the declaring module is rejected.
    fn bad(cap : Cap(IO)) : Cap(Db.Migrated) do mint_cap(cap) end

    -- ERROR: cap_narrow can no longer forge a proof cap in any position.
    fn steal(cap : Cap(IO)) : Cap(Db.Migrated) do cap_narrow(cap) end

    -- OK: pass-through is allowed
    fn relay(m : Cap(Db.Migrated)) : Cap(Db.Migrated) do m end
  end
end

The sanctioned way to mint a proof cap is the gated mint_cap primitive, which only typechecks inside a public fn of the declaring module and is erased at runtime; cap_narrow can never produce a proof cap, in any position, since it only attenuates ordinary IO caps.

Known gap: a cap_narrow result wrapped in a container through a polymorphic factory function can still forge a proof cap in some shapes. This is narrow and not yet closed — avoid laundering a narrowed IO cap through a generic container factory if you’re relying on proof-cap unforgeability for a security-sensitive boundary.

When to use proof caps

Proof caps suit ambient, payload-independent facts — things true about the system, not about a specific value:

The key test: is there a single, well-defined place in the codebase that produces this capability? If yes, a proof cap works cleanly. If initialization is diffuse, conditional, or happens in multiple places, a proof cap will feel awkward — use a runtime flag instead.

When not to use proof caps

Don’t use proof caps for per-value facts. If the guarantee must be tied to a specific value (“this String has been sanitized”), use an opaque refined type:

mod Sanitize do
  ptype Sanitized = Sanitized(String)   -- private constructor

  fn sanitize(raw : String) : Sanitized do
    Sanitized(escape_html(raw))
  end

  fn render(s : Sanitized) : String do
    let (Sanitized(text)) = s
    text
  end
end

A Cap(Sanitized) would prove “some string was sanitized somewhere,” but not that the string you’re about to render is the one that was sanitized. The opaque type ties proof and data together — you physically cannot pass an unsanitized string to render.

Don’t use proof caps when there’s no single mint point. Unforgeability is only meaningful when the minting surface is small and auditable. If the initialization is spread across many code paths, the cap gives a false sense of safety.

Typestate — tracking resource lifecycle

IO caps answer “is this module allowed to open a file?” Typestate answers “is this specific handle currently open or closed?”

Handle(R, S) from the standard library

stdlib/handle.march ships a canonical typestate handle:

always_linear type Handle(r, s) = Handle(Int)

The r parameter is a phantom resource tag and s is the current state. Because Handle is always_linear, dropping it without consuming it — or consuming it twice — are both compile-time errors.

tag ConnTag
tag Closed
tag Open

fn connect(cap : Cap(IO.Network)) : Handle(ConnTag, Closed) do ... end
fn open(h : Handle(ConnTag, Closed)) : Handle(ConnTag, Open) do ... end
fn query(h : Handle(ConnTag, Open), sql : String) : (List(Row), Handle(ConnTag, Open)) do ... end
fn close(h : Handle(ConnTag, Open)) : Handle(ConnTag, Closed) do ... end

The wrong call order is a type error:

let h0 = connect(net_cap)
let h1 = query(h0, "SELECT 1")  -- ERROR: expected Handle(ConnTag, Open), got Handle(ConnTag, Closed)
let h2 = open(h0)               -- OK
let (rows, h3) = query(h2, "SELECT 1")
let h4 = close(h3)

Declaring transitions

A transitions block names every valid state transition. The compiler verifies each via function exists with the right signature, and warns about functions that look like transitions but aren’t declared:

mod Db do
  transitions Handle do
    ConnTag: Closed -> Open   via open
    ConnTag: Open   -> Closed via close
  end
end

always_linear type for your own handles

always_linear type FileHandle(s) = FileHandle(Int)

tag FileClosed
tag FileOpen

fn open_file(path : String) : FileHandle(FileClosed) do ... end
fn read_file(h : FileHandle(FileOpen)) : (String, FileHandle(FileOpen)) do ... end
fn close_file(h : FileHandle(FileOpen)) : FileHandle(FileClosed) do ... end

tag — zero-arg phantom label types

tag Foo is shorthand for type Foo = Foo — a zero-argument phantom type for state labels and resource tags:

tag ConnTag
tag Closed
tag Open

When to use typestate

Use typestate when:

• A resource has a finite, well-defined lifecycle (closed → open → consumed)
• Calling operations in the wrong order is a programmer error worth preventing statically
• The resource must not be dropped without being explicitly released

Don’t use it for:

• Simple flags or booleans that change frequently at runtime — the type parameter overhead isn’t worth it
• Cases where the lifecycle state is dynamic and not known until runtime

The LSP shows typestate hover — hovering any Handle(R, S) expression displays the current state and all declared transitions from it.

Advanced patterns

Specialization tags — realtime exclusion

Tagged(X, T) annotates a capability with a policy. The key narrowing rule: a function taking Tagged(_, Realtime) is in a realtime context and cannot also hold Cap(Alloc), Cap(IO), or Cap(Panic). The compiler rejects mixed signatures:

type DSP = DSP
type Realtime = Realtime

-- ERROR: realtime functions cannot take Cap(IO)
fn bad(cap : Tagged(DSP, Realtime), io : Cap(IO)) : () do () end

-- OK: statically proven — no allocation, no IO, no panic
fn process(cap : Tagged(DSP, Realtime), buf : Buffer(Float32, 256)) : Buffer(Float32, 256) do
  ...
end

Tagged also covers type-indexed specialization (SIMD widths, buffer sizes) — monomorphization handles these for free:

fn fft(cap : Tagged(SIMD, N), buf : Buffer(Float32, N)) : Buffer(Complex32, N)
-- monomorphization produces fft_256, fft_1024, etc.

Capability environment records — reducing parameter count

When many functions need the same bundle of capabilities, threading individual Cap(X) parameters everywhere is tedious. Bundle them into a record instead:

type RuntimeEnv = {
  io    : Cap(IO),
  clock : Cap(IO.Clock),
  net   : Cap(IO.Network)
}

fn run(env : RuntimeEnv, data : Input) : Output do ... end

Narrow to a restricted set by constructing a smaller record — the type system enforces what the callee can do structurally:

type PluginEnv = { clock : Cap(IO.Clock) }

fn run_plugin(env : RuntimeEnv, plugin : Plugin) do
  plugin.run({ clock: env.clock })  -- plugin structurally cannot use IO or network
end

Each env module should provide named narrowing functions:

mod RuntimeEnv do
  fn narrow_for_plugin(env : RuntimeEnv) : PluginEnv do
    { clock: env.clock }
  end
end

Testing with capability environment records

Cap(X) values are runtime-erased, so you cannot swap them in tests. Pair the cap with a function field for swappable runtime behaviour:

type LogEnv = {
  log_cap : Cap(IO.Console),  -- compile-time gate, erased at runtime
  write   : (String) -> ()    -- runtime behaviour — swappable in tests
}

fn test_process() do
  let captured = Vault.new("test_capture")
  Vault.set(captured, "lines", Nil)
  let env : LogEnv = {
    log_cap: test_logger_cap(),
    write:   fn line ->
      match Vault.get(captured, "lines") do
      Some(xs) -> Vault.set(captured, "lines", Cons(line, xs))
      None     -> Vault.set(captured, "lines", Cons(line, Nil))
      end
  }
  let result = process(env, test_input)
  let lines = match Vault.get(captured, "lines") do
    Some(xs) -> xs
    None     -> Nil
    end
  Test.assert_true(List.any(lines, fn l -> String.contains(l, "expected message")), "should have captured the message")
end

Quick decision guide