Mutation

Everything above reasons over a fixed set of facts. mutate changes them, transactionally — it is the only mode that writes. The reliable, widely-used form is a Datalog-style body of operations:

pub mutate openAccount(a: Account, name: String) {
    insert iof(a, Account);
    update a: Account set { name = name };
}

insert iof(a, Account) records that a instantiates Account; update a: Account set { … } writes its fields. The body’s operations are insert iof, inserting a relation tuple, update, delete, and forget. insert iof(a, Account) is permitted because Account’s introducing metatype is not declared fixed: dynamic classification is the default, and the engine enforces the declared fixed and abstract modifier bits rather than reading any axis name.

Argon also has a richer imperative body — require guards that abort the whole mutation on failure, let bindings, an effectful if, typed-literal construction with a system-minted identity, field navigation, exact arithmetic, collection inserts paired with for, and match over constant patterns in both value and statement position. Its core executes today; the build refuses loudly on the forms that do not yet run, so a program never relies on a mutation that would die at runtime. The reference fixes the full imperative surface and its current status under mutate.

A mutation is atomic. A failed require guard, or any error during the body, commits nothing.

Individual retraction uses retract x;; several individuals form one atomic set with retract {x, y};. Retraction ends those individual lifetimes and cascades incident relation bindings when every immutable end’s dependent context is covered by the same set. A retraction is logical cessation, not erasure: the pre-retraction extent stays queryable bitemporally — the store retains what was.

Retraction — when a thing ceases

The right occasion for retract is narrow: an individual has genuinely ceased to exist in the domain. Its constitutive bindings — the immutable-ended relations that were about it — end with it, by cascade. That is the only lawful way an immutable binding leaves the store, and retraction is what fires it.

The canonical case — the passport is destroyed

A passport is issued to exactly one holder for the passport’s whole life: issuedTo fixes the holder end (no mut). The holder never changes; the only honest end of the binding is the passport ceasing to exist. Destroy the passport and its frozen issuedTo binding cascades away with it — the person it was issued to is untouched.

pub type Person;
pub type Passport;

// The passport's holder is constitutive: fixed for the passport's life.
pub rel issuedTo(mut passport: Passport, holder: Person) [0..*] [1];

pub mutate issue(p: Passport, h: Person) {
    insert iof(p, Passport);
    insert iof(h, Person);
    insert issuedTo(p, h);
}

// The passport is destroyed — it leaves the domain.
pub mutate destroy(p: Passport) {
    retract p;
}

Issue passport p1 to alice, then destroy p1. The Passport extent empties; alice survives in the Person extent; the issuedTo(p1, alice) binding cascaded away with the passport it was about:

── before: issue(p1, alice) ────────────────
query passports: 1 row(s)   (p1)
query people:    1 row(s)   (alice)

── after: retract p1 ───────────────────────
query passports: 0 row(s)
query people:    1 row(s)   (alice)

The binding did not have to be deleted — it could not be (delete issuedTo(p1, alice) refuses OE1402, an immutable end). Retracting the passport is the lawful exit, and the history of the issuance remains readable at any prior transaction time.

Notice which individual was retracted. The natural targets of retract are artifacts and dependents — a destroyed passport, decommissioned equipment, a terminated contract, a dissolved marriage — things whose constitutive bindings should die with them and onto which nothing else’s frozen bindings point. Retracting a person is usually the wrong instinct: people are what everything else’s constitutive bindings are frozen onto (a child’s bornTo, a passport’s issuedTo), so a person’s cessation drags every dependent into the retraction set — which is exactly the OE1404 friction below, and it is friction by design. A person who dies, emigrates, or closes an account has changed state, not stopped being an entity the model tracks; those are facts to assert, not retractions.

Nor is retract how you record damage or loss while you still care about the object. If the domain keeps answering questions about the thing in the present — is this passport valid? damaged? when was it reported lost? can it be reinstated? — then the thing is still an entity and its condition is ordinary state: insert iof(p, Damaged) (or a status property), leaving the passport addressable for repair, claims, and audit workflows. retract p is for when the model should stop tracking the identity in the present tense — present-view queries no longer return it, its cardinality slots free up (the holder could be issued a replacement passport where [0..1] would have blocked a second live one), and no future fact can be asserted about it. The pre-retraction history still answers as_of questions either way; the discriminator is whether you need to say new things about the individual going forward. Damaged means yes; destroyed means no.

