Trait contracts: clause union, supertraits, and reflective dispatch
Area: Traits Teaches: the trait atom — a rule-plane trait whose per-type
implclauses union under one head (dispatch is derivation), a supertrait acting as a requires-constraint, the partial-coverage guard that excludes uncovered individuals explicitly rather than by silence, enumeration/NAF over the catalog-closed$implementsrelation, and a#[static]conformance check. Prerequisites: concepts and<:;deriverule bodies; the reflective meta-plane (meta,implements,specializes). Run:ox build examples/trait_contracts && ox check --codes examples/trait_contracts— andox derive examples/trait_contracts/target/root.oxbin ServiceableKinds
A trait names a contract a type can implement. Inspectable requires a Due rule; each impl Inspectable for T supplies one clause, and the clauses union under the single Inspectable::Due head. Dispatch is not a vtable lookup — it is derivation: the reasoner fires whichever clauses match.
What to read in fleet.ar
Clause union — one head, three type-guarded clauses with per-kind thresholds:
pub trait Inspectable { derive Due(Self); }
impl Inspectable for Truck { derive Due(t: Self) :- t.hours >= 100; }
impl Inspectable for Crane { derive Due(c: Self) :- c.hours >= 50; }
impl Inspectable for Drone { derive Due(d: Self) :- d.hours >= 10; }
A supertrait is a requires-constraint (Rust’s :): impl Serviceable for T demands impl Inspectable for T, and the reflective surface closes over it — implements(t, Serviceable) entails implements(t, Inspectable). Serviceable covers only Truck and Crane; Drone is field-maintained.
The partial-coverage guard (D3.2). A bare NeedsService(a) over Asset would be OE1327 because Serviceable does not cover every kind. ShopQueue writes the dispatch-can-fail branch explicitly — uncovered drone individuals are excluded by the guard’s $implements join, never by silence:
pub derive ShopQueue(a: Asset) :-
implements(meta(a), Serviceable),
NeedsService(a);
Enumeration and NAF over the catalog-closed $implements — these read type names directly, with no instances:
pub derive ServiceableKinds(t) :- implements(t, Serviceable);
pub derive SelfMaintained(t) :- specializes(t, Asset), t != Asset, not implements(t, Serviceable);
A #[static] catalog-level conformance check discharges totally at ox check. It PASSES — the three Inspectable impls cover every declared asset kind:
#[static]
pub check EveryAssetKindIsInspectable(t: TypeRef) :-
specializes(t, Asset), t != Asset, not implements(t, Inspectable)
=> Diagnostic { severity: Severity::Error, code: "Fleet::E010", /* … */ };
Running it
ox check discharges the catalog-level conformance check and passes — every asset kind is inspectable:
$ ox check --codes examples/trait_contracts
ok
The catalog-closed reflective derives need no instances, so ox derive reads them straight off the type catalog:
$ ox derive examples/trait_contracts/target/root.oxbin ServiceableKinds
derive(ServiceableKinds): 2 tuple(s)
(fleet::Truck)
(fleet::Crane)
$ ox derive examples/trait_contracts/target/root.oxbin SelfMaintained
derive(SelfMaintained): 1 tuple(s)
(fleet::Drone)
ServiceableKinds = {Truck, Crane} (the free-t enumeration over implements(t, Serviceable)); SelfMaintained = {Drone} (the NAF complement). Once individuals are registered, InspectionQueue collects every asset past its kind’s threshold (truck 100h / crane 50h / drone 10h — the Inspectable cover is total), while ShopQueue admits only the guard-covered and clause-satisfying ones (the worn truck, the flagged crane) — never a drone, even a worn one: its dispatch fails visibly through the guard.
Honest caveats (what runs today)
- The package has no
demo.toml, and the instance-driven derives (Due,InspectionQueue,ShopQueue) need registered individuals —ox deriveover the bare artifact shows them empty. The catalog-closed reflective derives (ServiceableKinds,SelfMaintained) are the part demonstrable straight from the CLI; the instance-driven extents are pinned by the corpus test, which seeds via theregister_*mutations. - To see the failing conformance variant, retarget the check at
Serviceable(commented infleet.ar):Droneimplements noServiceable, soox checkfails withFleet::E010before any artifact is written.
This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the clause-union InspectionQueue, the D3.2-guarded ShopQueue (truck + crane, never a drone), ServiceableKinds = {Truck, Crane}, SelfMaintained = {Drone}, and the check’s catalog-level classification, so the trait surface 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
//! # Trait contracts — clause union, `implements`, and static conformance
//!
//! A single-module fleet-maintenance package exercising the full RFD 0026
//! trait surface as of slice 2:
//!
//! * a **multi-impl rule-plane trait** (`Inspectable::Due`) whose per-type
//! clauses union under one head — dispatch is derivation;
//! * a **supertrait** (`Serviceable: Inspectable`) acting as a
//! requires-constraint, and its logical consequence in the reflective
//! surface (`implements(t, Serviceable) → implements(t, Inspectable)`);
//! * the **D3.2 partial-coverage guard**: `ShopQueue` calls a member of a
//! trait that does NOT cover every Asset kind, made legal by the visible
//! `implements(meta(a), Serviceable)` conjunct — uncovered individuals
//! are excluded by the guard, never by silence;
//! * **enumeration** over the catalog-closed `$implements` relation (free
//! type position) and **NAF** over it;
//! * a **`#[static]` catalog-level conformance check** that discharges at
//! `ox check` (RFD 0025 D1 as amended: `TypeRef`/`TraitRef` vocabulary).
//!
//! The metatypes are declared in-package (`category`/`kind` are ordinary
//! `pub metatype` declarations, not language surface). `category` is
//! declared `abstract` (RFD 0027 D6) — the substrate-neutral modifier is
//! what exempts `Asset` from needing a covering impl of its own (no direct
//! instances ⇒ no coverage obligation); the package's sortality axis is
//! its own ontological vocabulary, inert to the compiler.
mod fleet;
fleet.ar
//! Fleet maintenance under trait contracts.
//!
//! ## The contracts
//!
//! `Inspectable` covers EVERY asset kind (three impls — clause union with
//! per-kind thresholds), so the bare member atom in `InspectionQueue` passes
//! the coverage gate outright. `Serviceable` covers only `Truck` and `Crane`
//! — `Drone` is field-maintained — so a bare `NeedsService(a)` over `Asset`
//! would be OE1327; `ShopQueue` writes the dispatch-can-fail branch
//! explicitly with the `implements(meta(a), Serviceable)` guard (RFD 0026
//! D3.2): drone individuals are excluded by the guard's `$implements` join,
//! never by silence.
//!
//! ## Expected behavior (pinned by the corpus test)
//!
//! * `Due` / `InspectionQueue` — every registered asset past its kind's
//! inspection threshold (truck 100h, crane 50h, drone 10h);
//! * `ShopQueue` — only covered+satisfying individuals: the worn truck
//! (mileage ≥ 10000) and the flagged crane; never a drone;
//! * `ServiceableKinds` — free-variable enumeration of the catalog-closed
//! `$implements` relation: exactly {Truck, Crane};
//! * `SelfMaintained` — NAF over `$implements`: exactly {Drone};
//! * `EveryAssetKindIsInspectable` — a `#[static]` conformance check whose
//! vocabulary is all reflective-sorted (`TypeRef` variable, `specializes`
//! + `implements` atoms), so it discharges totally at `ox check` — and
//! PASSES (the three Inspectable impls cover every kind).
//!
//! To see the failing variant, retarget the check at `Serviceable` (comment
//! below): `Drone` implements no `Serviceable`, so `ox check` fails with
//! `Fleet::E010` before any artifact is written.
// The sortality axis is the package's own ONTOLOGICAL vocabulary — the
// compiler never reads it (RFD 0027 D6). The substrate behavior comes
// from the `abstract` modifier on `category`: abstract types admit no
// direct instances, so the OE1327 coverage gate exempts `Asset` itself
// and quantifies over its non-abstract kinds.
pub metaxis sortality for metatype { sortal, non_sortal };
pub abstract metatype category = { sortality: non_sortal };
pub metatype kind = { sortality: sortal };
pub category Asset {
mut hours: Int,
mut flagged: Bool,
}
pub kind Truck <: Asset {
mut mileage: Int,
}
pub kind Crane <: Asset;
pub kind Drone <: Asset;
// ANCHOR: trait_union
/// Every asset kind must be inspectable — the package-wide obligation.
pub trait Inspectable {
derive Due(Self);
}
/// Shop-serviceable kinds. A supertrait (requires-constraint, Rust's `:`):
/// an `impl Serviceable for T` demands `impl Inspectable for T` — and the
/// reflective surface closes over it: `implements(t, Serviceable)` entails
/// `implements(t, Inspectable)`.
pub trait Serviceable : Inspectable {
derive NeedsService(Self);
}
// Clause union: one head (`Inspectable::Due`), three type-guarded clauses
// with per-kind thresholds. Dispatch is derivation.
impl Inspectable for Truck {
derive Due(t: Self) :- t.hours >= 100;
}
impl Inspectable for Crane {
derive Due(c: Self) :- c.hours >= 50;
}
impl Inspectable for Drone {
derive Due(d: Self) :- d.hours >= 10;
}
// ANCHOR_END: trait_union
// Partial coverage BY DESIGN: drones are field-maintained.
impl Serviceable for Truck {
derive NeedsService(t: Self) :- Due(t), t.mileage >= 10000;
}
impl Serviceable for Crane {
derive NeedsService(c: Self) :- Due(c), c.flagged == true;
}
/// Fully covered bare member atom — no guard needed (D3.1).
pub derive InspectionQueue(a: Asset) :- Due(a);
/// Partially covered member atom under the explicit D3.2 conformance
/// guard: fires only for individuals SOME classifier of which is covered
/// (existential over the multi-valued `meta`, §12.4) AND whose clause
/// body holds.
pub derive ShopQueue(a: Asset) :- implements(meta(a), Serviceable), NeedsService(a);
/// Free-variable enumeration over `$implements` (the OE0212 exemption):
/// which declared types carry the Serviceable contract?
pub derive ServiceableKinds(t) :- implements(t, Serviceable);
/// NAF over the catalog-closed `$implements` — stratification-safe:
/// asset kinds that do NOT carry the Serviceable contract.
pub derive SelfMaintained(t) :- specializes(t, Asset), t != Asset, not implements(t, Serviceable);
/// Catalog-level conformance check (RFD 0025 D1 as amended by RFD 0026
/// D6: every variable reflective-sorted — `TypeRef` here; `specializes` /
/// `implements` vocabulary). Discharges totally and finally at
/// `ox check` / `ox build`; `#[static]` makes instance-vocabulary drift a
/// hard error (OE1322) instead of a silent reclassification. PASSES: the
/// three Inspectable impls cover every declared asset kind.
// ANCHOR: static_conformance
#[static]
pub check EveryAssetKindIsInspectable(t: TypeRef) :-
specializes(t, Asset),
t != Asset,
not implements(t, Inspectable) => Diagnostic {
severity: Severity::Error,
code: "Fleet::E010",
message: format!("{} must implement Inspectable", t)
};
// ANCHOR_END: static_conformance
// The FAILING variant — retarget the obligation at Serviceable and the
// check fires on Drone at `ox check` (Fleet::E010, build refused):
//
// #[static]
// pub check EveryAssetKindIsServiceable(t: TypeRef) :-
// specializes(t, Asset), t != Asset,
// not implements(t, Serviceable)
// => Diagnostic {
// severity: Severity::Error,
// code: "Fleet::E010",
// message: format!("{} must implement Serviceable", t),
// };
pub mutate register_truck(x: Truck, hours: Int, mileage: Int) {
insert iof(x, Truck);
update x: Truck set { hours = hours, mileage = mileage, flagged = false }
}
pub mutate register_crane(x: Crane, hours: Int, flagged: Bool) {
insert iof(x, Crane);
update x: Crane set { hours = hours, flagged = flagged }
}
pub mutate register_drone(x: Drone, hours: Int) {
insert iof(x, Drone);
update x: Drone set { hours = hours, flagged = false }
}