Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Meta-calculus atom

Three declarations: metaxis, metatype, metarel. They make the language ontology-neutral by letting packages declare the concept-introducing keywords.

metaxis

metaxis-decl ::= 'metaxis' Ident 'for' target metaxis-body? ';'
target       ::= 'metatype' | 'metarel' | 'individual' | 'macro' | '[' target (',' …)* ']'
metaxis-body ::= '{' enum-body '}' | '=' TypeExpr ('where' refinement)?
enum-body    ::= Ident (',' Ident)*          // unordered
              |  Ident ('<' Ident)+          // totally ordered (chain)

pub metaxis rigidity for metatype { anti_rigid < semi_rigid < rigid };
pub metaxis sortality for metatype { sortal, non_sortal };
pub metaxis identity_provision for metatype { provides, inherits };
pub metaxis dependency_kind for metarel { existential, contingent, none };
pub metaxis ordinality for metatype = Nat;
pub metaxis weight for metatype = Real where _ > 0.0;

A metaxis characterizes the meta level: its values are assigned to metatypes (for metatype) and metarels (for metarel), never to a concrete type directly. The targets name the meta-sort the axis applies to — metatype for the concept tier, metarel for the relation tier — not the type / rel concept introducers. (A future for <DeclaredType> target — a type-specific refinement axis bound to one declared type — is left open by the model but not yet specified.)

Cross-axis constraints are check rules at module level, never embedded in the body.

metatype

metatype-decl ::= 'abstract'? 'fixed'? 'metatype' Ident '=' '{' axis-assign (',' …)* ','? '}' ';'
axis-assign   ::= Ident ':' value
value         ::= Ident | literal

A metatype body is a record of axis values, so each binding reads like a struct field — a single : separates the axis from its value.

pub abstract fixed metatype category = { rigidity: rigid,      sortality: non_sortal };
pub fixed metatype kind     = { rigidity: rigid,      sortality: sortal,     identity_provision: provides };
pub fixed metatype subkind  = { rigidity: rigid,      sortality: sortal,     identity_provision: inherits };
pub metatype role           = { rigidity: anti_rigid, sortality: sortal };
pub metatype phase          = { rigidity: anti_rigid, sortality: sortal };

A metatype name in scope is contextually a concept-introducing keyword: pub kind Person { … }.

Axes are pure user vocabulary. The axis bindings in a metatype body are the declaring package’s own ontology — validated against the declared metaxis domains (RFD 0027 D2), persisted on the wire, and queryable — but the compiler never reads an axis name. No axis assignment changes elaboration, coverage, or mutation semantics; importing a vocabulary cannot alter substrate behavior because its author happened to name an axis rigidity. The metatypes shown above (kind, subkind, role, phase, category) are example declarations of the kind a third-party UFO vocabulary package would ship — they are not language atoms, and no UFO vocabulary ships with Argon or its stdlib. Other vocabularies (BFO, GFO, custom) define their own metatypes with their own axis assignments; the language treats all of them uniformly.

Substrate behavior comes from two ontology-neutral modifiers (RFD 0027 D6) — the operational shadows of the classic meta-property distinctions, with PL precedents rather than ontological commitments:

  • abstract — no direct instances. Every type the metatype introduces refuses construction (insert T { … }), direct classification (insert iof(x, T)), and seeded assertion (positive pub fact T(x)) with OE0233; subtypes are unaffected, and pub not_fact T(x) (refuting membership) stays legal. Abstract types are exempt from trait impl-coverage obligations (Resolution) — they structure the hierarchy, and every individual is classified through some non-abstract subtype. abstract may also be declared per-type on a concept declaration (pub abstract type Vehicle { … }, the UML/PL convention); a type introduced by an abstract metatype is abstract with no override semantics.
  • fixed — classification decided at construction. insert iof / delete iof against a type introduced by a fixed metatype refuses with OE0234 (mutate); construction itself is unaffected. Dynamic classification is the default — the restriction is the opt-in, the same posture as check. Fixed classification is what makes static modal discharge sound (Modal operators); the Kripke-semantics justification (rigid designation = fixed classification) is mechanized in Argon.Reasoning.StaticDischarge and the mutation-gate theorem in Argon.Runtime.ModifierGates.

