Alpha-Haskell Language Specification

Status: normative for the Phase 0 bootstrap language

PRD identity: sha256:255c1b4861512fb715368799a0ab1d63aacb82fae6352a2aff0a2f50bd2f091c

1. Scope and conformance

Alpha-Haskell is the sovereign, dependently typed source language of the Alpha learning compiler. This document specifies the language that the trusted kernel accepts today. It does not describe planned syntax as if it were implemented.

A conforming implementation MUST:

parse source into a span-carrying surface tree without executing it;
elaborate names to de Bruijn indices before trusted checking;
accept a term only when the trusted kernel infers or checks its type;
enforce runtime quantities in the kernel, not as a lint;
normalize terms before deciding definitional equality;
represent effects explicitly in computation types;
reject unmarked divergence from the total fragment;
preserve proof and runtime identities through typed witnesses;
fail closed when a required proof, target, dataset, checkpoint, or device witness is absent; and
provide no host implementation as a fallback for a target operation.

The trusted source boundary is Alpha.Core.Trusted.*. Surface parsing, diagnostics, elaboration, target lowering, scheduling, package management, and runtime submission are untrusted in the proof-theoretic sense: their products must be checked by a smaller trusted boundary before they gain authority.

2. Lexical grammar

Source bytes must be canonical UTF-8. Outside quoted literals and comments, characters are ASCII; token separators are space, tab, LF, and CR. A line comment begins with -- and ends at newline or end of input. Non-ASCII whitespace is not a token separator. Other ASCII control bytes are payload only inside literals and comments; raw CR/LF remain forbidden in quoted literals.

Identifiers begin with an ASCII letter or _; subsequent characters may also be decimal digits, ', -, /, or .. let* is one reserved form head; * is not an identifier character. Natural literals are non-negative decimal integers. Punctuation is (, ), :, ., =, and the bind arrow <-.

Every token and surface term carries a half-open source span containing byte offset, one-based line, and one-based column positions. A lexical or parse failure is a structured Diagnostic with a stable code and a parse proof obligation.

3. Surface grammar

The implemented generation-zero grammar is prefix S-expression syntax:

term ::= identifier
       | "Type" natural
       | "Nat"
       | "zero"
       | "(" "succ" term ")"
       | "(" "Fin" term ")"
       | "(" "fzero" term ")"
       | "(" "fsucc" term term ")"
       | "(" "app" term term+ ")"
       | "(" "first" term ")"
       | "(" "second" term ")"
       | "(" "pair" term term term ")"
       | "(" "equal" term term term ")"
       | "(" "refl" term term ")"
       | "(" "transport" term term term ")"
       | "(" "pi" quantity identifier ":" term "." term ")"
       | "(" "lambda" quantity identifier ":" term "." term ")"
       | "(" "sigma" quantity identifier ":" term "." term ")"
       | "(" "effects" effect* ")"
       | "(" "computation" term term ")"
       | "(" "partial" term ")"

quantity ::= "erased" | "affine" | "linear" | "unrestricted"

effect ::= "State" | "Random" | "Device" | "File" | "Network"
         | "Divergence"

Application arity (reconciled 2026-09-03, LP-102). app is n-ary in the surface language: (app f a₁ a₂ … aₙ) with n ≥ 1 is a left-associated sugar that elaborates to nested binary core applications application (… (application (application f a₁) a₂) …) aₙ. The core (§4) keeps application f x strictly binary. A surface app with fewer than two operands is the hard error ALPHA-PARSE-APP. The earlier text declared app binary while the implemented parser (explicitApplication) has always folded extra operands; the corpus relies on the n-ary form pervasively, so the specification now records the implemented rule. Consequence for authors: an n-ary app supplies every trailing operand to the head — a helper-chain whose links are written as sibling operands instead of nested applications is grammatically valid but semantically over-applied (the "flattened chain" defect class); see debug/scan-flattened-chains.py.

3.1 Extended surface forms (reconciled 2026-09-03, LP-103)

The implemented parser accepts the following forms beyond the generation-zero grammar above. They are implemented and accepted; their edition status (stable / experimental) is assigned by the alpha-2026 edition manifest (LP-105), not here. The normative per-form table — head, arity, surface constructor, and the core builder it elaborates to — is generated from the sources at docs/generated/ALPHA-LIVE-FORM-INVENTORY.md (§ "Reconciliation table") by debug/form-inventory.py; this section is a grouped summary of that excerpt and must not be edited by hand where they disagree. A head that appears in the parser but not in that table is a specification defect.

