Albite

Albite 2.0-alpha

Albite 2.0-alpha (released as Tungsten by Spinning Cat Studios). Superseded by 2.0-beta.

A pre-release. The first part of v2.0 to be put in front of people outside the project. It is an alpha: the language will change before v2.0, and GitHub lists this release as a pre-release rather than as Latest.

These pages were checked against this release’s compiler — every code sample on them was run through it — rather than written from the changelog.

What will surprise you first

The compiler now refuses some programs that v1.5 accepted. Four rules, each with its own page showing a rejected program, the error, and what to write instead:

  • Every recursive function must be seen to stop (E0062). A parameter has to get strictly smaller — a piece taken out of it by match — at every recursive call. count(n - 1) over a Nat does not qualify. Mark code that genuinely recurses on a number #[partial]; the compiler’s own source does so over a thousand times. See Recursion the compiler can see ends.
  • A proof may not depend on a #[partial] definition (E0063), even through a wrapper. See Partial definitions in proofs.
  • A type may refer to itself only to the right of an arrow (E0061). See Strictly positive types.
  • A type whose recursion passes through a generic type cannot be matched on (E0064). See A recursive type nested inside a generic one.

Language

  • Signed integers. Int beside Nat: -7 is an Int, and 42 is one wherever an Int is expected. Division truncates toward zero; overflow and division by zero stop the program with a named line; to_int and from_int convert. See Values and types.
  • match on numbers, with literal, negative, | and variable patterns and if guards.
  • #[decreasing(arg)] names the parameter that shrinks when more than one does, and #[partial] opts a function out of the termination check.

Runtime

  • StringBuilder — the runtime’s growable string buffer, reached through extern "C". See Calling C.
  • ALBITE_ARENA=bump runs a compiled program on a bump-pointer arena: 1.3–1.7× faster on the project’s benchmarks. See the command-line reference.

Diagnostics

  • One mistake, one error. A broken definition is reported once, where it is broken, and not again at every use — so the first error is the one to fix.
  • albite explain error <code> takes the code a diagnostic prints.
  • Error underlines are in the right column after non-ASCII text.

Fixed

  • Tail-recursive functions over records and larger structures run in constant stack instead of overflowing.
  • Compiled programs call the right function when two imported modules define the same name. (The interpreter still does not — see Current limitations.)
  • Programs with mutually recursive data types compile in seconds, not minutes.
  • A generic type stored in a record field no longer causes a type mismatch between two types that print the same.

The full changelog, including the fixes specific to the macOS build and the compiler’s own tooling, is in the repository’s changelog/.

Still true

The known divergences between the interpreter and compiled output, the missing tactic language and the other gaps are listed, checked against this release, on Current limitations. The browser playground still runs v1.5.0 — see Installing Albite.