Reflection

The model is reflective: a program reads its own classification. Four intrinsics expose what would otherwise be the compiler’s private bookkeeping, as predicates a rule can range over.

• iof(x, T) tests whether x instantiates T. The rule-atom form x : T is sugar for it.
• meta(x) yields the <:-minimal type or types x instantiates — its immediate classifier.
• specializes(a, b) is the reflexive-transitive <: closure; the rule-atom form is a <: b.
• extent(T) enumerates the individuals that instantiate T.

A type used in value position is a value — a TypeRef — so these intrinsics take types as arguments and pass types as results. That is what makes them first-class predicates rather than compiler queries: a rule can quantify across types, count over them, and join them to data.

// reclassify any employee who manages someone, reading the catalog in a rule body
pub type Person   { name: String }
pub type Employee <: Person;
pub type Manager  <: Employee;

pub rel Supervises(boss: Employee, report: Employee);

pub derive promote(e) :- iof(e, Employee), Supervises(e, r), not iof(e, Manager);

promote ranges over the Employee extent, reads the Supervises relation, and tests membership with iof — including a negated membership test, not iof(e, Manager), which a non-reflective model could not phrase at all. Classification has become data the rule joins against, on the same footing as Supervises.

The consequence is that the catalog is queryable. extent(Manager) is a set a rule can count; specializes(Manager, Person) is a fact a rule can branch on. A program reasons about which types exist and how they relate, not only about the individuals under them — the foundation higher-order modeling builds on. The full signatures, the TypeRef sort, and the lowering to catalog relations are in Reflection.