A legal deontic vocabulary package

Area: Vocabulary & packages Teaches: how to publish a vocabulary — a package whose pub surface is upper-ontology concepts, introducer metatypes, an endpoint-constrained metarel, and catalog checks that a consumer gets for free when it imports the package. Prerequisites: machine parts (metarel endpoints, meta, specializes), and the meta-calculus. Run: ox build examples/legal_vocab_v0 && ox check examples/legal_vocab_v0 --codes

Ontological vocabulary is never built into Argon and never in std — a modeler ships it as an ordinary package and a consumer depends on it by path. This is the deontic counterpart of vocab_pkg_v0: a UFO-L modeler ships the deontic concepts, the directed-obligation relation, and the audits a legal modeler inherits. Its consumer is legal_catalog_v0.

What to read in root.ar

An axis orders the modalities. deontic_force is pure user vocabulary — the compiler never reads a force name — ordering the three modalities by the strength of the constraint each imposes:

pub metaxis deontic_force for metatype { permission < obligation < prohibition };

Introducer metatypes become the consumer’s declaration keywords. A consumer writes pub obligation PayRent <: … and the introducer gate resolves the keyword across the dependency boundary. Each binds its force on the axis:

pub metatype permission  = { deontic_force::permission,  legal_kind::norm };
pub metatype obligation  = { deontic_force::obligation,  legal_kind::norm };
pub metatype prohibition = { deontic_force::prohibition, legal_kind::norm };

The deontic relation constrains both endpoints. A directed obligation runs from a debtor to a creditor — both party-sorted, never a contract or a bare individual. The endpoint metatypes are verified at elaboration; a relation declared with this introducer whose endpoint is not party-sorted is refused (see legal_catalog_bad_v0):

pub metarel directed_obligation(debtor: party, creditor: party);

The vocabulary ships its own checks. Every variable is TypeRef-sorted, so each #[static] check discharges at the consumer’s ox check, reading meta(k) / specializes. OrphanObligationConcept flags a norm-tagged concept that anchors to nothing in the vocabulary:

#[static]
pub check OrphanObligationConcept(k: TypeRef) :-
    meta(k) == obligation,
    not specializes(k, TimedObligation)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "UFOL::W002",
        message:  "an `obligation` concept does not specialize `TimedObligation` — anchor it so its deadline discipline is inherited",
    };

Running it

The vocabulary itself checks clean — the checks fire on a consumer’s catalog, not on the vocabulary’s own declarations:

$ ox check examples/legal_vocab_v0 --codes
ok

The “free checks” property — that an imported check actually runs on the importing package — is demonstrated by the consumer legal_catalog_v0, where OrphanObligationConcept fires UFOL::W002 on the orphan norm concept.

This example is compiled in CI; the corpus auto-discovery parses and resolves it, and a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the package surface, so it 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.

//! `legal_vocab_v0` — a small UFO-L-shaped legal deontic vocabulary package,
//! published for a SEPARATE consumer (`legal_obligations_v0`) to depend on by
//! path (RFD 0030; the two-package vocabulary-authoring journey). It is the
//! deontic counterpart of `vocab_pkg_v0`: a vocabulary author (the
//! ArgUFO/UFO-L modeler) ships the upper-ontology deontic concepts, the
//! deontic relation, and the catalog checks a legal modeler gets for free.
//!
//! The deontic plane it ships, all on `pub`, for a consumer to import:
//!
//!   * A `deontic_force` **metaxis** — the modal force of a norm
//!     (`permission < obligation < prohibition`, ordered by strength of the
//!     constraint a norm places on the bearer). Pure user vocabulary; the
//!     compiler never reads a force NAME (the no-ambient-ontology rule —
//!     deontic vocabulary is NEVER built-in and never `std`).
//!
//!   * Three introducer **metatypes** the consumer uses as declaration
//!     keywords for its own norm concepts, each binding its force on the axis:
//!     `permission`, `obligation`, `prohibition`. A consumer writes
//!     `pub obligation PayRent <: …` and the §3.4 introducer gate resolves the
//!     keyword across the dependency boundary (RFD 0030 D2).
//!
//!   * A `party` introducer metatype — the legal subjects (debtor / creditor)
//!     a directed obligation runs between — and a `legal_relator` metatype for
//!     the contract that bundles the obligations (UFO: a contract is a
//!     *relator* truthmaking the parties' obligations).
//!
//!   * A binary introducer **metarel** `directed_obligation<debtor, creditor>`
//!     whose BOTH endpoints are metatype-constrained to be `party`-sorted
//!     (#311, RFD 0031 D1): a directed obligation runs from one legal party to
//!     another, never to a contract or a bare individual. The sibling
//!     `legal_catalog_bad_v0` fixture supplies a wrong-sorted endpoint and is
//!     refused OE0631 at elaboration.
//!
//!   * Two package-shipped catalog **checks** — `ProhibitionIsNotAnObligation`
//!     and `OrphanObligationConcept` — that fire on the CONSUMER's catalog at
//!     the consumer's `ox check` (the thing that makes a vocabulary REAL:
//!     imported checks run). They mirror the working `OrphanKind` pattern in
//!     `examples/vocab_pkg_v0`.