Naturals: (nat-eliminate motive zeroCase successorCase scrutinee) (arity 4, core RNatEliminate); (nat-less-than a b) (2, RNatLessThan); (nat-to-byte n) (1, RNatToByte); draft edition alpha-2027 only (L12k, PRD 08 N1): (nat-add a b), (nat-multiply a b), (nat-subtract a b), (nat-divide a b), (nat-modulo a b) (2, core RNatAdd / RNatMultiply / RNatSubtract / RNatDivide / RNatModulo) — natural arithmetic: each folds to a compact literal in O(digits) when both operands are closed naturals; subtraction saturates at zero, x / 0 = 0, x mod 0 = x (total, stated); an open operand leaves the node neutral in the normaliser, and erasure emits a RUNTIME node (RuntimeNatAdd … RuntimeNatModulo, opcodes 0x32–0x36) that the evaluator lane executes in one machine operation on 64-bit words — add and multiply trap on overflow exactly as succ does (coppelius D21, 2026-09-16; before that erasure refused an unfolded node and no lane executed it).
Decimal literals (draft edition alpha-2027, L12b): the token [-]digits.digits / [-]digits[.digits]e[-]digits (E accepted; exponent digits mandatory — 1e is ALPHA-LITERAL-MISSING-DIGITS; 1. is not a decimal) has NO type of its own: at an expected type definitionally Data.Float32Bits.InferenceFloat32 (F32) or Model.Parameter.ModelFloat64Bits (F64) it elaborates to that family's constructor record holding the exact round-to-nearest-even bits (one rounding, rational arithmetic; subnormals and underflow by the same rule; -0.0 keeps its sign); finite overflow is ALPHA-LITERAL-OUT-OF-RANGE; any other expected type, or none, is ALPHA-LITERAL-NEEDS-TYPE. An integer spelling at F32/F64 converts the same way. NaN and the infinities are never literals (Std.Float names them).
Bytes and byte: Byte, Bytes (types); (byte n) and (bytes b…) (literals, core RByteLiteral / RBytesLiteral); (byte-to-nat b) (1); (byte-equal a b), (byte-less-than a b) (2); (bytes-cons b bs), (bytes-append x y), (bytes-equal x y), (bytes-set-index bs i), (bytes-index-nonzero bs i) (2); (bytes-set-free-index bs i depth offset) (4); (bytes-length bs), (bytes-head bs), (bytes-tail bs), (bytes-checksum bs) (1); (bytes-eliminate motive emptyCase consCase scrutinee) (4, RBytesEliminate).
Bytes builder: (bytes-builder-empty) (0), (bytes-builder-chunk bs) (1), (bytes-builder-append l r) (2), (bytes-builder-build builder) (1), and (runtime-image-v4-build builder) (1, RRuntimeImageV4Build).
Computations and effects: (effect-row) (the effect-row type, 0, REffectRowType); (return effects value) (2, RReturn); (bind effects result first continuation) (4, RBind); draft alpha-2027 (do effects result (name <- computation) (computation)... (return value)) lowers to nested RBind/RReturn with the same row. A named step may state its quantity before the name; shorthand is unrestricted. See the do contract; (read-file path) (1, RReadFile); (write-file path contents) (2, RWriteFile).
Let: (let quantity name [: annotation] = value in body) (binder form, core RLet). The quantity is mandatory; omitting it is the hard error ALPHA-PARSE-QUANTITY. Draft alpha-2027 also accepts (let* (quantity name [: annotation] = value)+ in body), which lowers to nested RLet without substitution. See the let* contract.
Families and eliminators (structured forms, own parsers): (family F args…) (RFamilyApplication); (constructor F C args…) (RConstructorApplication); (eliminate F motive scrutinee (branch C binders… . body)…) (REliminate, branches exhaustive and in declaration order); branch is not a top-level form. Draft alpha-2027 additionally accepts named single-constructor record sugar: (record F (field = value)+), (project F field value), and (update F value (field = replacement)+). These elaborate respectively to the existing RConstructorApplication and REliminate core forms; they add no core constructor or serialized format. The normative contract is records. It also accepts readable exhaustive matching: (match F scrutinee (case C fields... [(ih induction)] . body)...) infers a constant motive from the expected result, while (match-with F motive scrutinee cases...) supplies the motive. Both lower to the existing REliminate; constructor order and hidden arities come from the checked family. The normative contract is matching. case is structural only within those forms, and ih is structural only as an induction-hypothesis marker immediately after the corresponding recursive field binder.

