Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

mutate

mutate-decl ::= attribute* 'pub'? 'mutate' Ident '(' param-list ')' ('->' TypeExpr)?
                '{' mutate-body '}'
mutate-body ::= ('require' '{' expr (',' …)* '}')?
                stmt*
                ('return' expr ';')?
stmt        ::= 'let' Ident (':' TypeExpr)? '=' expr ';'
             |  'match' expr '{' arm (',' …)* '}'
             |  insert-stmt | update-stmt | delete-stmt | upsert-stmt | amend-stmt
             |  'detach' 'delete' expr ';'                                  // ‡ refused, OE1353
             |  emit-stmt
             |  'for' Ident 'in' expr '{' stmt* '}'
             |  'if' expr '{' stmt* '}' ('else' '{' stmt* '}')?
             |  expr ';'
insert-stmt ::= 'insert' TypeExpr '{' field-init-list '}' ';'              // typed-literal insert
             |  'insert' TypeExpr '{' '..' expr (',' field-init-list)? '}' ';'  // spread: seed from a struct value
             |  'insert' Ident ':' TypeExpr '{' field-init-list '}' ';'   // ‡ named typed-literal — OE0001
             |  'insert' Ident 'into' expr ';'                             // insert binding into collection
             |  'insert' predicate-call '{' field-init-list '}' ';'        // relation insert with body
             |  'insert' predicate-call ';'                                // relation insert, no body
update-stmt ::= 'update' (Ident | pattern) 'set' '{' field-assign (',' …)* '}' ('where' expr)? ';'
field-assign ::= Ident ('=' | '+=' | '-=') expr
delete-stmt ::= 'delete' predicate-call ';'                                // delete iof(…) / delete Rel(…)
             |  'delete' (Ident | pattern) ('where' expr)? ';'             // ‡ entity / bulk delete — OE0001
upsert-stmt ::= 'upsert' pattern ('as' Ident)? upsert-clause+ ';'          // ‡ refused, OE1352
upsert-clause ::= 'on' 'insert' '{' field-assign (',' …)* '}'
               |  'on' 'update' '{' field-assign (',' …)* '}'
emit-stmt   ::= 'emit' Ident '{' expr '}' ';'
amend-stmt  ::= 'amend' predicate-call ';'                                 // belief-time withdrawal (RFD 0076)
             |  'amend' predicate-call '=>' predicate-call ';'             // atomic withdraw + correct

pub mutate sign_lease(t: Person, p: Property, rent: Money, term_days: Nat) -> Lease {
    require { rent > 0, term_days > 0 }
    let l = insert Lease(t, p) {
        monthly_rent: rent,
        start:        today(),
        end:          today() + term_days.days,
        status:       Pending,
    };
    emit AuditLog { LeaseSigned { lease: l, at: now() } };
    return l;
}

pub mutate hire_or_raise(p: Person, o: Organization, salary: Money) {
    upsert p.works_at(o) as emp
        on insert { emp.start_date = now(), emp.salary = salary }
        on update { emp.salary = salary };
}

pub mutate rebrand(old: String, new: String) {
    update c: Company set { name = new } where c.name == old;
}

An update of a bound target writes its mut fields directly. The ('where' expr)? filter (and the bulk/pattern target forms it implies, as in rebrand above) is refused at ox check / ox build (OE1318), never silently dropped.

The grammar shapes marked ‡ are loud refusals, not silent no-ops. Named typed-literal insert (insert l: Lease { … }; use let l = insert Lease { … } instead) and entity/bulk delete of a bound target or pattern with an optional where refuse with OE0001 — only delete predicate-call (delete iof(…) / delete Rel(…)) is admitted. detach delete refuses with OE1353 and upsert with OE1352.

delete Rel(…) and insert Rel(…) additionally pass the relation-end mutability gates (RFD 0076, Relations): a matched delete on a relation with any effectively-immutable end refuses at the write path with OE1402 (an unmatched delete stays an idempotent no-op), and an insert adding a new value at an immutable end whose endpoint fiber an earlier transaction already initialized refuses with OE1403 — checked before the OE1341 cardinality cap, atomically, so a refused body commits nothing. The gates read the closed extent: an insert into a subrelation is gated against every superrelation’s fiber too (still OE1403), and a premise write whose rule-derived consequences would vary an immutable-ended declared relation’s extent — retract a derived binding whose dependent context survives, or grow an initialized derived fiber — refuses the whole body with OE1397, even though no statement names that relation. The initialization set itself remains governed by the declared cardinality: on an immutable end the fiber’s value set freezes at its first asserting transaction, so a declared minimum of two or more is decidable exactly there — a body that initializes such a fiber with fewer distinct values refuses with OE1398 (the frozen set could never grow to complete it), whichever route initializes it: a direct insert, a subrelation insert, a rule-derived initialization, or a static fact set at build. A mutable end’s minimum keeps the deferred OW1342 posture.

