Functions & Effects

Markdown Open in ChatGPT Open in Claude

A Sema function signature is def name(x: T) -> R !{effects}:. The !{…} at the end is the effect row — the set of capabilities the function is allowed to use. This is the feature that lets Sema prove the deterministic core is deterministic, and that makes authority conspicuous rather than ambient.

The shape of a function

def candidate_score(bank: BankLine, entry: LedgerEntry) -> f32 !{model.embed}:
    return (bank.memo ~= entry.memo).score

def total(prices: list[Money]) -> Money !{}:      # `!{}` = provably no I/O, no model
    mut sum = prices[0]
    for p in prices[1:]:
        sum = sum.combine(p)
    return sum

Parameters are typed; the return type follows ->; the effect row follows the return type. Keyword arguments, defaults, *args, and **kwargs all work as in Python:

def total(*nums) -> int !{}:              # *args -> tuple of surplus positionals
    mut acc = 0
    for n in nums: acc = acc + n
    return acc

def configured(**opts) -> Config !{}:     # **kwargs -> dict of surplus keywords
    return Config.from_options(opts)

Effects are rows on the type

Sema types effects in rows, Koka-style. Each capability names a namespaced operation. The full, canonical vocabulary (shared across the whole language) is:

model.invoke  model.embed   model.load
fs.read       fs.write      net.connect     net.listen
proc.spawn    code.gen      code.exec       code.patch
db.read       db.write      db.schema
clock         random        ffi.call        memory.query   memory.retain
env.read      config.reload config.watch    observe.record observe.export
event.emit    event.subscribe
policy.change package.install  ui.render    human.approve

A function typed def f(x: int) -> int !{} provably performs no model calls and no I/O — the deterministic core is a type-enforced sublanguage, not a convention. This is the single most load-bearing property of Sema: everything in the !{} sublanguage is safe to fuse, replay, cache, and reason about.

Effect instances are parameterized — net.connect("api.internal:443"), fs.read("data/**") — and policies match on instances. See /governance/policy/.

An omitted row is inferred — never a wildcard

Writing no !{…} does not grant ambient authority. It asks the compiler to infer the minimal row from the body (fail-closed): a function that touches nothing infers !{}. Authority is always conspicuous, never the silent default.

Two rules make this enforceable rather than aspirational:

assure silver+ requires an explicit row on every declared function (sema check errors otherwise). Inference stays an assure bronze ergonomic; the published surface — the caller contract, the verification cache key — must state the row so a later code.exec shows up as a signature diff, not a silent change. (Exempt because their row is derived elsewhere: simulate/by model-backed defs, ported ports, and provide factories.)
!{*} is the explicit all-effects top (⊤) — a loud, greppable escape hatch for spikes and REPL work, not the meaning of silence. sema check warns on it at bronze and errors at silver+, and the runtime refuses to admit a !{*} row under any policy that bounds capability.

def summarize(text: str) -> str:          # no row written → inferred from the body
    return text.strip().slice(0, 200)     # touches nothing → inferred !{}

def summarize(text: str) -> str !{}:      # better: state it, so drift is a signature diff
    return text.strip().slice(0, 200)

Calling an op is checked; declaring a capability is open

There are two distinct rules, and the distinction is deliberate:

An effect row may name any capability. Rows are extensible: !{fs.raed} parses fine — you can declare a capability the runtime has never heard of.
But calling an operation is resolved like any builtin. A call to an unrecognized op on a known namespace — fs.raed("x"), json.pares(...) — raises NameError at the call site, rather than silently journaling an effect and returning None. Typos are caught, not swallowed.

Each effect namespace (fs, net, code, proc, observe, memory, event, env, config, package, ui) and each fixed-op library namespace (json, csv, http, sql, monitors) has a recognized callable surface and rejects unknown ops. Intentionally dynamic namespaces stay open by design: log (by level), and tools/mcp/skills/stream (by name).

Statement position is guarded too. The permissive parser accepts an unknown word …: as an inert directive (the declarative-config escape), so a typo (esnure false) or a misplaced clause (allow: 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. This is Sema’s no-silent-no-ops guarantee in action.

Effect rows compose through higher-order code

Because the effect row is part of the function type, a higher-order function cannot smuggle effects its own row does not admit. A parameter of function type carries its callee’s row:

# This function's own row must admit whatever `render` can do — you can't hide it.
def render_all(items: list[Renderer], render: (Renderer) -> str !{}) -> str !{}:
    return "\n".join([render(it) for it in items])

Lambdas

Lambdas are first-class typed closures — same effect-row-in-type discipline as named functions. Two spellings, identical meaning:

inc    = lambda x: x + 1
scaled = lambda x, k: x * k
double = x => x * 2                 # `=>` form

Lambdas are expression-position only. The effect row of a closure is inferred and travels in its type, so passing a closure that performs code.exec into a slot that admits only !{} is a type error.

Usage and spend are ambient, not threaded

Model calls cost tokens and money. Rather than thread a (result, usage) tuple through every call, Sema accumulates usage ambiently in a scope:

with meter as u:
    answer = write_report(facts)          # returns the value only
log.info("run", tokens=u.total_tokens, cost=u.cost, calls=u.total_calls)

with budget(calls=200, tokens=1_000_000) as b:
    research = deep_search(query)          # BudgetExceeded if it overspends

with meter as u: accumulates u.total_calls, u.prompt_tokens, u.completion_tokens, u.total_tokens, and u.cost (priced from [pricing] per_token). with budget(tokens=N, calls=M) as b: is a meter with a hard cap: a call that pushes spend past the cap raises BudgetExceeded rather than silently overspending. Meters and budgets nest; each call attributes to all enclosing frames. See /governance/budget/.

The guarantee lattice

Effects tie into Sema’s gradual-guarantee lattice — the status every obligation (type, contract, semantic predicate, policy) carries:

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

proved = discharged statically; checked = a sound runtime check with blame; statistical(α) = a calibrated conformal bound; best_effort = evaluated but unbounded; unchecked = a visible hole. The compiler inserts checks at region boundaries with blame labels naming the generative call at fault. A statistical(α) obligation requires an active monitor on its input stream — without one it decays to best_effort at the type level. See /neurosymbolic/verification/ and /governance/monitor/.

Failure modes and how they surface

Unknown op on a known namespace (fs.raed(...)) → NameError at the call site (not a silent no-op).
Misplaced/typo’d directive in a body → sema check warning.
!{*} under silver+ → sema check error; refused at runtime under any bounding policy.
Missing explicit row under silver+ → sema check error.
A closure escaping its declared effect row through a higher-order call → type error.