A vocabulary author writes both layers together — pub abstract fixed metatype category = { sortality: non_sortal, rigidity: rigid }; — the modifiers carry the behavior, the bindings carry the package’s ontology. Misplaced modifiers (fixed on a concept declaration, either modifier on a struct/enum/relation, duplicates) are refused at parse with OE0008.

metarel

metarel-decl  ::= 'metarel' Ident '(' endpoint-list ')' metarel-body? ';'
endpoint-list ::= endpoint (',' endpoint)*
endpoint      ::= (Ident ':')? Ident          // optional name, then metatype name
metarel-body  ::= '{' axis-assign (',' …)* ','? '}'

pub metarel mediation(mediator: relator, mediated: kind) {
    dependency_kind: existential,
};

pub metarel material(kind, kind) { dependency_kind: contingent };
pub metarel three_way_dependence(kind, kind, kind);

The metarel name is itself a contextual relation-introducing keyword (Relations): pub mediation Involves(m: Marriage, p: Person) declares a relation classified by mediation. The elaborator verifies the relation’s endpoint metatypes match the metarel’s positions. (An alternative decorator-attachment spelling — #[mediation] on a generic relation declaration — was sketched in earlier drafts but is not built: user-declared metarel names are not compiler directives, so the attribute form refuses at the directive registry, OE0705. The introducer form above is the supported surface.)

The stdlib ships a generic metarel for ontology-uncommitted use:

// in std::core — the generic metarel (opt-in via `use std::core::rel`,
// RFD 0038), shown as it is declared inside the stdlib (not a user file).
pub metarel rel<E1: metatype, E2: metatype>(E1, E2);

rel accepts any endpoint metatypes (inferred from the relation’s parameter types). After use std::core::rel;, the modeler can write pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*] for relations without committing to a specific ontological vocabulary. Vocabulary packages may re-export std::core::rel in their prelude as a convenience.

Reflection

Reflective sorts: Entity, TypeRef, Metatype

The substrate exposes three reflective sorts and a fixed lattice over them:

Metatype  <:  TypeRef  <:  Entity
  • Entity is the universal sort of all entities — individuals and type-references alike. A type is an entity (so it can itself be classified by a higher-order type; see Higher-order modeling). Entity <: Top.
  • TypeRef is the sort whose values are references to declared types (concept / construct / relation / metatype) — a handle into the closed, nominal catalog of declarations, in the manner of OWL-2 punning, Java’s Class<?>, or Haskell’s TypeRep. TypeRef is unsealed, so Metatype remains the only sealed primitive. Because TypeRef denotes a closed catalog of already-declared types rather than an impredicative universe, there is no Type : Type: the reflective layer is a predicative, stratified universe of codes, not a self-membership hierarchy.
  • Metatype is the sealed primitive that classifies all metatypes (kind, role, phase, …, and Metatype itself). Since Metatype <: TypeRef, every metatype name in scope is also a TypeRef value.

