The Alpha language and why it exists

Current system target: SOVEREIGN-LEARNING-SYSTEM-TARGET.md uses this handbook as its practical source-writing guide while taking the current compiler through self-hosting, native training, reload, and hello.

Status: comprehensive explanatory handbook for the current repository

Last researched against the Alpha repository: 2026-08-28

Repository: https://github.com/thomasdavis/alpha

Research baseline: Git 751ae75 plus the active 2026-08-28 worktree; only source-confirmed behavior is described as implemented, and uncommitted work is not treated as promoted evidence.

Normative language contract: docs/language/SPECIFICATION.md

Authoritative product direction: docs/PRD.md

Executable evidence state: docs/REBUILD-STATUS.md

1. Read this first

Alpha is a programming language, a compiler written in that language, and a long-term attempt to own the complete path from a checked learning-system description to the CPU and GPU instructions that execute it.

The shortest accurate description is:

Alpha is a project-authored, dependently typed, quantity-aware, effect-tracked language designed to express and compile complete learning systems. The Alpha compiler is being written in .alpha so it can eventually rebuild itself, emit its own native code, and remove GHC Haskell from the production dependency graph without replacing it with another hidden compiler or framework.

That sentence contains several separate goals. They must not be collapsed:

1. .alpha source exists for a compiler.
2. A trusted bootstrap compiler parses and checks that source.
3. The bootstrap compiler produces a working Alpha compiler.
4. The produced compiler compiles the identical source again.
5. successive compiler generations reach a canonical fixed point;
6. a manifest-bound seed can rebuild the current compiler without GHC;
7. the production compiler uses direct specialized native code rather than a generic embedded graph evaluator; and
8. that compiler can describe, compile, train, checkpoint, resume, evaluate, and run architecture-neutral learning systems.

Each item requires its own evidence. A historical fixed point does not prove a changed compiler generation. An ELF file is not automatically direct AOT code. A process consuming CPU is not proof that it advances. A type-shaped value called a certificate is not automatically a checked proof.

This handbook explains the language and the project at all of those levels. It is intentionally more approachable than the normative specification and more language-focused than the product requirements document. It does not silently change the language. If this guide conflicts with the manifest-bound specification or the trusted checker, stop: reconcile the implementation and version the specification deliberately.

2. What “Alpha Haskell” means

The project uses the name Alpha Haskell for the .alpha language. This is not ordinary Haskell source syntax and it is not a dialect accepted by GHC.

There are currently two Haskell levels:

The distinction is architectural, not cosmetic. New production compiler behavior belongs in .alpha. GHC Haskell exists temporarily to bootstrap and independently check the language while Alpha learns to build itself.

The desired final statement is not “there are no .hs files in Git.” It is:

The current production Alpha compiler can be rebuilt from an auditable, content-addressed seed without GHC, Cabal, libc, LLVM, a C compiler, an external assembler, or a vendor compilation runtime.

Haskell source may still remain as archived lineage, a deliberately independent oracle, a differential test implementation, or migration tooling outside the production dependency graph. Deleting every .hs file before the bootstrap exit is proven would remove the bridge and the independent witness at the same time. That would reduce confidence rather than increase sovereignty.

3. Why Alpha exists

3.1 The ordinary learning stack hides too much

A typical learning system relies on a tower of separately owned components:

model framework
  -> dynamic tensor graph
  -> graph compiler
  -> vendor compiler/runtime
  -> generated kernels
  -> memory allocator and command runtime
  -> device driver
  -> firmware and hardware

Types, shapes, layouts, differentiability assumptions, memory ownership, effects, numerical approximations, and target capabilities are often checked at different layers—or remain conventions in comments and tests. A fallback may silently move work to the host, change precision, change shape, or select a different implementation.

Alpha’s response is to make the important facts part of the program and its checked transformation path. The intended compiler owns:

• the source language and trusted dependent core;
• quantitative resource use and explicit effects;
• proof erasure and closure conversion;
• semantic, learning, operator, schedule, memory, and target IRs;
• x86-64 and accelerator instruction encoding;
• ELF and accelerator image construction;
• Linux syscall and exact device ABI boundaries;
• static memory plans, command streams, synchronization, and evidence;
• training, checkpointing, resume, evaluation, and inference artifacts.

The unavoidable external floor is the operating-system kernel, device kernel module, firmware, and physical CPU/GPU/storage/network hardware.

3.2 Learning systems are broader than tensors and Transformers

Alpha is deliberately not founded on a tensor operation, GEMM, a model family, reverse-mode AD, NVIDIA, or SM86. Those are important libraries, transforms, or targets, but none is the semantic root.

The language and IR architecture are intended to represent, without changing the trusted core:

• feed-forward and recurrent systems;
• scans and state-space systems;
• convolutional and spectral systems;
• sparse, graph, and event-driven systems;
• fixed-point and differential-equation systems;
• stochastic and diffusion systems;
• energy-based and implicit systems;
• reverse-, forward-, and mixed-mode differentiation;
• local, multi-phase, perturbation, population, and black-box learning;
• alternative algebras, including multiplication-light systems.

GEMM, attention, routed feed-forward layers, and Transformers should emerge as libraries over typed operators. They must not become privileged assumptions in the kernel.

3.3 Proof carrying does not mean “everything is theorem-proved”

Alpha separates several kinds of confidence:

• type and effect correctness;
• resource and ownership correctness;
• semantic preservation across compiler passes;
• numerical preservation under a named contract;
• physical execution on an exact target profile;
• performance qualification;
• empirical model quality.

A type proof cannot show that an RTX 3090 achieved a measured throughput. A benchmark cannot prove that erasure preserved semantics. A successful training run cannot prove compiler self-host identity. Alpha keeps those evidence kinds distinct and promotes an artifact only when the required combination is bound to the exact source, compiler, proofs, target, and data.

4. What Alpha is—and is not

Alpha is:

• a small ASCII source language with prefix S-expression terms;
• dependently typed, with universes, dependent functions, dependent pairs, equality, and indexed inductive families;
• quantity-aware, distinguishing erased, affine, linear, and unrestricted binders;
• effect-tracked, with explicit computation types and effect rows;
• total by default, with divergence explicit in the type;
• proof-erasing, so type/proof material need not survive into hot execution;
• strict about unsupported operations and missing evidence;
• intended to compile itself and then compile complete learning systems.

