State Machines

A great many domain concepts have a lifecycle: a Lease is Pending, then Active, then Expired or Terminated. An Order moves through Placed, Paid, Shipped, Delivered. A Patient cycles through Admitted, InTreatment, Discharged.

Argon has a dedicated construct for these — a lifecycle { … } block inside a concept body — that turns “this concept moves through phases” into a first-class part of the type system. The phases become subtypes of the parent concept. The transitions become rules. The reasoner can answer “what phase is this lease in right now” and “could this lease ever reach Terminated from where it is.”

This chapter teaches today’s lifecycle surface and shows where it is going.

A first lifecycle

Inside the Lease declaration:

pub relator Lease {
    id: String,
    tenant: Tenant,
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,

    lifecycle {
        initial Pending,
        Active,
        Expired,
        terminal Terminated,

        Pending -> Active { on: signed }
        Active -> Expired { on: term_end }
        Active -> Terminated { on: termination_notice }
        Expired -> Terminated { on: settled }
    }
}

Five things happen here.

Phases

Inside lifecycle { }, the first members are phases. Each phase is a subtype of the parent concept (Lease) — Pending, Active, Expired, and Terminated are all subtypes of Lease, picked out by which lifecycle phase a particular lease is in at a given valid time.

A phase can be marked initial (the entry state) or terminal (an exit state with no outgoing transitions). A phase can carry its own fields — Active { occupied_since: Date } says any active lease has an occupied_since field that the others do not.

The phase metatype (declared in our package’s metatypes.ar) carries the semantic weight: phase is anti-rigid (instances move through phases) and sortal. The compiler treats sibling phases as disjoint — a lease cannot be both Active and Expired at the same valid time.

Transitions

After phases come transitions: Source -> Target { clauses }. Each transition declares one allowed move from one phase to another.

A transition admits three inner clauses, of which only one — on: — is fully wired today:

The lease’s Pending -> Active { on: signed } reads: when the signed event arrives, transition to Active. The compiler turns this into a derive rule plus an event consequence.

Migration note (the big one for this chapter): the team is exploring a redesign that collapses lifecycle { … } into a top-level statemachine sugar, desugaring to an enum, a set of derive rules, and Transition events. The current lifecycle keyword stays through a migration window; the new shape sits next to it. The two forms are close enough that switching is mechanical:

Today:

pub relator Lease {
    ...
    lifecycle {
        initial Pending,
        Active,
        terminal Terminated,

        Pending -> Active { on: signed }
    }
}

Trajectory:

pub statemachine LeaseState {
    states { Pending, Active, Terminated }
    initial Pending
    terminal Terminated

    transitions {
        Pending -> Active :- signed(self), self.start_date <= today()
    }
}

The redesign’s body shape (:- pred-body => Transition(Pending, Active)) is more uniform with the rest of the language; today’s form is a curried sugar. Both produce the same runtime behavior. Do not rewrite working code today; expect the new form to be alias-accepted when it lands. See Appendix D.

What the lifecycle gives you

A lifecycle block is not just notation. The compiler does several things with it.

Disjointness for free

A Lease is in exactly one phase at a given valid time. The phase metatype encodes the disjointness; the compiler enforces it. You do not write a partition axiom over the phases. (This is one of the places the redesign tightens — see Appendix D.)

Phases as subtypes

pub query active_leases() -> [Active] :-
    ?l: Active
    => ?l

Active is a type. You can return phase-typed values; you can pattern-match on phases; you can dispatch behavior based on phase. The compiler tracks the subtype relationship so that an Active is also a Lease for any context that expects one.

Reachability checks

The compiler computes reachability from initial phases to terminal phases. If you declare a phase that is not reachable from any initial phase — say, you forget the transition into it — the compiler tells you. If you declare a terminal phase that has outgoing transitions, you get an error.

Bitemporal tracking

The runtime treats phase changes as events on the bitemporal log. A query against --as-of-valid #2026-04-15# answers “what phase was the lease in on April 15?” The phase history is queryable.

A worked time-travel pattern: the bitemporal/ variant in _catalog/lifecycle-block/ shows a lease declaring its lifecycle, transitioning through Pending → Active, and a query filtered by valid time:

pub relator Lease {
    id: String,
    start_date: Date,
    end_date: Date,

    lifecycle {
        initial Pending,
        Active,
        terminal Terminated,

        Pending -> Active { on: signed }
        Active -> Terminated { on: term_end }
    }
}

pub derive ActiveLease(l: Lease) :-
    l: Lease, Active(l)

