Vocabulary package: publishing your own classifying vocabulary

Area: Vocabulary & packages Teaches: a package can publish its own introducer metatypes, an introducer metarel, upper categories, and a catalog check — the building blocks a foundational ontology like UFO is made of. None of this is built into the language; it is all ordinary pub surface. Prerequisites: the meta-calculus introducers (metatype / metarel), see hello. Run: ox build examples/vocab_pkg_v0 && ox check examples/vocab_pkg_v0

This is the author side of the two-package vocabulary journey. vocab_pkg_v0 ships a small UFO-shaped vocabulary; vocab_consumer_v0 (a separate package) depends on it. The point is that Argon has no privileged ontology: a vocabulary is a normal package, and everything that makes UFO “UFO” — the kinds, the categories, the well-formedness checks — lives on this package’s public surface.

What to read in root.ar

Introducer metatypes — declaration keywords for the consumer. A metatype published pub becomes a keyword a downstream package declares its concepts with:

pub metatype category = { };
pub metatype kind = { };

A binary introducer metarel. Same idea, for relations: a published metarel is a keyword for declaring relations downstream:

pub metarel characterization<A, B>(a: A, b: B);

Upper-ontology categories the consumer specializes. These are concepts declared with the package’s own category introducer, forming a small hierarchy the consumer hangs its domain off of:

pub category Endurant;
pub category Substantial <: Endurant;
pub category Detached    <: Endurant;

A catalog check the vocabulary ships — and that fires on the consumer’s catalog. This is what makes a vocabulary package real rather than decorative. The check is #[static] and every variable is TypeRef-sorted, so it discharges at ox check/ox build time over the catalog of declared types — not over runtime individuals:

#[static]
pub check OrphanKind(k: TypeRef) :-
    meta(k) == kind,
    specializes(k, Detached)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "UFO::W001",
        message:  "a `kind` specializes `Detached` — specialize `Substantial` instead",
    };

It reads the reflective intrinsics meta (the metatype a concept was introduced with) and specializes (the declared hierarchy). It flags any kind that specializes Detached. Crucially, the check is written here, in the vocabulary, but it runs against the consumer’s pub kind declarations — imported checks travel with the vocabulary.

Running it

The vocabulary checks clean on its own — it declares no offending kind itself:

$ ox build examples/vocab_pkg_v0
wrote examples/vocab_pkg_v0/target/root.oxbin (7 events, 4334 bytes)

$ ox check examples/vocab_pkg_v0 --codes
ok

To see OrphanKind actually fire, you need a consumer with a catalog that violates it — that is the next example, vocab_consumer_v0.

Honest caveats (what runs today)

• This package declares no pub query and no individuals; it is pure vocabulary. Its value is realized at a consumer’s ox check — vocab_pkg_v0 alone has nothing for the check to fire on.

This example and its consumer are driven through the real ox binary by a pipeline test (oxc-driver/tests/cli_pipeline.rs): the test pins that this package checks clean and that OrphanKind fires on the consumer’s catalog, so the cross-package check can’t drift from the language.

Source

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

//! `vocab_pkg_v0` — a small UFO-shaped vocabulary package, published for a
//! SEPARATE consumer package to depend on (RFD 0030; the two-package
//! vocabulary-authoring journey, GO-journey (a) of the v0.2.1 release gate).
//!
//! What this package ships, all on its `pub` surface, for a consumer to import
//! with `use vocab_pkg_v0::{ category, kind, characterization };`:
//!
//!   * Two introducer metatypes — `category` and `kind` — that a consumer uses
//!     as DECLARATION KEYWORDS for its own concepts (the §3.4 introducer gate
//!     resolves them across the dependency boundary, RFD 0030 D2).
//!   * A binary introducer metarel — `characterization`.
//!   * A handful of upper-ontology categories (`Endurant`, `Substantial`,
//!     `Detached`) the consumer specializes.
//!   * A catalog `check` rule — `OrphanKind` — over `meta`/`specializes`. This
//!     is the property that makes a vocabulary package REAL: the check is
//!     shipped by the vocabulary and FIRES on the CONSUMER's catalog at the
//!     consumer's `ox check` (a `kind` that specializes the vocabulary's
//!     `Detached` is flagged). It mirrors the working `NoDeprecatedVehicles`
//!     pattern in `examples/check_constraints`.

// ── Introducer metatypes (the consumer declares concepts with these) ──
// ANCHOR: introducers
pub metatype category = { };
pub metatype kind = { };

// ── A binary introducer metarel ──
pub metarel characterization<A, B>(a: A, b: B);
// ANCHOR_END: introducers
// ── Upper-ontology categories the consumer specializes ──
// ANCHOR: categories
pub category Endurant;
pub category Substantial <: Endurant;
// A `kind` specializing `Detached` is an ontological smell the vocabulary
// flags on every consumer catalog (see `OrphanKind`).
pub category Detached <: Endurant;
// ANCHOR_END: categories
// ── Vocabulary-shipped catalog check ──
//
// Catalog-level: every variable is `TypeRef`-sorted, so it discharges at
// `ox check`/`ox build` (RFD 0025 §7.6). It fires (Warning) for any `kind`
// in the consuming catalog that specializes `Detached`. The check is written
// HERE, in the vocabulary; it runs on the CONSUMER's `pub kind` declarations.
// ANCHOR: check
#[static]
pub check OrphanKind(k: TypeRef) :-
    meta(k) == kind,
    specializes(k, Detached) => Diagnostic {
        severity: Severity::Warning,
        code: "UFO::W001",
        message: "a `kind` specializes `Detached` — specialize `Substantial` instead"
    };
// ANCHOR_END: check