Alpha is not:

• GHC Haskell with different file extensions;
• an indentation-sensitive language;
• a general Lisp with runtime macros and dynamic lists;
• a wrapper around GHC, LLVM, CUDA, Vulkan, Triton, or an external assembler;
• a tensor library with dependent types added around it;
• a Transformer-specific compiler;
• a dynamic dispatch layer that may fall back to a host implementation;
• self-hosted merely because an old compiler generation reached a fixed point;
• complete merely because broad Haskell reference structures exist.

5. Current evidence boundary

This section is a navigation aid, not a timeless release claim. The executable status report remains authoritative.

As researched on 2026-08-28:

The repository contains far more source than those open gates imply. Alpha uses an evidence maturity ladder so “source exists,” “builds,” “locally tested,” “certificate checked,” “physically attested,” “functionally qualified,” “performance qualified,” “quality qualified,” and “promoted” remain different states.

6. A first .alpha module

Actual module syntax is line-oriented. Terms inside definitions use S-expressions.

module Tutorial.Identity

def identity : (pi unrestricted value : Nat . Nat) =
  (lambda unrestricted value : Nat . value)

def main : Nat =
  (app identity zero)

Read it as follows:

• module Tutorial.Identity names the module.
• def identity : ... = ... declares and defines a value.
• (pi unrestricted value : Nat . Nat) is the dependent function type. The result does not happen to depend on value, so it behaves like Nat -> Nat.
• (lambda unrestricted value : Nat . value) constructs the function.
• main is the final program entry.
• (app identity zero) applies the function.

The same application may be written in ordinary application form:

def main : Nat =
  (identity zero)

Explicit app is usually clearer in compiler source because it makes a large application recognizable. Both forms accept multiple arguments and elaborate left-associatively:

(app choose first second third)

means:

(((choose first) second) third)

7. Source-file and module grammar

7.1 File order

A module has this order:

module Qualified.Name
import Earlier.Module
import Another.Earlier.Module

family ...
  ...
end-family

def first = ...
def second : ... = ...

The rules are strict:

1. The first significant line is module <qualified-name>.
2. Imports come next.
3. Family declarations come after imports and before value definitions.
4. Definitions come last.
5. Definitions are visible top-to-bottom; do not rely on forward references.
6. Imported modules must already have been checked in the ordered build.
7. The final compiled module must expose exactly one main.

Blank lines and comment-only lines are ignored by the module parser. Indentation is for humans; parentheses determine expression structure.

7.2 Names

Module names are dot-qualified components such as Compiler.RuntimeLowering. Imported values may be referenced with a slash-qualified name:

Compiler.Codegen/compileClosedNaturalElaboration

Use qualified references whenever provenance or ambiguity is possible. An unqualified reference imported from two modules is rejected rather than chosen by import order.

Declaration names start with an ASCII letter or underscore. Subsequent source characters may include ASCII letters, digits, apostrophes, underscores, and hyphens. The trusted core applies its own canonical-name checks during elaboration, so portable production names should prefer letters, digits, underscores, and apostrophes.

7.3 Definitions

Annotations are optional:

def inferred = zero

def checked : Nat = zero

Without an annotation, the trusted kernel infers the type. With an annotation, the body is checked against it. An annotation is not a cast.

A body may start on the definition line or a later line. A parenthesized body continues until delimiter depth returns to zero:

def two : Nat =
  (succ
    (succ
      zero))

An atomic body on the next physical line is one term. A new top-level declaration cannot silently terminate an unfinished expression.

7.4 Comments and lexical form

• Source is ASCII.
• Whitespace separates tokens.
• -- starts a line comment.
• Punctuation is (, ), :, and ..
• Natural literals are non-negative decimal integers.
• There are no string literals; byte sequences are written explicitly.
• There is no infix precedence to memorize.

Every token and surface term carries a half-open source span with byte offset, line, and column information. Parser and elaborator failures carry stable diagnostic codes and, where applicable, proof obligations.

8. Complete implemented expression surface

The manifest-bound Phase-0 specification describes the stable language contract for its exact bootstrap identity. The trusted parser in the current tree accepts a larger compiler-oriented primitive surface. The table below is an implementation inventory, not permission to change the language without a versioned specification and bootstrap manifest.

In the forms below, t is a term, q a quantity, x a binder, F a family, C a constructor, and E an effect-row term.

8.1 Atomic terms

8.2 Natural and finite-number terms

Runtime booleans currently use naturals:

false = zero
true  = succ zero

This is a bootstrap representation, not a claim that every future Alpha data type should encode booleans this way.

8.3 Byte and byte-sequence terms

bytes-set-index grows the sequence with zero bytes when needed. bytes-set-free-index leaves locally bound indices untouched and marks the corresponding outer index after applying depth and offset. These are compiler-bootstrap primitives, not a recommended general collection API.

8.4 Byte builders and compiler-image construction

Builders exist so compiler-scale encoders can preserve ordered chunk structure without repeatedly appending large flat byte sequences during elaboration. runtime-image-v4-build is a compiler-image primitive, not a generic user serialization function.

8.5 Dependent functions, applications, and pairs

The result type of applying a dependent function is obtained by substituting the argument into its codomain. The type of second substitutes first p into the Sigma codomain.

The trusted core has an internal let term used by compiler transformations, but the current surface parser exposes no let syntax. Use named definitions or lambda application in .alpha source.

8.6 Equality and transport

Definitional equality is decided after normalization. It is not textual equality and not pointer identity. Transport over reflexivity reduces to the transported value. Proof terms can erase when their quantity and use permit it.

8.7 Families, constructors, and eliminators

Branches must appear in constructor declaration order, cover every constructor, and have the exact binder arity derived from the checked family.

8.8 Effects and computations

The fixed effect vocabulary is:

State Random Device File Network Divergence

Closed rows must be in that canonical order and contain no duplicates. For example, (effects State File) is canonical while (effects File State) is rejected. Open rows make effect-polymorphic functions possible:

(lambda unrestricted e : (effect-row) .
  (return (effects File : e) zero))

partial is accepted only for a computation type whose effect row contains Divergence. It is an explicit boundary, not a hidden bottom value.

9. Dependent types in practical terms

Ordinary types classify values. Dependent types may mention values, allowing a program’s structure and its evidence to remain connected.

9.1 Universes

Type 0 : Type 1
Type 1 : Type 2
...

Nat, Byte, Bytes, and checked families at level zero inhabit Type 0. The universe of a dependent function or pair is the maximum universe required by its domain and codomain.

9.2 Dependent functions

(pi unrestricted length : Nat . (family Vec length))

The returned type depends on length. A function of this type cannot return a vector of an unrelated length without the checker noticing.

9.3 Dependent pairs

(sigma unrestricted length : Nat . (family Vec length))

This packages a runtime length with a vector indexed by precisely that length. When the first field is projected, the type of the second field specializes to that value.

9.4 Runtime facts as dependent packages

Target, configuration, dataset, and checkpoint facts eventually cross into compiled code as verified packages. The identity, schema, witness, and payload are connected by the type so code cannot verify one identity and then silently substitute another payload.

That is the general pattern Alpha wants throughout the stack: dynamic facts are allowed, but they enter as an existential package carrying the witness and proof that make them safe to use.

10. Quantities are executable contracts

Every pi, lambda, sigma, family binder, and family field records a quantity:

These are checked by the trusted kernel. They are not comments and a backend cannot weaken them.

Examples:

-- The proof/type input is unavailable after erasure.
(lambda erased proof : (equal Nat zero zero) . zero)

-- The resource must be consumed exactly once.
(lambda linear resource : Resource .
  (app closeResource resource))

-- Ordinary reusable data.
(lambda unrestricted value : Nat .
  (app combine value value))

Type-only positions do not consume a runtime value. Runtime branches are alternatives: the checker joins their minimum and maximum use counts. A linear value must be used exactly once on every runtime branch. Affine and linear values may not be captured by nested lambdas.

Quantities are the foundation for making double release, use after release, duplicate permits, and pre-fence reads unrepresentable. The final memory and runtime APIs are expected to consume allocation, initialization, synchronization, readability, final-use, and release states linearly.

11. Indexed families and structural elimination

Families are Alpha’s module-level mechanism for defining algebraic and indexed data. The syntax is intentionally explicit so a small project-authored parser and checker can own it.

11.1 A simple family

family Flag : Type 0
constructor Off
constructor On
end-family

Values are constructed explicitly:

def enabled : (family Flag) =
  (constructor Flag On)

11.2 Fields and recursion

family Tree : Type 0
constructor Leaf
field unrestricted leafValue : Nat
constructor Fork
recursive unrestricted leftTree
recursive unrestricted rightTree
end-family

field introduces an ordinary constructor field with an explicit type. recursive introduces a strictly positive recursive occurrence of the family. The family checker rejects malformed telescope order, duplicate names, non-positive recursion, incorrect results, and invalid indices.

11.3 Indexed families

This is a length-indexed vector skeleton:

module Tutorial.Vector

family Vec : Type 0
index unrestricted length : Nat
constructor VNil
result zero
constructor VCons
field unrestricted prior : Nat
recursive unrestricted tail
recursive-index prior
result (succ prior)
end-family

def empty : (family Vec zero) =
  (constructor Vec VNil)

def one : (family Vec (succ zero)) =
  (constructor Vec VCons zero empty)

def main : Nat = zero

Important details:

• parameter values are uniform across the family.
• index values may vary by constructor and appear in the family result.
• recursive-index entries describe the indices of the immediately preceding recursive field.
• result entries describe the constructor’s resulting family indices.
• constructor arguments contain parameters, ordinary fields, and recursive values in the checked telescope order; result indices are established by the declaration rather than passed as arbitrary unchecked tags.

11.4 Eliminators and induction hypotheses

Alpha does not trust unchecked pattern matching. Surface branches elaborate to a checked eliminator with exhaustive constructor coverage and exact branch arity.

(eliminate Flag
  (lambda unrestricted value : (family Flag) . Nat)
  enabled
  (branch Off . zero)
  (branch On . (succ zero)))

For each constructor branch:

1. every ordinary field contributes one binder;
2. every recursive field contributes its recursive value binder; and
3. every recursive field also contributes one induction-hypothesis binder.

Therefore a constructor with two recursive fields contributes four branch binders even before ordinary fields are counted. This is why EliminatorBranchArity should be solved from the family declaration, not by guessing from a call site.

The motive determines the result type for every scrutinee. When the result depends on indices or the exact constructor value, write that dependency in the motive rather than trying to recover it after elimination.

12. Totality, recursion, and divergence

The primitive total fragment contains no general fixpoint, exception, foreign call, or bottom constructor. Normal programs are total unless divergence is made explicit.

Structural recursion is accepted through checked family structure. A structural totality certificate must have exactly one clause for every constructor, and recursive calls must target fields the family checker marked recursive. Missing, duplicate, unknown, or non-structural recursion is a hard error.

Potentially divergent work belongs in a computation with Divergence in its effect row:

(partial (computation (effects Divergence) Nat))

This boundary matters for compiler correctness. Total normalization and proof checking cannot quietly inherit an unmarked loop from a utility function.

13. Effects and explicit sequencing

Effects are represented in types rather than inferred from ambient host behavior.

def copyFile :
  (pi unrestricted inputPath : Bytes .
    (pi unrestricted outputPath : Bytes .
      (computation (effects File) Nat))) =
  (lambda unrestricted inputPath : Bytes .
    (lambda unrestricted outputPath : Bytes .
      (bind (effects File) Nat
        (read-file inputPath)
        (lambda unrestricted contents : Bytes .
          (write-file outputPath contents)))))

bind requires:

• an effect row E;
• the final result type;
• a first computation of type computation E A; and
• a continuation from A to computation E B.

The same canonical row is checked on both sides. A missing effect is a type error, not permission to perform it anyway.