The relation-end mutability write gates — the ones that admit or refuse a delete R(…) / insert R(…) against an immutable end, and the individual retraction that would strand an immutable-ended binding (OE1402–OE1404) — are enforced by oxc-runtime in its end_mutability module; see relations for the rule they enforce.

The rebrand example assumes name is declared mut on Company. Per struct and enum — language built-ins (data declarations), fields are immutable post-construction unless explicitly marked mut:

pub type Company {
    #[intrinsic] founded: Date,    // construction-required; not updatable
    mut name: String,              // updatable via `update`-stmt
}

update-stmt admits writes only to mut fields. A field-assign targeting a non-mut field is rejected with OE0820 UpdateImmutableField. The elaborator validates each field-assign against the entity’s field-decl mut flag; rejection surfaces at build time, not at mutation invocation.

Insert from a pre-built value — the ..v spread

Concept construction is fused to insertion: there is no bare construction expression of concept type. Constructor machinery therefore lives in fns over struct values (struct and enum — language built-ins (data declarations)) — and the spread form lets such a value feed an insert without re-spelling every field:

pub type Person { name: String, age: Int }
pub struct PersonSeed { name: String, age: Int }

pub fn seed() -> PersonSeed = PersonSeed { name: "Ada", age: 36 };

pub mutate admit() -> Person {
    let v = seed();
    return insert Person { ..v, age: 37 };   // seed's fields, age overridden
}

The base v must evaluate to a struct value; its fields seed the field-init set by exact field name against the target’s declared fields (the whole <: chain — an inherited field is a match), and the explicit field: value initializers override same-named seeds, in either textual order. The merge happens before the construction gates, so the spread is field-init sugar and nothing downstream can tell the forms apart: required- field completeness (OE0207), primitive-refinement invariants (OE0668), abstract-type refusal (OE0233), fixed classification (OE0234), the value/individual boundary (OE0248), and declared-field validation all fire over the merged set exactly as the longhand spelling, and identity is still minted only by the event log at insert. There is no first-class unpersisted individual: the struct value is pure data (no identity) until the insert constructs the concept individual from it.

Field-name matching is total and loud, never lossy:

  • A required target field that neither the base nor an explicit initializer supplies refuses with OE0207, same as omitting it longhand.
  • An optional target field (T?) the base does not carry simply stays absent — no phantom write.
  • A source field with no declared target field (on the concept or any <: ancestor) refuses with OE0261 InsertSpreadFieldUndeclared: data the source value carries never silently vanishes on insert.
  • A base that is not a struct value — a scalar, an individual, an enum constant — refuses with OE0260 InsertSpreadSourceNotStruct.
  • More than one spread in one init list refuses at ox check / ox build with OE0263 StructLitMultipleSpreads (a second spread has no defined merge order); the same refusal governs the value struct literal’s functional-update spread. Combine the sources into one struct value first, then spread that.

The base is an ordinary body value position: a deductive read there refuses with OE1371 and an unbound name with OE1383, exactly as a field initializer would. mut on a target field is orthogonal — construction may set mut and non-mut fields alike, spread-fed or explicit.

The relation-insert-with-body form (insert P(a, b) { … }) does not take a spread while that host form itself refuses (OE0001); the field-init merge extends to it when the body form lands.

Field updates lower to append-only event pairs on the underlying property axiom (Storage layer): a retract event for the prior value and an assert event for the new. The proposition’s logical identity is the (entity_id, property_id) pair; the value is what changes. Bitemporal queries reconstruct prior values per Temporal substrate.

Mutations are transactional within the body; the kernel may reject mutations that violate refinement, consistency policy, or stratification — rejection surfaces to the caller as Result<T, Diagnostic> from the host runtime.

Dynamic reclassification — insert iof / delete iof. Because iof is a first-class predicate (Reflection), mutate bodies can dynamically classify and declassify entities by inserting or deleting iof tuples through the existing insert predicate-call / delete predicate-call forms:

