Higher-order modeling

Multi-level / higher-order theories live in ordinary first-party packages with zero compiler privilege — never in the language core and never in std. The substrate provides the primitives — iof (Reflection), <: (Vocabulary concepts and the generic type metatype), the meta-calculus (Meta-calculus atom), well-founded instantiation, stratified aggregates over the iof DAG (derive) — and theories layer on top. The substrate is deliberately neutral about which higher-order theory a model commits to, so none of them belongs in std (RFD 0043).

The mlt package’s ability to treat iof and specializes as first-class predicates — passing, counting over, and quantifying across type-values — rests on the substrate reflective sort TypeRef (Reflection), whose values are references to declared types; this realizes RP-003 GAP-1. The substrate TypeRef sort is the neutral handle layer and is distinct from any library construct built atop it: it is not an MLT* orderless Type term (whose powertype/order semantics live in that package) nor a vocabulary’s own Type_ concept (an ordinary declared type). TypeRef carries no order, potency, or categorization — those remain the theory packages’ concern.

Higher-order theories ship as unprivileged packages at tier:metaorder (Tier ladder), e.g.:

Each package provides:

• its metaxes (e.g., the mlt package declares pub metaxis order for metatype = Nat where { _ <= 16 }),
• its metarels (e.g., the mlt package declares pub metarel categorizes(higher: type, base: type)),
• the decorator forms as library #[procmacro]s (e.g., #[categorizes(Animal)] re-emits the decorated declaration and emits a re-checked MetaProperty on the categorizes metarel; #[order(2)] does the same on the order metaxis),
• derived level functions over the iof graph,
• check rules enforcing the theory’s axioms (e.g., the mlt package enforces Carvalho-Almeida S1–S5),
• the theory’s constraints as its own rules/checks over the neutral substrate — never compiler-reserved diagnostic codes; the substrate ships no theory-namespaced codes.

Intrinsic-by-default for higher-order types. When the mlt package’s cross-level decorators (#[categorizes], #[partitions], #[subordinate_to], #[power_type_of]) are applied to a type declaration, the type’s fields default to #[intrinsic] — every iof-instance must supply a value (field = value at kind level) or carry a from-navigation source (struct and enum — language built-ins (data declarations)). A field with neither emits OE1908 IntrinsicPropertyMissing against every iof-instance. Modelers opt a field out by declaring it T? (optional, yields None when absent). The field-default opt-out (field: Type = expr) refuses with OE0237 FieldDefaultUnsupported (see struct and enum — language built-ins (data declarations)). Parallel decorators in a potency, ml2, or user theory package may declare their own intrinsic-default rules.

A modeler picks a theory by listing its package in ox.toml and importing it: use mlt::*; brings MLT’s vocabulary into scope; a third-party vocabulary package (e.g. an externally-authored UFO package) may re-export mlt::* plus its own metatypes (kind, role, phase, …) on top.

The std::level::Stratified trait gives consumers a theory-agnostic level handle:

// in std::level
pub trait Stratified {
    type Level;
    fn level(self) -> Self::Level;
}

Each theory implements Stratified for its entities; consumers depend on the trait, not the theory.

See the stdlib reference (Stdlib (selected)) for full package documentation. Decidability tier metaorder (Tier ladder) admits unbounded multi-level / higher-order instantiation; theory packages may surface their own bounded variants (e.g., a package may cap MLT order to lower the module to a polynomial tier).

Prior versions of this specification embedded MLT directly in Higher-order modeling with built-in decorators and OE19xx diagnostic codes. That commitment is superseded; see spec/research/RP-003-mlt-as-library.md for the feasibility study and migration rationale.