The Type System

Argon’s type system is unusual on three dimensions. It is ontology-aware: the metatype calculus runs alongside type-checking, so the compiler tracks not just whether a value is a Lease but whether Lease is a rigid sortal relator. It is refinement-equipped: types can be sharpened by predicate sub-types, and the compiler proves the refinement fragment decidable. It is tier-classified: the type-checker knows which decidability tier each rule sits in and refuses to sit you above the package’s cap.

The metatype machinery the type-checker reads is itself user-declarable. UFO’s metatypes — kind, subkind, role, phase, relator — are built from the substrate forms covered in Chapter 2.1; the type-checker has no special-case knowledge of them.

Most readers will get value from the surface — primitives, concept types, generics, refinements, subtype reasoning, and the ⊤ type — without reaching for the calculus underneath. This chapter sticks to the surface.

Primitive types

Ten primitives live in std::math and reach a module via explicit use:

Primitives appear as field types, parameter types, return types, and atom positions inside expressions:

use std::math::{Nat, Int, Real, String, Bool, Date, Money};

pub kind Person {
    id: String,
    age: Nat,
    height_cm: Real,
    is_active: Bool,
    born_on: Date,
}

pub compute total_owed(principal: Money, monthly_payment: Money, months: Nat) -> Money =
    principal - (monthly_payment * months)

There is no implicit prelude. A bare primitive name without a corresponding use produces OE0101 UnresolvedIdentifier with a hint pointing at the right use path.

Literals are written naturally: 42 is a Nat (or promotes to Int / Real per context), 3.14 is a Real, "hello" is a String, true and false are Bool, #2026-01-15# is a Date. Numeric promotion follows the chain Nat → Int → Real. Money literals are written as plain numerics; the compiler dispatches to the Money type when the context demands.

Concept types

Every pub kind X { … } (or pub subkind, pub role, pub relator, …) declaration introduces both a concept and a type. You can write a Lease-typed parameter, a Tenant-typed field, a [ResidentialLease]-typed return value.

pub compute primary_tenant(l: Lease) -> Tenant =
    l.tenant

The subtype graph the metatype declarations + concept hierarchy define is exactly the subtype graph the type-checker uses. So you can pass a ResidentialLease where a Lease is expected, but not the other way around without an explicit narrowing.

Collection types

Multi-valued field types we met in Chapter 2.3:

[Tenant]                 // any number, including zero
[Tenant; >= 1]           // at least one
[Field; == 4]            // exactly four
[Modifier; <= 3]         // at most three

The cardinality clause is a structural constraint on the collection’s count, not a value-comparison. The same operators (>=, ==, <=) appear elsewhere with value-comparison semantics; the type-checker keeps the two uses separated.

The Top type

When a value is genuinely heterogeneous — a comment annotation that can apply to anything, a metadata blob — type it as ⊤:

pub kind Annotation {
    target: ⊤,
    note: String,
}

The Unicode ⊤ is the canonical spelling; ASCII Top parses as an alias.

A value of type ⊤ accepts anything, but the compiler knows nothing about it: dispatch, refinement, and field-access on ⊤-typed values is restricted because there is no static structure to reach into. Use ⊤ sparingly; it is genuinely the right tool only for heterogeneous metadata.

Refinement types

A refinement type is a sub-type of an existing type whose instances satisfy a predicate over the metatype calculus. The dedicated item:

pub subkind RigidLease : Lease where {
    A.rigidity == rigid
}

Read in English: “RigidLease is the subtype of Lease whose metatype profile carries rigidity == rigid.” Because Lease is declared as a relator and relator carries { rigid, sortal } in its profile, every Lease is a RigidLease — the refinement is near-tautological for this base. The pattern becomes useful when the base type’s metatype profile is not pinned by the declaration alone.

The where { … } block is a comma-separated conjunction of refinement predicates. Today’s surface admits predicates over the meta-property calculus only — atoms of the form A.<axis> == <value>, with not available for negation:

