Defined versus primitive

A refinement attaches a predicate to a concept, producing a subtype whose members satisfy that predicate. The keyword chooses what the predicate means for membership, and the two readings are not interchangeable. This is the description-logic split between a defined class and a primitive one — necessary-and-sufficient conditions against necessary-only — and Argon makes the modeler pick.

iff { P } is defined. P is necessary and sufficient: a value of the supertype is a member if and only if it satisfies P. Membership is derived. The substrate reads the underlying state, evaluates P, and classifies — the modeler never asserts membership directly.

pub type Adult <: Person iff { self.age >= 18 };

Any Person whose age is at least 18 is an Adult, automatically. To make someone an Adult you change their age; the classification follows. Asserting membership by hand — insert iof(p, Adult) — is rejected (OE0211), because for a defined concept the predicate is the source of truth, and a manual assertion could contradict it.

where { P } is primitive. P is necessary only: every member satisfies it, but satisfying it does not confer membership. Membership is asserted — conferred by construction or by an explicit insert iof — and P is enforced as an invariant at each membership write, never as a filter that widens the extent.

pub type Cleared <: Person where { self.clearance_score >= 50 };

A score of 50 or more does not make a Person Cleared. Clearance is granted by an authority; the where predicate is the standing guarantee that anyone granted it meets the bar. A grant to someone below the threshold is rejected (OE0668) — the invariant holds on every member — but a qualifying score sitting in the data confers nothing on its own. This is Rust’s where bound lifted from a function to a concept’s members: a constraint, not a definition.

The contrast is sharpest on a single population. Give four people ages over 18 and a clearance_score field; one of them, never granted clearance, carries a score of 70. The Adult extent is all four — iff classifies from state. The Cleared extent is only those granted — where confers nothing from the qualifying score alone. The same data, two opposite disciplines, chosen by one keyword. Argon by Example works this through in primitive_refinement.

A predicate may read several fields and combine them with &&, ||, and comparisons — iff { self.age >= 18 && self.status == "active" } defines an active adult — and it evaluates on the same exact value tower as every other value position: exact rationals for Real, Decimal, and Money, chronological comparison for dates.