Type-as-value. A declared type’s name in value position is a TypeRef value — Person, kind, and Metatype are all TypeRef values, distinguished from the type Person by syntactic position. This is the substrate’s type-as-value facility: a field or parameter may be typed TypeRef (or the bounded TypeRef<C>; see Built-in type forms) and carry a reference to a declared type. The runtime carrier is the declared-symbol reference Value::Name; on the wire, a TypeRef/Entity argument is a qualified class-path ("pkg::mod::Type", or {"$typeRef": "pkg::mod::Type"}) resolved to the declared type’s identity — entity refs (#i…) are not accepted for these parameters. See RFD 0023.

Reflection intrinsics

The substrate provides five reflection intrinsics — meta, iof, specializes, extent, and implements (RFD 0026; signature implements(t: TypeRef, tr: TraitRef) -> Bool, materialized as the catalog-closed $implements relation with supertrait closure and <: upward target-coverage, Reflective conformance: TraitRef and implements) — admitted in any rule body without a use declaration. The first three have syntactic-sugar atom forms in Rule-atom grammar; extent and implements are called directly. For meta/iof/specializes/extent, each type-position argument is a TypeRef value — a literal type-reference or a bound variable of sort TypeRef — which is precisely what makes the intrinsics first-class, value-polymorphic predicates: library code can pass, count over, or quantify across type-values (see Higher-order modeling and the unprivileged mlt package, realizing the spec/research/RP-003-mlt-as-library.md GAP-1). implements differs in two deliberate ways: its second argument is TraitRef-sorted (traits are not types and stay off the <: lattice), and because $implements is a finite catalog-closed relation, both of its positions may be free — enumeration is the intended use (Reflective conformance: TraitRef and implements).

meta has the signature meta(x: Entity) -> TypeRef: it returns the immediate classifier of x — its <:-minimal declared type — as a TypeRef value. Under multiple classification (an entity instantiating incomparable types, e.g. a UFO individual that is both a Person and a Customer with neither <: the other), meta(x) is multi-valued: it yields one TypeRef per <:-minimal classifier. (It is a Metatype value only when x is itself a type — e.g. meta(kind) == Metatype — since Metatype <: TypeRef.) x :: T is syntactic sugar for meta(x) == T.

meta() applies only to ontologically-classified concepts (those declared under a vocabulary or stdlib metatype). Calling meta() on a struct/enum-declared value is a category error — language-level data carries no metatype — and emits a diagnostic at elaboration.

Worked examples (each right-hand side is a TypeRef value): meta(Person) == type when Person is pub type Person { … } under std::core::type; meta(Person) == kind when Person is pub kind Person { … } under an imported (or locally-declared) UFO vocabulary; meta(kind) == Metatype; meta(Metatype) == Metatype (sealed self-instantiation). Metatype is the sealed primitive that classifies all metatypes; it is special-cased by the compiler. The classifier kind and the primitive Metatype are TypeRef values because Metatype <: TypeRef.

iof has the signature iof(x: Entity, t: TypeRef) -> Bool. The rule-atom form x : T (Rule-atom grammar type test) is syntactic sugar for iof(x, T). Because the type-position argument t is a TypeRef value, iof is a first-class predicate: it can be passed as a relation argument, counted over, or quantified across — for example, library code building higher-order theories (the unprivileged mlt package, Higher-order modeling, Stdlib (selected)) treats iof as a first-class predicate.

iof is read at two tiers. The individual/ABox tier is membership of an order-0 entity in a type, asserted by a pub fact T(x) ground atom. The catalog/type tier is a declared type×type membership — a type X declared an instance of a higher-order type T via the : T instantiation clause (Vocabulary concepts and the generic type metatype, pub kind USD : Currency). The subject x is itself a TypeRef value (a type used as a higher-order individual), so the same iof relation carries both; which tier a read sits in is decided by whether the subject is an individual or a type, not by a separate relation. The catalog tier is declaration-derived (never an ABox event), so a #[static] check (Rule atom — fn, derive, query, mutate, check) may read it and extent projects it at the type level.

specializes has the signature specializes(t1: TypeRef, t2: TypeRef) -> Bool. The rule-atom form t1 <: t2 (Rule-atom grammar specialization) is syntactic sugar for specializes(t1, t2). Same first-class, value-polymorphic motivation as iof — both arguments are TypeRef values.

iof and specializes apply only to ontologically-classified concepts. Calling them on struct/enum-declared values is a category error and emits a diagnostic at elaboration, parallel to the meta() discipline.

extent has the signature extent(t: TypeRef) -> Set<Entity> (t is a TypeRef value naming the type whose extent is enumerated). Returns the set of entities x such that iof(x, t) holds at the current state. Both function-style (extent(EmperorPenguin)) and UFCS method-style (EmperorPenguin.extent()) are admitted; the method form lowers to the function form.

Worked examples: extent(Person) returns all order-0 entities classified as Person; extent(BirdSpecies) returns all order-1 kinds that are iof-instances of BirdSpecies (e.g., {EmperorPenguin, GoldenEagle, Grouse, Pheasant}); extent(Metatype) returns the set of all metatypes in scope. extent() on a struct/enum-declared value is a category error, parallel to the other reflection intrinsics.

Relation-signature reflection (rel / arm). Two further reflection predicates reflect over declared relations (the relation tier of the reflective catalog, RFD 0031 D2), so a vocabulary package can write relation-level compile-time constraints:

  • rel(r: TypeRef, m: TypeRef) -> Bool — r is a declared relation and m its classifying metarel. One catalog row per declared relation.
  • arm(r: TypeRef, pos: Int, t: TypeRef) -> Bool — for relation r, pos is a 0-based arm position and t the endpoint type declared there. One row per (relation, position).

Both are catalog-closed (one row per declared relation / arm, never the ABox), so — like $implements — every position may be free and enumeration is the intended use. rel/arm are abstract reflection primitives, never ontological vocabulary; the metarel/type names a check matches on are user vocabulary, compared by catalog identity. A package-shipped check quantifies over the catalog to enforce an endpoint discipline:

// "an endpoint of a `characterization` relation must be aspect-sorted"
pub check BadCharacterization(r: TypeRef, t: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == kind
    => Diagnostic { severity: Severity::Warning, code: "UFO::W010", message: "..." };

(The metarel introducer itself also verifies its endpoint metatypes at elaboration — metarel, OE0631; $rel/$arm let a package extend or audit that discipline declaratively.)

Lowering. A declared type in value position lowers to the IR primitive Term::TypeRef. iof(x,t) (and x : t) lowers to the Core-IR typeTest atom and meta(x) == T (and x :: T) to the metaEq atom (spec/lean/Argon/CoreIR/RuleIR.lean); specializes(t1,t2)/t1 <: t2 has no dedicated atom and lowers to a reserved-head predicate, and extent(t) to an application of the extent builtin. Beneath Core IR, the reasoner evaluates these against catalog relations it materializes from the declarations — $iof (entity × type, closed under supertypes; this carries both tiers — the individual-tier rows from pub fact T(x) assertions and the catalog-tier type×type rows from each : T instantiation clause, the latter closed upward over the target type’s <: ancestors), $specializes (type × type: the reflexive-transitive specialization graph plus the built-in Metatype <: TypeRef <: Entity edges and the sibling TraitRef <: Entity edge), $meta (entity × its <:-minimal classifiers), $implements (type × trait, supertrait closure and <: upward target-coverage folded in — Reflective conformance: TraitRef and implements), and the relation-tier $rel (relation × metarel) / $arm (relation × position × endpoint type) — RFD 0031 D2. OE0212 MetaArgUnbound is the reserved refusal for an unbound argument of the four type-position intrinsics; implements is exempt by design — both of its positions enumerate over the catalog-closed $implements relation, which is the intended use.

Typical use: deriving cross-level properties of higher-order types from their instances.

#[categorizes(Bird)]
pub type BirdSpecies {
    numberOfLivingInstances: Int = extent(self).count(),
    averageHeight: Decimal = extent(self).map(|b| b.height).avg(),
}

The = expr field-default form shown above refuses with OE0237 FieldDefaultUnsupported (see struct and enum — language built-ins (data declarations) for the full disposition). Express cross-level derivations such as EmperorPenguin.numberOfLivingInstances with the from-navigation field form ([RFD 0005, struct and enum field navigation](constructs/struct-and-enum.md)) or an explicit derive/query rule (Rule atom — fn, derive, query, mutate, check).