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.