The current production x86-64 lowering has a deliberately narrow, fail-closed File computation implementation. It uses project-encoded Linux syscalls, handles complete reads and partial writes, rejects embedded NUL path bytes, and reports unsupported computation shapes as compiler errors. Other effect labels are part of the type vocabulary and future architecture; their presence does not imply every runtime lowering exists today.

Paths are Bytes, not host-language strings. For example, /tmp/input is:

(bytes 47 116 109 112 47 105 110 112 117 116)

That representation is verbose by design in the bootstrap language. A future standard library may provide checked text and path constructors without moving string parsing into the trusted core.

14. Elaboration, checking, normalization, and erasure

These compiler stages answer different questions.

14.1 Parsing

Parsing converts source to a span-carrying surface tree. It proves only that the lexical and syntactic structure is accepted. Parsing does not prove names, types, quantities, effects, totality, lowering, or execution.

14.2 Elaboration

Elaboration resolves source names and converts binders to de Bruijn indices. Local names are therefore diagnostic labels; core variable identity comes from binding position. Module imports and earlier definitions provide the global environment.

Elaboration rejects:

• unbound or ambiguous names;
• invalid universes and byte literals;
• unknown families or constructors;
• malformed branches;
• terms the trusted kernel cannot infer or check.

14.3 Trusted checking

The kernel checks:

• universe formation;
• dependent application and pair projection;
• indexed family construction and elimination;
• definitional equality;
• branch-sensitive quantity use;
• canonical effect rows and computation sequencing;
• explicit divergence boundaries.

The trusted boundary lives under Alpha.Core.Trusted.* in the Stage-0 oracle. Parsing, diagnostics, optimization, scheduling, and lowering are untrusted in the proof-theoretic sense: their results require validation before they gain authority.

14.4 Normalization and definitional equality

The checker normalizes terms before deciding definitional equality. Current reductions include:

• beta reduction of lambda application;
• natural and byte-sequence elimination;
• primitive natural, byte, and byte-sequence operations;
• pair projections;
• transport over reflexivity;
• constructor elimination with generated induction hypotheses;
• flattening of canonical effect-row tails;
• flattening of statically known byte builders.

This makes terms equal because of their computation, not because their source spellings happen to match.

14.5 Type-directed erasure

After checking, Alpha lowers a checked term to a runtime term. The runtime form retains values and operations but removes material whose type proves it has no runtime representation.

Erasure removes:

• universes and type constructors;
• equality and reflexivity proofs;
• transport motives and proofs;
• effect-row and result-type annotations;
• erased lambda binders and erased arguments;
• erased family fields.

Erasure retains:

• runtime naturals, bytes, pairs, constructors, and eliminators;
• runtime lambdas, applications, and captured environments;
• File reads and writes;
• computation sequencing;
• explicit partial computations;
• runtime family fields and recursion evidence.

Trying to read an erased de Bruijn slot at runtime is ErasedVariableUsedAtRuntime, a compiler error. The eraser does not synthesize a placeholder value.

15. The compiler pipeline

The intended final pipeline is:

.alpha source
  -> span-carrying surface syntax
  -> name resolution and dependent elaboration
  -> checked Alpha Core
  -> type-directed erasure
  -> closure conversion
  -> typed control-flow IR
  -> typed System IR
  -> typed Learning IR
  -> typed Operator IR
  -> validated rewrites
  -> proof-carrying schedule and static memory plan
  -> typed target and machine IR
  -> x86-64 and accelerator instruction encoding
  -> ELF and accelerator images
  -> independently checked evidence

The current bootstrap path reaches native execution through a generic runtime graph and runtime image. That bridge is valuable but is not the final direct AOT architecture:

checked Alpha Core
  -> erased RuntimeTerm
  -> runtime graph envelope
  -> fixed runtime image
  -> project-generated native evaluator ELF

The direct-AOT destination removes per-node graph dispatch from the production compiler:

checked Alpha Core
  -> erasure
  -> explicit closure conversion
  -> defunctionalization where required
  -> typed CFG
  -> typed x86-64 machine IR
  -> direct instruction bytes
  -> static ELF

An ELF produced by the generic evaluator path is standalone native execution, but it is not yet evidence for the direct-AOT milestone.

16. The compiler written in .alpha

The active canonical source list is not every .alpha file in the repository. It is the ordered closure in scripts/lib/alpha-compiler-sources.sh. At the 2026-08-28 research snapshot it contained 40 files, approximately 31,000 lines, 209 families, 543 constructors, and 1,342 definitions. Those counts describe scale only; they are not acceptance evidence and will change.

16.1 Frontend

16.2 Trusted semantic structures

16.3 Module compilation

16.4 Runtime lowering and native artifacts

16.5 Durable compilation

16.6 Drivers

ModuleGraphDriver.alpha is the canonical compiler entry. It reads the bundled compiler source from a fixed path, compiles it, and writes the resulting ELF.

ModuleGraphPhaseDriver.alpha is a distinct diagnostic compiler entry. It adds progress, resume, checkpoint, and causal telemetry behavior. Its source closure and fixed-point identity are intentionally separate from the canonical compiler.

Diagnostic instrumentation must never silently change the canonical product.

17. Runtime graph and image boundary

The runtime graph is a deterministic, pointer-free execution IR between erased terms and the native evaluator.

Its core invariants are:

• node identifiers are contiguous and zero-based;
• every operand points to an earlier node;
• cycles and forward references are rejected;
• every node is reachable from the final root;
• opcodes and payloads are versioned and bounded;
• constructor roles and eliminator binder counts survive erasure;
• unsupported partial computation is rejected rather than executed by a host fallback.

The variable-length graph envelope is transformed into a fixed-record runtime image so native code can address records directly. Runtime aggregate values use relative arena offsets instead of host pointers. Validators check alignment, extent, overflow, tags, arity, and reserved words before values gain runtime authority.

The Stage-0 RuntimeMachine is a deterministic semantic oracle. It models closures, environments, naturals, bytes, pairs, families, eliminators, and virtual File effects with explicit fuel. It performs no host file I/O. Native differential tests compare the generated evaluator’s result and effects with this reference machine.