Indexed-family declarations are module declarations checked by the same trusted inductive-family kernel used by the typed construction API. A family block uses family <name> : Type <level>, followed by ordered parameter, index, constructor, field, recursive, recursive-index, and result records, and terminates with end-family. Families precede value definitions, recursive occurrences are explicit, and only imported families enter a module's scope. Malformed order, missing terminators, duplicate or ambiguous families, non-positive fields, incomplete index results, and ill-typed telescope entries are hard errors. Eliminators retain exhaustive ordered branch checking.

Draft alpha-2027 quoted token forms

The text-literal token "…" denotes validated UTF-8 Text; the byte-string-literal token b"…" denotes exact Bytes. These are atomic tokens, not parenthesized heads, and are unavailable in alpha-2026. Their complete draft contracts are Text and Bytes. Neither extends the core constructors. Whole-source UTF-8 validity and half-open byte spans apply before parsing; human columns count scalars and LSP positions use its negotiated encoding. See the contracts for current qualification limits.

4. Core terms

The trusted core uses de Bruijn indices and contains exactly these forms:

variable i                 universe l
Nat                        zero
successor n                Fin n
finite-zero n              finite-successor n i
Pi q name A B              lambda q name A body
application f x            Sigma q name A B
pair SigmaType x y         first pair
second pair                equal A x y
reflexive A x              effect-row effects
transport motive proof x   effect-row effects
computation effects A      family F arguments
constructor F C arguments  eliminate F motive branches scrutinee
partial-computation C

Universe levels and variable indices are non-negative. Names are canonical ASCII identifiers. Effect rows are sorted and contain no duplicates.

4.1 Extended core forms (reconciled 2026-09-03, LP-103)

The block above is the generation-zero subset of the trusted core. The normative core is the RawTerm type in packages/alpha-core/src/Alpha/Core/Trusted/Syntax.hs, which has 57 constructors; every form listed above has its constructor (the generated inventory reports 0 §4 forms without one), and the kernel adds the following 33, each the elaboration target of a §3.1 surface form:

Naturals: RNatEliminate, RNatLessThan, RNatToByte.
Byte: RByte, RByteLiteral, RByteToNat, RByteEqual, RByteLessThan.
Bytes: RBytes, RBytesLiteral, RBytesCons, RBytesAppend, RBytesEqual, RBytesSetIndex, RBytesSetFreeIndex, RBytesIndexNonzero, RBytesLength, RBytesHead, RBytesTail, RBytesChecksum, RBytesEliminate.
Bytes builder: RBytesBuilder, RBytesBuilderEmpty, RBytesBuilderChunk, RBytesBuilderAppend, RBytesBuilderBuild, RRuntimeImageV4Build.
Binding and computation: RLet, REffectRowType, RReturn, RBind, RReadFile, RWriteFile.

The authoritative, always-current list is generated at docs/generated/ALPHA-LIVE-FORM-INVENTORY.json (diff.kernel_constructors_beyond_spec_core); a kernel constructor absent from this section is a specification defect, and a section entry absent from the kernel is an unimplemented core form and must carry an explicit status.

5. Universes and dependent types

Type l : Type (l + 1). Nat : Type 0 and Fin n : Type 0 when n : Nat. The universe of a dependent function or pair is the maximum of its domain and codomain levels.

Pi q x : A . B classifies functions whose argument has quantity q. Sigma q x : A . B classifies dependent pairs. Application substitutes the argument into the codomain. The type of second p substitutes first p into the pair codomain.

Equality is intensional in the primitive core. If x : A, then refl A x : equal A x x. Type checking uses definitional equality after normalization; it does not trust surface spelling or pointer identity.

Byte : Type 0 contains exactly the values 0 through 255. Bytes : Type 0 is the finite sequence of bytes. byte-to-nat, byte-equal, and byte-less-than are total; equality and unsigned ordering return the canonical Nat booleans zero and succ zero. bytes-eliminate is the dependent, structurally total eliminator for byte sequences. These operations remain in runtime erasure when their operands are not definitionally static.

If p : equal A left right, motive left : Type l, motive right : Type r, and value : motive left, then transport motive p value : motive right. Motive and proof are erased runtime positions. Transport over reflexivity reduces definitionally to value.

6. Quantities

Quantities are runtime-use contracts:

Quantity	Required runtime use
`erased`	exactly zero
`affine`	zero or one, never captured
`linear`	exactly one, never captured
`unrestricted`	any number