pub mutate enrol(p: Person) {
    insert iof(p, Student);                  // p is now a Student
}

pub mutate expel(s: Student) {
    delete iof(s, Student);                  // s is no longer a Student
}

The single-type insert iof(x, T) / delete iof(x, T) forms above classify and declassify an entity, subject to the gates below. Inserting an iof tuple over a relation concept — insert iof((p, into), EnrolledAt) for a named relation EnrolledAt — refuses: the tuple-argument form parse-refuses with OE0001 rather than silently doing nothing.

The substrate enforces two constraints on insert iof(x, T):

  1. Refinement gate (enforced). If T carries a defined refinement iff { … } (Refinement) — for example, pub type ExtinctSpecies <: BirdSpecies iff { self.numberOfLivingInstances == 0 } — the predicate is the substrate’s source of truth for membership: the modeler updates the underlying state (here, numberOfLivingInstances) and the substrate derives the iof classification automatically, so explicit insert iof(x, ExtinctSpecies) emits OE0211 IofInsertOnDefined and the mutation is rejected. If instead T carries a primitive refinement where { … }, membership is conferred by assertion, so insert iof(x, T) is permitted — but the predicate is a necessary invariant: an x that positively violates it (definite false, World assumptions (CWA / OWA)) is rejected with OE0668 RefinementInvariantViolated. The same invariant is checked when a primitive-where member is created by construction (insert T { … }) or when an update writes a field the predicate reads.
  2. Modifier gates (enforced — RFD 0027 D6). Re-classification is governed by the ontology-neutral fixed modifier on the target’s introducing metatype (metatype), never by any axis name: insert iof(x, T) / delete iof(x, T) where T is fixed-introduced is refused with OE0234 FixedReclassification — classification under such types is decided at construction (insert <T> { … } remains legal; construction is not re-classification). Admission is the absence of fixed: dynamic classification is the default, and a vocabulary opts its rigid metatypes into the restriction explicitly (pub fixed metatype kind = { … };) — an axis assignment like rigidity::anti_rigid is inert user vocabulary and grants nothing by itself. Likewise insert iof(x, T) against an abstract type — a direct instance — is refused with OE0233 AbstractTypeConstruct; non-abstract subtypes are unaffected. Both gates fire at ox check / ox build where the target is statically known and at the runtime write path otherwise, rejecting the whole mutation atomically. The membership-constancy theorem (Argon.Runtime.ModifierGates.runMutation_fixed_iof_constant) is what grounds static modal discharge over fixed-introduced types (Modal operators).
  3. Compatibility gate. x’s existing classification chain must include some supertype that T specializes (e.g. Student <: Person requires x: Person).

After insert iof(x, T), the entity x is classified under both its prior types and T. After delete iof(x, T), x is no longer classified under T but retains all other classifications. The substrate maintains a single global iof relation; insert/delete operate transactionally.

Bitemporal mutation forms. Per the temporal substrate (Temporal substrate, Effective-dating: valid time and the two as_of axes), an insert may carry an explicit valid-time at <date> qualifier — the assertion’s valid time begins on that civil day (RP-004 mutate). This form executes, on every insert arm: the write threads the date onto the event’s bitemporal extent, and an as_of <#date#> query reads it back. A typed-literal insert (insert T { … } at <date>, with or without the ..v spread) stamps the constructed individual’s membership and every field assertion with the same valid time, and an op-level qualifier wins over the call-level default valid-time an embedder supplies for the whole mutation (explicit intent over the per-call backdate).

pub type T;
pub type Evt { tag: String? }
pub mutate enact(x: T, effective: Date) {
    insert iof(x, T);                        // [VT: now → ∞]  [TT: now → ∞]  — atemporal default
    insert iof(x, T) at effective;           // [VT: effective → ∞]            — effective-dated
    insert Evt { tag: "x" } at effective;    // membership + fields, all [VT: effective → ∞]
}

The window form during [t1, t2] and a valid-time-qualified delete (bitemporal retraction — closing a valid-time interval rather than opening one) refuse loudly (OE1330) rather than silently applying at all valid times; the since <date> open-interval form executes on inserts, equivalently to at (an open interval from the anchor):

pub type T;
pub mutate retro(x: T) {
    insert iof(x, T) during #2020-09-01#;   // window VT
}