When the set is incomplete — OE1404 and its remedy

Retract too little and the build refuses. A child’s birth-mother is constitutive (bornTo fixes the mother end); a mother’s set of children grows over her life (mut child). Retract the mother alone while a child survives, and her child’s frozen bornTo binding would strand — the individual it depends on, the child, is still here:

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

pub mutate retractMother(m: Person) {
    retract m;              // OE1404 while a live bornTo(child, m) child survives
}

The refusal names the stranded end and the surviving dependent context, and hands you the completed retraction verbatim as a remedy: line:

OE1404: retracting `alice` would strand the immutable `mother` end of
`bornTo` — its dependent context (child=`childB`) still survives — an
immutable end stays fixed for the life of its dependent individuals, so
ending it needs at least one dependent-context individual to cease in the
same operation. Retract the dependent individual(s) so the binding retracts
by cascade; or, if this end is genuinely rebindable, declare it `mut`.
remedy: retract {alice, childB};

The remedy: line is the completed set — the individual you named plus every dependent-context individual its retraction would strand, iterated to the fixed point (if pulling in childB stranded her dependents, they would be in the line too). Paste it back to say exactly what the coverage rule needs:

pub mutate retractBoth(m: Person, c: Person) {
    retract {m, c};        // one atomic set covers the mother AND her child's context
}

The set is atomic: coverage is checked once over the whole set, so mother and child cease together and no binding strands. This is what makes the OE1404 message legible — it is asking you to complete the set, and retract {…} is how you say it.

These are invocation-dependent examples (OE1404 needs a pre-existing live tuple, so they are marked ignore), but the coverage rule they show is live: forget m; will not sidestep it either — erasure runs the same coverage gate and refuses while the dependent context survives.

A retraction set may span several statements

Two retract statements in one mutate body union into one cessation set, checked by one coverage gate — the remedy above must be expressible compositionally (a retract inside an if branch, a for body, or a match arm joins the same union):

pub rel bindsSpouse(mut marriage: Marriage, spouse: Person) [0..1] [2];

// A marriage's two spouse bindings are constitutive; the marriage is their
// shared dependent context. Retracting the marriage and both spouses in
// separate statements is ONE set — coverage holds over the union.
pub mutate dissolve(m: Marriage, s1: Person, s2: Person) {
    retract {m, s1};
    retract s2;
}

Retract is one of four lifecycle verbs

retract is not the tool for most changes. Reach for it only when an individual has ceased. The sibling verbs cover the other three shapes. The four occupy exactly one cell each of a 2×2 — grain (what the verb removes) against the nature of the removal: delete and amend work at the fact grain (a tuple that was true-then vs. one that was never-true), while retract and forget work at the entity grain (logical removal from the model vs. physical removal from the store).

amend targets a directly-asserted relation tuple — never a derived conclusion (you amend the premises, not the conclusion: a derived target refuses OE1406), and, as implemented, never a classification or property value. It corrects an asserted fact, not a relation: it never touches the relation’s declaration, its other tuples, or the participating individuals. All four verbs — delete, amend, retract (with its OE1400 guard), and forget — are enforced on this toolchain; amend is specified in RFD 0076 and realized by this change. The four differ in which view changes: delete moves valid time, amend corrects the belief record — both at the fact grain, both retaining queryable history — retract ends a lifetime and its cascade, and forget alone removes bytes from the served store.

The entity-grain cell has two verbs, not one, and the split is deliberate — retract exists in addition to forget on three axes. History: retract is logical, so the pre-cessation extent stays bitemporally queryable — audits and as_of reconstructions read the retained trail, and in regulated domains retaining superseded records is a legal requirement; were forget the only removal, ordinary cessation would destroy the very trail audits exist to read. forget physically erases the served record (leaving a tombstone in the durable journal). Privilege: forget is capability-gated as the right-to-erasure / compliance channel; retract is an ordinary statement, because ending an entity’s lifecycle is ordinary domain logic — were forget the only removal, every workflow that ends an entity would need the erasure capability, a privilege-escalation antipattern. Meaning: a retract is an event in the record (“ceased, and here is when”), so derived views and the amendment plane’s corrected view compose with it; forget removes the record-keeping itself (“no longer allowed to know”), and those same views are definitionally blind to a forgotten individual afterward. The two are not rivals: forget runs the same OE1404 coverage gate as retract, so it is strictly retract + physical destruction + a permission check — never a bypass of retraction’s semantics.

