Refinement: iff (defined) vs where (primitive)

Area: Refinement & types Teaches: the two ways a refined concept gets its members — iff derives membership from a predicate, where asserts membership and treats the predicate as an enforced invariant. This is the most consequential distinction in Argon’s type layer. Prerequisites: concepts and <: specialization. Run: ox build examples/primitive_refinement && ox run-scenario examples/primitive_refinement

Two refined concepts sit over one Person population, and the keyword decides who is a member:

// Defined: anyone satisfying the predicate is automatically a member.
pub type Adult   <: Person iff   { self.age >= 18 };

// Primitive: membership is granted by an authority; the predicate is a
// necessary invariant on members, checked at the grant — never a classifier.
pub type Cleared <: Person where { self.clearance_score >= 50 };

• iff (Adult) — membership is derived. You never assert it; the reasoner classifies every Person whose age >= 18. Asserting it directly (insert iof(p, Adult)) is refused with OE0211.
• where (Cleared) — membership is asserted. A clearance is conferred by an act (grant_clearance → insert iof(p, Cleared)); the predicate only guards that act. A qualifying score is necessary, not sufficient.

The teaching contrast

Run it and compare the two extents. After the scenario seeds four people:

query clearance::adults:  4 row(s)   — Adult (iff):   everyone 18+, auto-classified
query clearance::cleared: 2 row(s)   — Cleared (where): only the two who were granted

The decisive case is dave: he has clearance_score = 70 (≥ 50) but was never granted, so he is not Cleared. Under iff he’d be classified automatically; under where membership is conferred, never inferred.

Honest caveats (what runs today)

• Granting clearance below the invariant is rejected with OE0668 (the where predicate is enforced at the grant). Inserting an iff membership directly is refused with OE0211.
• Refinement membership is evaluated by the reasoner at query time against each individual’s fields, so the extents above reflect the seeded age/score values.

This example is compiled and run in CI; its iff/where runtime behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so it can’t drift from the language.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Primitive (`where`) vs defined (`iff`) refinement — RFD 0017.

mod clearance;

clearance.ar

//! Primitive (`where`) vs defined (`iff`) refinement — the description-logic
//! split between *asserted* and *derived* membership (RFD 0017).
//!
//! Two refined concepts sit over one `Person` population:
//!
//!   * `Adult` is **defined** (`iff`): any `Person` with `age >= 18` is
//!     *automatically* classified — the substrate derives membership. You
//!     cannot `insert iof(p, Adult)` (it would emit `OE0211`); you change the
//!     underlying `age` and the classification follows.
//!
//!   * `Cleared` is **primitive** (`where`): clearance is *granted* by an
//!     authority (asserted via `grant_clearance`). `clearance_score >= 50` is
//!     a **necessary invariant** on members — necessary, not sufficient.
//!     Having a qualifying score does NOT make you `Cleared`; someone must
//!     grant it. Granting below the threshold is rejected with `OE0668`.
//!
//! Expected runtime behavior (after demo.toml):
//!   * `Adult`   (iff):   {alice, bob, carol, dave}  — all are 18+, derived
//!   * `Cleared` (where): {alice, carol}             — only those *granted*
//!
//! The teaching contrast: `dave` has `clearance_score` 70 (>= 50) but was
//! never granted, so he is NOT `Cleared`. Under `iff` he would be classified
//! automatically; under `where` membership is conferred, never inferred.

pub type Person {
    mut age: Int,
    mut clearance_score: Int,
}

// ANCHOR: defined
// Defined: membership is derived from the predicate (auto-classified).
pub type Adult <: Person iff { self.age >= 18 };
// ANCHOR_END: defined
// ANCHOR: primitive
// Primitive: membership is asserted (granted); the predicate is a necessary
// invariant checked at the grant, never a query-time extent filter.
pub type Cleared <: Person where { self.clearance_score >= 50 };
// ANCHOR_END: primitive
pub mutate register(p: Person, age: Int, score: Int) {
    insert iof(p, Person);
    update p: Person set { age = age, clearance_score = score }
}

// ANCHOR: grant
pub mutate grant_clearance(p: Person) {
    insert iof(p, Cleared);
}
// ANCHOR_END: grant
pub query adults() -> Adult;
pub query cleared() -> Cleared;