$$predicate::=A.axis==value\mid \mathsf{not}A.axis==value$$

$$refinement::=\mathsf{pub}metatypeT:U\mathsf{where}\{{predicate}^{\ast }\}$$

Refinement bodies do not admit instance-level field comparisons (e.g., start_date < end_date) or arbitrary expressions. Instance-level invariants — “this lease’s start date precedes its end date” — ride on the assert items in Chapter 2.4, not on refinement types. The two mechanisms compose: a refinement narrows by metatype (A.rigidity == rigid); an assert narrows by instance value.

Three things make refinements useful:

1. The refinement fragment is decidable in PTIME. With respect to the size of the concept hierarchy and axis count, deciding membership in a refinement subtype is a polynomial-time procedure. ox check mechanically determines TBox-level refinement membership — given a concept declared pub subkind T : U where { … }, the compiler decides whether the refined type is satisfiable and how it sits in the subtype lattice — without invoking the reasoner.

   Status note: ABox-level refinement classification. Determining whether a specific individual (let l: Lease = { … }) actually inhabits a refinement subkind at evaluation time — i.e. assert l: ValidLease or assert ValidLease(l) against an l declared at the base type — is on the roadmap. Today the runtime classifies individuals by their declared concept and the saturation graph, but it does not yet evaluate refinement-predicate membership against an asserted individual; expect refinement-membership tests to mark #[unproven] until the classifier extends to ABox.

2. You can layer refinements. A refinement of a refinement composes by conjunction of axis-predicates.

3. Three-valued semantics ($K3$). Membership uses Kleene’s strong three-valued logic ($K3$, Kleene 1952) under the open-world assumption with the Pietz-Rivieccio “Exactly True” designation (Pietz & Rivieccio 2013): only $\mathsf{IS}$ on every conjunct admits membership; $\mathsf{CAN}$ leaves membership indeterminate; $\mathsf{NOT}$ rejects. The “Exactly True” framing — only $\mathsf{IS}$ counts as success — is the formal anchor for the fail-closed convention. Under closed-world assumption, $\mathsf{CAN}$ collapses to $\mathsf{NOT}$. That $\mathsf{CAN}$ at fixpoint completion really is genuine indeterminacy (no monotone extension of the input pins it to $\mathsf{IS}$ or $\mathsf{NOT}$) is one of the principal results stated in Chapter 5.1. Cross-standpoint federated queries lift to the four-valued $\mathsf{FDE}$ extension (Belnap 1977 / Dunn 1976) where source-level disagreement surfaces as $\mathsf{BOTH}$; per-standpoint refinement membership stays in $K3$. The full algebraic substrate is Approximation Fixpoint Theory (Denecker-Marek-Truszczynski 2000).

Variants: _catalog/concept-where-clause/{minimal,composition-with-derive,boolean-conjunction,tier-aware,negative-unsatisfiable}/. The boolean-conjunction/ workspace shows the multi-axis conjunction shape (A.rigidity == rigid, A.sortality == sortal); the tier-aware/ workspace caps the refinement to tier:closure via max_tier; the negative-unsatisfiable/ workspace declares a refinement whose body conjoins mutually-exclusive axis values — a tripwire for the post-elaboration refinement pass once the ABox classifier lands (Status note above).

A worked excerpt from _catalog/concept-where-clause/boolean-conjunction/src/prelude.ar:

// A rigid, sortal concept that also provides its own identity.
// The refinement reads three axes from the meta-property calculus
// and demands IS for each.
pub subkind IdentityProvider <: Concept where {
    A.rigidity == rigid,
    A.sortality == sortal,
    A.identity_provision == provides
}

// A field typed by this refinement only admits instances whose
// elaborated meta-property profile satisfies all three axes.
pub kind Registry {
    primary: IdentityProvider,
    aliases: [IdentityProvider; >= 0],
}

The body is a conjunction over the meta-property calculus axes from Chapter 5.1, not over instance fields. The compiler proves the fragment decidable in PTIME with respect to the concept hierarchy and axis count; the tier-aware/ variant tightens this further with max_tier: closure.