The graph evaluator remains a bootstrap bridge and oracle until the direct AOT compiler covers the compiler’s complete runtime subset.

18. Self-hosting, precisely

18.1 The stage sequence

For one frozen source generation:

Stage 0: pinned GHC-built bootstrap compiler
    |
    | compiles exact canonical .alpha source bundle
    v
Stage 1: Alpha-produced compiler
    |
    | compiles the identical source bundle
    v
Stage 2: successor Alpha-produced compiler
    |
    | compiles the identical source bundle
    v
Stage 3: another successor compiler

The fixed-point claim requires canonical identity across the accepted stages, after only explicitly documented canonicalization of permitted nondeterministic sections. Every stage must physically execute and consume the same ordered source identity.

18.2 Self-host levels

Never report only selfHosted = true. Report the level, exact generation, and evidence identities.

18.3 A compiler generation is a manifest, not a filename

A credible generation binds:

• repository and ordered module identities;
• per-module and complete bundle hashes;
• parent generation;
• canonical driver identity;
• proof-kernel and core-schema identity;
• runtime graph/evaluator identities while those remain;
• ALRI schema identity;
• target and ABI;
• Stage 0/1/2/3 hashes;
• invocation and environment;
• accepted certificates.

A file named alpha-compiler-x86_64.elf without those bindings is an artifact, not a current-generation self-host proof.

18.4 Historical proof versus current proof

The repository preserves a historical self-hosted seed and an earlier Stage-1/Stage-2 identity result. That is valuable evidence that the mechanism has worked for one exact historical source generation.

The compiler has since grown substantially. Current source must establish a fresh cycle. Reusing a historical output, passing --stage1-only, or comparing against an unbound seed cannot promote the current generation.

19. Removing GHC Haskell safely

“Remove Haskell” should mean remove ordinary GHC Haskell from the production bootstrap and execution dependency graph. It should not begin as a bulk deletion campaign.

19.1 What the Haskell tree currently contains

At the research snapshot, the repository had several distinct Haskell bodies:

The .alpha tree itself contained roughly 120 files and 40,000 lines at this snapshot, while the canonical compiler closure was the smaller ordered subset described earlier. The Haskell trees are still large because they combine the bootstrap, independent semantics, tests, and frozen legacy system. Raw line counts do not decide which dependency can be removed.

19.2 The safe exit sequence

The following order preserves the ability to prove what happened:

1. Freeze one current generation. Record the exact tree, canonical source closure, driver, schemas, toolchain, and proof-kernel identities.
2. Pass the complete fast gates. Parse, check, erasure-check, and lower the full canonical and diagnostic source closures.
3. Qualify durable resume. Force an interruption at a known declaration, resume from the exact checkpoint, and prove output identity with an uninterrupted run.
4. Produce current Stage 1. The pinned Stage 0 compiles the frozen canonical source and the output physically executes.
5. Produce Stage 2 and Stage 3. Each successor compiles the identical source with isolated inputs, outputs, telemetry, and manifests.
6. Establish canonical identity. Compare accepted compiler images under the documented canonicalization contract.
7. Promote a current seed. Bind the seed to the complete generation manifest and preserve recovery evidence.
8. Run the restricted no-GHC lane. Remove ghc, cabal, gcc, clang, as, and ld from PATH, disable the network, log every process, and rebuild the current compiler from the promoted seed.
9. Complete direct AOT. Lower the compiler’s entire runtime subset to typed control flow and direct machine code. Remove the generic graph evaluator from the production compiler path.
10. Establish diverse validation. Use independent checkers, differential semantics, negative programs, and a diverse bootstrap where practical.
11. Prune production dependencies. Only now remove GHC packages and build machinery from the release dependency graph.
12. Archive before deleting. Preserve the exact Stage-0 oracle and legacy source needed to audit historical generations, even if they leave the active production build.

19.3 What must be true before a Haskell component leaves

For each component, record:

• its production responsibilities;
• the .alpha modules that replace every responsibility;
• positive tests and forced negative tests;
• source/runtime semantic agreement;
• serialization and artifact compatibility;
• target lowering and physical execution where relevant;
• the exact generation that stopped depending on it;
• a recovery route if the new seed is lost or corrupt.

No component leaves merely because a same-named .alpha module exists. Replacement means the complete behavior is integrated, checked, exercised, and no longer reachable through the production dependency graph.

19.4 Why deleting the oracle too early is dangerous

A self-hosted compiler can reproduce the same bug forever. Fixed-point identity proves stability, not correctness. An independently structured oracle and negative corpus help distinguish “the compiler agrees with itself” from “the compiler preserves the intended language semantics.”

Sovereignty and independent validation therefore work together:

• the production artifact must not depend on GHC;
• the evidence program may deliberately compare against a frozen GHC oracle;
• neither implementation is accepted merely because it agrees with itself.

20. Resumability and telemetry are compiler semantics

The current compiler is large enough that a complete self-compilation can be a long-running operation. Treating it as one opaque process makes slow progress, a semantic loop, memory growth, and a dead process indistinguishable.

Alpha’s diagnostic compiler records:

• exact source, compiler, proof-kernel, schema, and driver identities;
• phase transitions;
• module numerator, denominator, and current module;
• declaration numerator, denominator, and current declaration;
• evaluator steps and compaction work while the evaluator remains;
• allocation, live bytes, peak bytes, RSS, and elapsed time;
• checkpoint encode, sync, promote, restore, and reject events;
• output paths, byte counts, hashes, exit status, and diagnostics;
• causal span entry/exit and parent relationships as the native protocol grows.

The Alpha program owns semantic progress markers. An observer may report them, but it may not invent progress from CPU use, wall time, a living PID, or file growth unrelated to a completed semantic unit.

20.1 Durable publication order

For a resumable transition:

compute pure next state
  -> encode checkpoint
  -> write complete candidate
  -> synchronize durable data
  -> atomically promote checkpoint
  -> publish progress marker
  -> begin next transition

Publishing progress before the corresponding state is durable creates a false resume point. Alpha explicitly forbids that ordering.

20.2 Snapshot identity

A declaration snapshot must validate at least:

