Compiler architecture#

How the pieces fit, and why the boundaries are where they are. The pipeline itself is docs/compiler/PIPELINE.md; this document is about the shape.

One engine, many tools#

There is exactly one implementation of the language. The formatter, linter, language server, test runner, documentation generator, REPL, debugger adapter, profiler and diff all answer from it. That is not a style preference: it is the only way two tools can be guaranteed to agree about what a program means. When alpha lsp reports a diagnostic, it is the same diagnostic alpha check reports, from the same run of the same checker, because the server calls the engine rather than modelling it.

The rule shows up in the harnesses: debug/lsp-check.py compares the server's references against alpha inspect references and requires them to be equal, not merely similar.

The packages#

The bootstrap compiler is a set of Cabal packages under bootstrap/haskell/packages/. The ones every program passes through:

The others carry the learning-system and device layers the bootstrap still owns:

Dependencies run one way: surface depends on core and proof, the compiler depends on core, surface, the semantic IR and the targets, and nothing depends on the executable.

The trusted kernel#

The kernel is small and is compiled with Safe Haskell. Everything a program's acceptance depends on lives there: inference, checking, definitional equality, quantity accounting, effect rows, totality and positivity. Elaboration outside the kernel may only produce core terms; it can never decide that one is well-typed.

Two consequences are worth stating because they constrain every other design choice:

• a tool that wants to know a type asks the kernel, and there is no second answer to fall back on;
• a cache may re-admit kernel-checked data only through a validated interface whose digests are checked first, which is the cache-trust boundary the incremental engine documents.

The lossless source model#

Source is kept losslessly: every byte lands in exactly one lexeme, and the concrete syntax tree can reproduce the file. The parser's token stream is a projection of that tree rather than an independent scan. This is what lets the formatter, the linter and the editor share spans with the checker, and it is checked corpus-wide (debug/cst-check.py; its run recorded in docs/generated/ALPHA-CST-CHECK.json covered 1084 files with zero contradictions).

The incremental engine#

The engine is a graph of modules keyed by content, not by timestamps. A key combines the module's source digest, its position, its dependencies' interface digests, the compiler identity, the edition and the schema version. A change that does not alter a module's interface digest does not disturb its dependents — which is why a comment-only edit re-checks one module while a changed literal re-checks the cone below it.

docs/compiler/INCREMENTAL.md covers the cache, its validation and its failure modes.

The two emission lanes#

The compiler can produce an artifact two ways, and the difference matters:

• the evaluator lane erases the program, reduces the erased term (Alpha.Compiler.ErasedReduction: applications of visible lambdas to atoms and small or once-used values, eliminators on known constructors, and functions inlined where a record of operations is passed to them, so an abstraction the source introduces is not interpreted on every call), compiles it to a runtime graph, and emits an ELF carrying that graph together with the evaluator that walks it. This is the bootstrap bridge, and it covers every form of the alpha-2026 edition. alpha build reports the reduction (erased-reduction event: nodes before and after, inlinings, applied), and a program the reduction would grow past four times its size is lowered unreduced.
• the direct lane validates the program as a closed functional closure, defunctionalizes it, lowers it to typed control flow, emits machine code, and wraps it in an object the linker places. It also covers every alpha-2026 form, and it is the lane that carries a source map from emitted code back to source lines.

The direct lane's emitter knows every slot's frame offset and extent, and knows a slot's VALUE only when the program determines it. That is the line between the two kinds of thing it does: a value it knows is materialized, and a value it does not — anything downstream of read-file — is computed by emitted instructions reading the length header a byte sequence carries. A program whose answer depends on a file is therefore not value-checked against the interpreters before emission, and its certificate records that rather than comparing against an invented empty file.

alpha build --direct demands the second and refuses to fall back, so what reaches direct AOT is never a guess. docs/compiler/ARTIFACTS.md records what each lane produces.

Where the boundaries are enforced#

• debug/authority-check.py keeps the documentation's claims and the registry's claims consistent.
• debug/differential.py requires that a compiler change preserve which programs are accepted, with which diagnostics, and which bytes are emitted.