Alpha7d4a2ac3
startView source

Getting started

The shortest route into Alpha is to write one complete module, ask the checker what it means, and keep the evidence boundary in view. The browser workbench uses the real repository-built compiler in a networkless, read-only sandbox. It checks source and reference-normalizes main; it does not claim native or physical execution.

Try a complete module

Open the REPL, keep the default example, and choose Check & evaluate.

module Playground.Main

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

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

The important parts are already visible:

  • Nat is a type and zero is a value;
  • pi is a dependent function type;
  • lambda introduces a function;
  • unrestricted permits any number of runtime uses; and
  • main is the expression the workbench asks the reference evaluator to normalize.

Read the result correctly

The workbench runs two separate phases:

  1. alpha check parses, resolves, elaborates, and checks types, quantities, effects, and totality.
  2. alpha repl loads the same module and reference-normalizes main.

A green result means those two named operations passed for the shown compiler identity and edition. It does not mean the module was lowered to native code, run on a GPU, self-hosted by the current compiler generation, or physically attested.

Work locally

From a checkout of thomasdavis/alpha:

cd bootstrap/haskell
cabal build alpha-compiler:exe:alpha
ALPHA="$(cabal list-bin alpha-compiler:exe:alpha)"
cd ../..

"$ALPHA" version --json
"$ALPHA" check --root Your.Module
"$ALPHA" repl --root Your.Module

Run the executable from a directory containing alpha.project so module roots, packages, edition, and cache policy are explicit.

Where to go next