Core and IR#

Alpha has two internal languages, and they answer different questions.

Core: what a program MEANS#

Core is the kernel's language. It is dependently typed, carries quantities and effect rows, and is the only thing the checker will look at. Elaboration produces it; nothing else may claim a core term is well-typed.

Properties that matter downstream:

• source origins travel with the term. Elaboration wraps core terms in RAnnotated source origins (Alpha.Core.Trusted.Syntax). They do not take part in checking or equality (withoutOrigin strips them), but the direct lane carries them to the code it emits, which is what the source map is built from: alpha debug verifies breakpoints against it and alpha profile --program attributes emitted bytes to source lines.
• definitions are positional. A module's definitions live in a shared context and refer to each other by de Bruijn position, not by copied value. Splicing values instead was measured at ~25 GB on the full closure; a reference costs nothing.
• quantities are part of the type. erased, affine, linear and unrestricted are checked by the kernel, so a linear buffer used twice is a type error rather than a lint.

The interface codec (Alpha.Core.Interface) serialises core terms canonically: one term has one encoding, which is what makes an interface digest meaningful.

The semantic IR: what a program DOES#

The IR is simply typed and exists to be lowered. It has three layers:

Functional expressions (Alpha.Core.FunctionalProjection) — a typed projection of core with naturals, bytes, byte sequences and function types. A core term the projection does not understand is REFUSED here, by name. That projection is where most of core's expressiveness is dealt with:

• family values, sigma pairs and equality proofs have no run-time shape, and do not need one. In a closed program every eliminator has a value to work on, so the KERNEL'S OWN weak-head reducer turns them into the branch, component or value they stand for. A family eliminator over data that only exists at run time becomes a DECISION TREE whose nodes are Boolean-natural conditions and whose leaves are constructor applications.
• a nat-eliminate becomes one of three things depending on its count: an unrolled chain when the count is a literal, a CONDITIONAL when the scrutinee is proven to be 0 or 1, and a LOOP when it is neither.

The direct lane covers every form of the alpha-2026 edition.

Defunctionalization (Alpha.IR.Semantic.Defunctionalization) — closures become first-order data plus a dispatch, so the backend never has to represent a function value. It does this by INLINING, which is why the one thing it cannot handle is a value whose shape is not known until the program runs: a loop's accumulator may not be a function, and that refusal is by name.

Typed control flow (Alpha.IR.Semantic.ControlFlow) — operations (signed-literal, boolean-literal, byte-sequence-literal, add-signed, add-immediate-signed, equal-signed, less-signed, mask-signed, boolean-to-signed; pair, first, second for records written side by side into one slot; inject-left, inject-right for tagged values tested by the ordinary branch; byte-sequence-length, byte-sequence-index, byte-sequence-tail, byte-sequence-cons, byte-sequence-append; read-file, write-file), blocks that bind operations, branches, LOOPS, and a return. Every operation carries its result type and its effects, and every reference is an index into a typed environment, so an ill-formed program cannot be constructed.

Two things about this layer are worth knowing before changing it:

• the effect row is an upper bound. A block's row is the merge of the operations in it; a return performs nothing and so inhabits any row. Which row a closed program lowers at is read off the EXPRESSION — does it read, does it write — rather than declared, and the evidence that a row absorbs an effect is a witness passed into the lowering, which is what lets one lowering serve pure and effectful programs alike.
• a loop's body has its own environment, not an extension of the enclosing one: the accumulator, the index, and one slot per capture. Captures are read once before the loop. That shape is what lets a loop survive defunctionalization, which inlines everything else it meets.

alpha inspect cfg reports what a program lowers to: blocks, branches, depth and each operation's count. The walk over the IR is total, so adding an operation without teaching the reporter about it is a compile error.

Why two languages#

Core answers "is this program meaningful?" and must therefore be expressive enough to state dependent types, proofs and quantities. The IR answers "what machine work does this program require?" and must therefore be small enough to lower without cleverness. Trying to make one language do both is how backends end up with an interpreter in the artifact.