Albite

A short tour

This is a whistle-stop tour: enough of the language to read most Albite code, with no attempt at completeness. Each topic has its own page under Language, linked as we go.

Functions and bindings

fn add(a: Nat, b: Nat) -> Nat {
    a + b
}

Parameter and return types are always written out. The body’s last expression is the result — no return needed, though return does exist for leaving early.

Inside a body, let introduces a binding, and the type annotation is optional whenever it can be inferred:

let x = 42;
let name: String = "hello";

let bindings end with a semicolon; the final expression does not. That single rule accounts for most early syntax errors.

Conditionals

if is an expression, so it produces a value and both branches must agree on its type:

fn describe(n: Nat) -> String {
    if n == 0 { "empty" } else if n < 10 { "small" } else { "large" }
}

Data types

Sum types list alternatives, each with its own payload:

type Shape =
    | Circle(Nat)
    | Rect(Nat, Nat)

Records have named fields:

type Point = { x: Nat, y: Nat }

Both are covered in Data types.

Pattern matching

match takes a value apart by its constructor. The compiler checks that every case is covered:

fn area(s: Shape) -> Nat {
    match s {
        Circle(r) => 3 * r * r,
        Rect(w, h) => w * h,
    }
}

Miss a constructor and it is a compile error, not a runtime surprise. See Control flow and pattern matching.

Records in practice

Fields are read with a dot. To build a new record from an existing one, use spread syntax:

fn shift(p: Point, dx: Nat) -> Point {
    { ...p, x: p.x + dx }
}

Functions as values

Functions are first-class. A lambda is written with bar-delimited parameters:

fn apply_twice(f: (Nat) -> Nat, x: Nat) -> Nat {
    f(f(x))
}

let inc = |n: Nat| n + 1;

Generics

Type parameters go in angle brackets:

fn identity<T>(x: T) -> T {
    x
}

Type arguments are usually inferred; supply them explicitly with turbofish when they cannot be — identity::<Nat>(42). See Generics.

Modules

mod declares a submodule, use imports from one. Paths are absolute from the crate root:

pub mod math;
pub mod greet;

use math::ops::{add, double};

Declarations are private unless marked pub. See Modules and visibility.

Proofs

The part that makes Albite more than a small functional language: a type can be a proposition, and a program that inhabits it is a proof.

theorem zero_eq_zero() -> Eq<Nat, 0, 0> {
    refl
}

Eq<T, a, b> is the proposition that a equals b at type T; refl proves it when both sides compute to the same value. That is the whole idea, and Proofs develops it.

Where next