• source identity;
• executing compiler identity;
• proof-kernel and schema identities;
• driver flavor;
• module and declaration positions;
• selected-module identity;
• complete global environment and usage state;
• remaining declaration tail;
• counters and fuel needed for exact continuation.

Fresh mode invalidates stale state. Resume mode fails on identity mismatch. There is no “best effort” restore into a different compiler generation.

20.3 Timeouts

A timeout is an observer boundary, not automatically a compiler failure. A canonical stage run continues until semantic completion, a real failure, declared resource exhaustion, or explicit operator interruption. Bounded timeout probes are diagnostic and non-promotable.

21. How to work on .alpha safely

21.1 Authoritative source closure

Do not guess module order with a filesystem glob. Load the repository-owned arrays:

source scripts/lib/alpha-compiler-sources.sh

printf '%s\n' "${alpha_compiler_sources[@]}"
printf '%s\n' "${alpha_compiler_diagnostic_sources[@]}"

The canonical and diagnostic closures intentionally end in different drivers.

21.2 Fast development loop

source scripts/lib/alpha-compiler-sources.sh
stage_zero="$(cabal list-bin alpha-compile)"

"$stage_zero" --parse-modules \
  "${alpha_compiler_diagnostic_sources[@]}"

"$stage_zero" --check-modules \
  "${alpha_compiler_diagnostic_sources[@]}"

"$stage_zero" --check-erasure-modules \
  "${alpha_compiler_diagnostic_sources[@]}"

"$stage_zero" --lower-modules \
  "${alpha_compiler_diagnostic_sources[@]}"

Run parse before check, check before erasure/lowering, and focused proofs before an expensive stage cycle. Use the complete ordered closure for authoritative results.

Do not invoke --parse-modules with exactly one source path. The current CLI’s positional modes can interpret a two-argument shape as source plus output. Use the complete closure or a deliberate multi-file prefix.

21.3 Focused source inspection

The Stage-0 surface parser is the source of truth for structural inspection. Where the alpha-ast developer tool is present, it can show a module outline, a definition tree, or the root-to-leaf AST path at a source position without inventing a second parser. A successful AST inspection proves syntax only; it does not prove typing or compilation.

21.4 Authoring style

• Put one semantic operation per line.
• Prefer named helper definitions over screen-sized nested continuations.
• Prefer n-ary (app f a b c) over hand-nested binary application.
• Align closing parentheses with the form they close.
• Give nontrivial intermediate operations names that describe their invariant.
• Import every family used in a signature directly.
• Qualify imported values when provenance matters.
• Keep proof data erased and runtime data explicit.
• Avoid unary naturals for compiler-scale lengths, offsets, hashes, and counts.
• Preserve global sharing with stable identities rather than repeatedly substituting complete bodies.
• Treat the first parser/checker error as the likely structural cause; later errors may be cascades.

21.5 Common diagnostics

22. Worked language examples

22.1 Ordered imports and qualified names

module Tutorial.Base

def origin : Nat = zero

module Tutorial.Consumer

import Tutorial.Base

def main : Nat =
  (succ Tutorial.Base/origin)

The build must supply Tutorial.Base before Tutorial.Consumer. The qualified name records provenance and remains unambiguous if another import defines origin.

22.2 Natural-number elimination

module Tutorial.Natural

def copyNatural :
  (pi unrestricted value : Nat . Nat) =
  (lambda unrestricted value : Nat .
    (nat-eliminate
      (lambda unrestricted current : Nat . Nat)
      zero
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : Nat .
          (succ induction)))
      value))

def main : Nat =
  (app copyNatural (succ (succ zero)))

The successor case receives both the predecessor and the induction result. The motive says that eliminating any natural returns a natural.

22.3 Effect-polymorphic return

module Tutorial.Effects

def returnWithFile :
  (pi unrestricted e : (effect-row) .
    (computation (effects File : e) Nat)) =
  (lambda unrestricted e : (effect-row) .
    (return (effects File : e) zero))

def main : (computation (effects State File) Nat) =
  (app returnWithFile (effects State))

Substitution flattens the open row and restores canonical order. The caller’s State effect is preserved while File is added.

22.4 A recursive family and eliminator

module Tutorial.ListLength

family NatList : Type 0
constructor Nil
constructor Cons
field unrestricted headValue : Nat
recursive unrestricted tailValues
end-family

def length :
  (pi unrestricted values : (family NatList) . Nat) =
  (lambda unrestricted values : (family NatList) .
    (eliminate NatList
      (lambda unrestricted current : (family NatList) . Nat)
      values
      (branch Nil . zero)
      (branch Cons headValue tailValues ih_tailValues .
        (succ ih_tailValues))))

def sample : (family NatList) =
  (constructor NatList Cons
    zero
    (constructor NatList Cons
      (succ zero)
      (constructor NatList Nil)))

def main : Nat =
  (app length sample)

The Cons branch receives three binders: the ordinary headValue, recursive tailValues, and the generated induction hypothesis ih_tailValues.

22.5 File copy with explicit effects

module Tutorial.Copy

def inputPath : Bytes =
  (bytes 47 116 109 112 47 97 108 112 104 97 45 105 110)

def outputPath : Bytes =
  (bytes 47 116 109 112 47 97 108 112 104 97 45 111 117 116)

def main : (computation (effects File) Nat) =
  (bind (effects File) Nat
    (read-file inputPath)
    (lambda unrestricted contents : Bytes .
      (write-file outputPath contents)))

This program’s effect is visible in main’s type. Native lowering either implements the exact checked File computation or fails; it cannot substitute a host-language file copy.

22.6 Equality and erased proof input

module Tutorial.Equality

def preserveZero :
  (pi erased proof : (equal Nat zero zero) . Nat) =
  (lambda erased proof : (equal Nat zero zero) .
    zero)

def main : Nat =
  (app preserveZero (refl Nat zero))

The proof is checked but has zero runtime uses. The application’s proof argument and binder disappear during erasure.

23. Learning-system architecture after self-hosting

Self-hosting is the immediate critical path because every later sovereign layer depends on a compiler that can reproduce and inspect itself. It is not the ultimate product.

The learning compiler separates these concerns:

Model and learning packages cannot import target packages. Target packages cannot invent model semantics. A target proves that it satisfies the requirements derived by the schedule and that the exact resource plan fits.

The first complete learning artifact must do more than print nonempty text. It must parse and check a learning program, derive schemas, compile host and accelerator code, initialize parameters, traverse data deterministically, train, checkpoint, resume identically, emit a standalone model, load it for inference, and bind all relevant identities. Quality and performance are later empirical gates, separate from functional compiler correctness.

24. Target and no-fallback contract

Alpha treats target support as a typed capability proof.

Selecting an asynchronous copy, tensor instruction, shared-memory tile, alias, or synchronization scheme adds explicit capability and resource requirements. The target must prove both legality and fit before machine lowering.

Unsupported behavior is an error. It is never permission to:

• run the operation on the CPU;
• use a framework implementation;
• switch to Vulkan, CUDA, LLVM, or a vendor compiler;
• reduce batch, precision, context, or model size;
• choose a smaller or decomposed kernel;
• reinterpret an unknown ABI;
• continue after a failed proof or short write.

Reference interpreters, scalar models, and legacy implementations remain useful when invoked explicitly as tests or oracles. They must not be reachable from a production target dispatch.

25. How to read progress claims

Use this translation table when reading issues, logs, or agent reports:

26. Documentation and evidence map

When these disagree, do not choose the most convenient version. Identify the exact generation, decide which contract changes, update it deliberately, and regenerate the affected manifest and evidence.

27. Common misunderstandings

“Why not just translate all Haskell to .alpha mechanically?”

Because the Haskell tree mixes several roles: bootstrap semantics, independent oracle, tests, tooling, reference architecture, and frozen legacy runtime. Mechanical translation can preserve accidental structure while losing the typed production boundary. Port responsibilities into the intended Alpha architecture, then prove parity and remove the dependency.

“If Stage 1 and Stage 2 bytes match, is the compiler correct?”

They show a fixed point for a bound generation if the orchestration and canonicalization are sound. They do not independently prove language semantics. Negative programs, differential semantics, proof checking, and diverse bootstrap evidence remain necessary.

“Why use S-expressions?”

They keep the lexer/parser small, explicit, deterministic, and feasible to own inside the bootstrap language. The project prioritizes semantic sovereignty and auditable structure over surface sugar during self-hosting.

“Why are file paths and text byte lists?”

The bootstrap vocabulary is intentionally small. Bytes give canonical, bounded, platform-auditable data without importing a host string runtime. Checked text/path libraries can be built above that foundation.

“Why does Alpha have compiler-specific byte primitives?”

The current self-host route needs efficient canonical serialization and analysis before a full optimized standard library exists. These primitives are versioned bootstrap mechanisms. They should not become universal assumptions of learning-system semantics.

“Why no fallback?”

A fallback invalidates the meaning of target, performance, memory, and sovereignty evidence. Alpha prefers an honest unsupported-operation error to a successful result produced by a different machine than the program claimed.

“Why not optimize the self-host compiler first?”

Correctness, exact resume, observability, and a current fixed point come first. An independently correct mechanism may initially be slow. Once it works, causal telemetry can guide optimization without changing semantics to satisfy an arbitrary stopwatch.

28. Glossary

Alpha Haskell : The project-authored .alpha language, not GHC Haskell.

Alpha Core : The small de Bruijn-indexed trusted term language after elaboration.

Stage 0 : The pinned GHC-built bootstrap/oracle compiler for one manifest identity.

Stage 1 / 2 / 3 : Successive Alpha-produced compilers built from the identical canonical source generation.

Fixed point : Canonical identity across successive compiler generations under an explicit canonicalization contract.

Canonical compiler : The production-identity driver and exact source closure used for fixed-point comparison.

Diagnostic compiler : A separate instrumented driver and source closure used to explain progress, failures, time, memory, and resume behavior.

Quantity : A trusted runtime-use contract: erased, affine, linear, or unrestricted.

Effect row : A canonical type-level set, possibly with an open tail, describing a computation’s effects.

Family : An algebraic or indexed inductive data declaration checked by the trusted family kernel.

Motive : The dependent result-type function used by an eliminator.

Erasure : Type-directed removal of proof/type data with no runtime representation.

Runtime graph : The deterministic closed execution IR used by the bootstrap native evaluator.

ALRI : Alpha’s versioned runtime/compiler image representation. The currently selected canonical compiler snapshot contract is ALRI v4.

Direct AOT : Specialized lowering of the checked program to control flow and machine code, without generic runtime graph dispatch in the production path.

Sovereign : Project-owned source-to-machine transformation without an undeclared compiler, framework, vendor runtime, or host fallback inside the production boundary.

Promotion : Binding complete, current, immutable evidence to an artifact after all required proof, execution, functionality, performance, and quality gates pass.

29. The north-star statement

Alpha is finished only when the following is evidence, not aspiration:

A small independently checked Alpha seed rebuilds the current compiler from the exact .alpha source generation without GHC or external code-generation tools; the resulting direct-AOT compiler checks its own language, emits its own host and accelerator machine code, and compiles architecture-neutral learning systems into complete, resumable, evidence-bound training and inference artifacts with no hidden fallback.

Until then, the correct posture is neither pessimism nor premature completion. Preserve every working bridge, label every boundary precisely, make the next semantic transition observable and resumable, and remove each bootstrap dependency only after the successor has proved it can carry the same load.

12. Twelve complete examples (R2)

Every fenced block below declares its class on the fence, and alpha doc --examples honours the declaration (Language & Testing Evolution DX-006, master §19.5): a runnable expect=N module is checked and its main is evaluated on the reference lane and compared with N; a native expect=N module is checked, built to an x86-64 artifact and executed, and its exit status is compared; a plain fence is checked (compile-only); an expected-invalid CODE fence must be rejected with that code; a fragment fence is checked for shape only. Nothing here is aspirational: the checker fails the documentation when an example stops doing what its fence says.

12.1 Numbers

module Guide.Numbers

-- closed naturals are compact literals; `nat-add` and `nat-multiply` fold in
-- the kernel, and a byte converts to a natural exactly
def forty : Nat = (nat-multiply 8 5)

