UFO constraints: metarel endpoints, signature reflection, per-type axis override

Area: Relations Teaches: the three relation/meta-property features a UFO 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/ufo_constraints_v0 && ox derive examples/ufo_constraints_v0/target/root.oxbin aspectEndpointIsAspect

A vocabulary author building an upper ontology (UFO) 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 ufo_constraints_bad is the refusal half.

What to read in root.ar

A metarel constrains its endpoints’ metatypes. characterization is a binary introducer metarel; its bearer position must be kind-sorted and its aspect position must be aspect-sorted. An ability inheres via an aspect, not a kind — and the compiler verifies it at elaboration:

pub metarel characterization(bearer: kind, aspect_of: aspect) {
    dependency_kind::existential,
};

A relation declared with this introducer whose endpoints match is well-formed; inheresVia does, because Person is a kind and Ability is an aspect:

pub characterization inheresVia(bearer: Person, aspect_of: Ability) [1..1] [0..*];

A vocabulary audits relation signatures declaratively. rel(r, characterization) 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 aspectEndpointIsAspect(r: TypeRef, t: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == aspect;

pub derive aspectEndpointIsKind(r: TypeRef, t: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == kind;

A type can override an axis its metatype binds. Role is introduced by kind, whose metatype binds rigidity::rigid — but a role is anti-rigid. The per-target override sets the type’s own effective rigidity, and the type-keyed t.rigidity projection reads the override, not the metatype default:

pub kind Role { rigidity::anti_rigid }

pub derive antiRigidTypes(t: TypeRef) :- t.rigidity == rigidity::anti_rigid;

Running it

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

derive(aspectEndpointIsAspect): 1 tuple(s)
  (<anonymous>::inheresVia, <anonymous>::Ability)
derive(aspectEndpointIsKind): 0 tuple(s)

The override wins: antiRigidTypes returns three types — aspect and Ability (anti-rigid by their metatype) and Role, whose per-target override beats the rigid it inherits from kind:

derive(antiRigidTypes): 3 tuple(s)
  (<anonymous>::aspect)
  (<anonymous>::Ability)
  (<anonymous>::Role)

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. inheresVia declares [1..1] at its bearer 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 corpus test (oxc-runtime/tests/examples_corpus.rs) pins the reflection and override behaviour. 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.

//! `ufo_constraints_v0` — the UFO-authoring proof for the v0.2.1 relation-
//! constraint plane (RFD 0031). A small UFO-shaped vocabulary that exercises,
//! end-to-end and corpus-pinned, the three relation/meta-property features a
//! vocabulary author (Gustavo/Tiago, building ArgUFO) needs and could NOT
//! express before:
//!
//!   1. **Metarel endpoint-metatype verification** (#311, RFD 0031 D1). The
//!      `characterization` metarel requires its aspect position to be
//!      `aspect`-sorted: an ability must inhere *via an aspect*, not a kind.
//!      `inheresVia(p: Person, ab: Ability)` is well-formed (`Ability` is an
//!      `aspect`); the wrong-sorted variant in the sibling refusal fixture
//!      (`ufo_constraints_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). `Role` overrides the
//!      `rigidity` its `kind` metatype binds — `meta(Role).rigidity` reads the
//!      per-target `anti_rigid`, not the metatype default `rigid`.

// ── Axes (pure user vocabulary; the compiler never reads a name) ──
pub metaxis rigidity for metatype { anti_rigid < semi_rigid < rigid };
pub metaxis sortality for metatype { sortal, non_sortal };
pub metaxis dependency_kind for metarel { existential, contingent };

// ── Metatypes: the introducer keywords this vocabulary ships ──
pub metatype kind = { rigidity: rigid, sortality: sortal };
pub metatype aspect = { rigidity: anti_rigid, sortality: non_sortal };

// ── A binary introducer metarel whose endpoints are metatype-constrained.
// Position 0 must be `kind`-sorted (the bearer), position 1 `aspect`-sorted
// (the inhering aspect) — verified at elaboration (#311).
pub metarel characterization(bearer: kind, aspect_of: aspect) { dependency_kind: existential, };

// ── Concepts declared with this vocabulary's introducers ──
pub kind Person;
pub aspect Ability;

// R-M9 (RFD 0031 D3): `Role` is introduced by `kind` (metatype rigidity
// `rigid`) but OVERRIDES rigidity to `anti_rigid` per-target — a role is
// anti-rigid even though its metatype is rigid.
pub kind Role {
    rigidity::anti_rigid,
}

// ── A characterization relation with CORRECT endpoint metatypes ──
// `Person` is a `kind`, `Ability` is an `aspect` — matches the metarel
// positions, so this is well-formed (#311 passes).
pub characterization inheresVia(bearer: Person, aspect_of: Ability) [1..1] [0..*];

// ── #312: relation-signature reflection ──
//
// Enumerate every relation classified by `characterization` together with
// its aspect-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 characterizationAspectEndpoint(r: TypeRef, t: TypeRef) :-
    rel(r, characterization),
    arm(r, 1, t);

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

pub derive aspectEndpointIsKind(r: TypeRef, t: TypeRef) :-
    rel(r, characterization),
    arm(r, 1, t),
    meta(t) == kind;

// ── R-M9: the per-target override is read by the TYPE-keyed `t.rigidity`
// projection (`t: TypeRef`). `Role` is introduced by the `rigid` metatype
// `kind` but its per-target override makes ITS rigidity `anti_rigid`. The
// metatype-tier `meta(t).rigidity` would still read the metatype default;
// `t.rigidity` reads the type's own effective value (override winning).
pub derive antiRigidTypes(t: TypeRef) :- t.rigidity == rigidity::anti_rigid;