Explicit erasure — forget. For compliance scenarios (GDPR right-to-erasure, sensitive-data redaction), forget removes the underlying tuple including its bitemporal history — removed from every served read and every write gate; the durable-replay journal retains the erased bytes closed (see the gate-and-read surface below):

forget x;                                               // bound individual; capability-gated

Only the bound-individual form forget <expr> is admitted; the forget iof(x, T) and bulk forget … where … shapes refuse with OE0001.

forget is capability-gated at the source level: a mutate body containing forget refuses to build (OE0730 ForgetWithoutCapability) unless the enclosing mutate declaration grants #[allow_forget]. Cascading derived facts are revised via DRed overdelete.

Erasure is measured at the gate-and-read surface: after forget x, no assert-polarity event on any plane or polarity introduces or references x (relation arguments are walked into nested collection values), and x’s pre-existing closing retractions are erased with their asserts. Each erased live event leaves one freshly-minted extent-closing retraction event — a body clone whose closed assert no longer exists, the receipt the durable-replay journal needs so a reopened store drops the re-added assert instead of resurrecting it — and the durable journal retains the erased history closed rather than expunging bytes. Neither replay artifact is served by a read or consulted by a write gate.

The capability does not exempt forget from the relation-end mutability gates (RFD 0076): erasing an individual bound at an effectively-immutable relation end while that end’s dependent context (the individuals at every other position) survives the transaction refuses with OE1404 — erasure may not stand in for the refused cascade. The dependent may cease in the same transaction through either channel (a logical retraction or another forget), and the gate reads every standpoint plane, exactly the planes the erasure sweeps. Erasing the dependent individual itself is the legal direction and takes its incident bindings with it.

Reasserting a tuple after retraction produces distinct VT intervals on the underlying store — the substrate does not coalesce on adjacent boundaries. Historical retract/reassert is queryable via audit projections.

Individual retraction — retract. retract ends one or more individual lifetimes and cascades their incident relation bindings. Two source forms lower to the kernel RetractIndividuals effect (RFD 0076):

retract x;              // a single individual
retract {x, y};         // an atomic set — one cessation set, one coverage gate

Every retract (and forget) target in a body joins ONE transaction-wide cessation set, gated once for immutable-end coverage: for a both-immutable binary relation, retracting only one endpoint refuses OE1404 (the surviving endpoint is its dependent context), while retract {x, y}; — or two separate retract statements naming x and y — covers both. A retract inside an if branch, a for body, or a match arm joins that same union. Re-introducing a retracted individual later in the same body — a re-classification, a relation endpoint, or a property write — refuses OE1400; an assert-then-retract nets clean and is admitted. Duplicate targets are idempotent.

Belief-time correction — amend. delete ends a binding’s valid time (it stopped being true); amend corrects the record (it was never true — a mis-recorded assertion, false ab initio). The two are deliberately distinct verbs so a correction can never be mistaken for a valid-time deletion. amend withdraws the assertion as false ab initio, releasing its contribution to any relation-end freeze (RFD 0076), while the bitemporal history retains what-was-believed-when — an auditable correction, not an erasure:

pub type Person;
pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

#[allow_amend]
pub mutate rescind(child: Person, wrong: Person) {
    amend bornTo(child, wrong);                          // withdrawal — truth unknown
}

#[allow_amend]
pub mutate correct(child: Person, wrong: Person, right: Person) {
    amend bornTo(child, wrong) => bornTo(child, right);  // atomic withdraw + correct
}

