Feature contract: integer literals and nat-literal#
Bare integers select a representation from the expected type in the draft edition. The explicit
(nat-literal N)head always retains Nat semantics. The bootstrap checker implements the broader contract below. Alpha frontend parity remains open; the qualified Alpha admission subset is described next.
The Alpha parser retains raw integer spelling, and ModuleChecker uses
Compiler.IntegerLiteral through contextual lowering. L11t qualifies declared
types, applications and lambda codomains. L11u extends this to family parameters
and indices, constructor fields and recursive arguments, including dependent
domains and local binder shadowing. Telescope probes query the existing checker
and do not appear in the returned core. Final annotation checking uses the same
contextual lowering. Closed natural successors now use the existing literal
reducer during type normalization, allowing a constructor result index such as
succ zero to match literal 1.
L11v accepts ordinary Type N in binder domains, module annotations and bodies,
and application arguments. Numeric level spelling uses the shared unsigned
natural decoder; declaration parsing preserves its existing state and AST shapes.
Fifteen universe assertions check exact returned types and normalized bodies,
including radix spellings, a codomain, application and an identifier named Type.
Eleven telescope assertions use the same bare spelling accepted by the bootstrap.
The identical-source bootstrap controls and native Alpha evidence are retained
under evidence/language-testing/L11v-source-controls/ and
evidence/language-testing/L11v-qualified-gate/. The older grouped (Type 0)
spelling remains accepted by Alpha but rejected by the bootstrap; diagnostic code
and origin equivalence are not established by these admission/refusal controls.
Family-header radix levels have not been qualified by this subset.
L11w introduced Compiler.NaturalMagnitude as the checked compact-magnitude
owner. Its payload is canonical little-endian decimal digit values, with empty
zero and at most 4096 significant digits. L11x qualifies 411 independent arithmetic,
iteration, admission and refusal assertions, plus exact maximum/overflow fixtures
for binary and hexadecimal spelling. Decimal maximum/overflow coverage remains in
the admission fixture. All four large-radix fixtures execute under the original
60-second, 3 GiB/no-swap limits; the earlier timeout/OOM evidence is retained.
Addition and normalization use the existing BytesBuilder primitive to avoid
repeated suffix copying. Radix conversion doubles canonical digits directly and
adds the small decoded digit first. Bounded carry arithmetic has exhaustive
independent vectors. Structural iteration avoids constructing the whole unary
value first; its cost still follows the requested number of steps. Internal
arithmetic lives in Compiler.NaturalMagnitudeArithmetic; the checked owner
validates external input. Exact evidence is in
evidence/language-testing/L11x-qualified-gate/SUMMARY.md.
L11z adopts canonical digit bytes in the existing Alpha Core and NamedCore literal nodes. Ordinary natural admission goes directly from spelling to this payload; inference rejects malformed or oversized payloads. Successor, comparison, low-byte conversion and structural elimination use the compact owner. The runtime encoding remains unary ALRI v4, so runtime expansion and structural elimination still cost the requested number of steps.
Core literal tag 19 and NamedCore tag 18 carry canonical bytes. Legacy tag-2
readers retain their distinct fixed64 and unary formats. Core term and
normalization pools write schema 2 and migrate schema-1 keys while preserving
validated identities, including memo keys and their target references. Native
fixtures cover ordinary 4096-digit module admission, 4097-digit refusal, mixed
successors, reducers, legacy reads and migrated cache hits. See
evidence/language-testing/L11z-regression/SUMMARY.md for exact qualification and
remaining failures.
The L11z evidence above did not establish explicit runtime-expansion and
normalization budgets, whole-path work counters, newer compile-time arithmetic
heads, complete compiler-snapshot restoration, explicit nat-literal, edition
and origin/span parity, declaration-domain literals or remaining checking
positions. Later qualification is recorded in language-refactor-goal.md; the
normalization-work coverage, including the subsequent normalization batch, is described below. Full feature
contract and release acceptance remain open.
Normalization work accounting#
Alpha type and beta normalization thread a checked U32 work budget with a default limit of 65,536 units. Structural visits, substitutions and natural-fold steps consume the shared budget. Exhaustion prevents acceptance and has diagnostic code 89.
Reducing a byte concatenation charges one application unit plus the lengths of both literal operands. The payload walker processes at most the remaining budget and stops when the payload ends. Four little-endian budget bytes govern bounded iteration blocks; a large budget needs no unary expansion. Exhaustion retains the last valid budget, and the concatenated result is supplied only after both payload charges complete. Neutral applications retain their application charge.
The executed boundary tests cover exact limits, partial budgets, invalid states, byte carry/borrow and U32 maximum. Runtime-fed tests include 1 MiB payloads and a wrong-output control.
Literal byte equality and natural comparison charge both input payloads before reduction. Byte length and natural-to-byte conversion charge the admitted payload; byte cons also reserves its output head. Neutral operands do not incur literal payload charges. Byte elimination reserves the scrutinee length before building its fold, then threads the remaining budget through each branch application and substitution.
Natural successor charges its magnitude length. Addition and subtraction charge
both input lengths. Nonzero multiplication additionally reserves right*left + right*right units for schoolbook products and accumulator growth. Division and
modulo additionally reserve nine left*right passes for decimal quotient trials.
Here left and right denote digit counts, not represented natural values.
Zero multiplication avoids the product reservation. These reservations govern
the existing checked reducers; they do not change their arithmetic results.
Generic elimination charges family/constructor name comparisons, branch visits,
argument sequence bookkeeping and substitutions. A branch with n arguments
must have between n and 2*n binders before unary arity subtraction is allowed.
Bookkeeping reserves sixteen sequence-product passes; actual substitutions use
the remaining shared budget. Missing branches and impossible arities remain
neutral, without traversing the represented binder count.
Variable-index shifts and predecessor operations reserve their unary operand before executing it. Branch depth addition reserves its iterated depth operand. The reservation cursor advances from zero only while budget remains; it never eliminates the requested natural. Bound variables below the cutoff and zero shifts retain their constant structural charge. Consequently exact historical substitution costs increase where they previously omitted index arithmetic.
These are algorithmic work units, not machine instructions, allocation counts or wall-clock guarantees. Runtime probes distinguish them from VM steps and memory. Bootstrap total-work accounting and whole-release acceptance remain open.
1. Lexical and grammar rules, including precedence and termination#
Two spellings, both draft-edition-only: the bare literal N (L10) and the
temporary head (nat-literal N). N is decimal (255), hexadecimal (0xff,
0xffff_0000) or binary (0b1010), with _ digit separators allowed only
BETWEEN valid digits of the radix. A leading - is part of the bare integer
token, including negative zero; it requires an expected signed type. At most 4096 decimal digits of value (ALPHA-PARSE-NAT-LITERAL- TOO-LARGE otherwise). A misplaced separator (1_, 1__0, 0x_1) is
ALPHA-LITERAL-BAD-SEPARATOR; an empty digit body (0x) is
ALPHA-LITERAL-MISSING-DIGITS. Under alpha-2026 any spelling is
ALPHA-EDITION-UNSUPPORTED-FORM.
2. Scope and binding rules, including generated names#
Binds nothing; a leaf. No generated names.
3. Type and quantity requirements#
Without an expected type, a nonnegative bare integer has type Nat. An expected
Nat also selects the compact natural. Expected U8/U16/U32/U64 require
0 through 2^width - 1 and reject a negative spelling, including -0. Expected
I8/I16/I32/I64 require -2^(width-1) through 2^(width-1)-1. Range checking precedes
construction, so signed minima are accepted and overflow never wraps.
Expected types propagate through annotations and aliases, application arguments,
lambda bodies checked against a function type, annotated lets, explicitly typed
pairs, family/constructor arguments,
equality/reflexivity operands and returned computation values. Lambda domains
and quantities remain those written in the source and are checked by the kernel.
Explicit (nat-literal N) stays Nat even under a word expectation. Negative
literals without a numeric expectation require a type. Float conversion and
remaining dependent-eliminator propagation are not implemented by this chunk.
An application synthesizes its function type first; it does not infer an inline
lambda's result type backward from the application result. Give such a lambda
an explicit function annotation (or annotate its literal body).
4. Effects, totality, and evaluation-order rules#
Pure, total, no effects. A literal scrutinee under nat-eliminate steps like its
unary form, so elimination is O(n); a literal is otherwise a value.
5. Elaboration into existing core or a specifically versioned new core extension#
Nat literals elaborate to RNatLiteral n (Alpha.Core naturalLiteral), using
alpha-checked-interface-v4 (v3 readers retained). Fixed-width literals elaborate
to existing Byte/word constructors from Std.Word; no new word core node or
serialization tag is introduced. Signed values use two's-complement bytes only
after the mathematical signed range has been checked.
6. Representation and target support, where relevant#
A compact literal is one core node regardless of magnitude. It erases to the existing UNARY runtime representation (ALRI v4 unchanged); arbitrary-precision runtime naturals remain out of scope. Word literals use the existing fixed-width byte records and execute through the existing x86-64 lane.
7. Error codes and primary/secondary origins#
ALPHA-PARSE-NAT-LITERAL-TOO-LARGE (over 4096 digits), ALPHA-PARSE-NAT-LITERAL
(missing literal), ALPHA-LITERAL-BAD-SEPARATOR, ALPHA-LITERAL-MISSING-DIGITS,
ALPHA-LITERAL-OUT-OF-RANGE, ALPHA-LITERAL-NEEDS-TYPE, and
ALPHA-EDITION-UNSUPPORTED-FORM under a non-draft edition. Primary origin is
the complete literal token, including its sign; CLI declaration ownership is
resolved from parsed source spans.
8. Formatting and migration rules#
Formatting preserves the literal lexeme, including radix, separators and sign.
The closed-natural-to-literal migration rewrites the explicit Nat head to bare
syntax; use it only where the expected type preserves Nat semantics. There is
no alpha-2026 migration because the syntax does not exist in that edition.
9. Positive, negative, execution, and edge-case tests#
tests/language/NatLiteralCompact.alpha (giant literal is one node; mixed
succ (nat-literal 4) ≡ nat-literal 5); debug/nat-literal-check.py (bounded
work for 10^3..10^12, the 4097-digit reject, the negative equality control); the
alpha-core kernel unit tests (literal↔unary, elimination parity).
debug/literal-typing-check.py checks all word boundaries against independently
constructed byte records through actual native execution, exact refusal spans,
formatting and edition rejection. debug/integer-literal-owner-check.py tests
the separate Alpha component against Python-derived bytes and failure tags.
The erased type-alias regression is tests/language/literals/ErasedTypeAlias.alpha;
its pre-change refusal is retained alongside L11s evidence.
10. Compatibility with the old edition, serialized forms, and cache keys#
The head exists only in alpha-2027; alpha-2026 is unchanged. Serialized cores
carrying a literal are alpha-checked-interface-v4.
Decimal (floating-point) spelling (L12b) — the same token family, typed by an expected F32/F64#
Token-level literal spellings are documented under this head by the L10/L11s precedent (the form inventory enumerates parser heads, not tokens). Suite:
reference/numeric/float-literal-kat.tsvthroughdebug/float-literal-check.py(in the gate).
1. Lexical and grammar rules, including precedence and termination#
[-]digits.digits, [-]digits[.digits]e[-]digits (E accepted). The exponent digits are
mandatory (1e is ALPHA-LITERAL-MISSING-DIGITS); 1. is not a decimal (the . stays
the lambda dot). Digit separators are not part of this form. Draft edition alpha-2027 only
(ALPHA-EDITION-UNSUPPORTED-FORM under alpha-2026). The significand is bounded like a
compact natural (≤ 4096 decimal digits, ALPHA-PARSE-NAT-LITERAL-TOO-LARGE).
2. Scope and binding rules, including generated names#
A leaf; binds nothing.
3. Type and quantity requirements#
Requires an expected type that is definitionally Data.Float32Bits.InferenceFloat32 (F32)
or Model.Parameter.ModelFloat64Bits (F64), through any alias; any other expected type, or
none, is ALPHA-LITERAL-NEEDS-TYPE. No quantity constraints.
4. Effects, totality, and evaluation-order rules#
Pure; a value. The conversion is exact rational round-to-nearest-even performed ONCE at
elaboration (Alpha.Surface.DecimalLiteral, no host floating point): subnormals and
underflow-to-zero by the same rule (below half the smallest subnormal → zero; exactly half → tie
→ even → zero); finite overflow is ALPHA-LITERAL-OUT-OF-RANGE. -0.0 keeps its sign bit.
5. Elaboration into existing core or a specifically versioned new core extension#
Elaborates to the EXISTING constructor application InferenceFloat32Bits b0 b1 b2 b3 /
ModelFloat64BitsValue b0 … b7 (little-endian byte literals). No new core node.
6. Representation and target support, where relevant#
The record is ordinary runtime data (four or eight bytes) on every lane; arithmetic on it is L13.
7. Error codes and primary/secondary origins#
ALPHA-LITERAL-OUT-OF-RANGE (finite overflow), ALPHA-LITERAL-NEEDS-TYPE (no float expectation),
ALPHA-LITERAL-MISSING-DIGITS (1e), ALPHA-EDITION-UNSUPPORTED-FORM (alpha-2026), all at the
literal's span.
8. Formatting and migration rules#
Printed from the source spelling (the inspect name is <digits>e<exponent>); no migration from
alpha-2026 (the form did not exist).
9. Positive, negative, execution, and edge-case tests#
debug/float-literal-check.py (in the gate): every finite row of the KAT as a refl law against its
record (both formats), every overflow row a negative module, the needs-type / missing-digits /
alpha-2026 rejections, a wrong-byte control, and a literal program built and executed. Bootstrap
tests in alpha-surface (front matter). The N5 .alpha specification converter is L12c.
10. Compatibility with the old edition, serialized forms, and cache keys#
alpha-2026 corpus unchanged. No serialized-form change (existing constructors).