Getting started#

This page takes you from nothing to a running Alpha program, then to a GPU training executable. If you only want to look around, the REPL runs the real compiler in your browser.

Requirements#

Build the compiler#

The current compiler is a Haskell bootstrap that compiles Alpha source, including the compiler's own Alpha packages.

git clone https://github.com/thomasdavis/alpha.git
cd alpha
(cd bootstrap/haskell && cabal build -O2 exe:alpha)
export PATH="$(dirname "$(cd bootstrap/haskell && cabal list-bin -O2 exe:alpha)"):$PATH"

alpha version
alpha doctor      # checks the workspace and lists every command

Your first program#

Save this as Hello.alpha:

module Hello

def double : (pi unrestricted n : Nat . Nat) =
  (lambda unrestricted n : Nat . (nat-add n n))

def main : Nat =
  (double 21)

Run it, then build it as a native executable:

$ alpha run --edition alpha-2027 --root Hello.alpha; echo $?
42
$ alpha build hello.elf --profile dev --edition alpha-2027 --root Hello.alpha
$ ./hello.elf; echo $?
42

main's natural number becomes the process exit status. The ELF is about 29 KB, static, and has no libc. Inside the Alpha repository the workspace manifest (alpha.project) already selects the alpha-2027 edition, so you can drop --edition there.

What you just wrote:

• module Hello names the module.
• (pi unrestricted n : Nat . Nat) is a function type. pi is the dependent function type; here the result type does not depend on n, so it reads like Nat -> Nat.
• unrestricted is the binder's quantity: n may be used any number of times at run time. The others are erased (never at run time), affine (at most once) and linear (exactly once).
• (double 21) applies double to 21.

When something is wrong#

Errors carry stable codes. Change unrestricted to linear in double: n is now used twice, which a linear binder forbids.

$ alpha check --edition alpha-2027 --root Hello.alpha
./Hello.alpha:4:3: ALPHA-QUANTITY-VIOLATION: [module Hello] linear binder n is used 2 time(s)

DiagnosticsReference · generatedDiagnosticsStable error codes, phases, and repair guidance. lists the catalogued codes with their repairs, and alpha explain CODE prints the entry for one.

Build a learning system#

Bob is the smallest system in the repository: a next-byte predictor. This builds it as one self-contained RTX 3090 training and inference executable (about 800 KB, about 40 seconds):

alpha build bob-rtx3090.elf --profile release --artifact-value artifact \
  --root systems/bob/src/Bob/Build/RTX3090Artifact.alpha

Each system's README explains its run protocol: train, continue from a checkpoint, predict. Learning systems lists every system and where it runs.

In the browser#

The REPL checks a module with the real compiler, then evaluates main and shows its type and value. It runs in a sandbox with no network and uses the reference evaluator, so nothing is compiled to native code there.

Where next#

• Language guideLearn · explanationLanguage guideThe full tour: syntax, types, quantities, effects and families, and why Alpha is built this way.: syntax, types, quantities, effects and families.
• Families and branchesLearn · analysisFamilies and branchesIndexed data, constructors, motives, recursion, and exhaustive elimination.: defining and consuming data.
• Language and compilerUnderstand · analysisLanguage and compilerHow source becomes checked core, typed machine work, native artifacts, and evidence.: how a program becomes an executable.
• SpecificationReference · normativeSpecificationThe normative language semantics and trusted boundary.: the exact rules, when prose is not enough.