Effects & Capabilities

An effect row is the part of a function’s type that says what authority the function may exercise — which model calls, file reads, sockets, subprocesses, and audited actions it can reach. In Sema this is not a lint or a convention layered on top of the language: it is in the signature, the type checker enforces it, and the runtime is built as a stack of handlers over exactly these operations.

This page is the conceptual home of the effect/capability system. For the full, alphabetized list of every effect and what it means at runtime, see the Effects Catalog. For how effects appear in ordinary function signatures alongside contracts and descriptors, see Functions & Effects.

Why effects are in the type

To ordinary languages a model call is just a function that returns a string, and a call to os.system(...) is just another function call. There is no type that says “this code can read files but not open sockets,” and no type that says “nothing reachable from here may run a subprocess.” Authority is ambient: any function can do anything the process can do, and the only defenses are review comments, a linter, or a runtime sandbox — all outside the language, all bypassable.

Sema takes the opposite stance, which is the object-capability discipline made syntactic: authority is conspicuous, never the silent default. A function declares the capabilities it uses in a row, the compiler checks that the body stays within it, and policies confine that row further. A later change that reaches code.exec shows up as a signature diff, not as a silent new behavior buried in a function body.

Syntax: the row on a signature

The row is the !{...} clause after the return type:

def import_statement(path: Path) -> Statement !{fs.read}:
    raw = fs.read_text(path)
    return parse_statement(raw)

def draft_summary(facts: list[Fact]) -> str !{model.invoke, observe.record}:
    return generate(render_facts(facts), 256)

The first function may read files and nothing else. The second may invoke a model and record to the observability journal — but it provably cannot touch the network, spawn a process, or write a file, because those effects are not in its row and the checker would reject a body that reached them.

Note

Effect instances are parameterized with parentheses: net.connect("api.internal:443"), fs.read("data/**"). Rows can name bare effects or specific instances, and policies match on instances — so a policy can allow net.connect("api.internal:443") while forbidding every other endpoint. Colon-namespaced spellings (net:model-egress) and bare-namespace aliases (the legacy model for model.invoke) are compile errors.

The deterministic core is !{}

The most important row is the empty one. A function typed !{} provably performs no effects at all — no model call, no I/O, no clock, no randomness:

def total_amount(lines: list[BankLine]) -> Money !{}:
    mut acc = Money.zero
    for line in lines:
        acc = acc + line.amount
    return acc

This is not a comment expressing intent. The deterministic core is a type-enforced sublanguage: the checker rejects any !{} function whose body reaches an effect. That is what makes the core reproducible, freely reorderable and parallelizable, and safe to call from anywhere. In the standard library, path algebra, arithmetic, the constraint solve engine, and pure data transforms all live in !{}. A pure function that happens to touch nothing infers !{} automatically (see below), so the deterministic core is the default floor, not an opt-in ceremony.

An omitted row is inferred, never a wildcard

This is the rule that trips up newcomers from other languages, and it is the crux of the whole design. Omitting !{...} does not grant ambient authority. It asks the compiler to infer the minimal row from the body, Koka-style. Inference is fail-closed: a function that touches nothing infers !{}; a function that reads a file infers !{fs.read}; nothing is granted that the body does not actually use.

Two rules keep that guarantee honest rather than aspirational:

• assure silver and above require an explicit row on every declared function. sema check errors otherwise. Inference stays an assure bronze ergonomic — fine while prototyping — but the published surface (the verification cache key, the caller contract) must state the row, so a later code.exec appears as a signature diff rather than a silent change. Rows derived elsewhere are exempt: simulate / by model-backed defs, ported def ports, and capability providers have no author-written row slot.
• !{*} is the explicit all-effects top (⊤) — a loud, greppable escape hatch for spikes and REPL work, and emphatically not the meaning of silence. sema check warns on !{*} at bronze and errors at silver+, and the runtime refuses to admit a !{*} row under any policy that forbids or bounds a capability.

!{*} is not the useful star

Do not confuse the all-effects top !{*} with an effect row variable !e, the parametric form for effect-polymorphic higher-order code — map(f: (A) -> B !e) -> list[B] !e reads as “map has whatever effects f has.” The row variable is precise and parametric; !{*} is concrete ⊤, the least informative row. The row-variable form is reserved for a later revision.

Calling an operation is checked; declaring a capability is open

Rows are extensible: an effect row may name any capability, so !{fs.raed} parses — the row grammar does not enforce a fixed vocabulary. But calling an operation resolves like any builtin. A call to an unrecognized op raises NameError at the call site rather than silently journaling an effect and returning None:

def broken() -> str !{fs.raed}:      # the ROW typo parses (rows are extensible)
    return fs.raed("data/x.txt")     # the CALL errors: NameError, fs has no `raed`

Every effect namespace — fs, net, code, proc, observe, memory, event, env, config, package, ui — has a recognized callable surface that is a superset of its canonical vocabulary, and the fixed-op library namespaces (json, csv, http, sql, monitors) likewise reject unknown ops. Only intentionally dynamic namespaces stay open by design: log (by level) and tools/mcp/skills/stream (by name). The result is that typos are caught, not swallowed — a core piece of Sema’s no-silent-no-ops ethos.

