Machine parts: metarel endpoints, signature reflection, per-type axis override

Area: Relations Teaches: the three relation/meta-property features a vocabulary author needs — a metarel that constrains its endpoints’ metatypes, a derive/check that reflects over relation signatures (rel/arm/meta) to audit them, and a per-type axis override that wins over the metatype default. Prerequisites: first-class relations, and the meta-calculus (metaxis / metatype / metarel, meta). Run: ox build examples/machine_parts_v0 && ox derive examples/machine_parts_v0/target/root.oxbin mountEndpointIsFitting

A vocabulary author building a classification vocabulary — here a small taxonomy of machine parts — does not just declare concepts: they declare the rules of well-formedness for the modelers who consume the vocabulary, and they want the compiler to enforce them. This example is the well-formed proof of three such features; its sibling machine_parts_bad is the refusal half.

What to read in root.ar

A metarel constrains its endpoints’ metatypes. attachment is a binary introducer metarel; its host position must be part-sorted and its mount position must be fitting-sorted. A component mounts via a fitting, not a bare part — and the compiler verifies it at elaboration:

pub metarel attachment(host: part, mount: fitting) {
    load_kind::load_bearing,
};

A relation declared with this introducer whose endpoints match is well-formed; mountedVia does, because Chassis is a part and Bracket is a fitting:

pub attachment mountedVia(host: Chassis, mount: Bracket) [1..1] [0..*];

A vocabulary audits relation signatures declaratively. rel(r, attachment) enumerates every relation classified by the metarel; arm(r, 1, t) reads its position-1 endpoint type; meta(t) reads that type’s metatype. Joined together, the vocabulary checks its own endpoint discipline — r and t are TypeRef-sorted, so this derives at the catalog tier:

pub derive mountEndpointIsFitting(r: TypeRef, t: TypeRef) :-
    rel(r, attachment), arm(r, 1, t), meta(t) == fitting;

pub derive mountEndpointIsPart(r: TypeRef, t: TypeRef) :-
    rel(r, attachment), arm(r, 1, t), meta(t) == part;

A type can override an axis its metatype binds. Gasket is introduced by part, whose metatype binds replaceability::permanent — but a gasket wears out and is consumable. The per-target override sets the type’s own effective replaceability, and the type-keyed t.replaceability projection reads the override, not the metatype default:

pub part Gasket { replaceability::consumable }

pub derive consumableTypes(t: TypeRef) :- t.replaceability == replaceability::consumable;

Running it

The vocabulary’s own audit confirms the discipline holds. The mount endpoint of every attachment relation is fitting-sorted (so the well-formed set is the whole set), and no attachment relation has a part in its mount slot:

derive(mountEndpointIsFitting): 1 tuple(s)
  (<anonymous>::mountedVia, <anonymous>::Bracket)
derive(mountEndpointIsPart): 0 tuple(s)

The override wins: consumableTypes returns three types — fitting and Bracket (consumable by their metatype) and Gasket, whose per-target override beats the permanent it inherits from part:

derive(consumableTypes): 3 tuple(s)
  (<anonymous>::fitting)
  (<anonymous>::Bracket)
  (<anonymous>::Gasket)

Honest caveats (what runs today)

• Maximum cardinality is enforced at the write path; a minimum above zero is recorded on the wire but not yet enforced in v0. mountedVia declares [1..1] at its host position, so ox build emits OW1342 naming the relation and position — a warning, not a refusal; the build succeeds.

This example is compiled and run in CI — the corpus auto-discovery parses and resolves it, and a driver test (oxc-driver/tests/cli/scenario.rs) pins that this package checks clean while its sibling refusal fixture is refused. If the language changes underneath it, the build breaks rather than the docs going stale.

Source

The package’s real Argon source, transcluded from the file this corpus compiles — what you read here is exactly what CI builds.