Layered refinements

pub subkind SortalLease : Lease where { A.sortality == sortal }
pub subkind RigidSortalLease : SortalLease where { A.rigidity == rigid }

RigidSortalLease is a refinement of a refinement. The compiler composes the predicates: a RigidSortalLease is a Lease whose meta-property profile satisfies both axis predicates.

Why metatype-axis-only

A refinement-type body that admitted arbitrary expressions over instance fields would be undecidable in general — equality on String and inequality on Decimal quickly take you out of any tractable fragment. Argon admits only the meta-property calculus’s three-valued state in the body precisely so the decidability proof goes through. Future cuts of the language may extend the fragment with carefully-chosen value predicates (A.rigidity == rigid plus f.size < 100, where f is a finite-domain field) — see Appendix D for the trajectory.

Narrowing and occurrence typing

Once a value is narrowed to a refinement type, subsequent uses see the narrower type. Argon’s occurrence typing is sound: a narrowing introduced at one point in a rule body remains valid for the rest of the body, and the narrowing survives composition with monotone rule application.

The CWA/OWA interaction is well-behaved as well: a narrowing established in a CWA context survives transition into an OWA context, because the narrowing is monotone in the information ordering, so adding open-world facts only strengthens it.

Subtype reasoning

The compiler’s subtype lattice is the closure of the supertype declarations across all visible packages. A few mechanics:

• A : B makes A a direct subtype of B. All of B’s fields are inherited; subtype-typed values are usable wherever B-typed values are expected.
• Multiple supertypes are admitted. A : B, C makes A a direct subtype of both. The compiler enforces field-name uniqueness across the closure and reports a diagnostic if B and C share a field name with different types.
• Refinements participate. pub subkind A : B where { p } makes A a refinement subtype of B; an A value can be used where a B is expected, but the reverse requires a refinement check.

The subtype operator is a primitive relation in the language core. The notation <: is the primary form; specializes is its keyword spelling; ⊑ is accepted as a typeset alternate:

pub derive AnyLease(l: ⊤) :-
    l <: Lease

: (instantiates) and <: (specializes) are first-class atoms in rule bodies, queries, and assertions. They are not user-declared pub rels — the type system builds on them.

Type-checking the running example

The lease tutorial accumulates refinement at this point. Add src/types.ar:

Refinements narrow by metatype, not by instance value — that constraint is what makes the membership decision tractable. Instance-level invariants (“this lease’s start date precedes its end date”) ride on assert items per Chapter 2.4. Here we use both: a refinement type that narrows by a meta-property axis, and an assert that gates instance-level admission.

use lease::*

// Refinement narrows by axis-predicate. The compiler composes the
// `where {...}` body against each candidate type's meta-property
// profile and decides membership without invoking the reasoner.
pub subkind RigidLease : Lease where { A.rigidity == rigid }

// `ValidLease` narrows by metatype as well — it's a `RigidLease` (so
// rigid) that's additionally sortal. Both predicates compose by
// conjunction over the axes declared in `metatypes.ar`.
pub subkind ValidLease : RigidLease where { A.sortality == sortal }

// Instance-level invariants live on `assert`, not on refinement bodies.
// The gate that checks `start_date < end_date` for each instance is an
// `assert` rule, decoupled from the type-system narrowing above.
assert valid_lease_dates(l: ValidLease) :- l.start_date < l.end_date
assert valid_lease_rent(l: ValidLease) :- l.monthly_rent > 0

And update prelude.ar:

pub use metatypes::*
pub use party::*
pub use lease::*
pub use rules::*
pub use queries::*
pub use computes::*
pub use mutations::*
pub use types::*

Then:

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.13s

ValidLease is now a type other items can reach for. A query that returns ValidLeases is well-typed:

pub query valid_active_leases() -> [ValidLease] :-
    ?l: ValidLease,
    ActiveLease(?l)
    => ?l

