Trait contracts: clause union, supertraits, and reflective dispatch

Area: Traits Teaches: the trait atom — a rule-plane trait whose per-type impl clauses 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 $implements relation, and a #[static] conformance check. Prerequisites: concepts and <:; derive rule bodies; the reflective meta-plane (meta, implements, specializes). Run: ox build examples/trait_contracts && ox check --codes examples/trait_contracts — and ox 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 derive over 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 the register_* mutations.
• To see the failing conformance variant, retarget the check at Serviceable (commented in fleet.ar): Drone implements no Serviceable, so ox check fails with Fleet::E010 before 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.