Everything in the system is bitemporal except what forget has touched, on two layers. At the query surface, forget destroys its target’s bitemporality by design: the axiom events and their bitemporal history are gone from the served store, so an as_of reconstruction — “what did we believe about x last March?” — returns nothing. That is the erasure contract, not a limitation: right-to-erasure requires that historical reconstructions stop answering, which a bitemporal retraction cannot deliver — after retract x, the same as_of query still answers in full, because a retraction is an ordinary event in the bitemporal record. At the storage substrate, the durable replay journal retains the erased events’ bytes closed alongside a tombstone — an append-only-durability necessity, not queryable history: no query path reaches those bytes, and replay reads the tombstone to re-erase so crash recovery is deterministic. (A regime requiring physical destruction of even those closed bytes is a storage-lifecycle / compaction concern, not language semantics.)

Retraction is not death. Ceasing to be alive is ordinary state — a fact you assert (insert iof(alice, Deceased)), and it leaves every proposition that was true of her, bornTo included, standing in both history and the present view: a dead mother is still someone’s mother. Ceasing to be an entity — the identity itself leaving the domain — is retract. The two are orthogonal, and only the second fires the cascade.

One record, four fates. A single bornTo fact routes to a different verb depending on what went wrong:

• The record was wrong — the birth was logged with a mother who was never this child’s mother (or was never a real individual at all). It was never true, so it is a belief-time correction: amend bornTo(child, wrong) => bornTo(child, right), or a standalone withdrawal amend bornTo(child, wrong) when there is no replacement. The child is untouched; the amended proposition returns to unknown — an uninitialized fiber is the legal “not yet recorded”, not a refutation — and the end-freeze releases as if it had never been set, so a later insert bornTo(child, right) admits where it would have refused OE1403. With the false tuple withdrawn, retract wrong alone is now admitted: coverage reads the net corrected view, where the amended tuple is no longer incident, so nothing strands — the exact refusal (OE1404) that retracting the mother alone drew before the amendment. Retraction without the amendment would be a lie (the child did not cease; nothing ended).
• The thing ceased — the mother genuinely leaves the domain, taking that whole branch with her: retract {mother, child} (the set covers her child’s constitutive context, per OE1404; her other constitutive bindings need their contexts in the set too). If she died but the child lives on, this is not the case — that is the Deceased fact above, not a retraction.
• The subject invoked erasure — a compliance request to remove a person’s data: forget subject, under #[allow_forget]. This is capability-gated physical erasure, reserved for privacy/compliance — not the everyday cessation channel.
• An association simply changed — a toy is given away. ownedBy(mut toy, mut owner) is a pure association, both ends mut, so it is neither retraction nor amendment: delete ownedBy(toy, kid); insert ownedBy(toy, newKid);. Direct tuple rebinding is admitted precisely because every end is mut.

The amend semantics described above are not sketch: they are fixed by the canonical design record — RFD 0076 and its mechanized amendment suite in the Lean substrate — so the belief-time reading, the OE1405/OE1406/OE1407/OE1409 refusals, and the net-corrected-view coverage stated here are specified, not provisional. The surface implementation that enforces them is present on this toolchain, so the amend-dependent steps above run. Because the design record governs the semantics, this description cannot silently drift from the shipped behavior.

The resurrection guard — OE1400

Retract an individual and then re-introduce it in the same transaction — re-classify it, name it at a relation endpoint, or write a property of it — and the whole transaction refuses:

pub mutate resurrect(p: Passport) {
    retract p;
    insert iof(p, Passport);   // OE1400 — p was retracted earlier in this transaction
}

OE1400: retracted individual `p1` was re-introduced: still classified as `Passport`.

The cascade released p’s constitutive bindings on the premise that p was gone; naming p again after that, in the same commit, would falsify that premise after the fact. (An assert-then-retract nets clean and is admitted — the retraction sweeps the earlier assertion.) The lawful form is a later transaction: once p is genuinely retracted, a subsequent transaction may re-introduce the identity, where the ordinary immutable-fiber freeze — not the resurrection guard — governs any re-asserted binding as a replacement assertion.