// ── Axes (pure user vocabulary; the compiler never reads a force name) ──
//
// `deontic_force` orders the three modalities by the strength of the
// constraint the norm imposes: a permission leaves the bearer free, an
// obligation compels an act, a prohibition forbids one.
pub metaxis deontic_force for metatype { permission < obligation < prohibition };

// `legal_kind` separates the two structural roles a legal concept can play:
// a `norm` is a deontic statement; a `subject` is a party or a relator that
// norms range over. Used by the shipped checks to tell norms from subjects.
pub metaxis legal_kind for metatype { subject, norm };

// ── Introducer metatypes: the keywords this vocabulary ships ──
//
// The three deontic modalities — each binds its force on `deontic_force` and
// is tagged `norm` on `legal_kind`. A consumer declares its norm concepts
// with these as keywords (`pub obligation PayRent <: …`).
pub metatype permission = { deontic_force: permission, legal_kind: norm };
pub metatype obligation = { deontic_force: obligation, legal_kind: norm };
pub metatype prohibition = { deontic_force: prohibition, legal_kind: norm };

// The legal subjects. A `party` is a legal person (debtor / creditor); a
// `legal_relator` is the contract that bundles and truthmakes the obligations
// (UFO: contracts are relators). Both are `subject`s, not norms.
pub metatype party = { legal_kind: subject };
pub metatype legal_relator = { legal_kind: subject };

// ── The deontic relation ──
//
// A binary introducer metarel whose BOTH endpoints are `party`-sorted: a
// directed obligation runs FROM a debtor TO a creditor (UFO-L's directed
// obligation between two legal subjects). The endpoint metatypes are verified
// at elaboration (#311) — a relation declared with this introducer whose
// endpoint type is not `party`-sorted is refused OE0631.
pub metarel directed_obligation(debtor: party, creditor: party);

// ── Upper-ontology concepts the consumer specializes ──
//
// `LegalSubject` is the root `party` the consumer's `Person` / `Company`
// specialize; `Contract` is the root `legal_relator`. Shipping these lets the
// consumer's parties and contracts inherit the vocabulary's structural roles.
pub party LegalSubject;
pub legal_relator Contract;

// ── Vocabulary-shipped catalog checks ──
//
// Catalog-level: every variable is `TypeRef`-sorted, so each discharges at
// `ox check` / `ox build` (RFD 0025 §7.6). They run on the CONSUMING catalog's
// concept declarations.
// A prohibition is a force category error if it specializes the deadline-
// bearing obligation root: a prohibition FORBIDS ("you must never X") — it does
// not OBLIGE a timed act, so it has no business inheriting an obligation's
// deadline. This check FIRES (Warning) for any concept the consumer declares
// with the `prohibition` keyword that ALSO specializes `TimedObligation`. It
// demonstrates a force-aware catalog audit reading `meta(k)`.
#[static]
pub check ProhibitionIsNotAnObligation(k: TypeRef) :-
    meta(k) == prohibition,
    specializes(k, TimedObligation) => Diagnostic {
        severity: Severity::Warning,
        code: "UFOL::W001",
        message: "a `prohibition` specializes a `TimedObligation` — a prohibition forbids, it does not oblige; declare it as a top-level `prohibition`"
    };

// Every concept declared with a deontic NORM keyword (`legal_kind::norm`) is
// expected to specialize one of the vocabulary's norm roots so its force is
// anchored. An orphan norm concept — `norm`-tagged but specializing nothing in
// this vocabulary — is flagged. This is the legal counterpart of
// `vocab_pkg_v0`'s `OrphanKind`.
#[static]
pub check OrphanObligationConcept(k: TypeRef) :-
    meta(k) == obligation,
    not specializes(k, TimedObligation) => Diagnostic {
        severity: Severity::Warning,
        code: "UFOL::W002",
        message: "an `obligation` concept does not specialize `TimedObligation` — anchor it so its deadline discipline is inherited"
    };

// The deadline-bearing obligation root the consumer's timed obligations
// specialize. Declared with this vocabulary's own `obligation` keyword; it
// carries the deadline field every directed, time-bounded obligation needs.
pub obligation TimedObligation {
    mut due: Date,
}