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

RFD 0023 — Reflective TypeRef: type-as-value in the meta-calculus

  • State: committed
  • Opened: 2026-06-07
  • Decides: the substrate’s type-as-value facility — a reflective sort TypeRef whose values are references to declared types, the bounded form TypeRef<C>, the runtime/wire carrier, and the first-class (value-polymorphic) forms of the four reflection intrinsics (meta/iof/specializes/ extent). This is the realization of RP-003 GAP-1 (“expose the reflection predicates as first-class so library code can pass/count/quantify over type-values”). It is Lean-first: the foundation landed in spec/lean/Argon/CoreIR/Term.lean (Term.typeRef) and spec/lean/Argon/MetaCalculus/Reflect.lean (sorts, lattice, the iof/specializes/extent relation semantics) before the Rust layers.

This RFD records a settled design (see .local-staged discussion). It does not introduce any higher-order theory into the core: MLT / Potency / ML2 remain std::* libraries (RFD 0009, RP-003); TypeRef is the neutral substrate they build on.

Question

Ontological modeling stores references to types as values: actionType: TypeRef, roleType: TypeRef, relatorType: TypeRef (110+ sites in the sharpe-ontology overlay). Today such a field/param does not resolve (no TypeRef sort), and a mutation parameter that should accept a declared TBox class reference ("residential_lease::core::Lessor") is instead validated as an ABox entity reference (#i123) and rejected. Separately, RP-003 established that for any higher-order theory to be a library, the substrate must expose iof/specializes/extent/meta as first-class predicates over type-values (GAP-1), which the IR does not yet do (iof is a syntactic typeTest, meta compares against an Ident, specializes/extent have no IR at all).

What is a type-as-value in Argon — its sort, its bounded form, its runtime/wire representation, and the first-class form of the reflection intrinsics — without leaking any higher-order theory into the core?

Context

  • Meta-calculus (§4) already specifies the four reflection intrinsics and a 3-level tower (meta(Person)==kind, meta(kind)==Metatype, Metatype sealed/self-instantiating); RP-003 §10 (resolved) canonicalized the argument sorts as Entity (value-position) and type (type-position) and made the intrinsics substrate-scope (no use). The book uses these but the substrate never realized first-class, value-polymorphic forms — that is the gap.
  • Prior thinking pre-figures this and retires the central risk. The vault’s RP-001/D-132 MLT-parent-theory campaign already adjudicated Girard’s paradox: the reflective layer is a predicative, stratified universe of codes (hypothesis-2-type-theoretic/s2-MLT-mapping.md §9.4), not an impredicative Type:Type. A TypeRef value is a handle into the closed declared catalog (à la OWL-2 punning / Java Class<?> / Haskell TypeRep), so iof/extent are predicates over that catalog — no self-membership at a fixed level.
  • Carrier already exists. The runtime Value::Name(NameRef) (“a declared symbol reference”) is content- addressable (RFD 0001), bitemporal-safe, total-Ord (Z-set keys), and round-trips CBOR↔path-string — the legacy EntityRef::Concept / unified-EntityId idiom. No new Value variant is needed.
  • Overlay evidence. The overlay’s type-valued fields are consumed only by == equality today; the bounded need (“a reference to one of a set of declared subtypes of X”) shows up as the current enum workaround — i.e. exactly a bounded TypeRef<C>.

Decision

D1 — A reflective sort TypeRef

TypeRef is the sort whose values are references to declared types (concept / construct / relation / metatype). It is unsealed. The lattice:

Metatype  <:  TypeRef  <:  Entity

Entity is the universal sort of all entities (individuals + type-references); a type is an entity (so it can be classified by a higher-order type — MLT higher-order). Because TypeRef is unsealed, Metatype remains the only sealed primitive (preserving the redesign’s “Metatype is the only sealed primitive” commitment — this is not an amendment). Chosen name TypeRef (over core Type) avoids the four-way collision with Top, std::mlt::star::Type, UFO Type_, and a vocabulary’s own pub type Type, and avoids reopening the delexicalization that removed a Type keyword.

D2 — Bounded TypeRef<C> is a refinement, not a core type-former

TypeRef<C> ≝ { t: TypeRef where specializes(t, C) } (RFD 0017, where = primitive/asserted). TypeRef == TypeRef<Top>. Subtyping is covariant — TypeRef<A> <: TypeRef<B> iff A <: B — which follows from the refinement ({t|t<:A} ⊆ {t|t<:B}), so no new structural subtyping rule is added. Membership is three-valued under OWA (per RFD 0007): specializes(t,C) unknown ⇒ not a member (success requires definite-true). Powertype / order / categorization semantics stay in std::mlt — TypeRef<C> carries none of them.

D3 — Runtime/wire carrier: Value::Name(NameRef)

A TypeRef value is a NameRef handle to a declared type (no new Value variant). On the wire, the SDK sends a qualified class-path ("residential_lease::core::Lessor"); the runtime resolves it to the type’s NameRef. coerce_json_arg_for_type gains one arm for TypeRef-typed params: path → resolve → Value::Name, short-circuiting before the ABox entity-ref path. Equality (==) already works. The TS SDK (oxc-gen) adds a class-path wire shape + serializer branch distinct from the existing #i… / entity-ref path.

D4 — First-class, value-polymorphic reflection intrinsics (GAP-1)

The four intrinsics accept/produce TypeRef values (a type-position argument is a Term — a Term.typeRef literal or a bound variable of sort TypeRef), so library code can quantify/count over types:

meta(x: Entity)                  -> TypeRef      // immediate classifier; amends book §4's `-> Metatype`
iof(x: Entity, t: TypeRef)       -> Bool         // sugar:  x : T
specializes(t1: TypeRef, t2: TypeRef) -> Bool    // sugar:  t1 <: t2
extent(t: TypeRef)               -> Set<Entity>

IR lowering convention (matches the temporal-operator precedent of reserved-head predicates — no new AtomIR constructors, so the Admittance/tier proofs are untouched):

  • iof(x,t) → AtomIR.predicate ["iof"] [x, t]; specializes(t1,t2) → predicate ["specializes"] [t1, t2].
  • extent(t) → Term.app (var "extent") [t]; meta(x) → Term.metaCall x (returns a TypeRef value).
  • The closed/literal sugar x : T keeps AtomIR.typeTest; x :: T keeps AtomIR.metaEq (fast path). The reasoner evaluates the reserved-head reflection atoms against the catalog’s iof/specializes graph.

D5 — Lean is canonical; the foundation landed first

Term.typeRef : Path → Term (the type-as-value primitive, @[language_interface]) and MetaCalculus/Reflect.lean (the sorts; reflectiveLeq proven a preorder so Subtyping.subtypeOf decides Metatype<:TypeRef<:Entity; ReflectCatalog with specializes proven a preorder, iof, and extentOf with its characterization x ∈ extentOf u t ↔ x ∈ u ∧ iof x t). The reflective sort edges are folded into the catalog’s <:-closure builder (not OR-ed at query time — a disjunction of two preorders is not transitive).

Rationale

  • Neutral substrate, theory as library — matches the meta-calculus pattern one layer up (RP-003): the core gains only “a value can reference a declared type” + first-class reflection; order/categorizes/ power_type_of live in std::mlt. The BFO/non-UFO smoke test still passes (a vocabulary uses TypeRef/meta with zero UFO/MLT in scope).
  • Sound by construction — codes-universe, not impredicative universe (D-132 / s2 §9.4). TypeRef unsealed keeps Metatype the lone sealed primitive.
  • Minimal blast radius — reuses Value::Name (carrier), RFD 0017 refinement (TypeRef<C>), the reserved-head-predicate IR convention (no AtomIR/tier-proof churn), and D-116’s precedent that a type-position may resolve to a handle (D-116 explicitly rejected “wrap a type in a synthetic concept”, validating a genuine sort).
  • Overlay-correct — == over Value::Name works immediately; bounded TypeRef<C> is exactly the enum-workaround need, done principledly.

Alternatives considered

  • Core sort named Type (demote std::mlt::star::Type → OrderlessType). Most ergonomic word, but a four-way name collision and reopens the delexicalization wound; and Type with Metatype <: Type would amend “Metatype is the only sealed primitive.” Rejected for TypeRef.
  • Entity + metatype-as-sort only (no dedicated reflective sort; RP-003 §10 canonical Entity/type). Most minimal, but : type reads as a keyword and conflates the generic metatype with the universal type-reference sort; a dedicated unambiguous TypeRef is clearer craft.
  • First-class generic Type<C> core type-former (covariant primitive). Adds a powertype-flavored core form and reproves variance; the refinement route (D2) is more neutral and reuses machinery.
  • Runtime-only coercer fix (accept a class-path for any concept-typed param, no sort). Smallest, but a non-design — pushes the type/individual distinction into ad-hoc coercion. Rejected.
  • MLT-order-indexed Type@n / potency in core. This is precisely what neutrality forbids in the core.

Consequences

  • New surface: TypeRef, TypeRef<C> as type expressions; Term.typeRef IR; meta/iof/specializes/ extent value-polymorphic. Book §4 amended (meta -> TypeRef); RP-003 §10 type-position sort named TypeRef (lowercase type remains the generic metatype). SUMMARY/Appendix updated.
  • Drift gate: Term.typeRef is @[language_interface] — the Rust oxc-protocol Term mirror gains a matching TypeRef variant (arity 1 over the name/path id).
  • Lean module inherits Classical.choice at the metalevel (D-132 OQ3) — already used in Foundation/Truth4, not new debt.
  • TypeRef must stay crisply distinct in spelling/scope from Top, std::mlt::star::Type, and any vocabulary’s Type_ (D-073) — no respelling that blocks a vocabulary declaring its own.

Open questions

  • Codomain scope — TypeRef references concept/construct/relation/metatype; the intrinsics stay category-errors on struct/enum data values (§4). (Recommended: include relations.)
  • extent(TypeRef<C>) — enumerate all subtypes of C (symmetric with extent(Metatype)). (Recommended: yes.)
  • Narrowing — should t: TypeRef narrow to TypeRef<K> after iof(t, K) (occurrence typing)? Deferred.

Implementation status (layered, each checkpoint green)

  1. ✅ Lean foundation — Term.typeRef + MetaCalculus/Reflect.lean; lake build green (1034 jobs), 0 sorry (commit a84d9e3).
  2. Protocol + drift — mirror Term::TypeRef in oxc-protocol; document Value::Name carrier; drift green.
  3. Resolver + checker — resolve TypeRef/Entity; fold the reflective edges into the <:-closure; TypeRef<C> refinement + covariance; 3-valued OWA membership.
  4. Instantiate — lower the four intrinsics to the value-polymorphic atoms (sugar preserved; fast-path closed types).
  5. Reasoner — evaluate the reserved-head reflection atoms over the catalog graph.
  6. Runtime + wire — the coerce_json_arg_for_type TypeRef arm (path → NameRef → Value::Name).
  7. SDK (oxc-gen) — class-path wire shape.
  8. Spec + overlay — §4 amendments; overlay migration where “any type-reference” is meant.