def two : Nat = (byte-to-nat (byte 2))

def main : Nat = (nat-add forty two)

12.2 Text and bytes

module Guide.Bytes

-- a byte string literal is ASCII, exact, and a value of `Bytes`
def greeting : Bytes = b"hello"

def punctuation : Bytes = b", world"

def main : Nat = (bytes-length (bytes-append greeting punctuation))

12.3 Records

module Guide.Records

family Point : Type 0
constructor PointOf
field unrestricted x : Nat
field unrestricted y : Nat
end-family

def origin : (family Point) = (record Point (x = 0) (y = 0))

def moved : (family Point) = (update Point origin (y = 7))

def main : Nat = (project Point y moved)

12.4 Matches

module Guide.Matches

family Shape : Type 0
constructor Circle
constructor Square
field unrestricted side : Nat
end-family

def corners : (pi unrestricted shape : (family Shape) . Nat) =
  (lambda unrestricted shape : (family Shape) .
    (match Shape shape
      (case Circle . 0)
      (case Square side . 4)))

def main : Nat = (nat-add (corners (constructor Shape Circle)) (nat-subtract (corners (constructor Shape Square 3)) 2))

12.5 Effects

module Guide.Effects

-- a computation names its effect row; `do` sequences computations and
-- `return` closes the row; `read-file` is the only way to get bytes from a file
def sizeOfInput : (computation (effects File) Nat) =
  (do (effects File) Nat
    (contents <- (read-file b"input.bin"))
    (return (bytes-length contents)))

def main : Nat = zero

12.6 Resources

module Guide.Resources

import Std.Foundation
import Std.Region

-- a buffer is linear: allocate, initialize, submit, await the fence, observe it,
-- read once, release exactly once -- each step is a phase the type records
def roundTrip =
  (lambda unrestricted block : Bytes .
    (let unrestricted finalUse =
      (stdBufferFenceObserved
        (stdBufferAwaitFence
          (stdBufferSubmit
            (stdBufferInitialize (stdBufferAllocate block))))) in
      (let linear buffer =
        (stdPairRightOf Bytes
          (family StdBuffer (constructor StdRegionPhase StdRegionFinalUse))
          (stdBufferRead finalUse)) in
        (stdBufferRelease buffer))))

def main : Nat = zero

12.7 Errors

module Guide.Errors

import Std.Foundation

-- an error is a value: `StdResult` carries either a failure or a success, and
-- a match decides what a caller does with each
def divideBy : (pi unrestricted divisor : Nat . (family StdResult Bytes Nat)) =
  (lambda unrestricted divisor : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . (family StdResult Bytes Nat))
      (constructor StdResult StdFailure Bytes Nat b"division by zero")
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdResult Bytes Nat) .
        (constructor StdResult StdSuccess Bytes Nat (nat-divide 12 divisor))))
      divisor))

def successes : (pi unrestricted result : (family StdResult Bytes Nat) . Nat) =
  (lambda unrestricted result : (family StdResult Bytes Nat) .
    (match StdResult result
      (case StdFailure message . 0)
      (case StdSuccess value . 1)))

def main : Nat = (nat-subtract (successes (divideBy 4)) (successes (divideBy 0)))

12.8 Test cases

module Guide.TestCases

import Std.Foundation
import Std.List
import Std.Diagnostic
import Std.Testing

-- a test case is a value; a suite is a list of them; the runner decides
-- nothing the suite does not decide itself (`alpha test`, kind alpha)
def caseNil = (constructor StdList StdListEmpty (family StdTestCase))
def caseCons =
  (lambda unrestricted testCase : (family StdTestCase) .
    (lambda unrestricted rest : (family StdList (family StdTestCase)) .
      (constructor StdList StdListCons (family StdTestCase) testCase rest)))

def additionCommutes = (stdTestCase b"addition-commutes" (stdCheckNaturalEqual (nat-add 2 3) (nat-add 3 2)))

def guideSuite = (stdTestSuite b"guide" (caseCons additionCommutes caseNil))

def main : Nat = zero

12.9 Properties

-- a property is a value too: a generator, a validity filter, the predicate,
-- a shrinker, a renderer, the draw count, the minimum executed and the shrink
-- budget; `stdPropertyOf` builds it and the runner reports the smallest
-- counterexample (the executed suite is packages/foundation/standard/tests/Std/StdRandomLaws.alpha)
def reverseTwiceIsIdentity =
  (stdPropertyOf (family StdList Nat)
    enumeratingGenerator
    alwaysValid
    reverseTwicePredicate
    stdShrinkListNatural
    renderNaturals
    (byte-to-nat (byte 20))
    (byte-to-nat (byte 20))
    (byte-to-nat (byte 6)))

12.10 Negative compiler tests

module Guide.Negative

-- a byte where a natural is expected is rejected at check time, on this line
def broken : Nat = (byte 1)

12.11 Replay

module Guide.Replay

import Std.Foundation
import Std.List
import Std.Diagnostic
import Std.Testing

-- a seeded suite is a FUNCTION of its seed, so a replay is the same manifest
-- case run again: `alpha test --replay guide-seeded` (the seed is data in the
-- manifest, `seed 1 2 3 4`), never a stored trace
def caseNil = (constructor StdList StdListEmpty (family StdTestCase))
def caseCons =
  (lambda unrestricted testCase : (family StdTestCase) .
    (lambda unrestricted rest : (family StdList (family StdTestCase)) .
      (constructor StdList StdListCons (family StdTestCase) testCase rest)))

def seededSuite =
  (lambda unrestricted seed : Bytes .
    (stdTestSuite b"guide-seeded"
      (caseCons (stdTestCase b"seed-length" (stdCheckNaturalEqual (bytes-length seed) 4)) caseNil)))

def main : Nat = zero

alpha test --replay guide-seeded --json     # the plan, the case and its receipt, again

12.12 Native execution

module Guide.Native

-- a program whose `main` is a natural builds to an x86-64 ELF on the direct
-- lane; its exit status is the natural (`alpha run`, `alpha build`)
def main : Nat = (nat-add 2 3)