Stdlib (selected)

Standard packages

The standard library is five packages. The compiler embeds each one’s root.ar via include_str! (oxc-instantiate/src/lower.rs) and elaborates it before every user build, so use std::… resolves to real declarations.

Higher-order type theories are not in std. MLT ships as the unprivileged first-party package mlt (packages/mlt, RFD 0043): its own metarels (categorizes, partitions, is_subordinate_to, power_type_of), the order metaxis, and the decorator #[procmacro]s, with zero compiler privilege — a consumer lists it in ox.toml and imports the vocabulary. Parallel theories (potency, ML2, …) ship the same way; the substrate stays neutral about which one a model commits to.

Per-package worked programs live in examples/, compiled and run in CI.

Note std::math is not a package. The numeric and temporal types (Nat, Int, Real, Decimal, Money, Date, …) are compiler-injected primordials resolved directly by the resolver, not imported from .ar source. The fixed-width primitives (i8–i128, u8–u128, f32, f64) are likewise compiler-provided under the std::math::primitive name, requiring explicit use.

Primordial types (lexically always in scope, no use required):

Nat, Int, Real, Decimal, Money, Date, Time, DateTime, Duration,
Bool, String, Top, Bot

These match how ontologists think — counts, measurements, monetary amounts — rather than machine-level widths. Fixed-width variants (i8–i128, u8–u128, f32, f64) ship in std::math::primitive for FFI, performance-critical paths, and binary-protocol interop; explicit use required.

The prelude is a package feature, not a compiler default (RFD 0038). There is no auto-imported std::prelude; a package’s [package].prelude (ox.toml, an array of use-tails) auto-prepends uses to its own modules, empty by default, opt-out per-module with #![no_implicit_prelude]. What is always in scope without any use is the substrate — the language primitives, not a library:

• Primordial types (above) and builtin type forms: Option<T> (Some/None), Result<T, E> (Ok/Err), Ordering (Less/Equal/Greater), Truth4, Truth4Of<T>, List<T>, Set<T>, Map<K, V>, Range<T>, plus the check surface Diagnostic / Severity. These are compiler-provided (is_builtin_type_form) and resolve directly — in scope everywhere, no import, no prelude.

type/rel are not ambient. Opt into the no-commitment baseline with use std::core::{type, rel} or a [package].prelude entry (RFD 0038) — exactly as you bring in any vocabulary. Every ontological commitment is visible in the source: vocabulary classifiers (UFO’s kind, BFO’s class, …) and the baseline type/rel alike resolve only against pub metatype / pub metarel declarations in scope — declared in the package or imported from an external vocabulary package (Name resolution, Vocabulary concepts and the generic type metatype); an unresolved introducer is OE0605 / OE0606. No vocabulary — not even the baseline — ships ambient. A vocabulary package may re-export std::core::rel (and/or type) in its own prelude.ar as a convenience.

Numeric tower and coercion

Modeling-surface numeric types (primordial, always in scope):

All numeric primitives are signed where signedness is meaningful. The runtime chooses an implementation width based on refinement bounds: Int where _ < 256 may compile to i16; unbounded Int defaults to arbitrary-precision.

Fixed-width primitives (std::math::primitive, requires explicit use):

i8, i16, i32, i64, i128, u8, u16, u32, u64, u128, f32, f64

For FFI, performance-critical paths, and binary-protocol interop.

Money arithmetic (per D-069):

Scalar multiplication and division accept any numeric type as the non-Money operand (the scalar widens implicitly to Decimal for the arithmetic). Money-to-Money addition and subtraction are currency-checked at elaboration when the operands have refined currency annotations. No implicit conversion Nat → Money or Decimal → Money; construct via Money::from_cents(n) or Money::from_decimal(d, currency).

Temporal arithmetic:

Date literals. A calendar date is written hash-delimited: #YYYY-MM-DD#. The hashes are load-bearing — they distinguish a date from arithmetic. A bare 2024-01-01 is integer subtraction (2024 − 1 − 1 = 2022), not a date; written against a Date-typed position it is refused with OE1340 and a directed hint toward the #…# form (the #date# silent-Int landmine, fixed in arc5). The inner text is an ISO YYYY-MM-DD civil date validated at compile time (month 01–12, day in range, leap years exact); a DateTime literal #YYYY-MM-DDTHH:MM:SSZ# carries a trailing T time.

pub type Invoice { mut issued: Date, mut paid: Date }

// `<int>.days` / `<int>.weeks` are duration sugar: a fixed whole-day count
// (`30.days` ⤳ 30, `2.weeks` ⤳ 14). `Date ± Duration` evaluates exactly.
pub derive overdue(i: Invoice) :- Invoice(i), i.paid > i.issued + 30.days;

