# §3. Type system > Sema language specification — §3 Type system. > Generated from `docs/LANGUAGE.md` §3. This is the normative specification; for a guided tour see the Language and Neurosymbolic sections. ## 3.1 Base types, collections, and core expressions Scalars `int` (arbitrary precision default; `i8..i64`, `f16/f32/f64` sized forms), `bool`, `str`, `bytes`; algebraic data: `struct`, `enum` (sum types with payloads; declaration and destructuring in §3.9), tuples (`tuple[T, U]`, literal `(a, b)`, destructured by irrefutable patterns, §5.13); generics with inference; `Option[T]` and `Result[T, E]` in the prelude — there is no `null`. Option values are written `Some(x)` and `None`; `Result` values are written `Ok(x)` and `Err(e)` (§5.20). `None` is the empty *variant* of a sum type, never a null reference — it is consumed by `match`, by the combinators, or by `?`/`unwrap` (§5.20), not by identity tests. Static typing throughout with local inference; the Codon divergence list applies (no monkey-patching, no dynamic member addition). **Numerics.** The default `int`/`Int`/`ZZ` domain is a signed arbitrary-precision integer with an `i64` fast representation and automatic promotion. Exact work is governed by a 16,384-bit resource ceiling; exceeding it is `ResourceLimit`, not machine overflow or a silent wrap. Source literals admit at most 4,300 decimal digits, while the tagged wire path admits the derived 4,933 digits needed to round-trip every runtime value. Integer `+`/`-`/`*`/powers/shifts/bitwise operations remain exact. Integer `/` computes the exact rational quotient before one checked rounding to finite `f64`; `//` is floor division (toward negative infinity) and `%` uses the divisor's sign, so for every nonzero integer `b`, `a == (a // b) * b + (a % b)` as in Python. Division/modulo by zero, non-real powers, and non-finite results raise typed errors rather than returning `NaN`/`inf`. Mixed finite integer/float comparisons use exact binary-rational comparison instead of rounding the integer through `f64`; conversions and fixed-width narrowing remain explicit constructors. **Width casts round through the real format**, so a sized type is observable, not cosmetic: - Floats: `f32(x)`, `f16(x)`, `bf16(x)`, `f8(x)` round `x` through IEEE binary32 / binary16 / bfloat16 / FP8-E4M3 respectively — `f16(0.1) != 0.1`, `f8(1000.0) == 448.0` (saturates), `bf16` keeps f32's range but 7 mantissa bits. This is the quantization behavior ML code needs, native. - Integers: `i8(x)`, `i16(x)`, `i32(x)`, `i64(x)`, `u8(x)`, `u16(x)`, `u32(x)`, and `u64(x)` are explicit narrowing conversions with two's-complement wrap (like a systems `as iN`): `i8(200) == -56`, `u8(300) == 44`. `int`/`Int`/`ZZ` construct the arbitrary-precision domain; fixed-width annotations are not yet retained as distinct runtime value types. **String methods** (a `str.method()` surface): `upper`/`lower`/`strip`/`lstrip`/`rstrip`, `split`/`join`/`replace`, `startswith`/`endswith`/`contains`, `find`/`rfind` (char index or `-1`)/`count`, `slice`/`substring`, `capitalize`/`title`, `isdigit`/`isalpha`/`isalnum`/ `isspace`, `repeat`, `len`. **Static type checking.** `sema check` verifies types before the program runs — call arity (too many / too few arguments), struct construction (unknown field names), a literal argument whose base type conflicts with a declared parameter (`add(1, "two")` where `add` wants two `int`s), a `return` whose base type conflicts with the declared return, and **trait-object conformance** (§3.9): an evident concrete type placed in a trait slot it does not conform to — a `Blob` in a `list[Shape]` argument or `Shape`-typed binding, or a non-`Ord` value passed where `[T: Ord]` is required. The checker is **conservative by design**: it only flags a mismatch when it can resolve a concrete type on *both* sides, so generative outputs (`simulate`), `ported` functions, extern helpers, untyped locals, and generics are left alone (typed `any`), and `int`/`float` interoperate. It is a whole-project pass (a function typed in one module is checked at its call sites in another), grown incrementally toward full local inference — the linter a type system would give you, today, with zero false positives on the example corpus. **Runtime call boundary.** An ordinary `def` binds positional arguments, keyword arguments, defaults, `*args`, and `**kwargs` before executing its body. Supported concrete annotations are checked at entry and return (including lossless `int` to `f64` widening), while erased generic and function annotations remain governed by their documented static semantics. A missing name, unknown method or namespace member, non-callable value, arity mismatch, invalid annotation, effect-row violation, or contract failure terminates with a typed error; none is converted to a stub, `None`, or a no-op. Selecting the bytecode VM preserves the tree-walker's value, error kind/message, source span, and call-frame trace for these boundaries. **Conditional expression.** `then if cond else else_` is an expression (only the taken branch is evaluated). It sits below every binary operator and above `lambda`/`=>` in precedence, and its `else` branch is right-associative so it chains: `a if p else b if q else c`. It is the concise form default trait methods lean on (§3.9); the statement `if` is §5.13. **Collections.** `list[T]`, `dict[K, V]`, and `set[T]` are built in, homogeneous, and value-semantic (§3.8). Literals and comprehensions are Pythonic: `[x for x in xs if p(x)]`, `{k: v for ...}`, `{x for ...}`; a comprehension is the sequential base case of the `parallel [...]` form (§5.17) with identical scoping and typing rules. Slices on `list`/`str`/`bytes` use Python syntax and return copies. Dict keys and set elements require types that are hashable with total `==`. Heterogeneous collections remain excluded (Codon divergence list); dynamic JSON-shaped data enters through the prelude `JsonValue` sum and leaves it at a typed boundary (`parse[T]` against a struct schema with field contracts — §3.4, §5.22), never via stringly subscripting. For canonical flattening (§3.2), `dict` and `set` flatten in sorted key/element order so embeddings and replay are order-independent. **Iteration.** The `Iterable` trait (§3.9) is the single iteration protocol: `iter()` returns an `Iterator[T]` whose `next()` returns `Option[T]`. `for x in xs:`, comprehensions, `parallel` and stream consumption both take `Iterable` operands; `Stream[T]` (§5.25) implements it with bounded-queue backpressure, so `for incident in stream:` is the consumption form. Generator functions (`stream def` bodies with `yield`, §5.25) are the lazy-producer surface; D39 resolves the Q10 deferral by making frames affine and pulls journal-ordered. **Function types.** Functions and lambdas are first-class values. The function type is written `(T, U) -> R !{row}`; the effect row is part of the type, so a parameter of function type declares the effects its callee may perform — a higher-order function cannot smuggle effects its own row does not admit. `coerce by`, `provide` factories, and reducer arguments are ordinary function-typed values. **Statements.** Retained Python statement forms: `if/elif/else`, `while`, `for ... in`, `break`, `continue`, `return`, `pass`, `match`. There is no `assert` — the token is reserved and rejected with a machine-applicable fix-it to `ensure`/`check`, whose statement-position forms are the assertion vocabulary, semantic assertions included (§5.4) — and no `try/raise` (failures are typed values, §5.20). Blocks introduce no new scope (Python binding rules); bindings made inside `if`/`expect` arms are visible after the block. The one exception is `with as x:` (§5.21): the `as`-binding is scoped to its block — the handle is affine and released at scope exit, so it cannot be referenced afterwards. **Prelude type commitments.** The following types are language-adjacent and committed in the prelude, not user code: `Path`, `Duration` (durations in `budget`/`restart`/`heal` clauses are quoted duration literals — `"2s"`, `"50ms"` — parsed at compile time), `Instant` (returned by `clock.now()`), `JsonValue`, `Tensor[T]`, `Atomic[T]`, `Mutex[T]`, `Task[T]` (§5.12), `Stream[T]`/`Window[T]` (§5.25), `DebugSnapshot` (§5.26), and the structured logging/console surface (`log.*`, `print`, `alert` — typed prelude events with normative routing, masking, and level semantics, §5.27). Their full APIs live in the stdlib reference, not this spec. ## 3.2 Semantic values and canonical flattening Every value of a type implementing the `Semantic` protocol carries a **lazily computed, cached embedding** alongside its exact representation (BRIEF §3.1; lineage: SymbolicAI's `Symbol.embedding`, [01 §9](./research/01-symbolicai.md)). `Semantic` is a *trait* (§3.9; this document previously called it a "protocol" — that word now exclusively means session types, §5.12). `str` implements it natively; Sema `struct`s and `enum`s derive it via **canonical flattening** unless the author explicitly opts out (enums flatten as descriptor + variant name + flattened payload, so categorical values are comparable and monitorable): a deterministic, compiler-generated rendering `flatten(v) -> str` of descriptors, field names, and field values, stable across runs and recorded in the ABI so embeddings are comparable across builds. FFI/opaque values need adapters before they become `Semantic`. - Embedding computation is **tiered**: default tier is an always-resident static-embedding model (~30 MB, hot-loop viable at ~40 µs/sentence CPU); escalation to a transformer embedder is explicit or scheduler-driven ([06](./research/06-runtime-substrate.md)). The tier is part of the judge identity (§3.3). - Because `~=` sites are compiler-visible IR operations, the optimizer may hoist embeddings out of loops, batch cold misses, and pre-embed string literals into the binary ([06](./research/06-runtime-substrate.md)) — an optimization no library can perform ([01 §14.6](./research/01-symbolicai.md)). - Embeddings never change observable semantics except through the graded operators of §5.1. ```sema struct Article: sem "A news article ingested from a feed" title: str sem "Article headline as published by the source" body: str sem "Full article body text" source: str sem "Publisher or feed identity" # a.embedding is lazy, cached, content-hash interned; flatten(a) is the canonical text. ``` Inline field descriptors are first-class syntax, not comments. They become part of canonical flattening, generated schemas, contract diagnostics, constrained decoding, and self-repair context. Long descriptors may still be declared out of line with `sem Type.field = "..."`. ## 3.3 Graded similarity: the `Sim` type `a ~= b` does **not** return `bool`. It returns a **`Sim`** value: ```sema struct Sim: score: f32 # in [0, 1], metric-normalized judge: JudgeId # full judge identity, see below calibration: Option[CalibrationId] # named calibration set, if any ``` `JudgeId` is the complete identity tuple `(model hash, prompt/template hash, decode + seed policy, metric + embedding tier)` — THEORY.md Axiom J; a decision site's static type additionally carries `(calibration-set id, threshold τ, α)`. Any component change is a semver-major change to program semantics. `Sim` is the only graded-truth carrier; where a graded value travels with its subject, the pair is written `(T, Sim)` — there is no separate `Scored[T]` type, and foreign projections (INTEROP.md's `sema.Graded`) are lowerings of `Sim` plus the site's `(τ, α)`. `Sim` is the single graded-truth substrate: `~=` scores, contract `check` results, and `semantics()` scores all inhabit it, so thresholding, evidence reporting, and the guarantee map treat them uniformly (BAML's `@check`-as-metadata generalized, [04 §2.2](./research/04-ai-native-languages.md)). **Coercion to control flow** is explicit or calibrated, never silent: - `if a ~= b:` is legal **only** when the comparison's judge carries a calibration (threshold chosen by conformal risk control / Learn-then-Test with declared α — [arXiv:2208.02814](https://arxiv.org/abs/2208.02814), [arXiv:2110.01052](https://arxiv.org/abs/2110.01052)); the guarded region types as `statistical(α)`. - `if (a ~= b).score > 0.9:` is always legal but the region types as `best_effort` unless the literal threshold is itself certified against a calibration set. - Uncalibrated judges compile with a warning and type as `best_effort`; they cannot guard `proved` or `checked` regions ([05 §6.2](./research/05-pl-theory-guarantees.md)). - The `if` rule generalizes to every **boolean coercion context** — `while` conditions, boolean operands, and a `bool`-returning position such as `return semantics(...)`: a calibrated verdict coerces with the enclosing region (and, through the signature's guarantee status, the caller's view of the result) typed `statistical(α)`; an uncalibrated coercion in any of these positions is a compile error, not a silent downgrade. - Boolean **conjunction/disjunction of calibrated guards** composes by union bound: a region guarded by two calibrated coercions types `statistical(α₁ + α₂)`. Chains that would push the summed α past the site's declared budget are compile errors. **Default-judge honesty (THEORY.md honesty clause).** The prelude's default judge ships *uncalibrated*: `~=` under it types `best_effort` until a named, domain-applicable calibration set is bound (package- or module-level binding). Corpus examples that annotate `statistical(α)` on default-judge sites assume such a binding is in force. **Non-properties, stated in the spec:** `~=` is reflexive and symmetric by construction, but **not transitive** — it is similarity, not equivalence ([05 §5 guarantee map](./research/05-pl-theory-guarantees.md)). Chained rewriting that assumes transitivity is a compile-time error. *Rejected alternative:* full provenance-semiring propagation of graded truth through all control flow (Scallop, [arXiv:2304.04812](https://arxiv.org/abs/2304.04812)) — the most principled published semantics, but it globalizes cost and complexity onto every branch; Sema thresholds at the branch with typed obligations instead, and keeps semirings as the candidate formalism for a future `graded` region feature (Open question Q2). ## 3.4 Semantic descriptors and boundary contracts Every public data boundary is also a contract boundary. `sem` is the descriptor form for human meaning at every useful granularity: field, struct, function, operator, bridge export, and long out-of-line declarations. Descriptors are not comments. They feed canonical flattening, constrained emission, contract diagnostics, stack traces, policy decisions, monitor channels, and self-repair context. A field declaration may carry a semantic descriptor, a deterministic refinement, and an optional normalizer: ```sema struct IntakeProfile: age: int sem "Human age in whole years; accepts numerals or spelled-out English" where 0 <= value <= 130 coerce by parse_age ``` `sem` is the field's natural-language meaning. `where` is checked over `value` after parsing or coercion. `coerce by` names a normalizer that may turn boundary data such as `"I am seventeen"` into the declared representation before validation. Field contracts are also the R2 stage of the decode-and-repair ladder (§5.22). A failed field contract produces a typed `ContractViolation` carrying field path, descriptor, raw value, normalized value if any, blame party, and stack trace. In supervised code the runtime can retry or repair the normalizer, but the invalid value is still typed as failed and cannot flow onward. Struct-level `sem` describes the object as a whole. It participates in canonical flattening before field descriptors, and struct-level `check semantics(...)` clauses validate holistic coherence after all fields pass their deterministic contracts: ```sema struct LocaleProfile: sem "Locale-routing profile; never a protected-class decision" display_name: str sem "User supplied display name" languages: list[str] sem "Languages the user can read" region_hint: str sem "Non-authoritative region hint for content localization" check semantics("region_hint is supported by languages and other profile fields", self, alpha=0.02) ``` Function and operator `sem` descriptors describe intent at call boundaries. When a boundary fails, the diagnostic contains the failed field path, enclosing struct descriptor, callable descriptor, policy envelope, semantic predicate, evidence, and stack trace. This is the native join-point where aspect-style validation happens, but as typed language semantics rather than decorator convention. Sensitive inferences, such as protected demographic classification from names or language signals, are not ordinary validators. They require an explicit policy grant and may not feed access, pricing, employment, medical, legal, or other adverse decisions unless the policy and domain law allow it. Sema can express such checks, but the default prelude treats them as policy-sensitive `semantics(...)` sites, not harmless class-level traits. ## 3.5 Trust labels (information flow) Every value carries a trust label from the lattice `untrusted < validated < trusted` (FIDES-style product of integrity with type, [arXiv:2505.23643](https://arxiv.org/abs/2505.23643); [08](./research/08-policy-governance.md)). Sources are language constructs, so labeling is nearly annotation-free: `simulate` outputs, network/file reads, and FFI returns are born `untrusted`; string literals and pure computation over `trusted` inputs are `trusted`. Sinks (`code.exec`, `proc.spawn`, SQL identifiers/fragments, tool dispatch, `ported` splice-in) require `trusted`. The lattice is ordered by trust: `untrusted` is bottom. **Propagation takes the meet** — any value computed from mixed inputs carries the *least* trusted label among them, so taint is sticky and no combination of operations can launder a label upward. **Endorsement** is the only upward move, and it has exactly two doors: passing contracts / *sound* verifiers (→ `validated`), or the audited human-approval effect `human.approve` (→ `trusted`). A *statistical* verifier (calibrated judge, `semantics()` pass) can never endorse above `validated` — no error bound converts a statistical verdict into `trusted`. Explicit endorsement sites use the `endorse` operation, which is itself policy-gated and journaled; capability values (`Cap[R]`), narrowing, and one-shot grants are specified operationally in GOVERNANCE.md §6 and defer to this section for the lattice and doors. Some sinks accept `validated`; `code.exec` never does without an explicit policy grant. This is the type-level mechanism behind BRIEF §3.5's "a prompt-injected `simulate` can emit text but nothing it produces can ever run." ## 3.6 Effects and capabilities Sema types **effects in rows** on function signatures, Koka-style ([Leijen, POPL 2017](https://dl.acm.org/doi/10.1145/3009837.3009872); [05 §3.3](./research/05-pl-theory-guarantees.md)). This list is the **one canonical effect vocabulary** for the whole doc set (GOVERNANCE.md §3 mirrors it and defers here): ``` 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 ``` Effect *instances* are parameterized with parentheses — `net.connect("api.internal:443")`, `fs.read("data/**")` — and policies match on instances (§5.8). Colon-namespaced spellings (`net:model-egress`) and bare namespace aliases (`model` for `model.invoke`) are illegal; the legacy bare-`model` alias is a compile error. `human.approve` is the audited human-approval effect that endorsement to `trusted` requires (§3.5); `policy.change` is the distinguished policy-mutation effect (§5.8); `event.emit`/`event.subscribe` belong to the event system (§5.19; `event.subscribe` is reserved for dynamic subscription, Q12). - A function typed `def f(x: int) -> int !{}` provably performs no model calls, no I/O — the deterministic core is a type-enforced sublanguage, not a convention. - `policy` (§5.8) grants and confines capabilities; capture checking ([Capturing Types, TOPLAS 2023](https://se.cs.uni-tuebingen.de/publications/boruch2023capturing.pdf)) makes confinement transitive over closures: a closure created under a no-`code.exec` policy stays `code.exec`-free even when invoked elsewhere. - The runtime is an effect-handler stack: record/replay, mocking, batching, and policy enforcement are all handlers over these operations ([05 §3.3](./research/05-pl-theory-guarantees.md); Pyro Poutines precedent, [arXiv:1810.09538](https://arxiv.org/abs/1810.09538)). **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 (Koka-style), which is fail-closed: a function that touches nothing infers `!{}`. Authority is always conspicuous, never the silent default (object-capability discipline; `unsafe`-style opt-in). 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 verification cache key (§3.4) and the caller contract — 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 (§5.22), `ported def ... from` ports (INTEROP), and `provide` (no row slot, §5.15). - **`!{*}` 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 forbids or bounds capability (it runs only under an unrestricting policy stack). Do not confuse it with the *useful* star: an effect **row variable** `!e` for effect-polymorphic higher-order code (`map(f: (A) -> B !e) -> list[B] !e` — "map has whatever effects `f` has"), which is parametric and precise. The row-variable form is reserved for a later revision; `!{*}` is concrete `⊤`, the least informative row. **Calling an operation is checked; declaring a capability is open.** An effect *row* may name any capability (`!{fs.raed}` parses — rows are extensible). But *calling* an operation resolves like any builtin: a call to an unrecognized op (`fs.raed("x")`, `json.pares(...)`) raises `NameError` at the call site rather than silently journaling an effect and returning `None`. Each 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 above, and the fixed-op library namespaces (`json`, `csv`, `http`, `sql`, `monitors`) likewise reject unknown ops. Intentionally *dynamic* namespaces (`log` by level, `tools`/`mcp`/`skills`/`stream` by name) stay open by design. Typos are caught, not swallowed. Statement position is likewise guarded: the permissive parser accepts an unknown `word …:` as an inert directive (the tier-0 declarative-config escape), so a typo (`esnure false`) or a misplaced suite 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 without closing the open design. **Custom capabilities — the row vocabulary is open.** The catalog above is the built-in vocabulary, not a closed set: a row may declare namespaces the runtime has never heard of — `!{mysql.query}` parses, is containment-checked, and is journaled like any built-in path. A custom effect is a **marker**: there is no namespace object behind it (`mysql.query(...)` in a body is a `NameError` at the call site), so the way to mint one is the **wrapper-module pattern** — a connector module whose public defs carry the custom effect *plus* the real underlying effects they exercise. Callers then transitively need BOTH labels: `sema check` rejects an uncontained caller (`call to payments_read requires undeclared effect(s) payments.read`), the runtime denies a call whose active row lacks the label, and a policy can deny either the domain label or the underlying capability by path, with scoped instances load-verified like any other rule (§5.8). ```sema # payments.sema — the connector module is the only place the label is minted. def payments_read(account: str) -> list[dict] !{payments.read, db.read}: return db.query("SELECT amount, account FROM payments WHERE account = ?", [account]) # main.sema from payments import payments_read policy NoPaymentReads: forbid cap: payments.read justification "auditors may not touch payment rows in this scope" def audit_exposure(account: str) -> int !{payments.read, db.read}: return len(payments_read(account)) def main() -> None !{payments.read, db.read, db.write, observe.record, ui.render}: db.exec("CREATE TABLE IF NOT EXISTS payments (account TEXT, amount REAL)") db.insert("payments", {"account": "acct-1", "amount": 12.5}) log.info("payments visible", rows=audit_exposure("acct-1")) with policy(NoPaymentReads): expect n = audit_exposure("acct-1"): log.info("policy failed to bite", rows=n) except Denied as d: # "policy NoPaymentReads denies effect payments.read in # audit_exposure(): forbidden capability" log.info("denied as designed", why=d.message) ``` Two honest boundaries. First, **effect vocabulary is authority labeling, not OS-level confinement**: `payments.read` gates payment rows only because the wrapper module is the sole minting site — a function holding plain `fs.write` cannot be prevented from touching database *files* by effect kind alone. Keep the underlying capability behind scoped instances (`fs.read("data/**")`, the `db.*` surface behind the wrapper) and let governance postures and the OS sandbox (GOVERNANCE.md) carry the confinement that labels cannot. Second, **typos vs. vocabulary**: `sema check` lints near-misses of the *built-in* namespaces in a row (`!{fss.read}` → "did you mean `fs`?"), while genuinely distinct custom names are intentional and stay clean — `mysql.query` is vocabulary, `fss.read` is a typo. **These operations are real, not mocked.** `path.*` is real path algebra (`join`/`basename`/`dirname`/`extension`/`stem`/`normalize`/…); `fs.*` reads, writes, appends, lists, copies, and removes real files under the project root; `env.*` reads/writes the real process environment; `memory.*` is a real per-run key/value store; `proc.*` and `code.exec` run real subprocesses and return `{stdout, stderr, code}`; `code.patch` edits files; `net.*` performs real HTTP over the standard library (plain `http://`; `https://` needs a TLS build and errors clearly otherwise); `db.*` is a real in-process table store (`insert`/`query`/`count`); `ui.*` is real terminal I/O. Two operations are deliberate rather than stubbed: `observe.*` records to the run journal (that *is* the telemetry sink), and `clock.now` returns a fixed epoch so runs are reproducible and the VM and interpreter agree — real wall time is `clock.wall_ms`/ `clock.wall_s`/`clock.mono_ms`. Every effect is still journaled, and policy gating (`§5.8`) applies at the function's effect row plus, for `net`, per endpoint. `net.*` performs real HTTP **and HTTPS** (a bundled rustls TLS stack — no system library to install). `net.get`/`post`/`put`/`patch`/`delete` return the response body; every form takes an optional trailing **options dict** exposing all the HTTP knobs — `headers` (a dict), `bearer` (token) or `auth` (a raw `Authorization` value), `query` (a dict of params), `timeout_ms`, `retries` (with `retry_backoff_ms`, linear backoff on transport failures), and `redirects` (max redirects to follow; `0` returns the 3xx without following). `net.request({url, method, …})` and `net.fetch(url, {…})` return the **full response** `{status, headers, body}`. For example: ```sema r = net.fetch("https://api.example.com/v1/items", { headers: {"Accept": "application/json"}, bearer: secrets.token, query: {"limit": "50"}, timeout_ms: 15000, retries: 3, retry_backoff_ms: 250, redirects: 5, }) # r.status, r.headers, r.body ``` `db.*` is a real embedded **SQLite** database by default (compiled from source, no server): `db.exec(sql[, params])` runs statements, `db.query`/`db.read(sql[, params])` return rows as dicts, `db.insert(table, row)` and `db.count(table)` are conveniences, with `?` placeholders bound from a list. The database lives at `/.sema/db.sqlite` — or wherever `[db] path` in `sema.toml` points. **The SQL backend is replaceable — by config or by a provider.** A DSN in `sema.toml` selects the built-in SQLite location: `[db] url = "sqlite:///data/app.db"`, `"sqlite://:memory:"` (ephemeral), or `[db] path = "…"`. A non-SQLite DSN (`postgres://…`) is not the built-in engine and errors with a pointer unless a provider is registered. To use a different **server**, register a `@provides("db")` provider (§5.52) — a Sema function `def backend(op: str, sql: str, params: list) -> any`. Every `db.*` call is normalized to `(op, sql, params)` and routed there, so you bring your own database without touching Rust. Reads return a `list[dict]`; writes return the row count. A ready Postgres backend over the Python bridge (psycopg) — copy this in: ```sema import python @provides("db") def postgres(op: str, sql: str, params: list) -> any !{net.connect}: dsn = config.get("db.url") # e.g. postgres://user@host/app return python.call("psycopg_bridge", "run", [dsn, op, sql, params]) ``` where `psycopg_bridge.py` is a few lines: `run(dsn, op, sql, params)` opens `psycopg.connect(dsn)`, executes `sql` with `params`, and returns `cur.fetchall()` as dicts for reads (`op in {"query","read","select"}`) or `cur.rowcount` for writes. MySQL is the same shape with `mysql.connector`. Because the contract is just `(op, sql, params) -> rows|count`, any driver — native binding, HTTP database, or Python — plugs in identically. **Usage and spend are ambient, not threaded.** `with meter as u:` accumulates every model call's usage within the block into `u` — `u.total_calls`, `u.prompt_tokens`, `u.completion_tokens`, `u.total_tokens`, and `u.cost` (priced from `[pricing] per_token`). No `(result, usage)` tuples to thread. `with budget(tokens=N, calls=M) as b:` is a meter with a hard cap: a model call that pushes spend past the cap raises `BudgetExceeded` rather than silently overspending. Meters and budgets nest; each call attributes to all enclosing frames. ```sema 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 ``` **Certified totality — `ensure total` (D129).** Koka's ladder distinguishes `pure` (``: no side effects, may diverge or raise) from `total` (a mathematical function). Sema's `!{}` is the `pure` analogue: no capability operations, but divergence and typed errors remain possible. The **total tier** is claimed with a signature contract — no new keyword, the claim vocabulary is contracts (§5.4), exactly like `ensure semantics(...)`: ```sema def mean_floor(xs: list[int]) -> int !{}: require len(xs) > 0 ensure total return sum(xs) // len(xs) ``` The claim reads: **for every argument satisfying the `require` clauses, evaluation terminates and produces a value of the return type.** `require` clauses are domain refinements, not exceptions — `mean_floor` is total on `{xs : list[int] | len(xs) > 0}`. The claim is verified statically by `sema check` AND at module registration before any def can run (`sema run` rejects exactly what check rejects); an unprovable claim is a loud **error**, never a silent acceptance. A verified clause is statically discharged: it never evaluates at runtime (`total` is not a value), and a claim reaching execution from an unverified path — a REPL fragment, a live patch — fails closed with a typed error. Hot-swapping any def in a module (§5.11 live heal) drops the module's verified status: a sibling's totality proof may depend on the patched body, so its next claimed call fails closed rather than trusting a stale proof, and a patch may not itself claim `ensure total`. The verified v1 fragment is **exact arithmetic** — where the mathematical claim is actually provable: - **Signatures**: every parameter and the return are annotated with exact types — arbitrary-precision `int`, `bool`, `str`, exact collections (`list`/`tuple`/`dict`/`set` over exact types), and user structs/enums whose fields are recursively exact. **Floats are excluded**: Sema floats raise typed errors on non-finite results (§ Numerics), so even `+` is partial there. The effect row must be the explicit `!{}`. - **Termination**: `while` is rejected; `loop until` requires `max_iters`; `for`/comprehension iterables must be provably finite (literals, `range`, exact-collection parameters, locals only ever bound to finite collections, a total callee's collection result); recursion — self or mutual — is rejected (no termination measures yet; rewrite iteratively). - **Partiality discharge**: `//` and `%` need a nonzero-literal divisor or a `require` fact (`require len(xs) > 0` licenses `// len(xs)`); `**` and shifts need a non-negative right operand the same way; sequence indexing needs `require i >= 0` and `require i < len(xs)`, dict subscripts `require k in d`. Facts discharge by **normalized AST equality over names never assigned in the body**, and the whitelisted mutating methods (`append`, dict insertion) are fact-monotone — they can only grow `len` and add keys — so a discharged fact cannot be invalidated behind the guard's back. `/` is rejected even on ints: it computes the exact rational and rounds through `f64`, which can raise on non-finite results. - **Callees**: other `ensure total` defs in the module, module `equation`s whose bodies stay in the exact math fragment (finite Σ/Π, polynomial arithmetic, nonzero-literal division — CAS constructs like `lim`, `∫`, derivatives, and symbolic variables are rejected: their kernels carry typed non-convergence outcomes), and a curated builtin whitelist (`len`, `abs`, `range`, `sum`, `bool`, `str`, `repr`; n-ary `min`/`max`). Higher-order values are rejected — effect-row polymorphism is the documented gap. What `total` does **not** claim, stated exactly: `ResourceLimit` and memory exhaustion are operational faults outside the semantic claim (the same status they have in every proof assistant's extracted code); `ensure` postconditions on a total def remain runtime-checked (a failure reports a bug, it is not admitted partiality); and dynamic type errors inside bodies are the static type checker's dimension, progressively closed as it grows. `sema doc` renders a **Total** badge only after re-running the verifier — intent is never rendered as proof. Widening the fragment — termination measures for recursion, exact `QQ` division under nonzero facts, float totality via interval analysis, Lean-certified escape hatches for programs outside the decidable fragment — is target spec, tracked in the D-log. ## 3.7 The gradual guarantee lattice Every obligation (type, contract clause, semantic predicate, policy conformance) has a status in the extended gradual-verification lattice: ``` proved > checked > statistical(α) > best_effort > unchecked ``` `proved` = discharged statically (types, SMT refinements, capability reachability); `checked` = sound runtime check inserted with blame; `statistical(α)` = calibrated conformal/e-process bound under exchangeability; `best_effort` = evaluated but unbounded; `unchecked` = visible hole. The compiler inserts checks at region boundaries with blame-carrying labels naming the generative call at fault (gradual verification lineage: [Bader/Aldrich/Tanter VMCAI 2018](http://www.cs.cmu.edu/~aldrich/papers/vmcai2018-gradual-verification.pdf), [Gradual C0, POPL 2024](https://dl.acm.org/doi/10.1145/3632927)). The `statistical(α)` point is new metatheory Sema must own ([05 §6.10](./research/05-pl-theory-guarantees.md)). **Language rule:** a `statistical(α)` obligation requires an active `monitor` on its input stream; without one it decays to `best_effort` *at the type level* ([05 §6.7](./research/05-pl-theory-guarantees.md)). The certificate is honest only while the deployment distribution matches calibration, and `monitor` is what guards that assumption. The rule applies **per calibrated decision site** — every calibrated `~=` branch and `semantics()` guard, not only `simulate` outputs. Where no explicit `monitor` declaration covers a site's input stream, the compiler derives one (§5.9, Decision record D15); a site the compiler cannot cover decays to `best_effort` with a diagnostic naming the missing monitor. ## 3.8 Bindings, mutability, and value semantics Bindings are **immutable by default**; `mut x = ...` declares a rebindable binding whose aggregate contents may be mutated in place. Assignment to a plain binding is a compile error; every binding is monomorphic (one type for its lifetime — rebinding cannot change type). Structs and collections are **value-semantic**: assignment and argument passing denote the value, not a shared alias, and the compiler is free to copy-on-write. There is no observable aliasing of mutable data outside the explicit shared-state types (`Atomic[T]`, `Mutex[T]`), which is what makes the §5.17 capture rule and the no-GIL runtime sound; the same capture rule applies verbatim to `scope`/`spawn` closures (§5.12), not only to `parallel` lambdas. Mutation interacts with the rest of the semantics in three fixed ways: 1. **Contracts.** A `struct` `invariant` is re-checked at every mutation of a guarded field through a `mut` binding and at every boundary crossing — an aggregate can never be observed with a violated invariant. 2. **Trust.** Writing a field re-labels the aggregate with the meet of its old label and the written value's label (§3.5) — mutation can only lower trust, never launder it. 3. **Constants.** Module-level plain bindings of literal or pure-`!{}` initializers are compile-time constants (`Money.zero` is this pattern via trait statics, §3.9). The prelude `state` module (used by the worked example, §7) is an ordinary checkpoint store over `fs.read`/`fs.write` effects — not hidden language magic. ## 3.9 Methods, traits, and conformance `struct` and `enum` bodies admit `def` (with contracts, effect rows, descriptors) — methods are ordinary functions with an implicit typed `self`; `mut def` marks methods that mutate `self` and is legal only through `mut` bindings (§3.8). Associated constants (`Money.zero`) are `def`-less bindings in the type body. A **trait** declares *required signatures* (bodyless `def`s), optional *default methods* (`def`s with a body), and *laws as contracts*, which makes trait obligations first-class verification targets (§5.7) rather than documentation: ```sema trait Mergeable: sem "Types with an associative combine, safe for unordered parallel reduction" def combine(self, other: Self) -> Self !{} # required law associative: combine(combine(a, b), c) == combine(a, combine(b, c)) struct Money (Mergeable, Semantic): currency: Currency minor_units: i64 def combine(self, other: Money) -> Money !{}: require self.currency == other.currency return Money(currency=self.currency, minor_units=self.minor_units + other.minor_units) ``` **Default (provided) methods.** A trait method that carries a body is a default: it is written once and grafted onto every conforming type that does not override it (the type's own definition always wins). This is Sema's answer to implementation reuse — the legitimate core of what class inheritance is used for — without a class hierarchy. A single required method can seed an entire interface: ```sema trait Eq: def eq(self, other: Self) -> bool trait Ord (Eq): # Eq is a *supertrait* of Ord def compare(self, other: Self) -> int # the one required method def less(self, other: Self) -> bool: # everything below is provided return self.compare(other) < 0 def eq(self, other: Self) -> bool: # satisfies the Eq obligation return self.compare(other) == 0 def clamp(self, lo: Self, hi: Self) -> Self: return lo if self.less(lo) else (hi if hi.less(self) else self) struct Ver (Ord): major: int def compare(self, other: Ver) -> int: # supply `compare`, inherit the rest return self.major - other.major ``` **Supertraits.** `trait Ord (Eq):` declares that every `Ord` type is also an `Eq` type; the supertrait's obligations flow down (a conformer must satisfy `Eq`'s required methods too, unless a default in the chain supplies them) and its defaults are available to `Ord`'s defaults. Supertrait sets meet transitively; cycles are rejected. **Bounded generics.** A type parameter may name the traits it must satisfy: `def maximum[T: Ord](xs: list[T]) -> T` bounds `T` by `Ord` (multiple bounds join with `+`: `[T: Eq + Ord]`). Type parameters are erased at runtime (§5.29); the bound is the declared obligation — surfaced to `sema check`, reflection (§5.23), and docs — that lets the body use the bound traits' surface and documents the contract to callers. The bound is **enforced at call sites** where the argument's concrete type is evident — passing a `Blob` that does not conform to `Ord` to `maximum` is a `sema check` error (§3.1 type checker). It is not (in v0.1) discharged by monomorphization, so a bound on a value whose type the checker cannot resolve is left to runtime dispatch. **Trait objects (open-world polymorphism).** A trait name used in type position — `x: Shape`, `list[Shape]`, `-> Shape` — is a *trait object type*: any value conforming to the trait, dispatched by its runtime type. This is how you get a heterogeneous collection behind one interface (the thing class hierarchies use inheritance for), and it composes with everything else: third parties add new conformers without touching a central `enum`. ```sema trait Renderer: def render(self) -> str struct Text (Renderer): body: str def render(self) -> str: return self.body struct Rule (Renderer): width: int def render(self) -> str: return "-" * self.width def render_all(items: list[Renderer]) -> str !{}: # one list, many concrete types return "\n".join([it.render() for it in items]) # dispatched dynamically ``` Method calls on a trait-object value resolve against the concrete runtime type (the same dispatch as `x.method()` everywhere); a call to a method the concrete type does not provide is a typed error at the call site. Because dispatch is by runtime type, no vtable or boxing is observable. **Trait-object slots are conformance-checked** (§3.1 type checker): a value whose concrete type is evident and does not conform — a `Blob` in a `list[Shape]` argument, a `Shape`-typed binding, or a `-> Shape` return — is a `sema check` error before the program runs. Closed-world alternatives — when the set of cases is fixed and you want exhaustiveness — remain `enum` + `match` (§5.13); trait objects are the open-world dual. **The `is` test.** `value is Type` and `value is not Type` return `bool`: true iff the value's runtime type *is* that concrete type, or *conforms to* that trait (transitively through supertraits). It is the narrowing/dispatch escape hatch for open-world code — `n = n + (1 if it is Rule else 0)` — and works on concrete types, traits, and built-in types (`x is int`). Identity comparison is meaningless under value semantics (§3.8), so `is` is repurposed as the type/conformance test. Conformance is declared in the type header (`struct X (TraitA, TraitB):`) or out of line with `impl Trait for Type:` — the out-of-line form is how FFI/opaque values gain `Semantic` adapters (§3.2) and how prelude types conform retroactively. **Conformance is checked** (§5.7 static leg): a type that declares a user-defined trait but leaves a required method unimplemented — its own or a supertrait's, and not covered by a default — is a hard `sema check` error naming the missing methods. Trait `law` clauses feed the L1 property engine: an `unordered` parallel reduce (§5.17) demands `Mergeable` with a killed-mutant record for `associative`, which is what "proved associative" concretely means. Core prelude traits: `Semantic` (embedding + canonical flattening), `Iterable`/`Iterator` (§3.1), `Hashable`, `Eq`/`Ord`, `Mergeable`. Blanket implementations and specialization are excluded from v0.1 (coherence: at most one `impl` per (trait, type) pair, orphan rule as in Rust). **Enum declarations and payloads.** Standalone form with optional payloads: ```sema enum Escalation: none notify(channel: str) page(oncall: str, deadline: Duration) match esc: case Escalation.page(oncall, deadline): dispatch(oncall, deadline) case Escalation.notify(channel): post(channel) case Escalation.none: pass ``` Variant payloads destructure positionally or by name in `case` patterns; enum `match` is exhaustiveness-checked (§5.13). The inline form (`sentiment: enum Sentiment: pos | neg | neutral`) remains sugar for a standalone payload-free declaration. ---