Idioms

This page answers: what’s the Argon way to do common things?

Each idiom names a common need and the canonical way to express it. Cross-links to the chapter or RFD that explains the underlying reasoning.

Re-export a foundational-ontology prelude

// In a leaf-package's prelude.ar
pub use ufo::prelude::*;

A package that builds on UFO re-exports UFO’s prelude so its consumers get the foundational-ontology vocabulary without explicit use ufo::prelude::* in every module. Same pattern works for BFO or any other foundational-ontology package.

See RFD-0011, ch04-01.

Group axiom declarations for symmetric constraints

disjoint(Person, Organization, System)

When multiple concepts share a symmetric structural relationship, prefer the dedicated declaration form (disjoint, complete, partition) over multiple pairwise where clauses.

See ch02-02, RFD-0018.

Anonymous individuals via `let _: T;`

let _: Sale;

When you need an individual to satisfy a constraint or pattern-match without naming it, let _: T; synthesizes an anonymous individual with a content-hash-derived identifier (__anon_<8-byte-blake3-hex>_<counter>). For block-local aliasing:

let _ as my_sale: Sale;

The handle my_sale is local to the enclosing block.

See ch02-02.

Diagnostic assertions in tests

test rejects_negative_age {
  expect { diagnostic OE0606 at //~ negative }
}

assert age(alice, -5)  //~ negative

expect { diagnostic <code> at //~ <marker> } matches the diagnostic against the source marker. This is the canonical way to test that a constraint or rule fires.

See ch03-03, RFD-0008.

Frame composition for shared test scaffolding

pub frame BasicCorporate {
  assert Organization(acme);
  assert Person(alice);
  assert works_at(alice, acme);
}

test scenario_a {
  using BasicCorporate;
  // ... test body ...
}

test scenario_b {
  using BasicCorporate;
  // ... different test body, same scaffolding ...
}

When multiple tests share setup, declare a pub frame and using it. Frames compose; multiple frames can be combined with conflict detection.

See ch03-03, RFD-0008.

Per-tier scoping at the granularity that matches need

// Module-scope (least granular)
#dec(tier:closure)

// vs declaration-scope (more granular)
#dec(tier:expressive)
pub derive complex_thing(X) :- ...

// vs block-scope (most granular)
#dec(tier:recursive) {
  pub derive ancestral(...) :- ...
}

Prefer the most granular scope that captures the actual need. Module-wide tier escalation hides the fact that one rule needed it; per-declaration scoping makes the requirement visible.

See tier-selection.md, ch05-03.

Why-provenance on derived facts

Every derive rule’s output carries why: PosBool(M) provenance automatically. To inspect:

query trace_classification(P) :-
  adult(P)
  => { person: P, why: meta(why_of(adult(P))) }

Provenance is a value field, not a separate query mechanism. It composes naturally with the rest of the expression grammar.

See RFD-0007.

Theorem marking on critical derivations

@[theorem]
pub derive every_adult_has_age(P) :- adult(P), exists(A, age(P, A))

When a rule encodes a structural invariant the system should mechanically verify, mark it @[theorem]. The compiler attempts proof; failure surfaces as OW0 warning. For tests asserting unprovable claims, use #[unproven] on the test instead.

See ch02-04, RFD-0008.

Multi-head defeasible disjunction

pub derive vehicle_class(V, "compact") :- size(V, "small")
pub derive vehicle_class(V, "midsize") :- size(V, "medium")
pub derive vehicle_class(V, "large") :- size(V, "large"), price(V, P), P > 30000

Multiple pub derive rules sharing a head act as disjunctive cases. They must agree on rule strength (all pub derive or all pub strict); mixing strengths produces OE0207.

See ch02-04.

Aggregate with `where` filter

pub derive total_revenue(O, T) :-
  Organization(O),
  T = sum(R) {
    Sale(S),
    sale_org(S, O),
    revenue(S, R)
    where status(S, "completed")
  }

Aggregate expressions admit a where clause that filters the witness set without changing the aggregate’s signature.

See ch02-04.

Compute with `ensure` for preconditions

compute capital_gain(s: Sale) {
  input { s: Sale }
  out { gain: Money, kind: String }
  ensure { s.proceeds >= 0, s.basis >= 0 }
  body {
    let gain = s.proceeds - s.basis;
    let kind = if gain > 0 { "gain" } else { "loss" };
    { gain: gain, kind: kind }
  }
}

ensure clauses validate inputs at call time; failures surface as compute-call diagnostics rather than corrupted outputs.

See RFD-0006, ch02-05.

Iterate-and-collect via comprehension

pub compute active_unit_numbers(b: Building) -> List[Text] =
    [u.number for u in b.units where unit_is_active(u)]

When the projection is a small expression — a field access, an arithmetic combinator, a constructor call — comprehensions read closer to the intent than the equivalent filter + map chain. The where clause is optional; the binder is fresh and local. Multi-source comprehensions are deferred to v2; in v1 chain two computes or compose two filter-maps when you need them.

See ch02-08, RFD-0039.

Optional unwrap with fallback

pub compute contact_or_placeholder(p: Person) -> Text =
    p.contact_email.unwrap_or("(no contact)")

unwrap_or covers presence-based defaulting. The fallback applies only to absence — unwrap_or(None(), d) returns d; unwrap_or(Some(undefined), d) returns the inner undefined, not d. K3-faithful semantics: presence is classical, inner truth state passes through.

When the intent is “either way, substitute a default,” chain a separate operation that operates on the inner value’s truth state.

See ch02-08, RFD-0037.

Rebuild-and-assign for collection-field mutation

pub mutation add_parent(l: Lease, p: Person) {
    do {
        l.parents = l.parents.append(p);
    }
    return l;
}

Collection operations are pure: append / union / filter / map return new collections, never mutating in place. In a do { } body, the idiomatic way to “modify” a collection field is to rebuild it and assign. Each assignment becomes a single GroundAssertion in the kernel’s append-only event log.

In-place mutators (l.parents.insert!(p)) are deferred. Use rebuild-and-assign in v1.