Research language · edition alpha-2027 (draft)

Compile a learning system, from its mathematics to its GPU instructions.

Alpha is a dependently typed language and compiler. You write a model, how it learns and where it runs as one program; the compiler checks all of it and emits every byte of a self-contained executable for the device you choose.

Get started Try it in the browser GitHub

Hello.alphaalpha-2027

module Hello

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

def main : Nat =
  (double 21)

alpha run → exit status 42

The vision1 min 36 s · sound on

One programThe model, its learner, the training run and the device pairing are one typed program. The compiler sees all of it before it specializes anything.Any deviceA device is a typed profile, not a runtime. Model code never mentions hardware, so moving to new hardware means adding a target, not rewriting the model.No fixed catalogueThere is no closed list of operators or kernels. Mathematics, memory layouts, schedules and GPU instructions are ordinary values you can recombine.Built for agentsEverything has a literal name, checks take seconds and errors have stable codes, so an agent can take a system apart and rebuild it safely.

01
Describe
Write the model, the learner and the run as ordinary Alpha definitions, with no device in sight. A separate pairing names the hardware.
02
Check
Dependent types, quantities and effects are checked across the whole program. Shapes, layouts and resource limits are facts, not comments.
03
Realize
The compiler plans memory, schedules launches and lowers each computation to the target's machine code, refusing anything that fails its hazard checks.
04
Run
The result is one self-contained executable that trains, checkpoints and predicts, talking to the device driver directly with no framework underneath.

systems/bob/src/Bob/System.alphathe model

-- No target, device, address, launch or runtime value is reachable from this
-- semantic root.  Concrete hardware enters only through Bob.Build.*.
def bobSystem : (family BobSystemConfiguration) =
  (record
    BobSystemConfiguration
    (bobSystemDefinitionValue = bobSystemDefinition)
    (bobSystemModel = bobModel)
    (bobSystemLearning = bobLearningSemantics)
    (bobSystemTrainingRun = bobTrainingRunSemantics)
    (bobSystemPrediction = bobPredictionSemantics)
    (bobSystemCheckpointSchema = bobCheckpointSchema))

Read the whole file →

systems/bob/src/Bob/Build/RTX3090.alphathe pairing

-- the compatibility contract: what the artifact demands of the card
-- against what the RTX 3090 profile supplies (Platform.Linux.Nvidia.
-- Compatibility); the first demand not met, by name (empty = admitted)
def bobRTX3090CompatibilityRefusal : Bytes =
  (nvidiaCompatibilityRefusal (bobCompatDemands runPodSM86QMDArchitecture) runPodRTX3090Supplies)

Read the whole file →

Feed-forward and recurrent networks
Scans and state-space models
Convolutional and spectral systems
Sparse, graph and event-driven systems
Fixed-point and differential-equation systems
Energy-based and implicit models
Forward-, reverse- and mixed-mode differentiation
Local, perturbation and population learning

Dependent types: Types can mention values, so a tile that does not fit shared memory, or a buffer of the wrong length, is a type error.
Quantities: Every binder is erased, affine, linear or unrestricted. Proofs and type-level data vanish from the executable by construction.
Explicit effects: Effects and partiality are part of a computation's type. Nothing performs I/O or diverges without saying so.
No fallbacks: If a target cannot do something, compilation stops with a stable diagnostic. Work never silently moves somewhere else.

Prompt

Clone https://github.com/thomasdavis/alpha and read AGENTS.md first.
Build the compiler: (cd bootstrap/haskell && cabal build -O2 exe:alpha).
Write a small Alpha module whose main computes a number, check it with
alpha check, run it with alpha run, and explain what each quantity in it means.
Then read systems/bob and explain how its model stays independent of the GPU.

LearnGetting started

Build the compiler and run a first program.

LearnLanguage guide

Syntax, types, quantities, effects and families, with examples.

ExploreLearning systems

The models written in Alpha and where each one runs.

ExploreHardware

Every target device and its typed profile.

UnderstandLearning systems in Alpha

How a learning idea becomes a checked, comparable experiment.

UnderstandPhilosophy

Why Alpha reopens the design space instead of freezing today's stack.