diff --git a/dsl/std/measure.dag b/dsl/std/measure.dag new file mode 100644 index 00000000000..d721182b9ca --- /dev/null +++ b/dsl/std/measure.dag @@ -0,0 +1,176 @@ +// std/measure.dag -- Measure / Quantity / Scale carrier (algebra-axis +// dimensional shape). +// +// Per Q-Unit-1..5 RATIFIED at gunbc#828 #issuecomment-4385412256 (2026-05-06), +// Q-Unit-1-Recanvas RATIFIED at gunbc#828 #issuecomment-4385539791 +// (outer carrier renamed from `Unit` to `Measure` to avoid collision with +// kernel `Unit` terminal-object type at `dsl/std/types.dag`), and +// Q-Refined-Phantom-Composition option (c) RATIFIED 2026-05-06 (literal +// `Refined, predicate>` form deferred to value-typed integration +// follow-up; this layer carries dimensional semantics via the `Quantity` / +// `Scale` tags only — no predicate refinement at the Measure level). +// +// Authority anchors (cited by rule-text quote per +// `brief-authoring-checklist.md`; bare line-number cites prohibited): +// - Practice 4 (`docs/modeling-discipline.md#4-coproduct-dissolution`): +// "Any new Rust enum with N >= 2 variants must have a checkpoint +// comment naming its classification (🟢/🟡/🔴), with a ledger entry +// if GREEN or a named trigger if YELLOW." +// - `feedback_construction_over_ratchets`: "Don't build the predicate +// ahead of consumer demand." +// - `feedback_reason_not_label`: "The predicate name is the label; +// the reason is the carrier's semantic content." +// Director ratifications recorded in gunbc#828 issue comments cited above. +// Worker brief lives outside this checkout (parent worktree); cross-program +// review reaches the brief through the gunbc#828 ratification thread. +// +// Scope (Phase-1 carrier landing): +// - `Measure` -- phantom-parameter carrier for dimensional types. +// - `Quantity` -- what is being measured (Time, Length, Mass, ...). +// - `Scale` -- SI decimal scale exponent (Atto..Exa, `One` = 10^0). +// - `scale_exponent(s: Scale) -> Int` -- structural exponent query +// (typed exponent authority; lets Grounding consumers and downstream +// algebraic consumers project a Scale value to its decimal exponent +// without re-encoding the table at each call site). +// +// NOT in scope (deferred per brief): +// - Aspect axis (PointKind / Magnitude / Instant / Rate) -> R4 C6. +// - Scale-agnostic `Duration` parametric form -> needs >=2 consumers. +// - 3-axis `AlgebraMachineRoundingProduct` -> R4 C5. +// +// COMPOSITION (S9 Phase-3 reframe per Q-Unit-4 RATIFIED outer-Refined / +// inner-Measure, with option (c) deferral of the literal Refined wrapper): +// +// Duration := Measure (Quantity-tagged; predicate deferred) +// Milliseconds := Measure (Quantity-tagged; predicate deferred) +// Seconds := Duration (Q-Unit-3 collapse) +// +// `Measure` is a phantom-parameter carrier: it has no runtime value +// structure. The semantic content of "non-negative time-magnitude" is +// carried by the `Quantity = Time` tag itself; predicate-bearing refinement +// is a downstream concern when `Refined<>` consumes a base with actual +// numeric inhabitants. Forward-flag: when value-typed dimensional refinement +// integration arrives, revisit the literal `Refined, +// non_negative>` form per Q-Unit-4 RATIFIED. + +module std.measure + +// --- Quantity: what is being measured ------------------------------------- +// +// PRACTICE 4 CHECKPOINT: 🟡 SCAFFOLD +// Dissolution trigger (Q-Unit-5 RATIFIED): "all Quantity values consumed +// by >= 1 Grounding emission rule". Until each value gates a real +// emission rule (Grounding consumer demonstrates need), the carrier +// is hand-modeled / speculative. Adding a new value without a +// corresponding emission rule violates +// `feedback_construction_over_ratchets`; new values require the P1 +// substrate-fact-introduction procedure with named consumer demand. +type Quantity = + Time + | Length + | Mass + | Memory + | Information + | DataRate + | Frequency + | Count + | Currency + +// --- Scale: SI decimal scale exponent ------------------------------------- +// +// PRACTICE 4 CHECKPOINT: 🟡 SCAFFOLD +// Same dissolution trigger as `Quantity`: "all Scale values consumed by +// >= 1 Grounding emission rule" (Q-Unit-5 RATIFIED). +// +// `One` is the unscaled identity (10^0) -- RATIFIED rename from `Unit` +// per Q-Unit-1 to avoid shadowing the outer carrier name and the +// kernel terminal-object `Unit` type. +// +// Scale is a typed exponent authority, not bare labels: the +// `scale_exponent` query below is the structural projection from a +// Scale value to its decimal exponent. Grounding consumers MUST go +// through `scale_exponent` rather than re-encoding the SI table per +// call site (single-source-of-truth invariant; cf. T-Numeric-Construction +// "single numeric authority" pattern). +type Scale = + Atto // 10^-18 + | Femto // 10^-15 + | Pico // 10^-12 + | Nano // 10^-9 + | Micro // 10^-6 + | Milli // 10^-3 + | One // 10^0 (identity scale; RATIFIED rename from `Unit` per Q-Unit-1) + | Kilo // 10^3 + | Mega // 10^6 + | Giga // 10^9 + | Tera // 10^12 + | Peta // 10^15 + | Exa // 10^18 + +// --- scale_exponent: typed exponent authority ----------------------------- +// +// Structural projection from `Scale` to its SI decimal exponent. This is +// the canonical query Grounding consumers and any downstream algebraic +// consumer (e.g., scale-arithmetic for unit conversion) bind against, +// rather than the bare variant names. Centralizing the table here means +// adding a new Scale value updates the exponent authority in one place. +// +// Total over all `Scale` inhabitants; exponents are i64-representable +// (range [-18, 18] in this enumeration). +fn scale_exponent(s: Scale) -> Int { + match s { + Atto => -18 + Femto => -15 + Pico => -12 + Nano => -9 + Micro => -6 + Milli => -3 + One => 0 + Kilo => 3 + Mega => 6 + Giga => 9 + Tera => 12 + Peta => 15 + Exa => 18 + } +} + +// --- Measure: phantom-parameter dimensional carrier ----------------- +// +// PRACTICE 4 CHECKPOINT: 🟢 PRIMITIVE +// Phantom-parameter carrier: widening adds Quantity / Scale values, not +// new Measure variants. The carrier itself has a single inhabitant per +// (Q, S) pairing; the type parameters tag dimensional semantics for the +// type system without runtime payload distinction at this layer. +// Per-target representation (Rust `std::time::Duration`, Python +// `datetime.timedelta`, Go `time.Duration`, etc.) is Grounding's job +// per Q-Unit-4 RATIFIED. +// +// CONSTRAINED-INHABITANCE GAP (P5 tracked scaffold): +// Denotationally `` must inhabit `Quantity` and `` must inhabit +// `Scale` for `Measure` to carry dimensional semantics. The current +// substrate has no parametric where-clause syntax (e.g., ` where +// Q : Quantity, S : Scale`), so this declaration accepts any type- +// reference for `` / `` at the parser/lower level. All intended +// consumers in Phase-1 / Phase-2 of the carrier landing instantiate with +// the ratified Quantity / Scale values (`Measure`, +// `Measure`, etc.); the constraint holds for those sole +// consumers by construction. +// +// Same gap as `GroupCompletion` / `FieldOfFractions` in +// `dsl/std/algebra.dag` (where-clause syntax is a substrate-feature +// lane, not per-carrier ceremony). Mechanical Quantity / Scale +// inhabitance witnesses are not declared at this layer for the same +// substrate reason. +// +// **Dissolution trigger:** when constrained-inhabitance / parametric +// where-clause syntax lands in the substrate (separate substrate-feature +// lane), tighten this declaration to require ` : Quantity, : +// Scale`. Existing call sites continue to type-check by construction. +// +// HARD BOUNDARIES (per Q-Unit RATIFIED + option (c) RATIFIED): +// - Phantom-parameter only -- no runtime payload, no value-level +// refinement (`non_negative` etc.) at this layer per option (c). +// - No mechanical Measure-witness derivation declared here -- same +// substrate gap as `GroupCompletion`; inhabitance lens follow-up. +type Measure