//! `machine_parts_v0` — the vocabulary-authoring proof for the v0.2.1
//! relation-constraint plane (RFD 0031). A small machine-parts classification
//! vocabulary that exercises, end-to-end and corpus-pinned, the three
//! relation/meta-property features a vocabulary author needs and could NOT
//! express before:
//!
//!   1. **Metarel endpoint-metatype verification** (#311, RFD 0031 D1). The
//!      `attachment` metarel requires its mount position to be
//!      `fitting`-sorted: a component must mount *via a fitting*, not a bare
//!      part. `mountedVia(host: Chassis, mount: Bracket)` is well-formed
//!      (`Bracket` is a `fitting`); the wrong-sorted variant in the sibling
//!      refusal fixture (`machine_parts_bad`) is refused OE0631.
//!
//!   2. **Relation-signature reflection** (#312, RFD 0031 D2). A
//!      vocabulary-shipped catalog `derive`/`check` quantifies over declared
//!      relations through `rel` / `arm`, joins their endpoint types' metatypes
//!      through `meta`, and audits the endpoint discipline declaratively.
//!
//!   3. **Per-type axis override** (R-M9, RFD 0031 D3). `Gasket` overrides the
//!      `replaceability` its `part` metatype binds — `Gasket`'s effective
//!      replaceability reads the per-target `consumable`, not the metatype
//!      default `permanent`.

// ── Axes (pure user vocabulary; the compiler never reads a name) ──
pub metaxis replaceability for metatype { consumable < serviceable < permanent };
pub metaxis granularity for metatype { atomic, composite };
pub metaxis load_kind for metarel { load_bearing, cosmetic };

// ── Metatypes: the introducer keywords this vocabulary ships ──
pub metatype part = { replaceability: permanent, granularity: atomic };
pub metatype fitting = { replaceability: consumable, granularity: composite };

// ── A binary introducer metarel whose endpoints are metatype-constrained.
// Position 0 must be `part`-sorted (the host), position 1 `fitting`-sorted
// (the fitting it mounts through) — verified at elaboration (#311).
pub metarel attachment(host: part, mount: fitting) { load_kind: load_bearing, };

// ── Concepts declared with this vocabulary's introducers ──
pub part Chassis;
pub fitting Bracket;

// R-M9 (RFD 0031 D3): `Gasket` is introduced by `part` (metatype
// replaceability `permanent`) but OVERRIDES replaceability to `consumable`
// per-target — a gasket wears out even though its metatype is permanent.
pub part Gasket {
    replaceability::consumable,
}

// ── An attachment relation with CORRECT endpoint metatypes ──
// `Chassis` is a `part`, `Bracket` is a `fitting` — matches the metarel
// positions, so this is well-formed (#311 passes).
pub attachment mountedVia(host: Chassis, mount: Bracket) [1..1] [0..*];

// ── #312: relation-signature reflection ──
//
// Enumerate every relation classified by `attachment` together with its
// mount-position endpoint type. Catalog-closed (`rel`/`arm`/`meta` over
// declarations), so `t` and `r` are TypeRef-sorted and this derives at the
// catalog tier.
pub derive attachmentMountEndpoint(r: TypeRef, t: TypeRef) :- rel(r, attachment), arm(r, 1, t);

// The vocabulary's own audit: the mount endpoint of every `attachment`
// relation IS fitting-sorted (so this WELL-FORMED-ENDPOINT set is the whole
// set, and the "part in the mount slot" set below is empty — the discipline
// holds across the consumer catalog).
pub derive mountEndpointIsFitting(r: TypeRef, t: TypeRef) :-
    rel(r, attachment),
    arm(r, 1, t),
    meta(t) == fitting;

pub derive mountEndpointIsPart(r: TypeRef, t: TypeRef) :-
    rel(r, attachment),
    arm(r, 1, t),
    meta(t) == part;

// ── R-M9: the per-target override is read by the TYPE-keyed
// `t.replaceability` projection (`t: TypeRef`). `Gasket` is introduced by the
// `permanent` metatype `part` but its per-target override makes ITS
// replaceability `consumable`. The metatype-tier `meta(t).replaceability`
// would still read the metatype default; `t.replaceability` reads the type's
// own effective value (override winning).
pub derive consumableTypes(t: TypeRef) :- t.replaceability == replaceability::consumable;