The compiler verifies at type-check time that every result row satisfies the ValidLease predicate. Bad data does not survive ox check.

Typed-domain metaxis values

A metaxis declaration may bind to a typed value space rather than a finite enum:

pub metaxis order : Nat for type
pub metaxis weight : Real for type where { _ > 0 }

metaxis <Name> : <Type> for <kind> admits values of the named primitive type. The optional where { _ <pred> } clause refines the admitted value-domain; the underscore _ is the candidate-value placeholder. A literal that fails type-check against the axis’s declared value_type emits OE0603 MetaxisValueTypeMismatch; a literal that satisfies the type but fails the refinement predicate emits OE0606 MetaxisRefinementViolation.

Typed-axis values flow into metatype declarations:

pub metatype kind = { rigid, sortal, provides, order = 1 }
pub metatype higher_order_type = { rigid, sortal, provides, order = 2 }

This is the foundation for multi-level theory: kind Person carries order = 1; higher_order_type Species carries order = 2; vocabulary-defined constraint rules over order enforce MLT axioms (specialization preserves order; instantiation crosses order by exactly one).

Reflection: meta() and std::meta

The compiler exposes two reflection surfaces over the type lattice. Both are usable in any rule body, query, assertion, or constraint. Both are pure: they evaluate at elaboration time against the resolved concept graph, no kernel call required.

The meta() intrinsic

meta(X) returns X’s metatype as a value. It is a compiler intrinsic, not a std::meta predicate. The argument is either a concept name or a bound variable.

pub kind Person {}
pub kind Employee : Person {}

// Test against a known metatype keyword
pub derive is_a_kind(c: Person) :- meta(c) == kind

// Explicit subject — the concept name itself
pub derive person_is_kind() :- meta(Person) == kind

meta() is part of the language substrate; no use declaration is required to call it. (use std::meta::* is for the seven reflection predicates covered below — a separate surface.)

The argument must be ground at rule-evaluation time. A free variable that no preceding atom binds emits OE0212 MetaArgumentNotGround:

// Compile error: ?z is unbound when meta() runs.
pub derive r(c: Person) :- meta(?z) == kind

Negation composes: not meta(c) == role is well-formed. The :: sugar form (Person :: kind to test meta(Person) == kind) lowers to the same atom. Tests Chapter 3.3 covers the testing-time idioms.

std::meta — universal reflection predicates

std::meta::* exposes seven typed-domain reflection predicates over the concept graph. They are universal: ontology-neutral, available without importing any vocabulary package, and structurally classified at tier:structural so they cost nothing in the decidability budget.

use std::meta::*

Examples that compile against std::meta::* alone:

use std::meta::*
use std::math::*

pub kind Person { name: String, age: Nat }
pub kind Employee : Person {}
pub kind Manager : Employee {}

// Walk the supertype lattice.
pub derive direct_super(c: Person, s: Person) :- supers(c, s)
pub derive any_ancestor(c: Person, a: Person) :- ancestors(c, a)

// Surface field names and the owning module.
pub derive has_field(c: Person, f: String) :- fields(c, f)
pub derive in_module(c: Person, m: String) :- module(c, m)

// Bind the metatype keyword as a string.
pub derive metatype_of(c: Person, m: String) :- metatype(c, m)

When to use which

meta() is for asking “what metatype is this?” — a single test against a keyword. std::meta::* is for walking the structure: every supertype, every field, every ancestor of every concept. Both compose with the rest of the rule grammar; neither carries foundational-ontology opinions. Vocabulary packages layer their own classifications on top — is_kind, is_rigid, is_relator — by composing these primitives.

std::meta and multi-level theory

std::meta::ancestors plus the order : Nat for type typed-axis from the previous section give you the substrate for multi-level theory enforcement:

pub metaxis order : Nat for type
pub metatype kind = { rigid, sortal, provides, order = 1 }
pub metatype higher_order_type = { rigid, sortal, provides, order = 2 }