// At the runtime, `ox query ActiveLease --as-of-valid #2026-04-15#`
// returns the leases that were in the Active phase on April 15,
// even if they have since transitioned to Terminated.

Variants: _catalog/lifecycle-{block,phase,transition}/{minimal,bitemporal,composition-with-derive,multi-transition}/.

Variations

A few common shapes worth recognizing.

Phase with fields

A phase can carry its own data:

Active { occupied_since: Date, last_payment: Date },

The intent: occupied_since exists on Active-typed values but not on Pending or Expired. Phase fields are reserved for data that only makes sense within a phase.

Note: today’s compiler accepts the syntax but emits OW1808 (“lifecycle phase data fields not yet elaborated”) because phase-field resolution is incomplete. Until that lands, keep phases bare names — Active, rather than Active { occupied_since: Date }, — and put per-phase data on the parent concept or on a related kind keyed by phase.

Guards and effects today

Until the unified consequence syntax lands, gate a transition by putting the precondition on the mutation that fires its trigger event, and emit downstream events from the same mutation. For the lease tutorial, the sign_lease mutation precondition checks the start date is valid, then emits signed; the lifecycle’s Pending -> Active { on: signed } does the rest.

pub mutation sign_lease(l: Lease, signed_at: Date) -> Lease {
    require {
        l.start_date < l.end_date
    }
    do { }
    emit LeaseSigned(l, signed_at)
    return l
}

The runtime publishes LeaseSigned into the bitemporal log; the lifecycle’s transition fires; the phase moves from Pending to Active. The event is queryable, audit-trailable, and contributes to provenance.

Migration note: when { … } and brings_about { … } clauses inside transitions become first-class once the unified consequence syntax lands — the redesign reads transitions as Pending -> Active :- signed(self), self.start_date <= today() => Transition(Pending, Active) and LeaseSigned(self). Same semantics; the rule-body grammar replaces the constraint sublanguage. See Appendix D.

Multi-source transitions

Two transitions can share a target:

Active -> Terminated { on: termination_notice }
Expired -> Terminated { on: settled }

The Datalog the compiler produces fans these out as separate rules with the same head; the disjunction is automatic.

Standalone state-machines

Sometimes the state machine is the whole point and the parent concept is just a peg to hang it on. Declare a minimal kind whose only purpose is to host the lifecycle:

pub kind ApplicationStatus {
    application_id: String,

    lifecycle {
        initial Submitted,
        UnderReview,
        Approved,
        terminal Rejected,

        Submitted -> UnderReview { on: review_started }
        UnderReview -> Approved { on: approved }
        UnderReview -> Rejected { on: rejected }
    }
}

Once the redesign lands, this becomes a top-level statemachine ApplicationStatus { … } declaration without the parent kind, but the semantics are the same.

Edge cases worth knowing

• lifecycle is inside a concept body, not an item-start construct. You cannot write lifecycle X { … } at module level today.
• Phases cannot be pub independently of their parent. Visibility flows from the host concept.
• A concept can have at most one lifecycle. If you find yourself wanting two state machines on the same concept, either model the second as a separate concept or use a phase-of-phase nesting (which the parser does not directly support today; see Phase-B’s open thread on hierarchical state machines).
• Phase names cannot collide with the host’s field names. The compiler reports a collision error.
• initial and terminal are contextual modifiers, not keywords. They lex as IDENTs and the parser dispatches on context.

Putting it in the running example

Update src/lease.ar to add the lifecycle:

use metatypes::*
use party::*

pub kind Property {
    id: String,
    address: String,
}

pub relator Lease {
    id: String,
    tenant: Tenant,
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,

    lifecycle {
        initial Pending,
        Active,
        Expired,
        terminal Terminated,

        Pending -> Active { on: signed }
        Active -> Expired { on: term_end }
        Active -> Terminated { on: termination_notice }
        Expired -> Terminated { on: settled }
    }
}

pub subkind ResidentialLease : Lease {
    bedrooms: Int,
}

pub subkind CommercialLease : Lease {
    permitted_use: String,
}

Then:

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.13s

The lease now has a lifecycle. We can ask ox query active_leases and the runtime knows how to filter by phase. We can mutate from Pending to Active via the existing sign_lease mutation, and the event flows through the lifecycle’s transition guard.

Summary

A lifecycle { … } block declares phases as subtypes and transitions as rule-events between them. The compiler gives you sibling-disjointness, subtype-typed phases, reachability checks, and bitemporal phase tracking. The lease tutorial now has a complete lifecycle. The redesign trajectory collapses the surface into statemachine sugar; today’s syntax stays through the migration. Next we test the model.