// `today()` reads the evaluation's current valid-time (a `Date`).
pub derive past_due(i: Invoice) :- Invoice(i), i.paid < today();

Duration construction. A duration is a count of whole days in this increment. The fixed-length units <int>.days and <int>.weeks lower at rule-term resolution to a Duration literal — no impl is needed, and they work in rule bodies today. The calendar-relative units .months / .years have no fixed day count (a month is 28–31 days depending on the anchor), so they are loud-refused with OE1337 rather than silently approximated; compute the target date explicitly instead. Sub-day units (.seconds / .minutes / .hours) await the sub-day Time value layer.

today() — the current valid-time of the evaluation, as a Date — is the one nullary date intrinsic that evaluates today (now() awaits the sub-day layer). It is fixed for the whole evaluation, so a rule stays a pure function of its snapshot; a served model’s deadline arithmetic advances with the wall clock across requests rather than baking a build-time date.

Operator semantics — division. / is exact field division on the numeric tower, on every plane (checker, runtime, reasoner). Statically, Int / Int : Real — the quotient of two integers is a rational, and the type says so; 7 / 2 evaluates to the exact rational 7/2, never a truncated 3. The inference is uniform: 20 / 5 : Real statically even though the value collapses at the carrier (next sentence) — soundly, since Int <: Real. At the value carrier, integral results collapse to Int per the tower-wide convention (20 / 5 is Int(4); integral Real values are Int at the carrier). All other arithmetic operators on Int × Int stay Int. Truncating integer division does not exist; if it is ever wanted, it will be an explicit operator, never /.

Coercion rules:

• Implicit widening: i32 → i64 → Int, Nat → Int, and Int → Real. Since Real is exact (RFD 0016), Int → Real is exact-into-exact (Int ⊆ Real mathematically): require perPeriodValue > 0 compares the Real against the Int literal 0 without an explicit 0.0, and Int + Real yields a Real; a pure-Int expression stays Int — except /, which is Real (operator semantics above). The inexact floats f32/f64 do not implicitly widen into Real — a float reaches the exact tier only via an explicit, lossy conversion (widening an approximate value into the exact tier must be a visible choice).
• Explicit narrowing: i64::try_into::<i32>() returning Result<i32, OverflowError>.
• No implicit truncation, ever.

Per RFD 0016, Real/Decimal/Money are exact (arbitrary-precision rational); the reasoner folds them exactly (so avg over a Real collection is exact). Custom-precision fixed-point and refinement-driven width selection are out of scope (Out of scope).

Effective-dating: valid time and the two as_of axes

Argon’s substrate is bitemporal (RP-004): every assertion carries two orthogonal time axes.

• Transaction time (TT) — when the system was told. The append-only event log’s stamp; an as_of <int> query reads “what the system would have said at TT = t” (the tx-counter axis). Audit/replay.
• Valid time (VT) — when the fact held in the world. Independent of when it was recorded; an as_of <#date#> query reads “what was VALID at VT = t, as currently believed.” Effective-dating.

The two are independent and composable: a query may pin TT alone, VT alone, or both (the full bitemporal point). They answer different questions — “what did we believe last Tuesday” (TT) versus “what rate was in effect on 2024-04-15” (VT) — and a model that conflates them (a hand-rolled effectiveFrom: Date field) cannot express the second cleanly.

Asserting at a valid time. A write carries an optional at <date> qualifier; the assertion’s valid time begins on that civil day (midnight UTC) rather than at write time. Both the imperative mutate-body form and the declarative pub fact form take it:

pub type StandardRate;

// effective-dated enactment: the membership holds FROM `effective` onward
pub mutate enact(r: StandardRate, effective: Date) {
    insert iof(r, StandardRate) at effective;
}

// the declaration-form twin — a top-level effective-dated assertion
pub fact StandardRate(rate2024) at #2024-01-01#;

The at <date> expression must evaluate to a Date (a #date# literal or a Date-typed value); a bare arithmetic value is refused (OE1339). The window form during <window> and bitemporal retraction (a valid-time-qualified delete) refuse loudly (OE1330) rather than silently applying at all valid times.

Reading at a valid time. An as_of <#date#> clause on a query projects the extent valid on that civil day:

pub type Rate;

// "what rate(s) were in force on this filing day?"  (the VALID-time axis)
pub query rate_on_filing_day() -> Rate as_of #2024-04-15#;

// "what the system believed at TT = 5 about VALID = now"  (the TX-time axis)
pub query rate_at_tx_5() -> Rate as_of 5;

A Rate enacted at #2024-01-01# is invisible to an as_of #2023-…# read and visible to an as_of #2024-…# read — the effective-dating round-trip. See examples/effective_dated_tax_v0 for the full rate-table transcript.