// MLT axiom (one form): specialization preserves order.
// A vocabulary package writes the structural rule against std::meta:
//   ancestors(X, A), meta(X) == M_X, meta(A) == M_A
//   => order(M_X) == order(M_A)

The compiler does not bake this rule in; it is a vocabulary-level constraint that consumes the universal reflection surface. That is the design intent — Argon ships the substrate, vocabulary packages contribute the discipline.

Decorators and the recognizer

Decorators are user-defined annotations whose semantics lower to logical formulas. A vocabulary declares a decorator with an explicit body:

pub decorator transitive(r: rel) on rel = {
    semantics: forall x y z. r(x, y) and r(y, z) -> r(x, z)
}

The compiler pattern-matches lowered decorator bodies against a closed set of recognized shapes (Transitive, Symmetric, Asymmetric, Reflexive, Irreflexive, Functional, InverseFunctional, QualifiedCardinality, DisjointClasses, CoveringClasses). A recognized rule gets fast-path treatment in the reasoner — enable_transitive_closure_for(r) for Transitive, and so on — and inhabits the structural tier even when the body’s syntactic form is FOL. Six normalization passes (alpha-rename, flatten-associative, push-negations-inward, implications-to-disjunctions, canonicalize-equality, sort-conjuncts) ensure equivalent formulas with different syntactic surfaces match the same canonical shape.

Decorator authors may pre-tag a body with lowers_to: <shape> for explicit fast-path declaration; the recognizer verifies the body matches the named shape and emits OE0232 RecognizedShapeMismatch on divergence. Bodies that don’t match any recognized shape fall through to generic Datalog evaluation — this is a normal outcome, not an error.

Tier classification (a brief look)

Every type-related construct is also classified at one of seven decidability tiers, the same ladder we met in Chapter 2.4. Refinement predicates that compose tier:structural atoms classify at tier:structural; refinements that include aggregates classify higher. A #dec(<tier>) directive at module / block / declaration scope binds an ambient ceiling; a refinement whose effective tier exceeds the ceiling produces OE0604 TierViolation.

A rule’s effective tier is min(syntactic_tier, recognized_tier). A forall x y z. r(x,y) ∧ r(y,z) → r(x,z) body is syntactically tier:fol, but the recognizer matches it as Transitive and the effective tier collapses to tier:closure — the rule passes a stricter ceiling that a non-recognized FOL body would not.

You will rarely see the tier classification surface unless you reach above tier:recursive. When you do, the compiler tells you, by name, which atom pushed the classification up. The InfoView panel in the editor extension (Chapter 4.3) shows the tier of any symbol on hover.

Edge cases worth knowing

• Refinements cannot be cyclic. pub subkind A : B where { p }, pub subkind B : A where { q } — the compiler rejects this at elaboration.
• ⊤ does not absorb subtypes. Lease is a subtype of ⊤, but a ⊤-typed binding does not implicitly narrow to Lease when used; you need an explicit type test.
• Primitive types are not concept types. You cannot declare pub kind Customer : Int { ... }. Concepts subtype other concepts; primitives are leaves of the type lattice.
• Generics have a future. Argon has the syntactic surface for generic parameters (<T: ordered>), but most of the running example does not need them. They land in detail in Part 5.

Putting it together

The type system gives you:

• A small set of primitives.
• A subtype lattice generated from concept declarations, refined per-package by visibility.
• Cardinality-constrained collection types.
• Predicate-subtypes via refinement, with mechanical decidability.
• A graded decidability classification that applies uniformly to types and rules.

The lease tutorial uses primitives, concept types, refinement types, and subtype reasoning. It does not yet use generics or modal-typed bindings; those wait for Part 5.

Summary

Primitives, concept types, collections, refinements, the Top type, and subtype reasoning. The refinement fragment is decidable; the subtype lattice is the closure of declarations; tier classification runs alongside type-checking. The lease tutorial now has refinement types that catch bad data at ox check time. Part 2 is complete.