Type-only positions do not consume a value. Runtime branches are analyzed as alternatives: their minimum and maximum usage bounds are joined. Capturing an affine or linear value in a nested lambda is rejected. Constructor recursive fields account for the consumption required by structural recursion.

Quantity checking is part of trusted type checking. A backend is not allowed to weaken it, and a failed quantity proof cannot become a warning.

7. Indexed inductive families

A family definition contains parameters, indices, a result universe, and an ordered constructor set. A constructor contains ordinary value binders, strictly positive recursive fields, and result indices.

The family checker MUST establish:

unique family and constructor names;
well-formed parameter, index, value, and recursive telescopes;
constructor result indices with the declared family arity;
strict positivity of recursive occurrences;
complete, ordered eliminator branches;
exact branch arities; and
branch result types obtained from the motive.

An eliminator first checks that the scrutinee has the named family, checks every constructor branch, and returns the motive applied to the scrutinee indices and the scrutinee itself.

8. Totality and divergence

The primitive total fragment has no general fixpoint, exception, foreign call, or bottom constructor. A kernel-checked primitive term is total unless it contains partial-computation.

Structural recursion is authorized by a StructuralTotalityCertificate. There must be exactly one recursion clause for every constructor, no unknown clause, and every recursive call must target a recursive field recognized by the checked family. Missing, duplicate, unknown, or non-structural calls are hard errors.

Potential divergence is explicit. partial C is accepted only when C is a computation whose effect row contains Divergence. The totality certifier rejects every term containing this marker.

9. Effects

The effect-label vocabulary is:

State Random Device File Network Divergence

effect-row is the kind of effect rows. (effects File) is a closed row and (effects File : e) extends the row variable e with File. Row variables are ordinary dependently bound terms whose type is effect-row; substitution flattens nested rows, removes repeated labels, and restores canonical label order. Consequently functions may quantify over an effect row and preserve or extend it without enumerating the caller's remaining effects.

computation E A is well formed only when E : effect-row and A is a type. Effects are represented in types; no operation may perform an unreported device, file, network, random, state, or divergent interaction.

The bootstrap computation terms are:

return E value
bind E result-type first continuation
read-file path
write-file path contents

return E value has type computation E A when value : A. bind requires its first operand to have type computation E A and its continuation to have type A -> computation E B; its result is computation E B. The continuation binder may use any declared quantity, which the kernel enforces. Both operands must use the same canonical effect row. read-file requires a Bytes path and has type computation (effects File) Bytes. write-file requires Bytes path and contents and has type computation (effects File) Nat, where the result is the number of bytes written. Embedded NUL bytes in a path are rejected by native lowering rather than truncating the path.

The production x86-64 lowering implements supported closed File computations with project-encoded Linux openat, read, write, close, and exit syscalls. Reads loop until EOF. Negative syscall results terminate with a hard failure status. Unsupported computation shapes and non-File rows are compiler errors; they are never interpreted by the bootstrap host.

For read-file input >>= \contents -> write-file output contents, native lowering preserves sequencing: it reads the complete input before opening the output. A direct anonymous mmap buffer starts at 65,536 bytes and grows by checked doubling through mremap; output handles partial writes, and the buffer is released with munmap. Equal input/output paths are rejected because the current filesystem model does not yet define an atomic in-place rewrite.

The bootstrap compiler also lowers canonical structurally total byte folds. Byte predicates are compiled from byte-equal, unsigned byte-less-than, canonical Nat booleans, and total Nat-eliminator conditionals into direct x86-64 comparison and branch instructions. A canonical Bytes filter compacts accepted bytes in source order in the owned input buffer before opening the output, then uses the same complete partial-write and cleanup contract. The compiler accepts only the checked fold shapes it can preserve exactly; an unrecognized predicate, accumulator, capture, or transformation is a compiler error rather than permission to interpret it on the host.

A canonical balanced-delimiter fold is the first parser-state lowering. It scans the owned input buffer from right to left, matching the structural order of bytes-eliminate, and encodes state as zero for an unmatched open/error, succ zero for balanced input, and larger naturals for unmatched closing depth. The open and close bytes are recovered from the checked Alpha fold and must be distinct. This is a bounded bootstrap parser primitive, not evidence of a complete parser or self-hosting compiler.

Canonical adjacent-run compression is represented as a nested, structurally total Bytes elimination: the outer fold examines the first byte of its already-compressed suffix and retains a new head only when it differs. Native lowering compacts the owned buffer in place. When its source is a canonical byte-map fold, classification and compression are fused into one scan while preserving the pure Alpha result byte-for-byte. This produces a token-kind run stream but does not retain identifier spelling or constitute the full Alpha lexer/parser required for self-hosting.

