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 0038 — The prelude, ambient scope, and symbol-precise stdlib loading

  • Status: discussion
  • Depends on: RFD 0009 (MLT-as-library / nothing-privileged), RFD 0030 (path dependencies)
  • Blocks: RFD 0037 D8 (relation-property re-home needs a real prelude to surface library attribute-macros without ceremony)

Summary

Argon’s prelude is specified but unbuilt: the reference designs a full Rust-like prelude (§3.4 four-tier resolution; §15 std::prelude::v1 with an auto-import set + #![no_implicit_prelude] opt-out), but the compiler implements none of it — three ad-hoc mechanisms stand in for it, it diverges from the reference, and the reference contradicts itself on the most basic question: whether type/rel are ambient. This RFD settles the ambient-scope architecture:

  1. Tier 0 — substrate. A fixed, hardcoded, non-opt-outable set: the names that are the language, not library declarations.
  2. Tier 1 — the prelude. A real, configurable, auto-imported (opt-out) prelude that carries no ontology by default — no type/rel. The prelude is a package feature (ox), not a compiler feature: there is no compiler-default prelude.
  3. Tier 2 — explicit use, with stdlib and dependencies loaded symbol-precisely (⊥-locality extraction) from the transitive use-graph — only what the program actually uses, never whole packages.

The frame is the existing oxc = rustc, ox = cargo split (the binaries already encode it: oxc is “the language compiler … pure source-to-artifact passes”; ox is “the project CLI”). oxc compiles loose files with substrate + explicit uses and no prelude; ox is the package tool where the manifest supplies the prelude, dependencies, tier, and world. We copy Rust’s split and manifest model but deliberately do not copy rustc’s rich auto-applied std::prelude — Rust can privilege std because it is a universal library; Argon structurally cannot privilege any vocabulary (RFD 0009). So the governing principle is: nothing from the standard library is privileged into ambient scope — not categorizes, and not the no-commitment baseline type/rel. Ontological commitment is always explicit and visible at the top of a module. This resolves the reference-manual contradiction in favor of its own better half (§4 / §15.0.1) and deletes the “auto-injected ambient type/rel” claims (§5.2 / §15).

Background — the validated problem

Ground truth, verified against the compiler (compiler/crates/) and by ox check:

  • The specified prelude is unbuilt. The reference fully specifies a four-tier resolution (local → use → auto-prelude std::prelude::v1::* → primordials, 03-modules.md §3.4) with #![no_implicit_prelude] opt-out, and §15 even enumerates a rich Rust-like auto-prelude (Option/Result/Ordering/traits/ macros). But the compiler builds none of tier 3: no std::prelude::v1, no #![no_implicit_prelude] (listed as a directive in §9 but absent from DIRECTIVE_REGISTRY, so it parses then fails OE0705). The prelude exists on paper, not in code.
  • The substrate/prelude boundary (clarification). Of §15’s auto-prelude list, the items that actually resolve today — Option/Result/Ordering/List/ Set/Map/Range/Truth4/Diagnostic/Severity — are Tier-0 substrate (hardcoded is_builtin_type_form + the check surface), not a library prelude. So “empty default prelude” (D2) never strips these — a package always has them. The empty default applies to the ontology/library layer (type/rel/ vocabulary). The not-yet-shipped traits/macros (Display/format!/…) are deferred: substrate-vs-prelude is decided when they land (lean: language macros and core operator-traits are substrate).
  • All seven stdlib packages load unconditionally. STDLIB_SOURCES (oxc-instantiate/src/lower.rs) is a fixed seven-element list; load_stdlib iterates it with no dependency graph, no opt-in, no opt-out. Every artifact carries std::mlt/std::kripke/std::fin/… axioms whether used or not.
  • Ambient leak in classifier position (demonstrated). Type references require use (pub rel R(World, World) with no import → OE0101, test T1). But metatype/metarel classifiers resolve local → ambient pin → workspace-unique (resolve_metatype_introducer/resolve_metarel_introducer, lower.rs:1171/1209); because every std package is loaded into the workspace, the workspace-unique arm makes every loaded metatype/metarel an ambient classifier — pub categorizes AB(A, B) checks clean with no use (test T2). This directly violates RFD 0009 (“MLT is an explicitly-imported library, nothing privileged”) and §5.2.
  • type/rel are hardcoded pins. if classifier == "type" { return std::core::type } (lower.rs:1182; :1220 for rel) — special-cased, not resolved through any inclusion mechanism.
  • Top/Bot have two sources of truth. Defined both as primordials (resolve.rs primordial_kind) and as pub types in std/core/root.ar.
  • The reference contradicts itself. §15.0.1: “No vocabulary ships with the language or the stdlib … external vocabularies may re-export std::core::rel in their own prelude as a convenience”; §4: “after use std::core::rel; the modeler can write pub rel …” — both explicit-inclusion. Yet §5.2 / §15: “std::core is auto-injected … pub type Foo works with no use.” These cannot both hold.

Infrastructure that already exists and we build on: ox.toml package manifests with [package]/[dependencies] (RFD 0030); inner-attribute parsing (#![...] → ATTR_INNER CST, validated against DIRECTIVE_REGISTRY); the prelude.ar / pub use pkg::prelude::* convention (§3). Infrastructure that does not exist: selective stdlib loading, a transitive use-graph (only mod-chain reachability and per-file import maps exist), and any prelude-control directive.

Decision

D0 — oxc is the compiler, ox is the package tool (rustc / cargo)

The two binaries (crates/oxc-driver/src/bin/) already encode the split:

  • oxc (rustc): compiles loose source files — “the pure source-to-artifact passes.” A loose file is not a package, so it has no prelude: only the Tier-0 substrate is in scope, and everything else is an explicit use. A bare oxc foo.ar with pub type Person {} and no import is an error (OE0605, unresolved metatype type) with a hint to use std::core::{type, rel}.
  • ox (cargo): the package tool. It requires an ox.toml, and the manifest supplies the prelude ([package].prelude, D4), dependencies, tier ceiling, and world. ox invokes the same oxc passes with that manifest context — exactly as cargo drives rustc.

Consequence: the prelude is a package feature, not a compiler default. The current standalone path single_file_workspace_with_stdlib (oxc-driver), which injects all seven stdlib packages into any loose file, is deleted — it is the auto-load-everything behavior this RFD removes. Loose-file compilation keeps working under oxc with substrate + explicit uses + symbol-precise extraction (D3); there is no separate “standalone mode” with divergent rules.

D1 — Tier 0: the substrate is fixed and is not the library

The always-in-scope, non-opt-outable set is exactly the language primitives — the carriers of the meta-calculus and type system, which have no library declaration form:

  • Primordials: Nat, Int, Real, Decimal, Money, Date, Time, DateTime, Duration, Bool, String, Top, Bot (and ⊤/⊥).
  • Builtin type forms: List, Set, Map, Range, Option, Result, Ordering, Truth4, Truth4Of, Path, Metatype, TypeRef, Entity.
  • Reflection intrinsics: meta, iof, specializes, extent, implements, implementors.
  • Aggregate heads: count, count_distinct, sum, min, max, avg, exists.
  • Modal operators, operators, true/false, the check surface (Diagnostic/Severity).

These stay hardcoded (resolved before imports), and the set is closed: adding to it is a language change, not a library change. Top/Bot are primordials (Tier 0); the duplicate pub type Top/Bot in std/core are removed (D5).

D2 — Tier 1: ONE prelude, carrying no ontology by default

There is exactly one auto-import mechanism. Two distinct roles were being conflated under the word “prelude” — separating them is what unsticks this (both exist in Rust too):

  • The auto-import set (role 1 — the prelude): what every module of a package gets without writing use. Configured by ox.toml [package].prelude (D4), default empty, opt-out per-module via #![no_implicit_prelude]. This is the one thing called “the prelude,” and it is a package concept.
  • A package’s exported public module (role 2): a normal module conventionally named prelude that pub uses the package’s public surface; consumers opt in explicitly with use pkg::prelude::*, or feed it into their own role-1 config. No special mechanism — just a module. The §3 prelude.ar convention is this. It is not a competing auto-prelude.

The earlier confusion (std::prelude::v1 and std::core::prelude both acting as global auto-preludes) is gone: there is one role-1 prelude per package, empty by default — the extension point, not a dumping ground.

type/rel are opt-in, with no special prelude for them. A package that wants the baseline auto-available in its own modules lists it in role 1 — [package].prelude = ["std::core::{type, rel}"]. A module (or a loose oxc file) that wants it without a package prelude writes use std::core::{type, rel} directly. A foundational-ontology package sets [package].prelude = ["std::ufo::prelude::*"] and never sees type/rel. The hardcoded pins (lower.rs:1182/1220) are removed; type/rel resolve through the prelude / imports like every other classifier.

A future #[cfg(...)]-style mechanism (Argon has none today) could conditionally configure the prelude — a clean home for “this build wants the core baseline” — but the manifest config covers the need now without a new language feature; cfg is noted as a later generalization, not a v1 dependency.

Rationale. The no-commitment baseline is itself a commitment — to neutrality. Defaulting it privileges that choice and forces every committed package to opt out of a commitment it never made (backwards). Making it opt-in (a) keeps the language neutral (RFD 0009), (b) makes every module’s metatype basis visible at its top, and (c) unifies resolution: classifiers and references both resolve local → imports/prelude → substrate, eliminating the T1/T2 asymmetry.

D3 — Tier 2: explicit use, symbol-precise extraction (not whole-package)

Loading is symbol-precise, not package-granular. use A::b::{c, D} brings in c and D and the transitive closure of declarations they depend on (endpoint types, supertypes, referenced relations, the symbols their bodies mention) — and nothing else from A::b. Pulling in all of A::b::* because one symbol was named is a hollow approximation and is rejected: the artifact must contain only what the program actually uses.

This is exactly ⊥-locality module extraction, which the substrate already mechanizes and proves conservative (spec/lean/Argon/Locality/; AGENTS.md §3.5 — “Σ-scoped CWA-conservativity, domain-conservative extraction for ghost individuals, chained extraction across import chains”). The compiler does not implement it today (all stdlib loads whole); D3 wires the existing, proven theory into the build:

  • Build the transitive use-graph — a new pass over use edges plus the dependency edges between declarations — seeded from the entry module.
  • Mint events for exactly the reachable declaration closure, across stdlib and path dependencies alike. use std::fin::{MonetaryAmount} ⇒ MonetaryAmount and its dependency closure, not the Currency/RoundingMode surface it never references; no use of std::fin ⇒ zero std::fin axioms.
  • The metatype/metarel introducer’s workspace-unique arm sees only the extracted/in-scope metatypes (imported or in the prelude) — never every loaded package. This is what closes the T2 leak.

Conservativity is a composition of two properties (validated by reading the whole spec/lean/Argon/ tree), both now Lean-proven for their core:

  • Ontology/concept layer — ⊥-locality module extraction → Σ-scoped CWA-conservativity (concept entailment): proven (Locality/ScopedConservativity.lean, DomainConservative, ChainedCwa).
  • Datalog/derived layer — a program slice (the rules in the dependency-closure of the used predicates) preserves the least-fixpoint on the closure predicates, i.e. derived extents + checks: proven for positive Datalog (Scratch/DatalogSliceRelevance.lean, agree_on_closure, axiom-free — Lean obligation L1, discharged). The existing Locality/ mechanization did not cover this (Seminaive.lean proves the module-id column is harmless — a different result). The extension to stratified negation + aggregates is L2 (below), gated meanwhile by the differential test.

The differential and determinism tests below guard the implementation; L1 discharges the positive-Datalog core of the derived-layer proof gap.

D4 — Prelude configuration: manifest default + per-module opt-out

Two controls, both honored:

  • ox.toml [package].prelude — an array of use-tails, each parsed exactly as if written use <entry>; and auto-prepended to every module of the package. Reusing the real use parser gives single / brace-list / glob / alias forms for free, with identical resolution and identical participation in the D3 use-graph (a prelude entry is an implicit use). Default empty. An entry that fails to parse or resolve is a hard error (explicit author intent), not an OW1240 warning (OW1240 stays for unknown keys).

    [package]
prelude = [
  "std::core::{type, rel}",   # opt into the no-commitment baseline
  "std::ufo::prelude::*",     # or glob a foundational ontology's public prelude
]

    Large preludes: point at your own prelude module. For a non-trivial prelude, the cleanest shape is a one-line config that globs the package’s own prelude module, with the actual re-exports written as real Argon code:

    [package]
prelude = ["pkg::prelude::*"]

    // prelude.ar
pub use std::core::{type, rel};
pub use std::ufo::prelude::*;
// … grows here, commentable, reviewable

    Validated against the resolver: pkg:: is the package self-anchor (resolve.rs:680, and it anchors at that package’s root even as a dependency, :681-684); a glob use pkg::prelude::* pulls in the module’s public surface including its pub use re-exports, which resolve transitively and cycle-guarded (resolve.rs:410-416, :452-453). This is role-1 (auto-import) pointing at role-2 (the exported module) — one mechanism, composed. Caveat (new): the prelude module must be exempt from auto-prelude injection into itself (else use pkg::prelude::* is prepended to pkg::prelude); the resolver’s cycle-guard catches the loop, but exempting the prelude module is cleaner.

  • #![no_implicit_prelude] — a per-module override. Add it to DIRECTIVE_REGISTRY (module position, ATTR_INNER); expose inner attributes on the SourceFile AST (today argon.ungrammar has only items:Item*); thread the flag into prelude injection. A module with the flag gets Tier 0 only — no auto-prelude — and must use everything else explicitly.

D5 — Resolve the spec contradiction; dedupe Top/Bot

The reference is amended to a single consistent rule: nothing from the stdlib is ambient; type/rel require use std::core::{type, rel} (or a prelude that re-exports them). Delete the §5.2 / §15 “auto-injected ambient type/rel” clauses; keep §4 / §15.0.1. Remove the pub type Top/Bot declarations from std/core/root.ar (Top/Bot are Tier 0 primordials).

Migration

This is a breaking change for any code relying on the leak or on the deleted standalone auto-load. Accepted (the corpus is ours).

  • Delete single_file_workspace_with_stdlib (oxc-driver). Loose-file compilation runs under oxc with substrate + explicit uses + extraction.
  • A corpus migration pass: every module that declares pub type/pub rel, or uses a stdlib classifier without importing it, gains the right use (std::core::{type, rel}, std::mlt::*, …) — or, if it is a package, the entry in [package].prelude.
  • Examples and single-file tests either run under oxc with an explicit use std::core::{type, rel}, or gain a one-line ox.toml (prelude = ["std::core::{type, rel}"]); the test harness (write_temp_source) writes whichever it needs.
  • The OE0605/OE0606 unresolved-introducer diagnostics gain a hint suggesting the likely use (e.g. “did you mean use std::core::{type, rel}?”).
  • The stdlib packages themselves declare their own dependencies via use (e.g. std::mlt uses std::core).

Acceptance tests

  1. Leak closed: pub categorizes AB(A, B) with no use → OE0606 (unresolved metarel introducer), not ok. (Inverts test T2.)
  2. Baseline opt-in: pub type Foo {} with no use and #![no_implicit_prelude] → OE0605; with use std::core::{type} → ok.
  3. Symbol-precise extraction: use std::fin::{MonetaryAmount} yields an artifact with MonetaryAmount and its dependency closure but not the std::fin declarations it never references; no use of std::fin ⇒ zero std::fin events. Assert over the event stream.
  4. No regression for committed vocabularies: use std::ufo::prelude::*; pub kind Person {} checks clean with no std::core in scope.
  5. Determinism preserved: byte-identical .oxbin across builds (S5) holds under extraction (the extracted set is a deterministic function of the use-graph).
  6. Extraction is conservative: for any program, the answers (derived extents, check firings, tiers) under symbol-precise extraction equal those under load-everything — spot-checked differentially over the corpus. The DL/concept half is the Lean-proven ⊥-locality property (Locality/); the positive-Datalog half is L1 (Scratch/DatalogSliceRelevance.lean, proven, axiom-free); the stratified-negation/aggregate cases (L2) rest on the differential test until mechanized.

Lean obligations

  • L1 — positive Datalog slice-relevance: DISCHARGED. Proven in spec/lean/Scratch/DatalogSliceRelevance.lean (theorem agree_on_closure): for a ground positive program, the slice (rules whose head predicate is in the dependency-closure of the used predicate set Q) and the full program agree, at every fixpoint iteration — hence at the lfp — on every atom whose predicate is in the closure of Q. So loading only the use-graph closure yields the same derived extents over the used predicates. Self-contained (no Mathlib), no sorry, and #print axioms reports it depends on no axioms at all (fully constructive) — the agreement is proven by induction on the fixpoint chain, not assumed ([[no-axiomatizing-the-conclusion]]). This is D3’s derived-layer conservativity for the monotone core, composed with the ⊥-locality result below.
  • L2 — stratified negation + aggregates (remaining). L1’s T is monotone (positive Datalog). Argon’s reasoning is stratified well-founded with negation and aggregates; the relevance result extends in the standard way, but a faithful proof must model the strata, so L1 does not by itself cover the non-positive cases. Until L2 is mechanized, the differential test (#6) gates those. (Per AGENTS.md the Rust reasoner leads the Lean on the reasoning layer.)
  • Already discharged (ontology layer): ⊥-locality → Σ-scoped CWA-conservativity (Locality/ScopedConservativity.lean), domain-conservative extraction (DomainConservative), chained across imports (ChainedCwa).

Spec reconciliation (reference edits)

  • 05-constructs.md §5.2, 15-stdlib.md §15/§15.0.1: delete “auto-injected ambient type/rel”; state the explicit-inclusion rule and the prelude tiers.
  • 03-modules.md §3.4: make the resolution order match D1–D3 (substrate is the floor, not auto-prelude-then-primordials); document #![no_implicit_prelude].
  • appendix-a-reserved-keywords.md: type/rel are not reserved ambient names.

Resolved (this RFD)

  • oxc = rustc, ox = cargo. The prelude is a package feature; there is no compiler-default prelude. Loose oxc files use substrate + explicit uses. single_file_workspace_with_stdlib is deleted.
  • One auto-import mechanism (role 1), distinct from a package’s exported prelude module (role 2). No std::prelude::v1, no std::core::prelude.
  • [package].prelude = an array of use-tails, default empty; per-module opt-out #![no_implicit_prelude]. Bad entry = hard error.
  • type/rel opt-in via [package].prelude or explicit use — never privileged ambient.
  • Loading is symbol-precise (⊥-locality extraction), never whole-package.

Open questions

  1. Extraction staging. Symbol-precise ⊥-locality extraction is substantial. It may land in stages, but the hollow package-level version must not ship — if an interim step is needed it must still be sound (over-approximate only in ways that never change answers, and log/document any conservatism). Sequence the use-graph pass and the extraction pass against the existing Lean theory.
  2. #[cfg(...)] as the eventual conditional-prelude mechanism — out of scope for this RFD, noted as the natural later home for build-conditional baselines.