Statement position is guarded the same way. The permissive parser accepts an unknown word …: as an inert directive (the declarative-config escape), so a typo like esnure false or a misplaced allow: clause inside a def would parse and do nothing. sema check warns on any directive in a def/simulate body that no runtime handler recognizes, so these silent no-ops surface at check time.

How effects compose across calls

An effect row is a lower bound on the callee’s authority that flows into the caller’s row. When f calls g, everything in g’s row is part of what f may reach, so f‘s inferred row is the union of its own operations and its callees’:

def read_config(p: Path) -> Config !{fs.read}: ...

def load_and_call(p: Path) -> Result !{fs.read, model.invoke}:
    cfg = read_config(p)                 # contributes fs.read
    return classify(cfg)                 # classify is !{model.invoke}

The effect namespaces this section owns are grouped by concern:

Namespace	Operations (representative)
model	model.invoke, model.embed, model.load
fs / net	fs.read, fs.write — net.connect, net.listen
proc / code	proc.spawn — code.gen, code.exec, code.patch
db	db.read, db.write, db.schema
env / config	env.read, env.write — config.reload, config.watch
observe	observe.record, observe.export
event	event.emit, event.subscribe
ui / audited	ui.render — human.approve, policy.change, package.install

human.approve is the audited human-approval effect that endorsement to trusted requires (trust labels); policy.change is the distinguished policy-mutation effect (policies); event.emit/event.subscribe belong to the event system. The one canonical list lives in the Effects Catalog.

Confinement is transitive over closures

Because policies confine an effect row and capture checking makes that confinement follow closures, a closure created under a policy that forbids code.exec stays code.exec-free even when invoked elsewhere. Authority does not leak out of the scope that granted it by being packaged into a lambda and passed away — the policy travels with the closure.

The runtime is an effect-handler stack

Effects are not only a static check. The runtime is an effect-handler stack over these operations, which is why the same vocabulary powers record/replay, mocking, batching, and policy enforcement — each is a handler intercepting the operation. It is also why the guarantees are testable: a build that never issues net.connect can be replayed offline; a model call can be mocked by installing a handler; a batch of calls is coalesced by the scheduler handler.

Every effect is journaled, and policy gating applies at the function’s effect row plus, for net, per endpoint. These operations are real, not stubbed: fs.* reads and writes real files under the project root, net.* performs real HTTP and HTTPS, db.* is a real embedded SQLite store, proc.*/code.exec run real subprocesses. Two are deliberate rather than mocked: observe.* records to the run journal (that is the telemetry sink), and clock.now returns a fixed epoch so runs are reproducible — real wall time is clock.wall_ms/clock.wall_s/clock.mono_ms.

The gradual guarantee lattice

Effects are one dimension of a broader honesty story. Every obligation — a type, a contract clause, a semantic predicate, a policy conformance — carries a status in the extended gradual-verification lattice, from strongest to weakest:

proved  >  checked  >  statistical(α)  >  best_effort  >  unchecked

• proved — discharged statically (types, SMT refinements, capability reachability). Effect-row conformance and the !{} core live here.
• checked — a sound runtime check inserted with blame: when it fails, the label names the generative call at fault.
• statistical(α) — a calibrated conformal / e-process bound under exchangeability (a passing ~= or semantics() guard).
• best_effort — evaluated but unbounded.
• unchecked — a visible hole.

The compiler inserts checks at region boundaries with blame-carrying labels, so a guarantee is never silently weaker than it looks — its status is part of the type.

Monitor-or-decay

A statistical(α) obligation is honest only while the deployment distribution matches calibration. The language rule: such an obligation requires an active monitor on its input stream, per calibrated decision site; without one it decays to best_effort at the type level. Where no explicit monitor covers a site, the compiler derives one; a site it cannot cover decays to best_effort with a diagnostic naming the missing monitor. This is why effects, contracts, and monitors are one system, not three.

Failure modes

• Reaching an effect not in the row → compile error, naming the operation and the row it violates.
• A typo in a call (fs.raed) → NameError at the call site; the row may parse, but the call cannot resolve.
• A misplaced directive in a body → sema check warning (silent-no-op guard), even though it parses.
• !{*} under a bounding policy → the runtime refuses to admit the row; it runs only under an unrestricting policy stack.
• A statistical(α) site with no monitor coverage → decays to best_effort with a diagnostic; the certificate is not silently trusted.

How it’s checked

• sema check <project> enforces effect-row discipline and the unrecognized-op / unrecognized-directive guards.
• sema assure <project> --grade silver (and gold) require an explicit row on every declared function and reject !{*}.
• Every effect is journaled at runtime, so record/replay reproduces exactly which operations ran.

See also

• Functions & Effects — effects in the context of ordinary function signatures, contracts, and descriptors.
• Effects Catalog — the complete operation reference.
• Policies — how a policy confines and grants a row.
• Provenance & Trust — trust labels and information flow.
• Verification — assure tiers and the lattice.