A canonical normalization fold may replace every byte accepted by a total predicate and collapse adjacent replacement runs. The native implementation retains all rejected bytes exactly and in source order, so whitespace normalization preserves identifier and keyword spelling while producing stable boundaries. The predicate and replacement byte are recovered from both checked branches and must agree; mismatched or non-canonical folds fail closed.

The vocabulary is intentionally small in the bootstrap. Extending it changes the language and trusted checker and therefore requires a versioned specification change, tests, and a bootstrap-identity update.

10. Elaboration and diagnostics

Surface names are elaborated to de Bruijn indices. Elaboration rejects unbound names, duplicate binders where prohibited, invalid universes, and every core construction that the trusted checker rejects. Diagnostics carry:

a stable ASCII code;
the source span;
a human-readable explanation; and
an optional typed proof obligation.

Error recovery may collect independent diagnostics, but it MUST NOT emit an authoritative checked term for an ill-typed subtree.

A module build is an ordered, non-empty sequence of named modules. Imports may resolve only definitions exported by earlier modules in that sequence. The final module must contain exactly one checked main; it alone determines the native program result. Empty builds, unresolved or forward imports, ambiguous names, missing main, and multiple final main definitions are compiler errors. Module composition does not authorize host-language evaluation or a fallback interpreter.

A value definition begins with def <name> [ : <type> ] =. Its body may begin on that line or on a later physical line. Parenthesized terms continue until their delimiter depth returns to zero; an atomic body on the following line is one complete term. Delimiter depth, not indentation or a host-language parser, determines continuation. An unmatched close, end of input with an unfinished body, or a new top-level declaration encountered before closure is a hard module error. The definition source span covers every consumed physical line.

11. Runtime witnesses

Configuration, target, dataset, and checkpoint facts cross into compiled code only as VerifiedFactPackage values. Each package existentially binds a type-level identity to:

a singleton fact kind;
a canonical non-empty ASCII identity;
a schema version proven to be at least one; and
a non-empty byte payload.

The identity cannot be swapped after verification because the witness, proof, and payload share the same type-level symbol. Runtime facts are evidence, not ambient strings.

12. Target and no-fallback contract

Target-specific operations require a target witness and must lower to a declared target program. On NVIDIA SM86, the production path is generated machine code submitted through the native runtime. A missing kernel, unsupported shape, failed proof, allocator exhaustion, launch fault, or device mismatch is an error. It is never permission to run a host implementation.

Reference interpreters and scalar models are test or proof oracles only. They must be invoked explicitly, must be labelled as non-production, and cannot be reachable from a production target dispatch.

12.1 Proof erasure artifact

After kernel checking, eraseChecked lowers a checked term to RuntimeTerm. The runtime data type contains variables, natural constructors, bytes and byte constructors, runtime lambdas/applications, retained pair fields, projections, constructors, eliminators, computation return/bind nodes, File read/write nodes, and explicit partial computation. It has no universe, type, equality, reflexivity, motive, effect-row, or proof constructors. Computation effect and result types erase, while effectful operations remain explicit so later stages cannot lose or invent an interaction.

Quantity-zero lambdas and arguments are removed. Equality transport erases to the transported runtime value. Attempting to use an erased de Bruijn slot in a runtime position is a hard ErasedVariableUsedAtRuntime error. Runtime terms have a deterministic length-framed binary encoding; this encoding, not a GHC closure or Show representation, is the artifact presented to later compiler stages.

The bootstrap verifier rejects Unsafe.Coerce, unsafeCoerce, unsafePerformIO, unsafeDupablePerformIO, and unsafeInterleaveIO anywhere in the Haskell source tree. Core, proof, and surface packages compile under Safe Haskell with unsafe-module warnings promoted to errors.

13. Bootstrap identity

The Phase 0 bootstrap is identified by:

this specification;
the authoritative PRD;
the trusted core, proof, and surface sources;
their Cabal package descriptions;
GHC 9.10.3;
cabal-install 3.12.1.0; and
the x86_64-linux bootstrap host.

bootstrap/verify.sh checks that identity without network access. Any byte change to an identified input invalidates the bootstrap manifest and requires a deliberate regeneration with new evidence.

14. Versioning rule

This document is normative only for the manifest that hashes it. Language extensions require a new manifest. Backward compatibility must be explicit; unknown syntax, effects, proof forms, runtime schemas, and target operations fail closed.