Functions

Declaring a function

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

Parameter types and the return type are always written out; Albite does not infer signatures. Inside the body, inference does most of the work.

The body’s last expression is the return value, with no keyword and no trailing semicolon.

Visibility

Declarations are private to their module unless marked pub:

pub fn my_api(x: Nat) -> Nat {
    x + 1
}

See Modules and visibility.

Early return

Since 1.5 — return did not exist in v1.0, where the last expression was the only way out of a function.

return leaves a function before its end, which is what you want for guard clauses:

fn first_nonzero(a: Nat, b: Nat) -> Nat {
    if a != 0 { return a; }
    b
}

return has the bottom type: an expression that never produces a value, and so fits wherever one is expected. That has one consequence worth knowing, because the error it produces is otherwise puzzling.

An if without an else, used as a statement, must have type Unit. Writing { return a; } — with the semicolon — gives the block type Unit and type-checks. Writing { return a } — without — gives the block the bottom type and fails with a mismatch against Unit:

fn ok(a: Nat, b: Nat) -> Nat {
    if a != 0 { return a; }     // semicolon: block is Unit
    b
}

fn broken(a: Nat, b: Nat) -> Nat {
    if a != 0 { return a }      // no semicolon: type error
    b
}

In an if/else used as an expression, both arms can return and no semicolon is needed, because the arms are the expression’s value:

fn pick(a: Nat, b: Nat) -> Nat {
    if a != 0 { return a } else { return b }
}

The compiler also warns (W0002) about code sequenced after a return, since it can never run.

A known divergence. return in statement position is currently ignored by the interpreter — albite run evaluates the unreachable code and returns that instead. Compiled binaries are correct. Until this is fixed, verify return-heavy code with albite compile rather than albite run. See Current limitations.

Recursion

Since 2.0-alpha — recursion is checked.

A function may call itself, but the compiler must be able to see that it stops: some parameter has to get strictly smaller — a piece taken out of it by match — at every recursive call. count(n - 1) on a Nat does not qualify, and is refused with E0062. Recursion the compiler can see ends shows what to write instead, including #[partial], which is the ordinary answer for code that genuinely recurses on a number.

Generic functions

Type parameters go in angle brackets:

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

fn const_fn<A, B>(x: A, y: B) -> A {
    x
}

Type arguments are inferred at the call site — identity(42) infers T as Nat. See Generics for what to do when inference cannot get there.

Lambdas

Anonymous functions bind their parameters between bars:

let inc = |x: Nat| x + 1;
let add = |a: Nat, b: Nat| a + b;

There is a second, longer spelling used mainly with the proof eliminators, where an explicit fn reads more clearly:

let step = fn(k: Nat, acc: Nat) => acc;

Both produce ordinary function values; use whichever reads better.

Function types

Functions are first-class. A function type is written with its argument types in parentheses:

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

For a single argument the parentheses may be dropped, which is common in generic code:

fn apply_generic<A, B>(f: A -> B, x: A) -> B {
    f(x)
}

Theorems

theorem is syntactically identical to fn. It declares that the signature is a proposition and the body its proof:

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

See Proofs.

Entry point

An executable needs a main. Its result is printed, and the process exits 0:

fn main() -> String {
    "hello world"
}

Any type with a printable representation may be returned — Nat, String, Bool, and so on.