The primitive amend R(args); withdraws positive evidence (the proposition returns to unknown, not refuted). The composite amend R(args) => R(args'); withdraws and asserts the corrected proposition against one transaction-time view, all-or-nothing (a refused corrected assertion commits nothing). Like forget, amend is capability-gated at the source level: a mutate body using it refuses to build (OE1405 AmendWithoutCapability) unless the enclosing mutate declaration grants #[allow_amend]; correction authority is further authorized per invoking principal, target-scoped, at the serving layer. Amendment is validated against one net corrected view of the transaction (withdrawals subtracted, corrected assertions and lifecycle effects overlaid), so it grants no coverage exemption to a companion cascade. Amending an established immutable fiber below its declared minimum refuses with OE1407; amending a purely rule-derived tuple (no asserted event to correct) refuses with OE1406. The composite corrects a fact of one relation: its withdrawal and correction must name the same relation, so a cross-relation amend R(old) => S(new) refuses at build with OE1409 (to change facts across two relations, delete one and insert the other). Correcting a refutation (not_fact) is deferred to the negative-facts mutation surface; amend here corrects positive relation assertions. An amendment releases exactly the one assertion it named — an assertion is an event, not a value-for-all-time — so a later re-assertion of the same tuple is a fresh initialization that re-freezes its immutable fiber: after amend R(a); insert R(a); a subsequent insert R(a') refuses (OE1403) exactly as it would with no amendment, whereas amend R(a); insert R(a'); directly (no intervening re-assertion) admits.

Body semantics

A mutate body lowers to the Operation IR and runs with all-or-nothing atomic commit: a failed require guard, or any error, emits nothing (RFD 0015). require preconditions, let bindings, typed-literal entity construction with system-minted identity, projection navigation (a.b.c) over committed state, collection inserts (insert … into …) with for iteration, sum / count aggregate guards over comprehensions, index projection (coll[i]), and effectful if/else (control flow is expression-valued; branches are blocks) all execute, returning the body’s tail value.

Name resolution in value positions. A bare identifier in a body value position — a relation-tuple argument, a constructor or update … set field value, a let right-hand side, a require guard operand, or the tail — resolves in order: a parameter or let / loop / match binder in scope first; then a declared type name (concept / trait / metatype / metarel / relation), which lowers to a TypeRef value exactly as it does in a rule body (Type-as-value) — the write side produces the same reference the read side dispatches on and the wire accepts as { "$typeRef": … }; then a module-declared individual (one introduced by a pub fact, resolved to its content-addressed identity). A binder therefore shadows both a declared type and a declared individual of the same name. A name that resolves to none of these is refused at ox check / ox build with OE1383 (no identity is ever synthesized for an unbound name), rather than building green and failing at the first run. A type-as-value LANDS only in a write position declared to hold one — a TypeRef / Metatype / TraitRef-typed relation endpoint or field; landing it in an entity/value position is refused with OE1384 at build where the declared signature is visible, and by the identically-worded runtime write gate otherwise. The same rules govern test bodies.

match in bodies. A value-position match (a let RHS, an update … set value, a tail / return value, or a require guard) matches over constant patterns (payloadless enum constants, literals, or-patterns, _; Pattern matching) and desugars to the same IfExpr chain a value if uses, with exhaustiveness enforced at ox check (OE0203). A statement-position match (arms running effects — the BPMN-gateway dispatch match d { Disposition::Clean => { update … }, Disposition::BreaksFound => { insert … }, _ => {} }) lowers to a right-nested Operation::If chain over the arm blocks’ operations (RFD 0015 Amendment 2): the same ordered first-match semantics, constant-pattern subset, and OE0203 exhaustiveness as the value desugar; arm blocks and if branches admit the full mutate statement set at any nesting depth. upsert, emit, and detach delete in a body refuse by name rather than dying generic or doing nothing silently: emit with OE1318, upsert with OE1352, and detach delete with OE1353.

Mutate-body arithmetic is exact (RFD 0016 / RFD 0029): require guards and let / field expressions route through one canonical evaluation core — pure-Int operands stay checked integers (overflow is a loud error, never a wrap), and any Real / Decimal / Money operand promotes to an exact rational (/ is the field operation, no truncation), so 0.1 + 0.2 == 0.3 holds exactly in a mutate body where it would fail in f64.

Reads see committed state. A body’s projections (a.b.c) read the store as committed before the mutation; a body does not observe its own not-yet-committed constructions. One consequence: constructing a collection-valued field and then insert … into that same field in a single body does not compose (the append seeds from committed state).

Deductive reads are iterands, not value terms. A pub query / derived-predicate deductive-plane read is set-valued. Its sole admissible use in a mutate body is as the iterand of a for x in <query> { … } loop, which binds each projected row in turn (lowered to a reasoner snapshot read over committed state, the same no-read-your-writes plane as above). A nullary read (for r in applicable()) iterates the whole extent; a parameterized read (for r in applicable_for(arg)) passes its bound arguments as the query’s sideways read-goal bindings, iterating only the rows the parameters select.

pub mutate mark_all() {
    for r in applicable() {
        insert iof(r, Done);
    }
}

A deductive read in a non-iterand term/value position — a let right-hand side, a require guard, an update … set value, a field value, or the tail — has no scalar value and is refused at ox check / ox build with OE1371 MutateQueryTermNotExecutable rather than passing the static gates and dying at the first runtime call:

pub mutate mark_term() {
    let x = applicable();
}