A small employment ontology: refinement + a concept hierarchy

Area: Refinement & types Teaches: how iff refinements layer over a concept hierarchy (<:), with mutable fields populated by a mutate and read back through queries — a realistic, end-to-end shape. Prerequisites: refinement (iff/where). Run: ox build examples/refinement_employment && ox run-scenario examples/refinement_employment

pub type Person   { mut weekly_hours: Int, mut direct_reports: Int }
pub type Employee <: Person;
pub type FullTime <: Employee iff { self.weekly_hours  >= 35 };
pub type Manager  <: Employee iff { self.direct_reports >= 1 };

Employee specializes Person; FullTime and Manager are defined subsets of Employee — a person is classified into them automatically by their fields, and is reclassified when those fields change. A single hire mutation establishes a person and populates the fields:

pub mutate hire(p: Person, hours: Int, reports: Int) {
    insert iof(p, Person);
    insert iof(p, Employee);
    update p: Person set { weekly_hours = hours, direct_reports = reports }
}

Running it

The scenario hires several people; full_timers and managers come back as the filtered subsets of the all_persons extent — the iff predicates evaluated per individual at query time. Change someone’s weekly_hours below 35 and they leave FullTime on the next read; classification follows the data.

This example is compiled and run in CI; its refinement behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

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

//! Refinement types: a typical employment ontology.

mod employment;

employment.ar

//! Refinement types: a typical employment ontology.
//!
//! Demonstrates:
//!   * Concept hierarchy with `<:` subsumption
//!   * Refinement predicates on subtypes (`where { ... }`)
//!   * Mutable fields (`mut`)
//!   * Mutations that establish individuals + populate fields
//!   * Queries that read refined extents
//!
//! Expected runtime behavior:
//!   * `Person` extent: every individual created via `hire`
//!   * `Employee` extent: same (everyone hired is an Employee
//!     iof-asserted by the mutation)
//!   * `FullTime` extent: only employees with `weekly_hours >= 35`,
//!     computed by the refinement at query time
//!   * `Manager` extent: employees with `direct_reports >= 1`

// ANCHOR: hierarchy
pub type Person {
    mut weekly_hours: Int,
    mut direct_reports: Int,
}

pub type Employee <: Person;
// ANCHOR_END: hierarchy
// ANCHOR: fulltime
pub type FullTime <: Employee iff { self.weekly_hours >= 35 };
// ANCHOR_END: fulltime
pub type Manager <: Employee iff { self.direct_reports >= 1 };

pub mutate hire(p: Person, hours: Int, reports: Int) {
    insert iof(p, Person);
    insert iof(p, Employee);
    update p: Person set { weekly_hours = hours, direct_reports = reports }
}

pub query all_persons() -> Person;
pub query all_employees() -> Employee;
pub query full_timers() -> FullTime;
pub query managers() -> Manager;