reference.md

Axiom Language Reference

A friendly, comprehensive guide to the Axiom programming language — a functional systems language that compiles to native code via LLVM, with no VM and no runtime. Memory comes from an mmap-backed bump allocator, and dead blocks are reclaimed by reference counting (memory-model.md MM-LIFE-2).

---

Table of Contents

1. Hello, Axiom!
2. Syntax Basics
3. Comments
4. Literals
5. Identifiers and Keywords
6. Types
7. Functions
8. Operators
9. Let Bindings
10. Conditionals
11. Pattern Matching
12. Algebraic Data Types
13. Structs
14. Type Aliases
15. Effects — effect, handle, and inference
16. Capability Records — what replaced traits
17. Modules and Imports
18. Packages — axiom.pkg, depend and crate
19. Macros
20. Printing and Formatting
21. Memory Primitives
22. Standard Library
23. AXTAG Metadata
24. Removed Features
25. The REPL
26. CLI Commands
27. Testing — axiom test
28. Compiler Pipeline
29. Cross-Compilation
30. Optimisation
31. Tips and Patterns
32. Further Reading

---

Hello, Axiom!

Every Axiom program needs a main function that returns Int. Here is the smallest possible program:

(import IO)

(:: main Int)
;@axiom:effect(io)
(fn (main)
  {
    (println "Hello, Axiom!")
    0
  })

Run it:

axiom run hello.ax

That's it. No headers, no build system, no runtime. The IO module is part of Axiom's own standard library, which reaches the kernel through raw syscalls, so this program links and calls no C function. An extern block is the one door that changes that (ffi.md).

---

Syntax Basics

Axiom uses S-expressions — everything is wrapped in parentheses. This takes a moment to get used to, but the payoff is a language with almost no syntax rules to memorize.

The General Form

(keyword arg1 arg2 ...)

Every expression is a list. The first element is always a keyword or operator, and the rest are arguments. There are no precedence rules to memorize — parentheses make the structure explicit.

Whitespace

Whitespace (spaces, tabs, newlines) separates tokens. It is not significant beyond that — you can format your code however you like.

---

Comments

; This is a line comment

#| This is a block comment.
   They can nest: #| inner |# |#

Line comments start with ;. Block comments use #| ... |# and can nest arbitrarily.

A block comment is trivia: it may sit between any two tokens, and its contents are not source. Nesting is counted, so the first |# closes only the innermost open comment. A block comment that is never closed runs to the end of the file and is not an error. A # that is not followed by | is AX1001, so # is not a comment character on its own.

;@axiom: metadata is recognised only in a line comment. Inside a block comment it is comment text like anything else.

---

Literals

42              ; Integer (64-bit)
3.14            ; Float (64-bit)
1_000_000       ; Underscore separators for readability
true            ; Boolean
false           ; Boolean
"hello world"   ; String
'x'             ; Character

String Escape Sequences

Sequence	Meaning
\n	Newline
\t	Tab
\r	Carriage return
\\	Backslash
\"	Double quote
\'	Single quote
\0	Null byte

String Literals Are Str Values

A string literal is a first-class string. It needs no conversion and can go anywhere a Str from the standard library can:

(println "Hello, Axiom!")
(strLen "Hello")                    ; 5
(strConcat "sum=" (fmtInt 42))
(strSlice "abcdef" 2 3)             ; "cde"

The compiler emits two globals per literal — the bytes, and a header whose last three words are the Str triple: length, byte address and owner, exactly the layout Str.strWrap builds. The first two words are the MM-LIFE-2b count/shape header every heap block carries, with the count all-ones: a static is never reclaimed, and the runtime's retain/release read the sentinel and leave it untouched. The literal's value points at the {length, bytes, owner} triple, so every consumer loads at +0/+8 as before; the owner word is zero, because a literal's bytes are loader-resident and no block's death may free them (MM-VAL-7):

@str_0    = private unnamed_addr constant [14 x i8]  c"\48\65\6C\6C\6F\2C\20\41\78\69\6F\6D\21\00"
@strhdr_0 = private unnamed_addr constant { i64, i64, i64, ptr, i64 } { i64 -1, i64 0, i64 13, ptr @str_0, i64 0 }, align 16

The emitter escapes every byte, so \48\65\6C... is Hello, Axiom! and its NUL; axiom emit-llvm on (strLen "Hello, Axiom!") prints exactly these two lines.

The literal evaluates to the triple's address. Its length is computed at compile time, so (strLen "Hello") is a load rather than a scan, and a literal costs no allocation at run time.

The bytes stay NUL-terminated as well as length-counted, so a literal can still be handed to a syscall or a C function that expects a C string. __addr is how you reach them:

"hello"                             ; the Str header
(__addr "hello")                    ; the bytes, as an address

Str.strFromLit remains the bridge for NUL-terminated bytes that arrive without a length — from a syscall buffer, say. Applied to a literal it is redundant: (strFromLit (__addr "hi")) scans for a length the compiler already knew, and "hi" is the same value.

What the literal replaced

Before literals carried their own header, every string in every program was written the long way:

(println (strFromLit (__addr "Hello, Axiom!")))

__addr took the literal's address and strFromLit scanned it with cstrLen to recover a length the compiler already knew. There were 350 such sites across stdlib/, self_host/ and the tests; all of them are plain literals now, which is why the form above appears in this document only as history.

A String is a machine word, and the checker knows which words are strings. Every Axiom value is one word, and a String is the address of a Str header — but since 2026-08-15 String and Int are DISTINCT types: the fiat that unified them is deleted, and (+ 1 "hi") is the AX3004 it always deserved. A literal still goes into a Vec or a Map value slot, because the containers carry type variables rather than spending the fiat; the explicit crossing where a handle is deliberately read as a word is spelled (cast Int s), and it appears exactly once in Str itself.

---

Identifiers and Keywords

Identifiers

Names are lowercase by convention:

myVariable
compute_sum
->

The character set is wider than that suggests, and deliberately so. An identifier's first byte is a letter, _, or one of

+ - * / % < > = ! & | ^

and every byte after the first is one of those, a letter, a digit, or '. That is what makes + a name rather than punctuation — (+ a b) is an ordinary application of a function called + — and it means set!, foo', empty-list and a+b are all ordinary names you may declare:

(:: half' (-> Int Int))
(fn (half' n') (/ n' 2))

Two exclusions are on purpose. ? is not an identifier character, so empty? is a lexer error (AX1001) rather than a name; admitting it is a language change to be made deliberately, with the tree-sitter grammar and the formatter moved alongside. And . is not one either, so tmp.1 is refused — . is field access, and :: is qualified module access (Mod::name), neither of which can be part of a name.

Names outside LLVM's own identifier set are quoted on the way into the generated code, so every name the frontend accepts is one the backend can emit. Twelve of these characters used to pass check and then kill opt; scripts/check-symbol-names.sh now sweeps all 94 printable bytes in three positions and requires each to be either refused with a span or compiled and run. See the self-hosting record.

Keywords

These words carry grammar rules. There is no reserved-word list in the lexer: each is an ordinary identifier everywhere except the position its rule claims — the head of a form, and for mut the head of a let binding. (let ((match 1)) match) binds a variable called match; (cast e) is read as the cast form whatever cast is bound to. Shadowing one is legal and a bad idea.

axiom fmt prints by the same rule since 2026-08-28: a keyword in parameter, let binder, pattern, argument or effect-name position is printed as the identifier it is (tests/fmt/parity/190-keyword-param.axp through 195-effect-keyword-atom.axp, and 070-keyword-in-expr.axp, which pinned the refusal until then), and the formatter refuses exactly the heads the parser refuses - consume and begin, AX2004 (196-consume-head-refused.axp, 197-begin-head-refused.axp) - plus mut at a let binding's head, which is the marker and not a name (194-mut-binder-head-refused.axp, AX2001 from check too). Until then the formatter reserved every word in this table in every position, which was the retired Rust compiler's lexer rule, and refused (fn (g data) data) while check accepted it.

Keyword	Purpose
fn	Define a function. This is the language's spelling
define	Legacy. The old spelling of fn: accepted so that old source still parses and read as fn, rewritten to fn by axiom fmt, and written by nothing in the tree
lambda	Anonymous function
let	Local variable binding
mut	Marks a let binding assignable
set	Assign to a mut binding
while	Loop while a condition holds
for	Loop over a range, (for i lo hi body), or over a (Vec a), (for x xs body) — one keyword, two shapes, since 2026-09-03
region	Bracket an allocation scope: (region r body) reclaims everything body allocated when it ends and answers body's value (Regions, since 2026-09-03)
parallel	Run bindings beside the caller and join them in the order written — processes by default, threads under --threads (parallel)
if	Conditional expression
cond	Multi-branch conditional
match	Pattern matching
data	Algebraic data type
struct	Product type with named fields
type	Type alias
subtype	Range-constrained subtype of Int (below), since 2026-09-09
trait	Reserved — removed 2026-08-31, reports AX2004; an interface is a capability record
impl	Reserved — removed 2026-08-31, reports AX2004; an instance is an ordinary value
import	Import a module
pub	Public visibility
deriving	Refused (AX2004, 2026-08-14) — it parsed and derived nothing; derive is explicit declaration macros (macro-system.md MAC-CAP-9)
effect	Declare an effect type
handle	Handle effects
linear	Reserved — removed 2026-08-25, reports AX2004
consume	Reserved — removed 2026-08-25, reports AX2004
alloc	Allocate memory
sizeof	Size of a type
alignof	Alignment of a type
cast	Type cast

Removed Keywords

These words still have a rule, and the rule is a refusal (AX2004). Using one in head position reports what to write instead:

Keyword	Replacement
union	Use data for a tagged sum or struct for a product
foreign	Write an extern block (see below); or use the standard library, which needs no FFI

extern — binding Rust

An extern block names symbols in a static archive. Each item carries its type inline and the linker symbol it binds:

(pub extern "axiom_demo"
  (add         :: (-> Int Int Int) (symbol "axffi_add"))
  (countVowels :: (-> String Int)  (symbol "axffi_count_vowels")))

Build against the crate with one flag — the driver runs axiom-bindgen when the crate's axiom/ module is missing or older than its src/, runs cargo build --release when the archive is missing (each only if the tool is on PATH), and links the archive because the block's library name says so:

axiom build --input p.ax --output p --crate path/to/crate

(--link-lib NAME --link-search DIR and $AXIOM_LINK_SEARCH remain as explicit overrides; an $AXIOM_PATH entry's ../target/release is searched too.) The emitter writes declare i64 @axffi_add(i64, i64) #0 for every item the program CALLS and the call site emits the same call i64 @sym(...) an internal call does. Five rules:

• The type is inline and required. A separate (:: name Type) draws AX3015; an item without :: type is a parse error.
• An item's signature names only Int, Float, Bool, Char, String and Foreign — one machine word each way — plus a callback parameter: an arrow of arity one to three whose leaves are words (Int, Float, Bool, Char). A type variable, a tuple, any other function type or a declared type ((Option Int), Handle, a struct) is AX3036: such values cross as a Foreign handle or through the generated wrapper (a Vec<T> result becomes a Vec; a Rust #[axiom_record] struct becomes a data type whose fields cross one word each).
• (symbol "...") is the only clause; any other head is a parse error naming it. Write it explicitly — a static link is one flat namespace and the default is the Axiom name.
• Calling one contributes the IO effect, exactly as __syscallN does, and it propagates transitively.
• A fn spelled like an item is a duplicate (AX3006); two blocks naming one library are not.

A symbol no linked archive defines is AX4004 at the item, before the toolchain runs — in three voices: nothing linked at all, an archive linked that lacks the name (with the nearest axffi_* name it does hold), and the search path it used. The check reads the archives' symbol tables, so a prefix of a real name is refused as the typo it is. A symbol the archive exports under a different shape — every #[axiom_export] shim carries a descriptor, axffi_add__sig_ii_i — is AX4005 at the item.

The other direction is --emit-staticlib: axiom build --input lib.ax --output libaxiom_lib.a --emit-staticlib archives a module with no main, every pub fn a C symbol under its own name, for a Rust (or C) host to link; --emit-rust-binding lib.rs beside it writes the Rust module that declares and wraps them (Int→i64, Float→f64, Bool→bool, Char→char, String→&str in and AxString out, a data/struct→a Rust struct/enum, Option/Result→Rust's own), synthesising the accessor shims those conversions need into the archive, and naming in a comment any function whose type it does not carry (a type variable, a tuple, an arrow).

foreign is not this feature renamed and remains AX2004. See docs/ffi.md.

---

Types

Primitive Types

Type	Description
Int	64-bit signed integer
Float	64-bit floating point
Bool	Boolean (true / false)
Char	A Unicode code point: 'A' is 65, 'é' is 233, '世' is 19990, '😀' is 128512
String	String (pointer)
()	Unit (no value). A type only — (:: main ()) and (:: f (-> () Int)) are accepted, and symbols renders the empty tuple as (). There is no unit value: () in expression position is AX2001 expected expression, as it is in [] and (set), and nothing in the language produces or consumes one
Unit	A distinct type constructor spelled Unit, not a synonym for (): symbols renders (:: a (-> () Int)) as (() -> Int) and (:: b (-> Unit Int)) as (Unit -> Int). Unit was missing from the parser's type-keyword set until 2026-08-10, so it was a bare unresolvable constructor that nothing asked about until signature types began to be resolved — see the self-hosting record
Void	Void
Any	Generic pointer
Foreign	An opaque pointer into memory Axiom did not allocate and does not own, held as one word (see ffi.md). Distinct from Int on purpose: tyCompat matches named constructors by name, and the distinction is load-bearing rather than documentary — a Foreign field is left OUT of the ARC reference map (docs/memory-model.md MM-LIFE-2d), so @axiom_release never follows it. Measured on (struct T (a : String) (b : Foreign) (c : String)): the map is payload words [0, 2]. (cast Foreign x) is the explicit way in and out
Handle	A Rust value Axiom OWNS a share of: a counted block of the foreign form holding the Rust pointer and its destructor (stdlib/Ffi.ax, ffi.md). A reference like String — mapped in a cell that holds it, released at a let's scope end — and when its last share goes the release runtime runs the Rust Drop once. axiom-bindgen wraps each opaque Rust type in its own data type around a Handle, so Counter and Widget stay distinct; ffiHandleClose destroys the value early and leaves the block inert

Sized Integers and Floats — Removed

I8–I128, U8–U128, Isize/Usize, Double and F32/F64 are refused (AX3002) since 2026-08-14. They were accepted names with no representational effect — every one lowered to a full-width i64, incompatible with Int so no operator accepted one — and the float spellings emitted integer arithmetic on double bit patterns, silently, because the emitter keys float arithmetic on the name Float alone (docs/memory-model.md MM-VAL-3c, MM-VAL-4b). Int is the one integer type and Float the one floating type; the real conversions are __intToFloat/__floatToInt.

Compound Types

(-> Int Int)           ; Function: Int -> Int
(-> Int Int Int)       ; Curried: Int -> Int -> Int
(* Int)                ; Pointer to Int

[T] and (A B) - the list and tuple types - are refused as AX2004 removed-construct, with migration advice naming the replacement. Both checked in signatures while no literal, no pattern and no runtime representation existed behind either: [1 2 3] is AX2001 expected expression, and (1 2) in expression position is read as an application of 1. A checked type no value can inhabit is worse than one that does not parse. Sequences are (Vec T); products are struct, sums are data. () is untouched: it is unit, and widely used.

Type Casting

cast reinterprets one word as another type. The type comes first and the expression second:

(cast Float someBits)

The word itself is unchanged — there is no conversion, no check and no runtime cost, which is why the real numeric conversions have their own names (__intToFloat, __floatToInt). cast is how a program crosses a distinction the checker is otherwise keeping for it: (cast Foreign x) in and out of an opaque pointer, (cast Int s) where a String handle is deliberately read as a word. It is the entry point to The Unsafe Layer, and everything that section says about what the checker stops proving applies from here.

Type Variables and Polymorphism

(data Maybe (a)
  (Nothing)
  (Just a))

The (a) after the type name introduces a type parameter. Types can be polymorphic — the same Maybe can hold any type.

Region Annotations

A signature may name the region a reference lives in, with @name as the last thing inside a type's parentheses:

(:: lookup (-> (Vec String @r) Int (String @r)))
(:: intern (-> (String @s) (Table @r) (Sym @r)))

@r and @s are region parameters: chosen by the caller through the arguments, once per call, as a type variable is. A region named in a signature outlives the function's own region — its caller's current one — and two named regions are unordered: neither is known to outlive the other. A signature that names no region is region-monomorphic in the caller's current region, so a program that never writes @ is the one-region instance, and an annotated program emits byte for byte what its un-annotated spelling emits: the annotation lives in a word of the type node that no reader of a type consults (scripts/check-region-escape.sh section 1 holds tests/stdlib/468-region-signatures.ax against its stripped twin, 1,652 lines of identical IR on 2026-09-03).

The annotation buys one rule, MM-RGN-3 of memory-model-v2-design.md §2.3: a value may be stored into, returned into, or captured by a place only if the value's region outlives the place's. Four codes, all errors, one fixture per shape in tests/diagnostics/645–649:

Code	Refuses
AX3060	a store — a set, a field write, a raw __store64, or a store a CALLEE makes through its parameter — whose place outlives the value
AX3061	a result that does not live in the region the signature names for it
AX3062	either of the above when the value is a closure, reported against the capture that makes it short-lived
AX3063	a call whose arguments do not agree on a region the callee names, or a signature naming a region on its result that no parameter supplies

An un-annotated callee is checked by reading its body, not by invariance. The checker computes, per function and as a fixpoint over the call graph like the effect row, which parameters its body stores a fresh value into and which parameters flow into which: vecPush stores its second parameter into its first, so (vecPush v x) is refused when x's region does not outlive v's and accepted when both live in one region, and (strLen s) on a string from any region is legal because nothing flows into s. The same facts answer restrict(no-escape) below. Two limits are stated rather than hidden: a call the compiler cannot resolve — through a parameter, a closure, a field — is assumed to store every argument into every argument; and nothing this stage compiles allocates into a named region, so a value the body allocates lives in the caller's region and cannot be stored into a @r place or answered as (T @r) — which includes growing a container that lives in @r, because vecPush allocates. Allocating into a named region is stage S4 of the design note.

The annotation is read from the declared signature only; the checker's instantiation copies of a type carry none, which is why the emitter never sees one. @ on its own stays AX1001, and @r anywhere but the end of a type's parentheses is AX2001.

Type Signatures

Every function has an optional type signature declared with :::

(:: add (-> Int Int Int))

This says add is a function that takes two Ints and returns an Int. The (-> A B C) syntax means a function that takes A, then B, and returns C. The type is curried; a top-level function still is not partially applicable, though a lambda is (see Partial Application).

Effect Types

Functions can carry effect annotations that the compiler checks:

(import IO)

(:: main Int)
;@axiom:effect(io)
(fn (main) (println "hello"))

The compiler validates that the body actually performs the declared effects.

---

Functions

Functions are the heart of Axiom. Every function has an optional type signature and a definition.

The fn form

(:: add (-> Int Int Int))
(fn (add x y)
  (+ x y))

define is legacy

(:: add (-> Int Int Int))
(define (add x y)
  (+ x y))

define is the old spelling of fn, and fn is the language's. The parser still accepts define so that old source parses, and reads it as fn; it is not a second style and not a choice. axiom fmt rewrites it to fn — tests/fmt/parity/182-define-rewrites.axp pins (define legacy 7) becoming (fn (legacy) 7) — and nothing under self_host/, stdlib/ or examples/ writes it. Write fn; when you meet define in old code, format the file.

Multi-Parameter Functions

(:: add3 (-> Int Int Int Int))
(fn (add3 x y z)
  (+ x (+ y z)))

Functions with No Parameters

(:: answer Int)
(fn answer 42)

Multi-Statement Bodies

Use braces for sequencing:

(fn (verbose-add x y)
  { (println "adding") (+ x y) })

The value of a brace block is the value of its last expression. Single expressions in braces are unwrapped automatically — { 42 } is just 42.

Function bodies, let bodies, if branches, and lambda bodies also support implicit sequencing without braces:

(import IO)

(:: main Int)
;@axiom:effect(io)
(fn (main)
  (println "Starting...")
  (println "Working...")
  0)

Lambda (Anonymous Functions)

(lambda (x) (+ x 1))

(lambda (x y) (+ x y))

(lambda (_) 42)    ; Ignoring a parameter with wildcard

Partial Application

One rule decides both halves, and it is the one AX3013's own note gives: a partial application has to hold the arguments it was not given, and a top-level function has no closure record to hold them in. A lambda has one. So a lambda may be applied to some of its arguments and a top-level function may not, however its signature is spelled.

A lambda applied to fewer arguments than it takes is a value. It holds what it was given and takes the rest, in order:

(:: main Int)
(fn (main)
  (let ((subFrom10 ((lambda (x y) (- x y)) 10)))
    (subFrom10 3)))                      ; 7 — 10 - 3, not 3 - 10

That value is ordinary in every way that was measured (tests/selfhost/988-lambda-partial-application.ax pins all of it): arguments may be supplied one at a time over as many applications as the lambda has parameters; a captured variable survives the partial, so the closure holds both what it captured and what it was handed; the partial escapes the function that built it, which is what makes (fn (mkAdder n) ((lambda (x y) (+ x y)) n)) a working adder factory; and it stores in a struct field typed (-> Int Int) and calls back through .f.

A top-level function is AX3013, and no signature changes that (tests/diagnostics/110-partial-application.ax pins the refusal):

(:: add (-> Int Int Int))
(fn (add x y) (+ x y))

(:: addFive (-> Int Int))
(fn (addFive) (add 5))

(:: main Int)
(fn main (addFive 1))
; error[AX3013]: partial application of `add`: it takes 2 argument(s)
;                and 1 were supplied

The workaround is the rule restated: give it a closure record by wrapping it in a lambda, (lambda (y) (add 5 y)).

The count is taken at the spine's root, not at each application. ((add3 1 2) 3) on a three-parameter top-level add3 is one call with three arguments and compiles; (let ((h (add3 1 2))) (h 3)) supplies two to the spine and is AX3013. The same flattening is why (((lambda (x y z) ...) 1 2) 3) is an ordinary saturated call.

Over-application is AX3004, not AX3013: once the arrows are consumed the result is no longer a function, and applying it reports "expected function type, found Int". A lambda's parameters carry no declared type, though, so an argument of the wrong type is not caught — ((lambda (x y) (- x y)) 10 "oops") compiles. That is a property of lambda generally and not of partial application.

_ holes — the explicit spelling

An application with at least one bare _ among its direct arguments desugars to a lambda, one fresh parameter per hole in left-to-right order. It is the spelling to reach for when the missing argument is not the last one, and it works on a top-level function — where partial application does not — because the desugaring is what builds the closure record:

(:: sub (-> Int Int Int))
(fn (sub x y) (- x y))

(:: main Int)
(fn (main)
  (let ((subFrom50 (sub 50 _))           ; (lambda (y) (sub 50 y))
        (subTo50 (sub _ 50)))            ; (lambda (x) (sub x 50))
    (- (subFrom50 8) (- (subTo50 50) 0))))   ; 42 - 0

A call with no hole is untouched, so AX3013 still fires exactly as it did. Holes apply to a lambda's arguments too — ((lambda (x y) (- x y)) 50 _) is a one-parameter function. _ keeps its unrelated meaning as a wildcard pattern; expression position had no prior meaning for it to collide with, and a bare _ there used to be AX3001. tests/selfhost/989-hole-partial-application.ax pins the holes, 988-lambda-partial-application.ax the lambdas.

---

Operators

All operators are prefix — they go before their arguments, just like any other function.

(+ 1 2)             ; 3
(- 10 3)            ; 7
(* 4 5)             ; 20
(/ 10 2)            ; 5
(% 10 3)            ; 1

(== 1 2)            ; false
(!= 1 2)            ; true
(< 1 2)             ; true
(> 1 2)             ; false
(<= 1 2)            ; true
(>= 1 2)            ; false

(&& true false)     ; false
(|| true false)     ; true

(- 5)               ; -5 (negation, unary)

(& 12 10)           ; 8   bitwise and
(| 12 10)           ; 14  bitwise or
(^ 12 10)           ; 6   bitwise xor
(<< 1 10)           ; 1024
(>> 1024 3)         ; 128

>> is arithmetic, so the sign bit is preserved: (>> -1024 3) is -128.

&& and || short-circuit: the right-hand operand is evaluated only when the left one does not already decide the answer. This is what makes a guard mean what it looks like — (&& (< i n) (== (strByte s i) c)) never reads s at i unless i is in range.

Int is 64-bit and two's complement. Negation of the most negative value yields itself rather than a positive number, which is why Fmt detects that value with a predicate rather than by comparing against a literal: there is no literal for it, and (- 0 9223372036854775807) is one greater than it.

The Eighteen, With Their Types

Operators are built in and always available — no import brings them in, and none can be shadowed. These are the types axiom symbols --builtins <file> prints for them, beside the memory primitives:

Operator	Signature
+, -, *, /, %	(Int -> (Int -> Int))
&, |, ^, <<, >>	(Int -> (Int -> Int)) — bitwise and, or, xor, shift left, shift right (arithmetic)
==, !=, <, >, <=, >=	(Int -> (Int -> Bool))
&&, ||	(Bool -> (Bool -> Bool))

Eighteen in all. The signature is curried because that is how the checker holds every function type; a call supplies both arguments at once, as the examples above do.

---

Let Bindings

Use let to introduce local variables:

(fn (compute n)
  (let ((x (+ n 1))
        (y (* x 2)))
    (+ x y)))

Bindings are evaluated in order — later bindings can reference earlier ones.

Mutable Bindings and while

A binding is immutable unless it is marked mut. A mut binding can be assigned with set, and while loops while its condition holds:

(fn (sumTo n)
  (let ((mut i 0)
        (mut acc 0))
    {
      (while (< i n)
        (set acc (+ acc i))
        (set i (+ i 1)))
      acc
    }))

The while body takes any number of expressions, so a loop that updates two variables needs no extra brackets. The whole form evaluates to 0 — a loop that ran zero times has no last iteration to take a value from.

set also writes a field, through a dotted path. The field carries the mut; the binding does not have to:

(struct Counter (mut n : Int) (step : Int))

(fn (bump c)
  (set c.n (+ c.n c.step)))

The path is resolved by name, so the offset — and the tag word a data constructor carries ahead of its fields — is the compiler's problem rather than yours. (set a.b.c v) writes c on the value at a.b, so it is c that must be declared mut and not b: the store mutates the inner value, not the slot holding it.

What set will not take is an arbitrary place expression: the target is a name or a field path, never a computed one, so (set (f x) 1) is a syntax error that says so instead of type-checking its way to a report about a non-assignable expression. A field write needs mut on the field and nothing on the binding — mut on a binding governs rebinding the local, which is a different operation. Raw memory is still reachable through memSetWord, which is what Vec and Map use to write slots that are not declared fields, and which no mutability marker gates.

Assigning to a binding that is not mut is a compile error:

(let ((x 0))
  (set x 1))     ; AX3012: cannot assign to immutable binding `x`

The report points at the declaration as well as the assignment, with a machine-applicable fix rewriting x to mut x — the fix belongs where the binding is introduced, not where it is used.

This is a real loop. while lowers to a branch back to a condition block, so a million iterations run in constant stack at -O0. Iteration by recursion still works and tail calls are guaranteed, but non-tail recursion remains stack-bounded — so a fold written as (+ (f i) (loop (+ i 1))) is the shape to avoid at scale. Optimisation has the three spellings side by side and the measured depth.

for — the counted loop and the container loop

for is one keyword with two shapes, told apart by how many operands follow the binder:

(for i 0 n                 ; the RANGE: i over [0, n), ascending
  (set acc (+ acc i)))

(for x xs                  ; the CONTAINER: x over each element of a (Vec a)
  (println x))

(for i lo hi body) runs body once per i in [lo, hi); a range whose hi is at or below lo runs zero times, backwards included (tests/stdlib/466-for-loop.ax, terms 1–3). (for x xs body) runs body once per element of the (Vec a) xs, with x bound to the element at whatever type a is — a (Vec String) prints directly and so does a (Vec Int) (terms 7 and 8), which is the one case the two loop macros the HTML DSL (stdlib/Html.ax, itself deleted on 2026-09-04) used to carry could not share. Both shapes evaluate to 0, as while does, and nesting is an ordinary nesting of scopes (term 10, 3 × 4 = 12 with each counter its own).

Exactly one body expression, and that is forced rather than chosen. A parser knows no types, so arity is the only discriminator it has: three operands after the binder is the range, two is the container. A variadic body would make (for x xs a b) ambiguous with the range, so several expressions go in { ... }, and a fifth element is a parse error that names both shapes rather than the one the parser happened to be attempting (AX2001, tests/diagnostics/625-for-shape).

Both ends are read once, before the loop, and that is a correctness property. The hand-written shape this replaces —

(let ((mut i 0)) (while (< i (vecLen xs)) { BODY (set i (+ i 1)) }))

— re-reads (vecLen xs) every iteration, so a body that pushes onto xs is a loop whose length moves under it. for binds lo and hi, or the container and its length, before the first iteration; terms 4 and 5 of 466 push onto the very vector the bound came from, and the loop still runs exactly its entry count.

It desugars to let, while and set in the parser (parseForExpr, self_host/parser.ax), so nothing after the parser knows the keyword exists: no AST tag was added, and the IR a for emits is the IR of the loop above with its bound hoisted. Measured: a range over println and the let/while/set it stands for, written by hand, emit byte-identical IR, 1,196 lines against 1,196.

Hygiene without a renamer. The desugaring's own bindings are for$lo, for$n, for$i and for$v, and $ is AX1001 unexpected character inside an identifier, so no program can write them and none can be captured by them: a caller's own i, n and v bound around a loop read as the caller's after it (466 term 6). The element read is the qualified Vec::vecGet and the length Vec::vecLen, so a program declaring its own vecLen cannot capture them — term 12 declares one that answers 99 and the loop still runs twice, and tests/diagnostics/626-for-not-a-container holds the same ablation. A program with no path to Vec at all, because no import reaches it, gets AX3001 undefined variable Vec::vecLen at the for: a diagnostic rather than a silence.

Iterating something that is not a container is refused at your expression, not at the keyword. (for x n body) over an Int underlines n: AX3004 type mismatch: expected Vec _a, found Int (626). Two rows per site, because the desugaring reads the container twice — once for its length, once per element — and the checker does not poison a binding after one bad use; the second row carries the keyword's span so the pair reads as two uses rather than as one report printed twice.

for is a keyword only at the head of a form, like every word in the table above: it is a parameter name, a let binder and a pattern variable everywhere else (466 term 11), fmt prints it as the identifier it is (tests/fmt/parity/199-for-arg-position.axp), and a macro of your own named for is dead code that still type-checks, because the keyword head wins with no diagnostic — measured, (macro (for a b c d) 42) followed by (for k 0 2 0) answers 0. fmt lays a for out as it lays out while: the binder and its bounds on the head line, the one body indented under them (198-for-head-layout.axp).

range in the prelude is the same loop as a macro — (range i lo hi body), stdlib/Pre.ax — and it stays. The compiler's own sources are built by the committed seed, which predates the keyword, so self_host/ and stdlib/ cannot write for until a reseed follows it (scripts/reseed.sh's rule: land the construct, reseed, then use it). The keyword's range shape mirrors range's template binding for binding, so the two agree by construction.

parallel — bindings that run beside the caller

(parallel p ((a e1) (b e2) ...) body...) evaluates every binding's expression at once, beside the caller, binds each answer to its name, and runs the body with them. The bindings are joined in the order written, always — a is bound before b whichever finished first — so which child finished first is not observable through the form, which is MM-PAR-5's rule for the process pool (memory-model.md) applied to a language form. p names the region the form runs in; today it is bound to that region's arena mark, a word, and the typed regions of memory-model-v2-design.md are what give it a type.

(fn (both n)
  (parallel p ((a (slow n)) (b (fast n)))
    (+ a b)))

Two lowerings, one surface. By default each binding is a process: fork, one shared page for the answer, wait4 — the isolation MM-PAR-3 makes true by construction, and a lowering that imports nothing (scripts/check-freestanding.sh sweeps the fixture that uses it and holds it at zero). Under axiom build --threads each binding is a thread: the platform's pthread_create, and the emitted runtime's eight mutable globals go thread_local so every thread allocates in an arena of its own (MM-PAR-6). scripts/check-parallel.sh builds the same fixture both ways and requires the same bytes on stdout and the same exit status, including from a binding that traps: under processes the child dies and the join re-raises its status; under threads the trap already ends the whole process (tests/stdlib/471-parallel-trap.ax, status 77 out of both). Section 8 of that gate runs four bindings that allocate — three 20,000-element Vecs and a 16 KB String built eight bytes at a time — and requires the thread lowering's bytes to be the process lowering's, which is the executed form of "one arena per thread": every parallel binding this repository ran before 2026-09-04 was arithmetic, so nothing had ever called axiom_alloc from a second thread.

Where the two lowerings stop agreeing: two bindings that both fail. With one trapping binding they answer the same status. With two, they do not, and the difference is not a bug in either — it is what the two lowerings are. Under processes the joins run in argument order, the first join re-raises its child's status, and nothing after it runs, so the status is the binding written first, always (10 runs per order, 2026-09-04). Under threads a trap is exit_group from the thread that took it, there is no join to reach, and the status is whichever binding failed first — 72 in 6 runs of 10 and 77 in the other 4, from the same binary on the same machine. The two backtraces interleave on fd 2 as well. If a program can have two bindings fail at once and cares which status it exits with, that program wants the default lowering, which is the deterministic one. scripts/check-parallel.sh section 9 pins the process lowering's statuses exactly and requires the thread lowering's to be one of the two traps, which is all a gate can assert about a race.

What a binding may answer is a word. The desugaring wraps each expression in a (-> Int Int) thunk and the join answers Int, so a binding whose expression is a String is refused where it is written — AX3004: expected (Int -> Int), found (_a -> String) on the expression (tests/diagnostics/641-parallel-word.ax). Under processes the answer crosses an address space through one page; under threads it would have to be promoted out of another thread's arena, which is the typed promotion of the regions design and not this form's. mut on a binding is a parse error (AX2001, 640-parallel-shape): a binding is bound once, at its join.

What a binding may capture. Words. A binding that captures a reference the parent holds is refused as AX3064 at the occurrence — under threads that value is shared with the parent and its count is touched from two threads with no fence, and axiom_retain/axiom_release are a plain load-add-store rather than an atomicrmw, so an increment is lost and a block a live reference still names is freed (MM-PAR-6). The rule is the language's and not the lowering's: it does not depend on --threads, because a program must not mean two different things depending on how it was built. Pass the value in through the thunk's word argument, or build a copy of it inside the binding.

This paragraph said "the thread lowering does not yet check … a binding may capture any name in scope" until 2026-09-03. AX3064 landed in 0.7.3 and the sentence did not move — measured against this compiler, a parallel binding capturing a String is refused at the occurrence.

__proc_spawn/__proc_join are exempt, and that is a statement about the primitive rather than a concession to a flag: they name the forked lowering, whose isolation is MM-PAR-3 by construction, so the child reads its own copy-on-write copy. stdlib/Par.ax is built on that exemption — a bounded pool that runs an Axiom closure over whatever the caller captured.

AX3064 also refuses the indirection: a spawn whose thunk is a frame-local name of arrow type - a parameter, a let-bound function - draws it at the name, because whatever function that name holds may close over a reference and the checker cannot tell from the spawn (tests/diagnostics/643-parallel-capture-hop.ax). Write the lambda at the spawn, or name a top-level function. A thunk that is neither a lambda nor a bare name - a call result, a conditional - is still accepted and still open work: no parallel written in source can reach that shape, since the parser's desugaring always emits a literal lambda, and it is reachable only from a hand-written __par_spawn or __thread_spawn.

Where it is not available. --threads on freebsd-* or windows-x86_64, and __thread_spawn there, are refused at build time (AX4006). freebsd's process lowering is available and measured, and measured by execution rather than by assembling: the Tests (freebsd-x86_64) leg boots FreeBSD 14.4 in a VM and runs the stdlib corpus there, 470-parallel, 471-parallel-trap and 476-par-pool among its 109 cases.

On windows-x86_64 there is no fork either, so neither lowering exists. A build for it warns AX4007 — a warning, not a refusal: the module still emits, with every spawn and join lowered to a trap, so a program whose parallel sits on a path it never takes still builds and still runs there. What the warning buys is being told at build time instead of at the first spawn, where the program prints axiom: parallel is not available on this target and exits 79. A spawn the kernel refuses is status 78 on every target.

A trap inside a binding, and its backtrace. The walk stops at main, because above main are the C runtime's frames and this module's symbol table cannot name them. A thread's stack has no main on it, so under --threads the walk used to run past @__axiom_par_entry and print two frames of the platform's thread runtime under this program's own symbols; it stops at that entry now (scripts/check-parallel.sh section 10, which ablates a compiler to show the frames come back without it).

The form is desugared by the parser into lets over three pairs of primitives — __par_spawn/__par_join, which follow --threads, and __thread_spawn/__thread_join and __proc_spawn/__proc_join, which name their lowering — each spawn (-> (-> Int Int) Int Int) and each join (-> Int Int), all carrying IO, so a parallel in a body claiming no-io is refused as a syscall there is. Nothing in self_host/ uses the form yet: the committed seed cannot parse it, and the rule is land, reseed, then use. stdlib/Par.ax spells the __proc_spawn/__proc_join pair directly instead, which the seed's stage1 compiles without trouble — the form is what the seed cannot parse, not an application of a primitive it registers.

Sequential Let Bindings

You can also write let bindings sequentially:

(let ((x 1))
  (let ((y (+ x 1)))
    (+ x y)))

---

Conditionals

if Expressions

(:: abs (-> Int Int))
(fn (abs n)
  (if (< n 0)
      (- 0 n)
      n))

if is an expression — it returns a value. Both branches are required.

cond — Multi-Branch Conditional

(:: classify (-> Int String))
(fn (classify n)
  (cond ((< n 0) "negative")
        ((== n 0) "zero")
        ((> n 0) "positive")))

Each branch is a (test body) pair. The first matching branch wins. An optional else clause can be added as the last argument.

---

Pattern Matching

match is one of Axiom's most powerful features. It lets you destructure values by their shape.

Basic Matching

(:: fromMaybe (-> Int (Maybe Int) Int))
(fn (fromMaybe default val)
  (match val
    ((Nothing) default)
    ((Just x) x)))

Matching Constructors with Fields

(match val
  ((Cons h t) h)
  ((Nil) 0))

Matching Literals

(match x
  (42 "the answer")
  (_ "anything else"))

Nested Patterns

(match lst
  ((Cons h (Cons h2 t)) ...)
  ((Nil) ...))

Nesting is checked and bound all the way down: inner constructor tags are tested recursively and each level's fields are extracted, so the arm above binds all three of h, h2 and t.

Wildcard Pattern

Use _ to match anything and ignore the value:

(match val
  ((Just x) x)
  (_ 0))

Exhaustiveness Checking

Axiom checks at compile time that every constructor of the matched type is covered. Missing constructors are a compile error (AX3005).

;; Correct: all constructors covered
(match val
  ((Nothing) default)
  ((Just x) x))

;; Incorrect: Missing Nothing arm — compile error AX3005
(match val
  ((Just x) x))

Arity is checked with it. A constructor pattern that names the wrong number of fields — ((Just) ...) or ((Just x y) ...) for a one-field Just — is AX3009, separately from the AX3005 that reports a constructor left uncovered.

The Built-in Option Type

Axiom provides a built-in Option type with Some and None constructors, always available without a data declaration:

(:: safeDiv (-> Int Int (Option Int)))
(fn (safeDiv a b)
  (match b
    ((0) (None))
    (_ (Some (/ a b)))))

(:: main Int)
(fn main
  (match (safeDiv 10 2)
    ((Some x) x)
    ((None) 0)))

---

Algebraic Data Types

Define custom types with constructors:

; Optional value
(data Maybe (a)
  (Nothing)
  (Just a))

; Linked list
(data List (a)
  (Nil)
  (Cons a (List a)))

; Binary tree
(data Tree (a)
  (Leaf)
  (Node (Tree a) a (Tree a)))

; Ordering result
(data Ordering
  (LT)
  (EQ)
  (GT))

The (a) after the type name is a type parameter — like generics in other languages.

Struct Variants — Named Fields Per Constructor

A constructor's fields can be named instead of positional:

(data Shape
  (Circle { r : Int })
  (Rect { w : Int, h : Int })
  (Point))

Values are built positionally, in declaration order:

(Circle 7)
(Rect 3 4)

and read back by name, either through field access or in a pattern:

(fn (describe s)
  {
    s.r                                    ; field access by name

    (match s
      ((Circle { r = r })       r)         ; named
      ((Rect   { h = h, w = w }) (* w h))  ; order does not matter
      ((Point)                  0))
  })

Named patterns buy three things a positional pattern cannot:

Order independence	{ h = h, w = w } binds what its names say. Reordering two same-typed fields in a declaration cannot silently swap them at every match site.
Partiality	A field the arm does not name is simply not bound — no _ placeholder to keep in step with the constructor's arity.
Punning	{ w, h } means { w = w, h = h }.

So the common case is short:

(match s
  ((Circle { r })    r)
  ((Rect { w, h })   (* w h))
  ((Point)           0))

Punning and explicit binding mix freely, and named patterns nest:

(match x
  ((Wrap { inner = (Rect { w, h }), tag = t }) (+ (* w h) t))
  ((Wrap { tag = t })                          t))

Positional patterns keep working on the same type; named fields add a spelling rather than replacing one.

How ADTs Actually Run

A data type is assigned one of three representations, computed once per type from its constructors (codegen.ax's ctorsRep; memory-model.md MM-VAL-8 is normative). Tags are globally unique across the program, not per type.

Condition	Representation
every constructor is nullary	a value is its tag, an immediate below 4096; nothing allocates
mixed nullary and fieldful	nullary constructors are immediate tags; fieldful ones are heap blocks
no nullary constructor, or the type's tags would reach 4096	every value is a heap block

A heap block holds the tag in word 0 and its fields in words 1.., one 8-byte word each. Because an immediate tag and a block address can arrive in the same slot, a match over a mixed type tells them apart with a runtime < 4096 test — every address a value is handed out at is at or above that bound (MM-VAL-9). In (data L (Nil) (Cons Int L)) the constructor (Nil) lowers to the immediate 2 and matching it is an icmp eq i64 2, 2 with no allocation at all; tests/stdlib/270-nullary-unboxed.ax and tests/selfhost/400-mixed-nullary.ax pin the two unboxing shapes.

Recursion needs no special case in either direction: a field whose type is the type being declared is just another 8-byte word holding that value's address, so (data List (a) (Nil) (Cons a (List a))) lowers with no cycle detection, no indirection table and no boxing rule of its own. Building a List is that type as a whole program.

Deriving

derive is explicit declaration macros, not a clause: write (deriveEq T) where you want it, and the macro generates a real FUNCTION — checked and compiled like a written one, and called by name. (deriveEq Colour) gives eqColour, (deriveShow Colour) gives showColour; measured, both are ordinary F rows carrying #generated=deriveEq/#generated=deriveShow. Until 0.6.0 the template generated a trait impl instead, dispatched by the argument's type; the macro machinery is unchanged and the declaration it expands into is now a plain fn (see Macros for a complete deriveEq and macro-system.md §10.2 for the fieldful form).

The deriving clause is refused (AX2004, since 2026-08-14). It had parsed and been silently discarded from the day it was written — its names never reached the AST, and no instance was ever derived — and a clause that does nothing is worse than one that does not parse (MAC-CAP-9's settled decision):

(data Colour () (Red) (Green) deriving (Eq Show))
; error[AX2004]: `deriving` parsed and derived nothing, and is now refused

---

Structs

Products of named fields:

(struct Point
  (x : Int)
  (y : Int))

There are no layout modifiers. packed, repr(C) and align(N) were documented here and accepted by nothing: the parser has always answered AX2001 for all three. Axiom does cross the C ABI now — an extern block links a static archive — but nothing crosses it as a struct: a scalar goes one word each way, and a record crosses as its fields (ffi.md §8). There is no layout for a modifier to change.

A field is immutable unless it is declared mut, exactly as a let binding is. mut goes on the field, inside its parentheses — not on the struct:

(struct Counter
  (mut count : Int))

Writing count on a Counter is then legal; writing any field of a Point above is AX3012. Writing a field has both halves.

The : is not optional. It is what makes the form a field declaration at all — the grammar's own note is that a declaration and a construction "only become visible at the :" — so (x Int) is not a shorter spelling of (x : Int). It used to be accepted anyway, with the written type skipped and the field left at the empty type variable, and the consequence was not cosmetic: fldClass cannot classify a variable, so the field was left out of the block's reference map and out of MM-LIFE-2c event 5, and a value stored into it was released by its own owner while the field still pointed at the block — a use-after-free out of a program check accepted, measured at exit 139. It is now AX3056, an error, at the field's name, on all three spellings that reach the empty variable: no :, a : whose type is not a type, and a bare (x) (tests/diagnostics/388-struct-field-untyped.ax).

Constructing, binding, and reading a field

Construction is positional: the constructor is the struct's own name, and its arguments are its fields in declaration order. A value binds to a let, passes to a function and returns from one like any other:

(struct Point
  (x : Int)
  (y : Int))

(:: shift (-> Point Int Point))
(fn (shift p n) (Point (+ p.x n) p.y))

(:: sum (-> Point Int))
(fn (sum p) (+ p.x p.y))

(:: main Int)
(fn (main) (sum (shift (Point 1 2) 10)))     ; exits 13

There is no named-field spelling, and the two spellings a reader reaches for both fail without mentioning structs at all. (Point (x 1) (y 2)) reads x and y as variables and reports AX3001 twice — with + offered as the nearest binding in scope, which is how far the compiler is from understanding what was meant:

(struct Point (x : Int) (y : Int))

(:: main Int)
(fn (main)
  (let ((p (Point (x 1) (y 2)))) p.x))
; error[AX3001]: undefined variable `x`
; error[AX3001]: undefined variable `y`

(Point :x 1 :y 2) stops earlier still, at the colon, with AX2001 "expected expression, found :". Handing over the wrong number of fields is AX3008 at the constructor — "struct Point expects 2 field(s), found 1" — trailed by an AX3004 cascade wherever the half-built value is used; the wrong type in a field is a plain AX3004 at the offending argument.

.field binds to a name, not to an expression. a.b.c chains left to right, reading the c of the value at a.b, and a field access is an ordinary expression anywhere a value is wanted. But the suffix is parsed onto an identifier token, so a call's result cannot be dereferenced in place — (mk 5).x and even (p).x are AX2001 at the dot. Bind it first:

(struct Point (x : Int) (y : Int))

(:: mk (-> Int Point))
(fn (mk n) (Point n 2))

(:: main Int)
(fn (main) (mk 5).x)
; error[AX2001]: expected expression, found `.`

A field the type does not have is AX3007, anchored at the field name, and it answers for every type rather than only for structs: n.x where n is an Int reports "field x not found on type Int".

A struct renders without any declaration of yours — (format (Point 1 2)) is {x = 1, y = 2}.

Writing a field

set writes through a dotted path (Mutable Bindings and while has the general rule), and the write needs mut on the field — and nothing on the binding. This is accepted and exits 9:

(struct Point
  (mut x : Int)
  (y : Int))

(:: main Int)
(fn (main)
  (let ((p (Point 1 2)))
    { (set p.x 9) p.x }))

p is an immutable let, and that does not matter: mut on a binding governs rebinding the local, and mutating what a binding points at is a different operation gated by a different marker. Drop the mut from x and the same program is refused, at the field name in the write:

(struct Point
  (x : Int)
  (y : Int))

(:: main Int)
(fn (main)
  (let ((p (Point 1 2)))
    { (set p.x 9) p.x }))
; error[AX3012]: cannot assign to field `x` of `Point`: the field is not declared `mut`

The report is anchored on x in (set p.x 9), not on the declaration: the struct is often in another file, and a diagnostic's span belongs to the unit it was raised in. The help names the line to write — `(mut x : Int)` — and there is no machine-applicable fix for the same reason. tests/diagnostics/467-set-immutable-field.ax pins it, and tests/selfhost/561-field-store-mut.ax pins that a mut field still writes.

This is new in 0.6.0, and it breaks source compatibility — a program that wrote an unmarked field compiled before and is refused now. It takes no line in compat/BREAKING: that file's subject is the standard library's public surface, and the surface did not move (measured — the 619 normalised AXSYM rows are byte-identical across the change, and no #fields= entry carries mutability). The migration it did cost is 30 fields across 16 declarations, every one of them found by compiling the tree and reading the refusals. Before it, mut on a field was parsed and discarded, which parseOneField said in as many words at the time — the marker was "not recorded ... only skipped" — so the program above compiled and exited 9 with no marker anywhere. That is the shape AX2004's explain text calls worse than no marker at all: "a marker that reads as an ownership guarantee and supplies none is worse than no marker, because a reader spends trust on it." linear, consume and deriving were removed from this language for exactly that; mut on a field was enforced instead, because unlike those three it had a rule worth keeping.

Because the write goes through the value rather than the binding, it reaches through a parameter, and a callee's store is visible to its caller. This exits 42, over a nested path — note that inn needs no mut, because the store mutates the Inner it points at rather than the inn slot:

(struct Inner (mut v : Int))
(struct Outer (inn : Inner))

(:: bump (-> Outer Int))
(fn (bump o) { (set o.inn.v (+ o.inn.v 1)) o.inn.v })

(:: main Int)
(fn (main)
  (let ((o (Outer (Inner 40))))
    { (bump o) (bump o) o.inn.v }))

memSetWord is not gated by any of this. It takes a block and a word index and writes it, which is what Vec and Map use for slots that are not declared fields; a field declared without mut is protected from set, not from raw memory.

Type parameters

A struct may take type parameters, in the parenthesised spelling data already uses — (struct Boxed (a) (val : a)). The first group is ambiguous here in a way it is not in a data, because a struct's other groups are FIELDS and start lowercase too, so the rule is that a parameter list is lowercase names and nothing else: (a b) is parameters, (start : Int) is a field because of the colon, and (msg String) is a field because String is uppercase — which is what keeps tests/diagnostics/388-struct-field-untyped.ax's three AX3056 refusals intact.

Construction stays positional and the parameter is fixed by what is handed over, so one declaration serves every instantiation in the same program:

(import Str)

(struct Boxed (a)
  (val : a))

(:: main Int)
(fn (main)
  (let ((bi (Boxed 7)) (bs (Boxed "abc")))
    (+ bi.val (strLen bs.val))))     ; exits 10

tests/selfhost/901-parameterised-struct.ax pins two parameters staying independent across one shared instantiation.

Fields that hold functions

A field's type can be an arrow, and that is what makes a parameterised struct an interface — it is what replaced traits in 0.6.0, and Capability Records is the whole story, including how effects cross the boundary. The struct mechanics are these.

Both call spellings work: (c.render 7) applies the field directly, and ((c.render) 7) parenthesises the access first. They are the same call rather than merely equivalent — the two spellings emit byte-identical IR under emit-llvm. This exits 5:

(import Fmt)
(import Str)

(struct ShowOf (a)
  (render : (-> a String)))

(:: showInt (ShowOf Int))
(fn (showInt) (ShowOf fmtInt))

(:: main Int)
(fn (main)
  (let ((c showInt))
    (+ (strLen (c.render 123))
       (strLen ((c.render) 45)))))

A top-level function of two or more arguments cannot be handed over by name, and this is the limit a reader meets first. It is AX3013, and it is not about structs: naming add where a value is wanted reports "partial application of add: it takes 2 argument(s) and 0 were supplied — add takes 2 arguments, so it cannot be used as a bare value". Every capability record in this document that is built from a named function holds an arity-1 one for exactly that reason.

(struct Ops (g : (-> Int Int Int)))

(:: add (-> Int Int Int))
(fn (add x y) (+ x y))

(:: main Int)
(fn (main)
  (let ((o (Ops add)))
    (o.g 5 3)))
; error[AX3013]: partial application of `add`: it takes 2 argument(s)
;                and 0 were supplied

Wrap a wider function in a lambda, which does get a closure record to keep arguments in. And once the field holds a lambda it may be applied to some of its arguments: partial application works for a lambda, and it is only a top-level function that has nowhere to put the arguments it was not given (Partial Application). (o.g 5) below is a value, and the program exits 8:

(struct Ops (g : (-> Int Int Int)))

(:: add (-> Int Int Int))
(fn (add x y) (+ x y))

(:: main Int)
(fn (main)
  (let ((o (Ops (lambda (x y) (add x y)))))
    (let ((add5 (o.g 5)))
      (add5 3))))

---

Type Aliases

(type StringList () = [String])

A type alias gives a name to an existing type. It does not create a new type — StringList and [String] are interchangeable: the alias is expanded before checking in every position that names a type — a function signature, a struct field, and a data constructor's fields — and its float flags are rewritten with it, so the checker and the emitter cannot disagree about a (type Real = Float). The two record positions were added on 2026-08-23: an alias there stayed nominal, so (R 1 s) drew AX3004 against its own field, and behind that the emitter's fldClass could not classify the alias, forced the block to a leaf, and dropped the reference map that a String in the NEXT field needed — 80 bytes an iteration, on the field that was spelled correctly (tests/stdlib/374-arc-alias-field.ax). A PARAMETERISED alias — (type Pair a = ...) — needs substitution and is not expanded; it behaves nominally. tests/selfhost/973-type-alias.ax

Range-constrained subtypes

(subtype Positive is Int range 1 .. 10)
(subtype NonNeg is Int range 0)

A subtype names a subset of Int's values. It is a distinct type, not an alias: a Positive is not an Int where the checker compares names, and the base is Int and only Int. The check is at the conversion, enforced at run time by the same compare-branch-trap a contract lowers to (status 80), because the compiler has no value analysis that could discharge it statically:

• (cast Positive v) traps unless 1 <= v < 10. A lower-only range checks >= with no upper bound.
• Passing a base value to a (-> Positive Int) parameter, or returning one through (-> Int Positive), checks at the boundary the same way.
• Widening needs no check: a Positive already proved its range, so (cast Int p) and passing one where Int is declared are free.

Subtype values compute as Int — arithmetic and println treat a Positive as the Int it constrains. tests/selfhost/134-subtype-checked.ax pins the satisfied conversions; 135-subtype-violated.ax pins the status a failed one exits with.

---

Effects

Axiom infers each function's side effects transitively - a fixpoint over every function body, so a syscall three calls down still counts - and validates any ;@axiom:effect(...)/;@axiom:pure claims against what it inferred. A refuted claim is an error (AX3010); one the walk was not in a position to check is a warning (AX3037). Effects do not appear in function types. Untagged functions ARE policed: silence is the claim "performs no IO", and a body performing IO under it is AX3042, an error. Only IO is REQUIRED - Alloc and Mut are ambient, inferred and reported but never demanded, and the line was measured rather than chosen, and re-measured 2026-09-08 (scripts/check-effect-distribution.sh pins the whole histogram in two views): of the 4,271 declarations symbols --calls self_host/main.ax lists for the compiler and its standard library, 2,700 perform something at all, and 2,037 of those perform exactly Alloc,Mut - which is every function that touches a String or a Vec. Mut anywhere is on 2,526 of the 2,700, so requiring it would be requiring a tag on 94% of everything that has an effect at all. The stdlib view agrees: 410 of 821 perform, 178 of those exactly Alloc,Mut, with two singletons carrying custom effects (Assert, Fallible) and 3 rows marked #effects-incomplete. IO is the one effect a caller cannot learn without opening the callee. Alloc and Mut are still DECLARABLE, and checked when declared: ;@axiom:effect(mut) over a body that writes a field is accepted, and over one that does not it is AX3010. The same holds for a custom effect. What is special about IO is that its absence is itself a claim. axiom symbols --diagnostic-format ai reports the inferred set as #effects=... beside any declared tags; the default human table has no metadata column and shows neither.

Effect Polymorphism

A higher-order function's summary has two halves: the concrete effects its own body performs, and the effect-transparent parameters - the parameters it calls (directly, through a let alias, or by passing them onward to another function's effect-transparent position). (fn (apply f x) (f x)) performs nothing concretely and everything its first argument performs; axiom symbols reports that as #effect-params=f beside #effects=..., and every call site instantiates the mark with the argument actually passed.

Claims are validated against the concrete half. ;@axiom:pure on apply stands - "pure modulo its function parameters" is what purity means on a higher-order function - and a declared effect the body does not perform concretely is accepted when a callback could supply it. The exception is a claimed effect that no declaration introduces at all: nothing could ever supply it, so it warns regardless.

restrict(...) is read differently, and deliberately. "No IO modulo its function parameters" is not what a reader takes restrict(no-io) to mean, so a transitive restriction on a body that calls one of its own parameters is AX3051 - unverifiable - rather than accepted (restrict(...) below). The difference is not a policy choice: pure describes a body, and a restriction is a guarantee about calling it.

Attribution is otherwise unchanged: a reference to a named function answers for that function's effects at the reference site, and a lambda literal answers for its body where the literal appears.

When the Walk Cannot Answer

A call whose head the walk cannot resolve to a function makes the inferred set a lower bound rather than the set. Four shapes reach it:

shape	example
a head that is not a name	((b.f) x), an if or match in head position
a let bound to anything but a name or a lambda literal	(let ((g b.f)) (g 7))
a pattern binder	(match h ((Wrap f) (f 7)))
an unfollowable value handed to an effect-transparent position whose declared type could hold a function	(fn (p h b) (h b.f))

The first three are one route through memory wearing three spellings - a function value goes into a struct, a data constructor or a container in one place and is called in another, and no call edge runs between them.

The fourth is not a memory read at the call. h is a parameter, so calling it is modelled; that is what effect transparency is for. What is not modelled is the value handed into the transparent position. "Pure modulo its function parameters" excuses h; it does not excuse an argument the walk cannot name, and b.f is a word out of a struct that the transparent parameter will call.

And it asks the callee's signature which positions those are. An arrow, a type variable or poison can hold a callable value; a concrete Int cannot, so a value the walk could not follow, landing in an Int position, hides nothing — applying it is AX3004 and the program does not compile. (fn (twice f x) (f (f x))) under (-> (-> Int Int) Int Int) is therefore complete, and the same body under (-> (-> a a) a a) is not, because a caller may instantiate a to an arrow. Until 2026-08-31 the argument's shape decided alone, and vecSiftDownBy — (cmp (memGetWord d r) (memGetWord d k)) against a cmp declared (-> Int Int Int) — published the standard library's sort as a lower bound on the strength of two machine words its own signature calls integers, so restrict(no-io) over anything that sorted answered AX3051 rather than yes or no.

The walk records that, symbols prints it as #effects-incomplete, and claim checking splits on it:

• a claim of ABSENCE (;@axiom:pure, ;@axiom:effect(pure)) cannot be validated against a lower bound, so it draws AX3037, a warning;
• a claim of PRESENCE (;@axiom:effect(io)) is left alone, because an unresolved call may be exactly where the effect comes from, and reporting missing IO there would be a mis-report rather than an omission.

A lambda's own parameter is marked identically and is unreachable today: a called lambda parameter does not type-check (AX3004), so no well-typed program gets there. The marker is set anyway, because the alternative would record that the binder was attributed somewhere, and it is not.

The same lower bound reaches handle. A handled-effects list cannot be checked against a lower bound either, so a handle whose body contains an unresolved call draws AX3038 - a warning, where AX3011 (the same question answered) is an error. That gap was not cosmetic: an effect operation reached with no handler installed aborts the process with status 71, and until 2026-08-24 with no message at all, so a handle whose body reached an effect through a struct field turned a compile-time refusal into a runtime trap. The trap now prints axiom: unhandled effect on stderr - which makes the fault legible without making it any less a runtime fault, and is why AX3038 is still worth having.

Definite and possible

The opposite departure is an effect the body MAY perform without the walk being able to say it does, and it is recorded per effect, not per row. One shape produces it:

shape	example
a bare arrow-typed name outside argument position	(fn (handoff k) shout) - shout is handed back, not called; (ConsoleOf writeLine) - it is stored in a capability record

There was a second until 0.6.0: a trait method with more than one implementation, where the fixpoint unioned every implementation because dispatch picked one and the walk could not say which. trait and impl are AX2004 now, and dispatch through a record's field is not a resolved call at all — it contributes nothing and marks the row #effects-incomplete instead.

Every effect the referent's row carries arrives as possible: the body may perform it, through whoever calls the value. An effect the body reaches by a call is definite. The two spellings of one effect can both be present - a body that calls shout and also names it - and each consumer reads the half it is entitled to:

• AX3042 and the contradicted arm of AX3010 read the definite half. An untagged function whose row holds IO only as possible is not accused; a ;@axiom:pure over it draws AX3037, cannot be checked, exactly as over a lower bound. A definite IO beside a possible Alloc is accused: until 2026-08-29 one row-global marker excused the whole row, so every untagged function one hop above a println with a {hole} compiled clean and printed - the hole went through Show's four trait implementations, and the excuse for their Alloc was excusing the writeStr.
• AX3011, the missing arm of AX3010 and restrict(...) read the union. A handle list must name what the body may reach, and a claimed effect the body may perform is not missing.
• symbols prints the union as #effects=, and when some member is possible and not definite adds #effects-overapprox with #effects-possible=A,B naming which. (fn (handoff k) shout) renders #effects=IO #effects-overapprox #effects-possible=IO; a function that prints "n={n}" renders #effects=Alloc,IO,Mut with no admission, because everything the hole's rendering can contribute is also definite there.

One shape is a lower bound wearing an upper bound's clothes and is recorded as the lower bound it is: a call that supplies more arguments than the callee's own parameters - ((handoff 1) n) - applies the callee's result, a value the walk cannot follow, so the row is #effects-incomplete as well.

AXTAG Keys

The key namespace is open: a key the compiler does not know is metadata, is recorded, and is not checked. agent:readonly draws nothing and is meant to.

A key one edit - or one change of case - from a key the compiler knows

• pure, effect, raw, pre, post, restrict, isr, unhandled - draws AX3039. ;@axiom:pur is not a purity claim, so nothing checks it as one, and a body performing IO under it drew no AX3010 at all: the tag read like a guarantee and bought silence. A key the compiler knows is never a near miss of another one it knows: pre is one insertion from pure, and drew "did you mean pure?" until 2026-08-29. Knowing a key and checking it are separate: pre, post and restrict were known ahead of their checks, and until a key's check lands it is recorded and not checked exactly as an unknown one is - what knowing it buys is that a slip FROM it is reported. All three are checked now; the sentence is kept because it is the rule a NEXT key arrives under. A key containing : is never reported, because a namespaced key is deliberate by construction and its distance from pure is not evidence about anything.

restrict(...) - what a declaration does NOT do

;@axiom:restrict(name, name, ...) is a claim that this declaration does not do something, answered from analysis the checker already performs and used to throw away. The list is CLOSED - a name outside it is AX3052, an error, because inside the one key the compiler has said it checks an unknown name is a claim and not metadata. Eight restrictions are checked:

Restriction	Decided by	Scope
no-io	IO is not in the effect row	transitive
no-alloc	Alloc is not in the effect row	transitive
no-foreign	no call-graph path reaches an extern item	transitive
no-cast	no cast head in this body	LOCAL
no-cast:deep	no cast head in this body or in any function it reaches	transitive, opt-in
no-recursion	no cycle in the call graph reachable from this declaration	transitive
strict	a MODIFIER: an unsettleable claim in this set is AX3057 (error), not AX3051 (warning)	—
no-wrap	no integer +, - or * head in this body	LOCAL
no-escape	nothing this body allocates flows into any of its parameters, read off the region facts (Region Annotations); refuted through a named callee (vecPush grows its argument), unverifiable over a call the walk cannot resolve	transitive

Every transitive violation names its path. The checker walks the call graph breadth-first from the claiming declaration to the nearest entry where the effect enters - a syscall primitive, an extern, a builtin whose row is seeded (__argc, __alloc), or a function whose row carries the effect while no callee does, which is an alloc form or a handle in that body and is said so - and renders the hops in the resolved spellings symbols --calls prints, Mod$name among them, so a path cross-checks #calls= hop for hop:

E AX3049 ... "`parseConfig` claims `restrict(no-io)` and the body performs IO: parseConfig -> readSection -> IO$writeStr -> Sys$sysWriteAllFd -> Sys$sysWriteFd -> __syscall3"

no-recursion is a cycle, which is global by definition: a depth-first walk over the same graph, and the diagnostic renders the walk from the declaration to the repeated function - ping -> pong -> pang -> ping, or entry -> countdown -> countdown when the cycle is below the claim. A while loop is not recursion. It pairs with scripts/check-stack-depth.sh, which measures the compiler's stack need dynamically: a region under no-recursion is one whose stack need is bounded by its depth rather than by its input, the same property from the static side.

Three are transitive by construction and two are not, and the difference is not a policy choice. no-io and no-alloc read the effect row, which is already a transitive fixpoint (effects are inferred transitively, above): a function calling an IO-performing function has IO in its row, and a check reading the row has no local reading available to it. no-foreign walks the call graph symbols --calls prints, because the row cannot tell IO through a syscall from IO through an extern and the graph can. no-cast is lexical - a cast is an act the body that writes it performs, not a property that propagates - so it is checked in this body only and reported at the cast, and a callee's casts are the callee's claim to make. Measured: 653 (cast in self_host/ and stdlib/ against 3,196 fn declarations, so a transitive no-cast would refuse nearly every program that reaches the standard library - which is why the transitive reading is the separate, opt-in spelling no-cast:deep: this body's casts at their spans, and the nearest reachable function whose body casts, once, at the declaration, with the path. sizeof and alignof are not casts here: they read a layout and reinterpret nothing. no-wrap is lexical for the same reason: on Int operands +, - and * lower to plain add/sub/mul with no nsw (measured: self_host/codegen.ax emits no with.overflow intrinsic and no nsw/nuw flag anywhere), so a silent wraparound is an act the body performs by writing the operator, reported at the operator itself. stdlib/Err.ax's addChecked, subChecked and mulChecked are the checked alternative, every one (-> Int Int (Result Int Error)); a body that switches to one pulls Alloc into its own effect row (constructing the Result allocates), which is why no-wrap cannot be satisfied together with no-alloc or pure by a body that needs arithmetic - docs/checked-arithmetic-design.md is the design note.

Being lexical, it matches a spelling, and two things wearing those spellings cannot wrap. Neither is refused, and tests/diagnostics/394-restrict-no-wrap-exempt.ax is the pair, each beside the case that keeps the exemption narrow:

• the three operators on Float operands, which lower to fadd/fsub/fmul. There is no wraparound to refuse, and addChecked is (-> Int Int (Result Int Error)), so the fix the diagnostic named did not typecheck against one either. A Float + nested inside an Int + still reports the outer operator.
• the for keyword's own counter increment. for desugars in the parser to (set for$i (+ for$i 1)) beneath a (< for$i for$n) guard, and every generated node carries the keyword's span - so the diagnostic named a + the source does not contain and underlined the word for, with no fix available, since a loop counter cannot be a Result. The guard is what makes skipping it sound rather than convenient: the body runs only while for$i < for$n, so the increment cannot pass INT_MAX. A loop written out by hand is still refused - the author wrote that operator - and so is arithmetic in the loop's body.

A violation is AX3049, an error with no warning stage, for the argument that made AX3010 one: the tag is a claim the author wrote, and a build shipping a false one publishes a guarantee the program does not keep. Deleting the tag silences it and withdraws the claim; an unrestricted function is never asked. A claim this walk cannot settle is AX3051, a warning in tests/diagnostics/severity.policy, and there are three readings.

Two are about a row that is not closed, one direction each: an effect ABSENT from a row that is a lower bound (#effects-incomplete), or present only as a POSSIBLE effect (#effects-possible=, the row's #effects-overapprox admission). An effect present in a lower bound, or definite beside a possible one, is a violation.

The third is about a row that IS closed and answers the wrong question. A body that CALLS one of its own parameters is effect-transparent — symbols says so, #effect-params=f — and what it performs is decided by the argument each caller passes. Effect Polymorphism above records that ;@axiom:pure on (fn (apply f x) (f x)) stands, because purity is a claim about a BODY; a restriction is not read that way by anyone, so a transitive restriction on such a function is AX3051 rather than silence. Measured before this reading existed: (fn (runIt f n) { (f "x") n }) under restrict(no-io) checked OK with no diagnostic at all and printed to stdout at run time, and no-recursion was silent over runIt -> back -> runIt, a cycle whose middle edge is a parameter the graph has no edge for. A body that performs the effect concretely AND calls a parameter is AX3049: refuted beats undecided.

strict — when unproven must mean refused. restrict(no-io, strict) is the same claim with a different answer where the walk cannot settle it: AX3057, an error, instead of AX3051. The default stays a warning for the reason above — a body dispatching through a stored function is a correct program the walk cannot follow, and refusing it would make that shape unwriteable under any restriction rather than merely unverified. strict is the author's side of that argument, per declaration: a restriction on a sensitive operation is asked for as a guarantee, and a reader who sees restrict(no-io) and assumes it was checked is worse off than one who sees nothing.

strict is a modifier and not a restriction. It names nothing a body must not do, so it is neither dispatched as a restriction nor reported by AX3052 — restrict(strict) alone restricts nothing and is silent. A claim the walk refutes is still AX3049, not AX3057: refuted beats unproven, the same way it beats unverifiable. A claim the walk settles and finds kept is silent, which is what strict is asking for. tests/diagnostics/393-restrict-strict.ax carries all seven arms.

no-cast and no-wrap never draw AX3051 under any of the three: both are lexical, are checked whether or not a call resolved, and a parameter cannot change the bytes of this body.

A restriction is a per-declaration claim. A tag attaches to the declaration written below it, on the :: or on the fn, and both are read as one set; symbols renders it as #restrict=no-io,no-alloc on the function's row. There is no module-wide form - measured, a tag above (import IO) attaches to the import and to no function's row - and module scope is deferred: a module-wide claim is written on each declaration, where symbols shows it. A restrict tag is not an effect claim and does not stand in for one: a restricted function that performs IO without effect(io) draws AX3042 like any other, and restrict(no-io) over it draws AX3049 as well.

isr - an interrupt entry point

;@axiom:isr marks a function the hardware calls by name with no arguments, which must not allocate. It is two claims in one tag: the declaration takes no parameters, and its body keeps restrict(no-alloc). A parameterised isr draws AX3010 at the declaration - the tag contradicting what is written under it - and an allocating isr draws AX3049 naming no-alloc, with the same path, the same AX3051 warning where the walk cannot settle the claim, and the same strict composition as a written restriction, because it is checked as one: the tag pushes no-alloc into the claim set the walk already answers. An author who writes both spellings is checked once, not twice. tests/diagnostics/651-isr-params.ax and 652-isr-alloc.ax pin the two refusals; scripts/check-isr.sh holds the composition with --emit-staticlib, where every pub fn of the file is already a C symbol under its own name - so a pub ISR is reachable by name, checked for parameters, and checked for allocation, and an allocating one is a compile error rather than a heap corruption. Only pub functions become symbols; a private isr is still checked, which is what makes the tag meaningful on a helper nobody calls from C.

pre(...) / post(...) - a claim the compiler CANNOT decide

;@axiom:pre(EXPR) and ;@axiom:post(EXPR) are the one pair of keys here whose claim the checker cannot refuse, and the design follows from that rather than from taste. restrict(...) is refused statically because the effect row and the call graph are fixpoints the checker already computes; (> n 0) is a statement about a VALUE, and there is no value analysis in this compiler at all - measured, grep -v '^ *;' FILE | grep -c 'constFold\|constantFold\|interval\|rangeOf\|abstractVal' over self_host/typecheck.ax, self_host/codegen.ax and self_host/expand.ax answers 0, 0 and 0. The comment lines are excluded because the sentence making the claim matches the pattern it quotes; without the exclusion it answers 1, 1, 1, all three of them that sentence. A claim nothing checks is a comment, and this project refuses those, so a contract is compiled into the body and checked on every call - which is what Ada does, and for the same reason.

;@axiom:pre((> n 0))
;@axiom:post((>= result 0))
(:: half (-> Int Int))

(fn (half n) (/ n 2))

(half 0) writes axiom: precondition failed in `half`: (> n 0) on fd 2, prints the backtrace, and exits 80, beside MM-EXEC-16's 70/71/72, the FFI boundary's 73, 74's absent syscall ABI, 75's invalid arena mark, 76's reset past a live handle and 77's out-of-range index. 80 is the contract trap's own row since D3 (2026-09-08) — before that it shared 77 with the index trap, which a supervisor could tell apart only by the sentence on fd 2 (docs/subtypes-design.md keeps the history). There is no flag to turn the checks off: a check that is off by default is a comment by default.

Where	on the :: or on the fn; both are read as one list, in source order, exactly as restrict(...) is. Several pres and several posts on one declaration are all checked, in the order written
Scope	the parameters, in BOTH - and result in a post
Type	Bool
May do	nothing. The expression's own effect row must be empty of DEFINITE effects
Refused by	AX3050, an error
Costs	a post costs the tail-call rewrite

Purity, and why it is not a blanket refusal. A contract is evaluated on every call, so one that allocates or writes changes the program by being stated. That is expressible today without moving any part of the effect system: Alloc is ambient as a declarable claim - only IO can be written in an effect(...) - but it is in the row like any other effect, and restrict(no-alloc) already reads the same row. The vocabulary a predicate needs is allocation-free already: measured from symbols --calls over self_host/main.ax, vecLen, vecGet, strLen, strEq, strByte and memGetWord carry no effects at all, while strConcat, fmtInt and vecNew carry Alloc,Mut. A contract may compare, index, measure and test; it may not build. Only a DEFINITE effect is refused - an effect that reaches the row only as possible arrived because the expression NAMES a function without calling it, and naming one performs nothing.

result, and no 'Old. result names the function's answer in a post, and its type is the DECLARED result - the signature's arrows peeled by as many parameters as the definition has. It names nothing in a pre, which runs before the body, and nothing on a declaration with no ::, which declares no result type for it to have; both are AX3050. Ada pairs Post with 'Old because Ada's parameters can be assigned; Axiom's cannot (AX3012), so for a scalar parameter the name means in the post exactly what it meant in the pre and 'Old would be a synonym. What a post cannot see is a change made THROUGH a reference parameter - a memSetWord into a struct the caller still holds - and nothing here pretends otherwise. That is the deliberate omission, not an oversight.

What a post costs. The body's value has to be observed, so it is bound - (let ((result BODY)) { check result }) - and a let's INITIALISER is not a tail position. Measured on one self-recursive function: bare and under a pre its IR holds no call to itself (the loop rewrite fired), under a post it holds one. A pre is a block whose last expression is the body, and a block's last expression IS a tail position, so it costs nothing. Both directions are pinned by scripts/check-contracts.sh section 5.

tests/diagnostics/385-contract-malformed.ax pins the six refusals with the five controls that keep them from being blanket ones; tests/selfhost/132-contract.ax runs six satisfied contracts including one 200,000 deep under a pre, and 133-contract-violated.ax pins the status. docs/contracts-design.md is the design note.

unhandled(trap) - an effect whose unhandled operation is the design

;@axiom:unhandled(trap) is written above an (effect ...) declaration and is the one AXTAG key that belongs to a declaration other than a function or a signature. It says that reaching an operation of this effect with no handler installed is a deliberate abort rather than a missing handler, and it is what AX3053 reads before deciding whether to report one.

The value is exactly trap. Any other word leaves the check on - unhandled(abort) buys no silence - which is the visible failure rather than the quiet one, and a key one slip from unhandled draws AX3039 at the effect declaration like any other near miss. symbols renders the tag on the effect's own row as #unhandled=trap, so a policy gate over the AXSYM stream can list which effects a program allows to abort.

stdlib/Test.ax carries it on Assert, and load-bearingly: axiom test generates a main that runs each test inside its own recovery point, so every assertion in a file under test reaches that main undischarged, and the 71 an unhandled assertFail raises is exactly how a failed assertion ends one test while the tests declared after it still run. stdlib/Fallible.ax deliberately does NOT carry it - its own header calls an unhandled operation "a programmer error and not a record's fault" - so a batch loop that forgets its handler is named at compile time.

tests/diagnostics/371-379 pin each restriction with the controls that keep it from being a blanket refusal - a callee that casts under no-cast, a syscall under no-foreign, Alloc,Mut under no-io - and the path through a capability record's field, a module boundary, a seeded builtin, a callback and an alloc form; 379 pins direct, mutual-at-depth-three and through-a-capability-record recursion beside a four-deep chain and a while loop that stay silent. scripts/check-restrictions.sh is the gate: a restriction changes no emitted byte, a compiler whose checkRestricts answers nothing goes red, and every restricted declaration in the tree is on tests/agent/restrictions.allow with the verdict the compiler gave it - the manifest is why symbols had to union a signature's tags with the function's.

Until 2026-08-22 neither happened. The sentinel that records an unresolved call had been in the source, skipped by two consumers and produced by nobody since f6ddc2e removed its last producer, so an empty set read as an acquittal:

(struct Box (f : (-> Int Int)))

;@axiom:pure
(fn (runner b) ((b.f) 7))   ; accepted, ran, wrote to stdout

runner compiled clean and symbols printed #pure with no #effects= beside it. The same shape under ;@axiom:effect(io) drew a false claim unsupported: missing IO.

The mark is deliberately conservative. An if or match head whose arms are all named functions is attributed by the reference-site rule and is still called incomplete, because the walk did not resolve the call; so is a lambda's own parameter, and so is a let bound to the result of a call that returned a closure the walk had already walked. Being loud about a limit is the same choice AX3021 makes, and for the same reason: the alternative is a silence that reads as an answer.

Six files in the 269 swept by scripts/check-diagnostics.sh carry a mark - tests/stdlib/140-function-values.ax, tests/stdlib/280-function-application.ax, tests/selfhost/530-fn-in-ctor.ax, 590-lambda-nested.ax, 950-multi-param-lambda.ax and 999-placeholder-under-arrow.ax, ten marks between them. All six are the corpus's own function-value tests, none makes a claim, and no function in self_host/ or stdlib/ is marked at all.

Getting there needed one thing removed rather than added. findFnEnt answers 0 for every form parsed as an application without being a function - cast first of all, and every struct and data constructor with it - and that branch used to run the escape walk, which marked a parameter effect-transparent for appearing inside a cast. memSetWord carried #effect-params=value on the strength of (cast Int value) alone, and it does not call value. That was not only imprecise: a transparent parameter suppresses the missing-effect half of AX3010, so the wrong mark bought silence. With it left in, marking unfollowable arguments put the sentinel on 7,768 functions; with it gone, ten.

The remaining honest gap: passing an effect-polymorphic function itself as a callback does not instantiate the callee's marks (higher-rank flows).

The Unsafe Layer

A signature whose result names a type variable that no parameter mentions is not parametric polymorphism:

(:: conjure (-> Int a))

The caller chooses what a is, nothing witnesses the choice, and the callee cannot have produced a value of it. forall a. Int -> a is inhabited only by non-termination in a sound system; here it is inhabited by a machine word, so the signature is an unchecked coercion wearing a polymorphic spelling. Measured: (strWrap (conjure 42) 8) type-checks OK and the binary exits 139 - 42 dereferenced as a String pointer. The same shape reaches through vecGet, because a Vec carries no element type, which is how a Vec holding an Int reads back as a String.

The same unsoundness reaches one level in, through a function-typed parameter, where the callee still chooses the type:

(:: apply1 (-> (-> a Int) Int))
(fn (apply1 f) (f (cast a 42)))
(apply1 strLen)

a is on a left side, so a rule reading SIDES calls it witnessed. It is not: a parameter is a position the caller fills, and the left of an arrow inside that parameter flips back to one the callee fills - apply1 has to make an a to call f at all, and nothing the caller hands over says what one is. Until 2026-08-25 that drew nothing, checked OK and exited 139. The spine is split by variance now, so a variable with a position the callee produces and none the caller supplies is refused wherever it sits.

Two shapes follow from reading variance rather than sides. (-> (-> Int a) Int) is accepted - the caller's own function produces the a, which is the shape all ordinary higher-order code has, and (-> (-> a b) a b) is witnessed on both counts. And the rule reads the signature, so (fn (apply1 f) 0) - a body that never calls its callback and therefore never fabricates anything - is refused too.

Such a declaration draws AX3040 unless it is tagged ;@axiom:raw. The tag is not permission and does not make the read safe. What it buys is that the unsafe layer is finite and can be asked about:

axiom symbols FILE --diagnostic-format ai | grep '#raw'

No declaration in this repository carries it any more. Fourteen did when the tag was introduced on 2026-08-23; all fourteen were migrated the same day, and the tag remains as the guard against a fifteenth.

The obvious repair was wrong, and the compiler would not have told you. Making all fourteen concrete produces 1,223 type errors, and writing (cast T ...) at each site fixes every one of them - while classifying that value's evidence 0, which suppresses its retain where the parameter is a type variable and its release where it is concrete. Measured both ways in memory-model.md MM-VAL-22. That would have traded a type-system unsoundness for a memory-model regression, 1,223 times, in silence.

The vehicle that works is a typed accessor: the cast goes at a RETURN, inside a function whose declared type carries the truth, so callers see that type and the evidence word is computed from it (MM-VAL-23). Each raw reader was split into the word and a view - nodeA/nodeAName, memGetWord/memGetWordStr, vecGet/vecGetStr - and the call sites renamed, driven by the compiler's own AX3004s and verified one flip at a time.

Two readers got (Option String) instead, because a view has to re-derive its value and they cannot: replReadLine reads stdin and readModuleSrc reads a file. The hot readers deliberately did not - nodeModule and modOf are asked per declaration and per name, and boxing there would cost more than the question is worth.

What this does NOT fix: a Vec still carries no element type, so vecGetStr is an unchecked reading of a word rather than a checked one. The difference is that it is now said, at the call, in one word - where before the type system agreed silently that a Vec holding an Int could be read as a String.

Ordinary parametric polymorphism is unaffected. (:: witnessed (-> a a)) is silent, because the argument supplies the value and witnesses the choice.

Built-in Effects

Effect	Meaning
IO	Reaches the outside world: a __syscallN, or __argc/__argv — reading the command line is reading input the process did not compute. The second half arrived 2026-08-25 (memory-model.md MM-EXEC-9a); before it, a ;@axiom:pure function could read the command line and the claim was accepted
Pure	No side effects
Alloc	Heap machinery, not strictly allocation: a call reaching __alloc — every Vec/Map/Str growth, every memAlloc — and, since 2026-08-25, the three arena primitives, because a reset ends every block allocated since a mark. handle contributes it too, for installing evidence, which allocates nothing either. The (alloc T) keyword contributes it and was the only contributor until 2026-08-23, which had it exactly inverted (memory-model.md MM-EXEC-9a)
Mut	Mutable heap state: (set base.field v), and the __store8/__store64 primitives it lowers to — the second half arrived 2026-08-25 (memory-model.md MM-EXEC-9a), which is why vecPush and mapInsert carry it. Since 2026-08-29 the atomic writers __atomic_store/__atomic_add/__atomic_cas and __fence carry it too; __atomic_load deliberately does not, for __load64's reason. Plain set on a mut local is deliberately not Mut - a local's mutation is invisible outside its function, while a field store is visible through every alias of the value
Div	Divergence (infinite loops). Spellable, never inferred — nothing in the compiler produces it, so a ;@axiom:effect(div) claim is reported unverifiable (AX3037, a warning) rather than unsupported, even over a body that plainly does not terminate — a claim the compiler never looks for is a fact about the analysis, not the body. Inferring it needs a termination analysis this compiler does not have; the cheapest sound rule (self-call or any while) marks 65% of the compiler divergent and is false on almost all of them

There were six until 2026-08-30. Err was accepted as a sixth built-in name — a handle list could write it — and nothing in the compiler ever inferred it, so the name resolved and denoted nothing. A handle list was also the only place it resolved at all: the AXTAG path lowercases its value, so ;@axiom:effect(err) looked for an undeclared custom effect named err and reported missing err. A name a list may write, that nothing produces, and that its own tag spelling cannot reach, is a hole in a table rather than an effect. (handle 5 (Err) 0) now draws AX3016, which is what a list naming something undeclared has always drawn, and Err is an ordinary name again — (effect Err ...) declares an ordinary effect (error-model.md records the retirement beside the AX3054 it shipped with).

Declaring an Effect Type

(effect Console
  (log :: (-> String Int)))

An effect declaration introduces each operation as a callable name: (log "hi") type-checks against the operation's signature and dispatches at runtime through the innermost installed handler (below). An operation must declare that signature: (effect E (op)) is AX3055, an error, because the handler check and the call's arity check both stand on the arrow and on nothing else - without it the operation registered as a wildcard of arity -1, and (op 1 2 3) on a one-argument handler checked clean and SIGSEGVed. Calling an operation performs the effect - log's callers infer #effects=Console, transitively, and ;@axiom:effect(console) claims validate against it (custom tag values match declarations case-insensitively). Operation names join the ordinary value namespace: colliding with a function in the same module is a duplicate definition (AX3006, tests/diagnostics/455-effect-op-collision.ax), cross-module collisions resolve by the one-bare-name rule, and an operation cannot be used as a bare value - wrap it in a lambda ((lambda (x) (log x))) where a function value is needed. Declaring an effect named after a built-in (IO, Pure, Alloc, Mut, Div, or the lowercase alloc) is AX3054, an error. It used to be accepted, and the acceptance was useless in a way nothing reported: a handle list resolves a built-in name to the BUILT-IN, so the custom effect could never be handled - (handle (emit 1) (IO) h) around its own call drew AX3011 unhandled effect IO, on the handle that names it. Without a handle it was quieter and worse: an untagged main performing the custom IO read #effects=IO with no #effect=io and drew nothing, so the row said the program reached the outside world when it did nothing of the kind.

Annotating Functions with Effects

Use AXTAG metadata above the function declaration:

(import IO)

(:: main Int)
;@axiom:effect(io)
(fn (main) (println "hello"))

The compiler validates that the body actually performs the declared effects.

Handling Effects

handle plays two roles, decided per effect in its list, and it NAMES a larger set than it DISCHARGES.

Naming is exhaustive and is checked: an effect the body performs that the list omits is AX3011, an error. That is what makes the list a description of the region rather than a wish, and it means a built-in in the list is never an accident — the form does not compile without it.

Discharging is narrower. For a built-in effect the handler expression is not evaluated and the whole form lowers to its body, so nothing intercepts anything: the syscall still runs, and the effect still reaches the caller. Naming IO acknowledges it; it does not remove it.

; Names IO, which AX3011 requires. Does NOT discharge it: `IO` is still
; in this function's inferred set, and a `;@axiom:pure` claim on the
; enclosing function is contradicted.
(handle (println "hello") (IO) 0)

This is the rule the declared-effect section below already stated — "the list documents, the declaration decides what dispatches" — and until 2026-08-23 this section contradicted it and the compiler implemented this one. A named built-in was subtracted, and the erasure ran the wrong way in three shapes, all measured (tests/diagnostics/348-handle-discharge.ax):

• a function could claim ;@axiom:pure, acknowledge IO inside, be reported #pure, and write to stdout — while the only diagnostic landed on its honest caller, for truthfully declaring the I/O the callee had hidden;
• an inner handle subtracted before an outer (Pure) measured, so the one construct in the language that refuses to emit could be switched off by the code it was guarding;
• and it did not need anyone to be lying: (Console IO), the spelling the section below documents, silently erased the I/O from an honest function, which AXSYM then reported as #effects=Alloc.

For a declared effect, handle installs its handler for the body's dynamic extent - evidence-passing, tail-resumptive: an operation performed anywhere in that extent (any call depth) invokes the innermost installed handler in the operation's place, the handler's return value is the operation's result, and execution continues.

(handle
  (log "hi")            ; dispatches to the lambda below
  (Console)
  (lambda (s) { (println s) 0 }))   ; `s` is the `String` `log` declares

The handler is checked against the operation's declared arrow. A lambda handler's parameters take the arrow's parameter types - s above is a String, so println renders it with no cast - and its result is held to the arrow's result; any other handler expression (a top-level function passed bare, a closure a call built, a literal) is checked as it is and its type compared. A handler that does not fit is AX3004: the integer 0 for a (-> Int Int) operation, or a lambda answering a String where the operation answers Int. Both checked clean until 2026-08-29 and were memory-unsafe at run time - a SIGSEGV when the dispatch applied 0, a string's address plus one flowing into the caller's arithmetic (tests/diagnostics/386-handler-type.ax). The form's own type is its body's, so (println (handle (ask 1) (Ask) h)) selects the Int rendering that ask declares; until the same day the form answered the checker's wildcard, which is why every handle in the tree was spelled (cast Int (handle ..)).

The rules that make this predictable:

• Nesting shadows and restores. The innermost handler wins while its handle is live; the previous one answers again when it exits.
• A handler runs under the evidence at its installation. An operation the handler itself performs dispatches outward to the next handler, never back into itself - which also matches the static story, since a handler's own effects propagate past its own handle.
• No handler in dynamic extent is a trap. The program exits with code 71 rather than continuing on a value nothing produced — and the compiler now says so where it can see it. A handle is the only construct that discharges a custom effect, so an effect still in main's row when inference finishes is one nothing handled, and that is AX3053, a WARNING. Two approximations decide its severity rather than caution: a lambda's operations count where the lambda is written, so a worker bound before the handle that covers its call is reported although it runs (exit 20); and the let of a handle form is an opaque local, so a closure built inside a handle and called after it pops is not reported although it traps (exit 71). An error would refuse the first and accept the second. ;@axiom:unhandled(trap) on the effect declaration says the trap is the design and silences it; see "AXTAG Keys" above.
• A multi-argument operation's handler is a curried chain - (lambda (a) (lambda (b) ...)) - because application is one argument per step. A flat (lambda (a b) ...) is the same chain - the parser curries every multi-parameter lambda - and is checked against (-> A B R) exactly as the nested spelling is; this bullet said it was tuple-typed and refused, which was false, and 386-handler-type.ax pins both spellings accepted.
• In inference, the handled effect subtracts from the body's contribution like a built-in, the handler's own effects count at the handle site (installing it entails maybe running it), and the form performs Alloc (the evidence record). AX3011 still requires the list to name every effect the body performs, so a body whose inner handlers do I/O lists (Console IO) even though only Console is intercepted - the list documents, the declaration decides what dispatches.

Current limits, each a stable diagnostic rather than a silent miscompile: one custom effect per handle (nest them for more), only single-operation effects handled dynamically, and a handle list naming an undeclared effect is AX3016. The self-hosted compiler parses, checks and emits both effect and handle, evidence globals and the unhandled-operation trap included (docs/memory-model.md MM-EXEC-10 is the measured probe).

---

Capability Records

An interface in Axiom is a capability record: a parameterised struct whose fields are functions. (struct Name (a) (f : (-> a B))) declares the shape, and a value of it is built by handing the constructor the functions that implement it. This is what replaced traits and impl in 0.6.0 — the record is an ordinary value, so it can be built at run time, passed as an argument, stored in a Vec, or generated by a macro, none of which a trait instance could do.

Effects cross a record boundary, and this is most of the point of the record: its members are ordinary functions, so they declare their own effects the way every other function does. There is no member-tag rule to learn, no place to write an effect list on the declaration, and no exemption — an untagged writeLine whose body calls println draws AX3042 at its own name, exactly as it would outside a record.

(import IO)

(struct ConsoleOf (a)
  (print : (-> a Int)))

;@axiom:effect(io)
(:: writeLine (-> String Int))

;@axiom:effect(io)
(fn (writeLine s) (println s))

(:: main Int)
;@axiom:effect(io)
(fn (main)
  (let ((c (ConsoleOf writeLine)))
    (c.print "hi")))

What crosses the field is possible, not definite, and the difference is worth knowing before it surprises you. Calling c.print is an application of a value the walk cannot resolve to one function, so main above renders

#effects=Alloc,IO,Mut #effects-incomplete #effects-overapprox #effects-possible=Alloc,IO,Mut

and the three consumers of an effect row read it as Definite and possible says they do, measured on exactly this program:

• the ;@axiom:effect(io) claim on main is accepted — a claimed effect the body may perform is not missing;
• main with no tag at all is not accused. AX3042 reads the definite half, and nothing here is definite, so the silence stands;
• ;@axiom:pure over the same call is AX3037 — "pure claim cannot be checked: the body calls a value the compiler could not resolve" — a warning, not the AX3010 a refuted claim gets.

Swapping the implementation is swapping the value handed to the constructor: a ConsoleOf built from a function that appends to a buffer type-checks against the same field signature. The row it produces is still an upper bound, so name the function at the call where a claim has to be checked rather than merely permitted.

---

Modules and Imports

Split a program across files with (import Mod.Sub ...):

; Math/Ops.ax
(pub :: square (-> Int Int))
(pub fn (square x) (* x x))

; main.ax
(import Math.Ops (square))    ; only bring in `square`
; (import Math.Ops)            ; would bring in every pub decl

(:: main Int)
(fn main (square 5))

Visibility

All declarations are private by default — they are only visible within the defining file. Mark a declaration with pub to make it importable from other modules:

(pub :: square (-> Int Int))  ; public — importable
(pub fn (square x) (* x x))   ; public — importable

(:: helper (-> Int Int))      ; private — only visible in this file
(fn (helper x) (+ x 1))       ; private — only visible in this file

The pub keyword goes before the declaration keyword, inside the same parenthesized form:

Private	Public
(:: name type)	(pub :: name type)
(fn (name args) body)	(pub fn (name args) body)
(data Name ...)	(pub data Name ...)
(struct Name ...)	(pub struct Name ...)
(macro (name pat) body)	(pub macro (name pat) body)

pub controls which names are visible outside the module, not which declarations the program contains. A module's own bodies reach its own declarations whether or not they are pub, so a module with private helpers imports and behaves exactly like one without. Naming a declaration a module does not export is AX3023, which says which module it belongs to.

Both halves matter, and until 2026-08-10 there was only one: a private declaration was deleted from the program by whatever imported it, which broke the module's own calls to it — and if the importing file happened to define the same name, those calls silently reached that definition instead. See the self-hosting record.

macro obeys pub like everything else since 2026-08-14: a macro without it is AX3023 at the invocation, naming the module it belongs to, and a name list that asks for a private macro is refused at the import (tests/diagnostics/485-qualified-private-macro.ax, tests/diagnostics/440-import-name-list.ax). effect is the remaining exception and is exported unconditionally — an operation of an unmarked effect is callable from any importer, because an operation name carries no module.

How Imports Work

• A dotted module path maps directly to a file path: Math.Ops resolves to Math/Ops.ax. The path it is looked up on is the search order below, and its first entry is the entry file's own directory — the file passed to check/build/run/emit-llvm, not whichever file happens to contain the (import ...). So a deeply nested module reaches a sibling of the entry file by the same path the entry file would write (measured: sub/Mid.ax importing a Helper that sits beside main.ax resolves).
• (import Mod.Sub) with no name list makes every pub top-level declaration visible.
• (import Mod.Sub (a b)) makes only the named ones visible; the module's other pub names stay out of scope.
• An import's name list is checked, at the import: a name the module does not declare, or declares without pub, is AX3023 on the import form itself and says which of the two it was (tests/diagnostics/440-import-name-list.ax).
• Imports are transitive (A imports B imports C brings C's declarations into A too) and diamond-safe (two different modules both importing C merges C exactly once).
• Qualified access is supported: Mod::name resolves to name declared in Mod. Imported declarations still join the importing module's flat top-level namespace by default; use Mod::name to disambiguate when the same name exists in multiple modules.
• Types resolve by module, not by import order (2026-08-24). A data, struct or type name is not rewritten to Mod$Name the way a fn is, and the lookup used to take the first declaration in the merged list — so two modules that each declared a Config had one winner for the whole program, chosen by which (import ...) came first, and the loser's own bodies were compiled against the winner's field offsets at exit 0 with no diagnostic. A bare type name now means, in order: a declaration in the referencing module, then a module-less one (the entry file, or a builtin like Option), then the single module that declares it. A name two or more modules declare, referenced from a module that declares neither, is AX3044 naming them. Mod::Name is not the escape — it does not parse in type position; narrow one of the imports with a name list, or rename one declaration.
• A module path that doesn't resolve to a real file is AX5001, reported before type-checking starts. Two of a project's declared dependencies providing one module is refused before compilation, naming both files and the manifest — see Packages.
• Every diagnostic in a multi-file build is attributed to the file and source text it came from, in every one of the human, ai and json formats: a build that spans four files reports an error in the third against the third file's bytes and span, not against the entry file's.

The search order, stated exactly

Stated exactly, because a shorter version of this sentence was wrong for a year. The library is found automatically: AXIOM_STDLIB overrides its location, axiom.pkg's depend and crate lines add a project's own dependencies (see Packages), and AXIOM_PATH — colon-separated — adds further module search directories.

Resolution is a ladder of SUFFIXES over a list of DIRECTORIES, and the suffix is the outer loop:

for suffix in .<os>-<arch>.ax, .<os>.ax, .ax:
    for dir in  the entry file's own directory
                each `depend` in axiom.pkg, in file order
                each `crate` in axiom.pkg's axiom/ directory, in file order
                each $AXIOM_PATH entry, in order
                each --crate DIR's axiom/ directory
                $AXIOM_STDLIB, or the stdlib beside the binary:
        if <dir><module><suffix> is a readable file, that is the module

The manifest's two keys sit together, above $AXIOM_PATH, for one reason: the manifest travels with the source and the variable travels with the shell. The command-line --crate stays below it, because a flag someone typed is not something the project said.

So a project does shadow a standard-library module with its own file of the same name — but only at the same suffix, and only from the entry file's own directory: a depend or crate that would displace a library module is refused, see Packages. A more target-specific file anywhere on the path beats a less specific one nearer the entry file: measured 2026-08-25, a project's own Sys/Platform.ax loses to the standard library's Sys/Platform.darwin.ax, which is the mechanism that makes one (import Sys.Platform) resolve per target and is not a bug. The claim this paragraph replaced — "a module in the entry file's own directory always wins" — was false on exactly that case. scripts/check-packages.sh gates the order.

---

Packages

A project says what it depends on in an axiom.pkg beside its source, or at any directory above it up to eight levels:

# axiom.pkg
name     myapp
version  0.1.0

depend   vendor/axiom-json
depend   ../shared/modules
crate    vendor/axiom-greeter

depend names a directory of modules, resolved against the manifest's own directory so the project relocates. Each one joins the module search path after the entry file's directory and before $AXIOM_PATH — the position the search order above gives it. The manifest travels with the source and the variable travels with the shell, so when both can answer, the declared dependency wins. A key and its value are separated by any run of spaces or tabs.

crate names a native dependency (2026-09-03). depend names a directory of .ax and nothing else, so a package whose reason to exist is a Rust archive could not be declared at all: the shell could say it and the manifest could not. Measured on 0.7.3 — one tree, one libaxiom_greeter.a already on disk — AXIOM_PATH=vendor/greeter/axiom axiom build app.ax exited 0 and ran, while depend vendor/greeter/axiom exited 4 with error[AX4004]: no archive is linked.

A crate names a crate directory: a Cargo.toml beside an axiom/ holding the generated binding module. DIR/axiom/ joins the module search path in depend's slot, and DIR/target/release — together with a workspace's, one and two levels up — joins the link search path, which is what --crate DIR already fed. So the archive is found and linked with no flag at all:

$ cat axiom.pkg
name  myapp
crate vendor/axiom-greeter
$ axiom build app.ax
Build successful: myapp

Three things are refused at the manifest, before a byte is compiled: a crate directory that is not there, one with no Cargo.toml (which is what makes crate mean crate rather than a second spelling of depend), and one with no axiom/.

A manifest crate never runs cargo. --crate DIR on the command line does — it regenerates a stale binding module and builds a missing archive (ffi.md §12) — and the manifest deliberately does not. A command line is a person asking; axiom.pkg is a checked-in file that arrives with a clone, and "the compiler executes no code from a source file" (Macros) would stop being true of the one file whose whole job is to be trusted. Run cargo build --release, or one axiom build --crate DIR, once; the manifest carries it from then on, and until then an unbuilt archive is AX4004, whose help already says exactly that. scripts/check-packages.sh pins the pair: the manifest build must leave DIR/target absent, and the same directory passed as --crate must create it.

name is the executable's default name (2026-08-31). axiom build with neither --output nor -o used to write the literal output, for every project on the machine; it now writes the manifest's name, in the working directory, and still writes output when there is no manifest — so a tree that never had one is unchanged:

$ cat axiom.pkg
name    myapp
$ axiom build app.ax
Build successful: myapp

Because the name is spent as a file name it is checked like one: it is letters, digits, ., - and _, and is neither . nor ... A name that is not — ../escaped, say — is refused at the manifest, not resolved into a path the command line never mentioned. version is still recorded and read by nothing.

A manifest line that means nothing is refused (2026-08-31), at axiom.pkg:LINE and before anything is compiled: an unknown key, a key with no value, and a second name or version (repeating depend is how you declare two dependencies, so that one is allowed).

$ axiom check app.ax ; echo $?
error: ./axiom.pkg:2: unknown key `dependd`
       The manifest's keys are `name`, `version`, `depend` and `crate`,
       and `#` starts a comment. An unknown key used to be ignored, which
       made a misspelled `depend` report as every module it would have
       provided going missing - one at a time, naming this file never.
3

"Used to be ignored" is measured rather than feared: on 0.6.1 a misspelled key, a valueless key and a tab between key and value all produced the identical error[AX5001]: cannot resolve import at exit 1, which names the import and every directory searched and never the file that was supposed to have added one.

Two dependencies may not provide one module. That is the property that makes this more than a search path, and it is refused before a byte is compiled:

$ axiom check app.ax ; echo $?
error: two dependencies in ./axiom.pkg provide the module `Widget`:
       a/Widget.ax
       b/Widget.ax
       One of them would win by declaration order and the other's
       modules would compile against declarations they never named.
3

Before this, whichever directory came first won, silently, and the loser's modules compiled against a package they had never named — the value-namespace twin of the type collision AX3044 closed on 2026-08-24 (Types resolve by module), with the same failure mode: a wrong answer at exit 0.

The rule covers crate too — the fault is in the search path, not in which key put a directory on it — and, since 2026-09-03, nested modules. Two dependencies each holding Sub/Widget.ax, the file (import Sub.Widget) resolves to, used to build and exit with the first one's answer: the check did one directory listing and never descended, and the gate's own fixtures only ever wrote top-level modules. It walks three levels now, and names the module the way an import spells it, Sub.Widget.

A dependency may not provide a standard-library module either (2026-09-03). depend and crate sit above the library in the search order, so a dependency carrying a Fmt.ax replaced the real one for the whole program — every module that imports Fmt, not only the one that wanted the dependency. Measured on 0.7.3: a vendored copy of stdlib/Fmt.ax whose fmtInt answered "HIJACKED" made the program print HIJACKED, at exit 0, with no diagnostic anywhere. That is now refused at the manifest, naming both files. The entry file's own directory is untouched and still shadows a library module — that is a file you wrote, and the search order above documents it.

What this is not, said out loud so nobody has to discover it: there is no registry, no lockfile, no version constraint and no fetching. A dependency is a path on this machine, a crate included. Each of those is a policy decision that wants a maintainer to make it, and a half-made one is worse than the mechanism it would rest on (compatibility.md §4 records it among the things not promised). A lockfile in particular is not a step toward a fetcher: while every dependency is a path the user already controls, a digest over one closes no surface and changes on every edit of their own vendored code. And the compiler will not run another project's build system unless the command line asks it to. scripts/check-packages.sh is the gate — 42 checks, whose negative probe removes the manifest and requires the same program to stop resolving, so nothing else can be what found the module.

---

Macros

A macro rewrites its invocation into a template, before the type checker runs. The compiler executes no code from a source file: expansion is substitution and nothing else.

(macro (when test body) (if test body 0))
(pub macro (unless test body) (if test 0 body))

(when (== n 40) 5)          ; becomes (if (== n 40) 5 0)

The name lives inside the head parens, like a function's. A macro is applied to exactly as many arguments as it declares parameters — too few or too many is AX3018.

Arguments are substituted as syntax, so one used twice in a template is evaluated twice:

(macro (twice x) (+ x x))
(twice (readLine))          ; reads twice

Expansion is hygienic in the binder direction. A binder the template introduces cannot capture a name from the call site:

(macro (addTo x) (let ((tmp 100)) (+ tmp x)))
(let ((tmp 1)) (addTo tmp))     ; 101, not 200

A macro name is not a keyword. A binding of the same name wins:

(macro (v) 9)
(fn (f v) v)                    ; the parameter, not the macro

Because the expansion is checked like ordinary code, a mistake inside a template is an ordinary diagnostic — including exhaustiveness on a match the macro generated. The diagnostic anchors at the invocation.

A macro can also produce declarations (2026-08-14). The rule form — the macro's bare name, then one rule whose pattern head repeats it — generates one declaration per template form when invoked at top level:

(macro defWrap
  ((defWrap nm target extra)
   (:: nm (-> Int Int))
   (fn (nm x) (+ (target x) extra))))

(defWrap w1 base 1)             ; declares w1, a wrapped base
(defWrap w2 base 100)           ; and w2 - names are parameters

Templates may generate fn, ::, data, struct, type and effect declarations and further macro invocations; an argument standing in a name position must be a bare identifier; a macro is invocable from the entry file and from a module over its own declarations, where the template's own pub decides what leaves the module. Everything outside that surface is refused loudly — AX3027 at the invocation (axiom explain AX3027), or AX3021 at the macro's own line for an unsupported template kind. A useful side effect of the form existing: a typo'd declaration keyword like (fnn (broken) 3) is now AX3027 naming fnn, where it used to be a bare syntax error that stopped the parse.

A declaration macro can ask about the program's types — through the syntax/* query vocabulary, a closed set of questions the expander answers from the declaration list at compile time, with no user code running. Three of them are enough to make deriveEq over any sum type an ordinary macro:

(pub macro deriveEq
  ((deriveEq T)
   (:: (syntax/join eq T) (-> T T Bool))       ; names eqColor
   (fn ((syntax/join eq T) a b)
     (match a
       (syntax/for (C (syntax/constructors T)) ; one arm per ctor
         ((C) (match b ((C) true) (_ false))))))))

(data Color () (Red) (Green) (Blue))
(deriveEq Color)                               ; eqColor, checked code

A query with no answer — an unknown syntax/ head, constructors of a struct, a query outside a template — is AX3028 (axiom explain AX3028), never a default. The syntax/ prefix is reserved in declaration names.

Structs and fieldful constructors are covered too: (syntax/fields S) iterates a struct's field names, (syntax/binders C x) names a constructor's fields as hygienic pattern binders, and (syntax/fold && true ...) chains a comparison over them — the spec's deriveEq and deriveLenses both run verbatim, and a derived function composes with the next derive.

Three more answer one value where one value is needed, and each is what a shipped prelude macro is written in terms of:

Query	Answers	The macro that spends it
(syntax/name C)	the constructor's spelling, as a String literal	deriveShow — (deriveShow Shape) gives you showShape : Shape -> String. A tag is an integer at run time, so this is the only route from a constructor to its name
(syntax/arity C)	its field count, as an Int literal	deriveArity — a heap block records its tag and never its arity, so this is the only route to that number either
(syntax/defined n)	whether n names a visible declaration	showOr — (showOr T x "?") renders with showT if the program derived one and answers the fallback if it did not. The if is decided at expansion time and the losing branch is deleted, which is what makes the query useful: the branch naming showT would not type in a program without it

(syntax/join a b) also stands where a reference stands, so a macro can call what it names — ((syntax/join show T) x) — and can feed another query's argument, which is how showOr asks about a name no source file spells.

Macros match on the shape of their arguments and repeat a template over a variable number of them. A rule-form macro's parameters are PATTERNS — a binder, _, a literal matched by value, or a parenthesised form of patterns — its rules are tried in order with the first match winning, and its last element may repeat, which is how a macro becomes variadic (tests/selfhost/392-macro-patterns.ax 127, 393-macro-ellipsis.ax 63, 397-nested-repeat.ax 170, 398-arm-ctor-splice.ax 155, 399-decl-splice.ax 45).

A rule list may also reserve head spellings with a (literals ...) header: a reserved identifier matches one binding and binds nothing, compared by binding rather than spelling, so a + the macro means is not hijacked by a caller's own + (tests/selfhost/402-literal-dispatch.ax 19; a member no pattern spells is AX3066).

Rules come in both template kinds with no guessing: macro with a name heads declaration rules, emacro with a name heads expression rules over one expression template each (tests/selfhost/403-expr-rule-macro.ax 153).

What they still cannot do: read a repeated binder as a same-form test ((- e e) is AX3020, last-wins), and generate import or a nested macro (AX3021 — each would reopen a phase that already ran). (deriving (Eq) is refused outright — see Deriving.) The normative specification is macro-system.md; macro-system.md is the measured detail and the order the rest is planned in.

---

Printing and Formatting

Printing is two macros and no per-type functions. println and eprintln come from IO; format, which answers a String instead of writing one, comes from Fmt (and arrives with IO, which imports it).

There is deliberately no newline-less print. A partial-line printer exists in C-descended libraries because assembling a line out of pieces was expensive, so you emitted the pieces instead; here the line is assembled at compile time, so (println "ok {name} in {ms:>4}ms") is one call and one syscall where four prints were four. For bytes with no newline and no rendering there is writeStr, which is the primitive and is also one call. print is not a name in this language at all — (print "hi") is AX3001 undefined variable, measured, and not a private name refused at its module boundary.

(import IO)

;@axiom:effect(io)
(fn (main)
  (let ((name "world") (n 42) (pi 3.14159))
    {
      (println "Hello {name}")            ; Hello world
      (println "n={n} pi={pi:.2}")        ; n=42 pi=3.14
      (println n)                         ; 42
      (let ((row (format "{name:<10}{n:>5}")))
        (println "[{row}]"))              ; [world        42]
      0
    }))

Holes

A hole names a binding in scope at the call. There is no argument list and no positional {}: the name goes in the string.

{name}          render `name` by its static type
{name:SPEC}     render it the way SPEC says
{{   }}         a literal brace

name may be anything the language can name, because the hole uses the lexer's own identifier charset — {empty-list} works.

Specifiers

SPEC := [align] ['0'] [width] ['.' precision] [type]
align := '<' (left) | '^' (centre) | '>' (right, the default)
type  := 'x' (lowercase hex) | 'X' (uppercase hex)

Written	Means	Expands to
{n}	the value's own rendering	(format n)
{n:x}	hexadecimal	(fmtHex n)
{x:.2}	two decimal places	(fmtFloatPrec x 2)
{n:>8}	right-aligned in 8 columns	(fmtPadLeft (format n) 8)
{s:<8}	left-aligned	(fmtPadRight (format s) 8)
{s:^8}	centred	(fmtPadCenter (format s) 8)
{n:04}	zero-padded, sign kept in front	(fmtPadZerosLeft (format n) 4)
{x:>10.2}	both, composed	(fmtPadLeft (fmtFloatPrec x 2) 10)

Everything above happens at compile time. A specifier is not interpreted while the program runs — it chooses a function, once, during macro expansion. (println "hi") compiles to a single writeStr of a single static constant whose bytes already end in a newline; nothing parses a format string at run time, because no format string survives to run time.

Both halves are checked

• Shape is the expander's: an unclosed {, a stray }, an empty {}, or a malformed specifier is AX3031, with the caret inside the string on the offending byte.
• Type is the checker's: a specifier picks a function with a type, so {s:.2} on a String is AX3004 on fmtFloatPrec's Float parameter. An unbound hole is AX3001; a hole with no rendering — a type variable, a function value, a Foreign, or a data/struct holding one of those — is AX3025.

Rendering your own types

A hole lowers to a reserved head the checker resolves from the argument's static type at the call — the way it already resolves == on two Strings into a content comparison — and a data or struct needs no declaration to be interpolable: its rendering is derived from the declaration, in the language's own spelling. (format x) is how you write that lowering by hand; there is no other spelling for it, and since 0.7.4 the head itself is not a name a program can write.

(import IO)

(data Colour (Red) (Green) (Blue))
(struct Point (x : Int) (y : Int))

(:: main Int)
;@axiom:effect(io)
(fn (main)
  (let ((c (Green)) (p (Point 1 -2)))
    { (println "the colour is {c}")       ; the colour is Green
      (println p)                         ; {x = 1, y = -2}
      (println (Some p))                  ; (Some {x = 1, y = -2})
      0 }))

Static type	Renders as
Int, Float	fmtInt, fmtFloat — 42, 2.500000
Bool	true / false
Char	the character literal, escaped as the lexer spells it — 'x', '\n', 'é'
String	its own bytes at top level, so (println s) means what it always meant; quoted, with escapes, inside a structure — {name = "bo\"b"}
a data value	a constructor application, a nullary constructor bare — (Some 3), (Cons 1 (Cons 2 Nil)), None; a struct-variant constructor positionally, as it is written — (Circle 7)
a struct value	{x = 1, y = 2}, fields in declaration order

Nesting composes — (Wrap {x = 3, y = 4} Green (Some "hi")) — and a recursive type prints in full. A value that reaches itself (a mut struct field is assignable, so (set c.next (Some c)) builds one) prints ... at the back-edge instead of never returning: {v = 7, next = (Some ...)}. One renderer is generated per concrete type at its first use, as an ordinary function appended to the program and checked and compiled like anything written; symbols does not list it, because a generated name is not a symbol. tests/stdlib/450-show-builtin.ax pins every row of the table.

The rule: the compiler decides how a type prints, and a program cannot override it. That was the intent from 0.3.8 and it was not true until 0.7.4, in a way nothing in the documentation admitted: a hole lowered to a call named show, which is an ordinary identifier, so an entry file declaring (:: show (-> a String)) captured every hole in the program — silently, at exit 0. tests/selfhost/383-format-capture.ax measured that hijack working for as long as it worked. The head is spelled format# now, # is not an identifier character (AX1001), and the same fixture measures the hole reaching fmtInt through a file that still declares its own show. The escape hatch is a function whose result is interpolated:

(:: showColour (-> Colour String))
(fn (showColour c)
  (match c ((Red) "red") ((Green) "green") ((Blue) "blue")))

(let ((s (showColour c)))
  (println "the colour is {s}"))          ; the colour is green

There is no override left to write. A (impl (Show T)) used to win at the call over the derived rendering; impl is AX2004 since 0.6.0 and stdlib/Show.ax is deleted in 0.7.4, so the compiler's rendering is the only one, inside a structure and out. Pre's deriveShow still writes showT — an ordinary function you call by name, exactly like showColour above. show itself is not a name the standard library declares any more: (show 1) is AX3001, and tests/diagnostics/621-show-removed.ax pins it.

When the type is not known

Rendering is by the static type, so a value whose type the compiler cannot name has no rendering and is AX3025. One shape does this:

(println (vecGet v 0))                    ; AX3025: vecGet answers `a`

A handle was the second until 2026-08-29 - (println (handle (ask 3 4) (Ask) h)) drew the same code because the form answered the checker's wildcard; it is typed by its body now and renders the Int that ask declares. Name the type and the accessor works too — which is exactly the information the old printlnInt carried in its name:

(println (cast Int (vecGet v 0)))

Migrating from the old surface

IO used to export a function per type. It no longer does.

Was	Now
(println s) where s : String	unchanged — a String renders as its own bytes
(printlnInt n)	(println n)
(printInt n)	(println n), or (writeStr stdout (format "{n}")) to keep the line open
(println (fmtInt n))	(println n)
(println (fmtHex n))	(println "{n:x}")
(println (fmtPadLeft (fmtInt n) 8))	(println "{n:>8}")
(println (fmtFloatPrec x 2))	(println "{x:.2}")
(println (strConcat "n=" (fmtInt n)))	(println "n={n}")
(print "a") (print b) (println c)	(println "a{b}{c}") — one call, one syscall
(print s) (no newline wanted)	(writeStr stdout s)
(println (vecGet v 0))	(println (cast Int (vecGet v 0)))
a literal containing { or }	double it: {{, }}

printlnLit is unchanged: it takes an address of NUL-terminated bytes, which is not a type-rendering question. (printLit, the newline-less form, is private to IO — calling it is AX3023.)

---

Terminals

Sys answers the four questions a line editor needs — is this descriptor a terminal (sysIsatty), what are its current attributes (sysTermSave), put it in raw mode (sysTermRaw), put it back exactly as it was (sysTermRestore) — plus its size (sysTermSize, read back with sysTermRows/sysTermCols). Key decoding, escape sequences and history are not here; this is the floor an editor is built on.

The buffer a caller saves state into must be sysTermStateBytes long, and that is a call rather than a constant on purpose: struct termios is 72 bytes on Darwin, 36 on Linux and 44 on FreeBSD, so a hand-picked size still round-trips on the machine it was tested on. sysTermRaw edits a private copy and never writes to the caller's saved bytes, because a REPL that exits leaving the terminal in raw mode gives the user a shell with no echo and no line editing.

Raw mode clears ECHO, ICANON and IEXTEN; IXON, ICRNL, ISTRIP and BRKINT; OPOST; and sets VMIN 1 / VTIME 0. ISIG is the caller's choice — sysTermRaw's third argument — because ^C raising SIGINT is what a REPL usually wants and a byte the editor can bind is what a full-screen editor wants. c_cflag is not touched.

Which targets implement it, and which honestly do not:

Target	Terminals	How the numbers were established
darwin-aarch64, darwin-x86_64	yes	Measured on a darwin-aarch64 host: a C program compiled against the machine's own headers printed every macro and every sizeof/offsetof, and the round trip was executed under a pty
linux-x86_64, linux-aarch64	yes	Quoted from the kernel's uapi headers at v6.6 (asm-generic/{ioctls,termbits,termbits-common,termios}.h), the struct declarations compiled verbatim to fix the layout, and the layout cross-checked against TCGETS2's own size field
freebsd-x86_64	yes	Derived from _IOC in sys/sys/ioccom.h with the arithmetic shown in the module, checked three ways: the same macro reproduces Darwin's real request numbers, the derived sizeof matches the size field the numbers carry, and the results equal the libc crate's FreeBSD constants
windows-x86_64	no, and it says so	Windows has no termios and no ioctl; its mechanism is GetConsoleMode/SetConsoleMode against a HANDLE, and nothing in this tree can execute it. Sys.Platform.ttyUsesTermios is 0 there and every call answers a negative result rather than a plausible one

The no row is the point. An ioctl request number is a command selector plus a byte count, so a number borrowed from the wrong platform does not fail cleanly — it names some other command, or copies the wrong number of bytes into a buffer sized for a different kernel. Every constant in the four implemented modules carries a comment saying how it was established, and stdlib/Sys/Platform.windows.ax carries the mechanism Windows would need so that whoever has a Windows box does not have to rediscover it.

Memory Primitives

The standard library is built on these low-level primitives, and so is any code that needs to talk to the machine directly. They are the layer where the type system stops — every argument and result is an Int.

Primitive	Meaning
(__syscall0 n) ... (__syscall6 n a1 ... a6)	Raw syscall. Returns the result, or -errno on failure, on every platform
(__load8 base i) / (__store8 base i v)	Byte at base + i
(__load64 base i) / (__store64 base i v)	Machine word at base + i * 8
(__atomic_load p) / (__atomic_store p v) / (__atomic_add p v) / (__atomic_cas p expected new) / __fence	Sequentially consistent atomics on the machine word at byte address p (the address itself, not base + i * 8): a load; a store; an add that answers the word before it; a compare-and-swap that answers the word it found, so it stored new iff the answer equals expected; and a full fence. A store and the fence answer 0. The four that write or order carry Mut; the load computes, as __load64 does. No thread exists for them to synchronise with (memory-model.md MM-PAR-1); tests/stdlib/440-atomics.ax pins their single-threaded meaning
(__alloc bytes)	Address of bytes fresh zeroed bytes
(__retain h) / (__release h)	Take or hand back a share of the counted block at h
(__retainref v)	Take a share of v iff v is a reference — decided from the call's type, so an Int argument emits nothing. The store that hides a value behind a cast Int uses this
__axiom_arena_mark / (__axiom_arena_reset m)	Read the allocator's waterline (it takes no argument), and roll it back to a mark
(memMarkArray h n) / (memMarkLeaf h)	Say that payload words 0..n-1 of the block at h are handles, or that none is — the array form, Mem. n is the caller's ELEMENT count and not the block's size: the allocator's own word count is a size class it clamps to 0 past 16,383 words, and reading the length out of it silently reclaimed nothing above 131,072 bytes (0.7.4, compat/BREAKING). There is no reader: the bit is the RUNTIME's instruction and is ambiguous against an allocator with a different clamp, so a container carries its own flag (memory-model.md MM-LIFE-2h)
(__axiom_recover m thunk)	Arm a recovery point at mark m and run thunk: out of memory, an unhandled effect and a division by zero answer this call with 70, 71 or 72 instead of exiting. Outside one they still exit (error-model.md ERR-REC-6)
(__addr "literal")	Address of a string literal's bytes

axiom symbols --builtins <file> prints the full list, primitives and the built-in operators together, with the type of each — see Symbol Listing.

Syscall numbers are not built into the compiler — they live in stdlib/Sys/Platform.<os>[-<arch>].ax, and the module resolver picks the file matching --target. Adding a syscall is a standard-library change, not a compiler change.

So does everything else that is ABI rather than language. Sys.Platform is a table of numbers, not of OS names, and portable code branches on a capability it exposes rather than on which file resolved — openNeedsDirFd, pollUsesKqueue, usesSyscallAbi, ttyUsesTermios. That is what keeps Sys.ax free of a platform list, and it is what lets a target answer no to a whole facility: ttyUsesTermios is 0 on windows-x86_64, which has no termios and no ioctl, and every terminal call there answers a negative result instead of a fabricated one. See README § Terminals for the support matrix and how each platform's constants were established; scripts/check-stdlib-api.sh asserts that all five Sys/Platform.*.ax files declare the same public names, which is what makes an unimplemented target a declared answer rather than a missing symbol.

Allocation

(:: memAlloc (-> Int Int))
(fn (memAlloc bytes)
  (__alloc bytes))

Memory comes from the backend's mmap-backed bump allocator. There is no free to call, and there is no wait for process exit either: every heap block carries a reference count, and a block whose count reaches zero is walked and re-issued from a size class (docs/memory-model.md MM-LIFE-2b/2c, tests/stdlib/359-arc-str-bytes.ax). Defining axiom_alloc yourself does not replace the allocator: the name is refused (AX3026) — the override seam does not exist. Before that refusal the program passed check and failed in opt with invalid redefinition of function 'axiom_alloc' (docs/memory-model.md MM-ALLOC-8).

Regions

(region r body) brackets an allocation scope: the allocator's waterline is read when body starts and rolled back when body ends, so everything body allocated is reclaimed in one pointer move, and the form answers body's value.

(fn (serve conn)
  (let ((mut served 0))
    {
      (while (hasRequest conn)
        (region req
          {
            (answer conn (render (parse (readRequest conn))))
            (set served (+ served 1))
          }))
      served
    }))

Every string the request built dies when req ends; served, an Int, is written through. That is the per-request reset docs/memory-model.md MM-ALLOC-22 measures for the pre-forked server, written as a keyword instead of a __axiom_arena_mark beside a let — with one difference that matters in a loop. A hand-written mark allocates its 24-byte cell on the heap, below the waterline it then records, so the cell is never reclaimed; a region's cell is a stack slot (self_host/codegen.ax, emitRegion), so two thousand iterations leave the waterline where they found it (tests/stdlib/168-region.ax, terms 2 and 3).

This is stage S2 of docs/memory-model-v2-design.md §4: a checked scope with no types yet. What "checked" means today, and what it does not, is stated rather than implied:

• The value must be a scalar. The form hands body's value past the reset by value, and only an Int, Bool, Char, Float or Unit survives that: a String is a descriptor over a second block, a struct is a block, a closure is a record, and every one of them would point at reclaimed memory. A region answering any other type is AX3059 at the body (tests/diagnostics/631-region-escape.ax). Answer a count, a status or a hash; a reference has to be built outside the region until typed regions (S3) can promote one.
• A store out of the region must be a scalar. (set x v) inside the region, where x was bound before it opened, is AX3059 when v is not a scalar — and so is (set x.f v), a store into x. (set served (+ served 1)) above is fine, which is what makes a region per loop iteration writable.
• A nested region may not reuse an open name. (region r (region r ...)) is AX3058 (tests/diagnostics/630-region-name-shadowed.ax): regions are ordered by nesting (MM-RGN-2), and a name that meant two open extents could not be ordered. Two sibling regions may share a name. Nothing can refer to a region by name yet; the @r in type position that will is S3's, and it resolves against the same stack.
• What it does not see. A call that stores a region-allocated reference for you — vecPush onto an outer vector, memSetWord into an outer block — and a raw Int that is an address are the program's obligation under docs/memory-model.md MM-ALLOC-16, exactly as they are for a hand-written mark. S3 is what closes them.
• The runtime's traps still fire. A region's mark is taken inside whatever handle extent encloses it, so MM-ALLOC-16b's status-76 trap has nothing to say (168, term 8), and nested regions reset innermost-first by construction, so neither does MM-ALLOC-16a's 75. Resetting an outer hand-written mark inside a region is the same fault it always was, and traps the same way.

A region contributes Alloc to its function's effect row — the row the three arena primitives carry, because a reset is heap machinery whether or not the body allocated — so a restrict(no-alloc) body cannot contain one. A program that writes no region emits what it emitted before this keyword existed: byte-identical IR for the compiler's own 202,021 lines, measured against the previous commit's compiler, and scripts/check-region-scope.sh holds the mechanism behind that (no region, no cell), the reclaim as a peak-RSS ratio, the fixtures' row counts, and the ablation — with the refusal switched off, hello world stored into an outer binding from inside a region reads back as the string built after it.

region is an ordinary identifier off the head of a form, like every keyword (Keywords); axiom fmt prints it as while is printed (tests/fmt/parity/210-region-head-layout.axp).

---

Standard Library

Axiom ships a standard library written in Axiom. It reaches the operating system through raw syscalls, not through C, so a program that links nothing else contains no call to libc — not for printing, not for allocation, not for file I/O; the library needs no FFI to do any of it. scripts/check-freestanding.sh is the gate on that, and an extern block linking a Rust crate is the deliberate exception (ffi.md §15). Naming an external symbol is what that block is for, with Rust on the other side through the C ABI; foreign, the construct that used to spell it, is removed and reserved at AX2004 (Removed Keywords). On windows-x86_64 there is no syscall ABI and the same library reaches the OS through kernel32; there the gate turns around and holds every import to scripts/platform-allow.windows.txt, eight names, a list that may not carry a libc name.

Modules at a Glance

Twenty-three modules, all of them Axiom source under stdlib/. A name a module does not mark pub is not part of its surface — reaching one is AX3023 — so grep '^(pub' stdlib/M.ax is always the authoritative answer to what a module exports. The table below says what each module is for and names its surface; every public name, with its type, its effects and a one-line summary, is in stdlib-api.md, which is GENERATED — an Axiom program (examples/axdoc/axdoc.ax) reads the library's own source for the public surface and axiom symbols for the effect row, and scripts/check-stdlib-api.sh regenerates it on every CI run and requires the result to be byte-identical.

Module	Provides
Pre	the prelude macros: when, unless, cond2, cond3 (conditional macros), deriveEq, deriveShow, deriveArity, showOr
Mem	raw memory: memAlloc, memAllocMapped, memMarkArray/memMarkLeaf, memCopy, memSet, memCmp, memGetByte/memPutByte, memGetWord/memSetWord
Str	the byte view of a Str: strFromLit, strAlloc, strLen, strByte, strCmp, strEq, strSlice, strDup, strConcat, strFindByte, strStartsWith, strSplit, strCStr. String literals are already Str values — see String Literals Are Str Values
Utf8	utf8Len, utf8CharAt, utf8DecodeAt, utf8FromChar, utf8Next, utf8Offset, utf8Slice, utf8Width, utf8SeqLen, utf8IsCont, utf8Valid (the character view of a Str)
Vec	growable Int array: vecNew, vecNewRef, vecWithCapacity, vecWithCapacityRef, vecFree, vecPush, vecPop, vecGet, vecSet, vecLen, vecCap, vecLast, vecClear, vecSort, vecSortBy
Map	mapNew, mapNewRefVals, mapWithCapacity, mapWithCapacityRefVals, mapFree, mapHas, mapGet, mapGetStr, mapInsert, mapRemove, mapLen, mapCap, mapUsed (open-addressing Int→Int hash map)
Fmt	the format macro, and the functions a format specifier selects: fmtInt, fmtHex, fmtHexUpper, fmtFloat, fmtFloatPrec, fmtPadLeft, fmtPadRight, fmtPadCenter, fmtPadZerosLeft, fmtIntWidth. A hole's rendering is chosen by the compiler from the value's static type (Int, Float, Bool, Char, String, and any data or struct of those) and lowered to the functions in this module; an argument shape with no rendering is AX3025. format lived in a Show module until 0.7.4
Err	Result (Ok/Err), the Error record, isOk/isErr, okOr, unwrapOr, mapOk/mapErr, andThen, try!, toOption, withContext, and the checked arithmetic divChecked, remChecked, shlChecked, shrChecked (error-model.md is the specification)
Fallible	fallibleMalformed — the operation a batch loop's callee performs on a malformed record — and the handlers that answer it without unwinding: fallibleSkip, fallibleDefault, fallibleCounting; the skip sentinel fallibleSkipped/fallibleIsSkipped; the FallibleTally a counting handler writes, fallibleTally/fallibleCount (error-model.md ERR-REC-7)
Intern	internNew, internFree, internIntern, internFind, internLookup, internCount (string interner)
Sys	the syscall layer: sysWriteFd, sysReadFd, sysWriteAllFd, sysReadAllFd, sysReadLineFd, sysOpenPath, sysCloseFd, sysExitWith, sysFailed, sysErrno, stdin/stdout/stderr; the filesystem (below); and the process layer sysSpawn, sysRun, sysRunPath, sysWaitPid, sysEnv, sysArgc, sysArg, sysGetPid, sysNowMicros
Path	pathDir, pathBase, pathExt, pathStem, pathJoin, pathReplaceExt, pathWithSlash, pathIsAbsolute, pathLastSlash, pathExtIndex, pathClean — decisions about bytes, no syscalls
IO	println, eprintln (macros — see Printing and Formatting), writeStr (bytes, no newline, no rendering), readLine and readAll (a descriptor's next line, or the rest of it — (readLine stdin) is how a program reads what was typed or piped at it), the raw-address variants printlnLit/readFileLit, exit, die, todo (a hole that types as any result and never returns, printing todo: <what> and exiting 70 — it is what AX3005's machine-applicable fix writes into each missing arm); and the filesystem (below)
Ffi	ffiHandleNew/ffiHandlePtr/ffiHandleClose, the out-cell (ffiCellNew, ffiCellWord, ffiCellFree) and the Vec conversions a generated binding needs (ffi.md)
Json	jsonParse, jsonWrite, and the constructors and accessors between them — written for JSON-RPC
Rpc	the LSP base protocol's framing over a file descriptor: rpcRead, rpcWrite, and the reader rdNew/rdBuf/rdFilled
Par	parMapWords — a bounded pool of concurrent tasks over __proc_spawn/__proc_join, joined in submit order; parRunAll is that pool over external commands, and parRunOne/parArgvVector the pieces underneath. Replaced Job at 0.7.4
Http	the request parser httpRead over a buffered HttpReader (httpReaderNew/httpReaderWith), the HttpReq record with httpHeader/httpHasHeader/httpQueryParam/httpDecode, the writer httpRespond/httpRespondRaw/httpFail with httpStatusText and httpContentType, the router routerNew/routeAdd/routeStatic/routeNotFound/routeDispatch over HttpHandler cells, httpPathSafe, httpServeFile, httpServeOne, and the ceilings httpMaxHead/httpMaxBody
Test	assertEq, assertNe, assertStrEq, assertTrue, assertFalse, testFail, and the Assert effect a failed assertion performs — what axiom test discovers and isolates (error-model.md ERR-REC-6)
Agent.Tags	axsymParse, axsymLine, and the accessors over one parsed line: symTag, symHasTag, symEffects, symDerivedPure, symAgentTag, symHasAgentTag. Reads the AXSYM stream rather than the compiler's internals (agent-harness.md §3.2)
Tui.Keys	terminal input bytes to key events, as a pure function: the KeyEv record and its KEY_*/MOD_* tables, keyScan (buffer, valid length, offset → one event), and keyResolve for a prefix that stopped arriving. The CSI and SS3 grammars are PARSED — parameter bytes, intermediates, final — and only then interpreted, so an unbound but well-formed sequence (a mouse report, a cursor-position reply, an OSC title report) is consumed whole and reported KEY_NONE rather than typed into the line one byte at a time. Multi-byte characters go through Utf8; there is no second decoder. Every function is restrict(no-io,no-foreign), which is what lets tests/selfhost/975-key-decode.ax gate the whole escape grammar with no terminal in the loop
Tui.Edit	a line editor over a gap buffer of code points: insert, backspace, delete, cursor by character and by word, line start and end, the four kills with one 16-entry kill ring, yank and yank-pop, and a redraw that stays correct when the line WRAPS — the forced newline at (pcols + n) % width == 0 is what drives a terminal's deferred wrap and makes one row formula true at every cursor position. It performs no I/O: ledRefresh appends fragments to a caller's Vec. What counts as a word is the caller's wordChars, and the prompt arrives already painted and is measured with tuiVisLen, so nothing here knows what language is being typed. Also tuiCat, the allocate-once join the refresh needs
Tui.Term	the only part that touches a descriptor: the KeyIn reader over sysReadFd, the 30ms timed wait that resolves a lone ESC (built on the netPoll* readiness layer — measured on a pty, not assumed), termRawEnter/termRawLeave around one call, termFlush, and termEditLoop, which answers a line or None at end of input. Raw mode is entered per LINE and left around evaluation, so a caller's ordinary output needs no CR injection and an exit from inside a command cannot leak raw mode

The Filesystem

Two layers over the same syscalls. Sys takes a raw NUL-terminated char* because it hands one straight to the kernel; IO takes a Str, copies it so a strSlice cannot be handed on unterminated, and is the one to reach for.

Question	IO (takes a Str)	Sys (takes a char*)
read a whole file	readFile	sysReadFile
read one line of a descriptor	readLine	sysReadLineFd
read a descriptor to end of input	readAll	sysReadAllFd
write one, truncating	writeFile	sysWriteFile
add to the end of one	appendFile	sysAppendFile
duplicate one	copyFile	—
move or rename	renamePath	sysRename
delete a file	removeFile	sysUnlink
is it there?	fileExists	sysFileExists
is it a directory?	isDir	sysIsDir
how big?	fileSize	sysFileSize
why can it not be read?	readErrno	sysReadErrno
make a directory	makeDir	sysMkdir
make it and its parents	makeDirAll	—
remove an empty directory	removeDir	sysRmdir
what is in a directory?	listDir	sysReadDir
where am I?	cwd	sysGetCwd

Every call answers a value or a negative errno; nothing throws.

The two descriptor readers take an Int in both layers — stdin, or what sysOpenPath answered — and what IO adds there is the descriptor in the error's message. Both answer Result, with end of input inside the Ok ((Ok None) for a line, (Ok "") for the rest), because a read that fails is not an input that ended and a stream cannot be asked readErrno afterwards. readLine performs one read(2) per byte so that it never takes a byte it does not answer; stdlib/Sys.ax records the measured cost and what to use for bulk input instead.

Three things are worth knowing before using them.

readFile answers "" for four different situations — a missing file, an empty file, a directory, and a file that could not be opened. readErrno is the discriminator: 0 readable, 2 missing, 13 not permitted, 21 a directory.

listDir is sorted and drops . and ... readdir order is the filesystem's and differs between machines, so a program that walks a directory is not reproducible unless something sorts. Sys.sysReadDir is the unsorted primitive, and it keeps the two dot entries — which is what lets its empty answer mean failure and nothing else, since a readable directory always holds them.

There is no stat, and no chdir. struct stat's layout differs by platform, so the questions it answers are open, read and lseek here instead. chdir exists on every target and is absent because nothing calls it: a process that changes directory has invalidated every relative path anything else is holding. See the self-hosting record.

(import IO)
(import Path)

(:: main Int)
;@axiom:effect(io)
(fn (main)
  {
    (makeDirAll "build/out")
    (writeFile (pathJoin "build/out" "notes.txt") "first\n")
    (appendFile "build/out/notes.txt" "second\n")
    (println (readFile "build/out/notes.txt"))
    (println (pathExt "build/out/notes.txt"))       ; .txt
    (println (pathStem "build/out/notes.txt"))      ; notes
    (println (pathReplaceExt "build/out/notes.txt" ".md"))
    (removeFile "build/out/notes.txt")
    (removeDir "build/out")
    (removeDir "build")
    0
  })

A walk over a directory is ordinary recursion over the Vec listDir answers — there is no for-loop and none is wanted:

(import IO)
(import Path)
(import Str)
(import Vec)
(import Err)

; Every `.ax` file in `dir`, with its size, one per line.
(:: report (-> String (Vec Int) Int Int))
;@axiom:effect(io)
(fn (report dir names i)
  (if (>= i (vecLen names))
      0
      (let ((p (pathJoin dir (cast String (vecGet names i)))))
        {
          (if (strEq (pathExt p) ".ax")
              ; `fileSize` answers a `Result`: the failure is in the
              ; type, so a size and an errno are not the same Int. Match
              ; it - `(unwrapOr (fileSize p) 0)` would report an
              ; unreadable file as zero bytes, and `unwrapOr` is safe
              ; only where the fallback is genuinely equivalent to the
              ; error (error-model.md states that rule and the three
              ; fixtures that broke it).
              (match (fileSize p)
                ((Ok size) (println "{p}  {size}"))
                ((Err e)   (let ((why (errorText e))) (eprintln "{p}  unreadable: {why}"))))
              0)
          (report dir names (+ i 1))
        })))

(:: main Int)
;@axiom:effect(io)
(fn (main)
  {
    (makeDirAll "build/reports")           ; parents included; EEXIST is success
    (report "stdlib" (listDir "stdlib") 0) ; sorted, so two machines agree
    (appendFile "build/reports/log.txt" "swept stdlib\n")
    0
  })

vecGet answers Int — the truth about a machine word — so a name read out of the Vec is crossed back with (cast String ...), which is the same typed-accessor rule the Map pair follows.

A Str Is...

A Str is a length-prefixed, NUL-terminated string. It is the address of a three-word header:

• Word 0: length in bytes
• Word 1: address of the bytes
• Word 2: the block owning those bytes, or 0 when no block does

The owner word (added 2026-08-15) is what lets a slice keep its parent's buffer alive by arithmetic: strSlice shares the bytes and inherits the owner rather than naming its parent, so the chain is one hop deep however many times a slice is cut. Zero means the bytes are nobody's to free — a literal's belong to the loader, a syscall buffer's to the kernel. See memory-model.md MM-VAL-7.

The bytes are always NUL-terminated in addition to being length-counted. This means strCStr can hand a path straight to a syscall without copying, and a Str can contain a NUL byte.

The Lit names — printlnLit, readFileLit — take a raw NUL-terminated address rather than a Str. They are rarely what you want now that a literal is a Str: (println "hi") is both shorter and cheaper than (printlnLit (__addr "hi")). They remain the way to handle bytes that arrived without a length, such as a syscall buffer.

Text Is UTF-8, and Str Stays Bytes

A Str holds bytes, and Str's own operations are byte operations: strLen counts bytes, strByte reads one, strSlice cuts at byte offsets. That is deliberate and will not change. Every syscall write hands (strData s) and (strLen s) straight to write, every hash folds over bytes, and every buffer sizes itself in bytes - a strLen that answered in characters would write the wrong number of bytes to a file descriptor.

The character view lives beside it, in Utf8:

(import Str)
(import Utf8)

(strLen  "héllo")            ; 6 - bytes
(utf8Len "héllo")            ; 5 - characters
(utf8CharAt "aé世" 2)        ; 19990, the code point of 世
(utf8Offset "aé世" 2)        ; 3, the byte offset it starts at
(utf8Slice "héllo, 世界" 7 2) ; "世界", sharing the original's bytes
(utf8FromChar (cast Int '世')) ; a new one-character Str

This is the same split Rust draws between len() and chars().count(), and it works because a Char is already a code point: (utf8DecodeAt "é" 0) and 'é' are both 233. Character indexing is O(n) in the byte length - UTF-8 is variable-width and nothing builds an index - so walk a string with utf8Next rather than by rising character index, or the loop is quadratic.

Decoding answers None rather than a guess when there is no character to read: past the end, on a sequence cut short by the end of the string, or on a byte that begins no sequence at all. Inventing a value would be worse than refusing one: read as bytes-with-zeros, the first byte of 世 decodes to U+4000, an ordinary CJK character, and the tail byte of é to ©.

It answered -1 until 0.7.5, and the reason it stopped is worth carrying. The paragraph here used to say "a sentinel rather than an Option because every data value heap-boxes - the same argument strFindByte, vecGet and mapGet already make". Every clause of that is now false: a function whose every tail is None or (Some e) is two registers and no block (docs/unboxed-sums-design.md §5b), so utf8DecodeAt, utf8CharAt and strFindByte all answer (Option Int) while keeping restrict(no-alloc); vecGet traps on an index it cannot serve rather than answering 0; and mapGet never had a sentinel - its absent answer is a default the caller supplies.

Iteration is never blocked by bad input, though: utf8SeqLen answers 1 for a byte it does not understand, so utf8Next always advances and no decoding loop can hang on a corrupt file. utf8Valid is the explicit question when a caller needs a verdict on the whole string.

Encoding is total in the other direction: utf8FromChar always produces well-formed UTF-8, because anything that is not a Unicode scalar value - negative, a surrogate, or past U+10FFFF - is encoded as U+FFFD. So (utf8Valid (utf8FromChar x)) holds for every x.

Most of Str needed no change at all, for two reasons worth knowing rather than rediscovering. UTF-8 orders bytes the same way Unicode orders code points, so strCmp, strEq and strStartsWith are already correct on text. And UTF-8 is self-synchronizing - no multi-byte sequence contains a byte below 0x80 - so strFindByte searching for an ASCII byte can never match the middle of a character.

---

AXTAG Metadata

AXTAGs are source-embedded agent metadata preserved from ;@axiom:<key>(<value>) comments immediately above a declaration. The compiler validates what it can and surfaces accepted tags as #-metadata on AXSYM lines.

Syntax

;@axiom:effect(io)
(fn (main) (println "hello"))

;@axiom:pure()
(fn (pureFn x) (* x x))

;@axiom:no_refactor
(fn (legacyFn x) x)

;@axiom:owned(arena=frame)
(fn (ownedFn x) x)

Common AXTAG Keys

Key	Meaning
effect(io)	Declares that the function performs I/O
pure	Declares that the function has no side effects
no_refactor	Hints that the declaration should not be modified by automated refactoring
owned(arena=frame)	Ownership metadata; accepted and unenforced — the wording predates the reference-counting decision (docs/memory-model.md MM-LIFE-7)

The compiler validates effect(io) claims against what the body actually performs - a __syscallN, or a call to something that performs one - and pure claims against the absence of any effect. A mismatch the compiler can decide is an error (AX3010); a claim it cannot check - because the body calls a value it could not resolve - is a warning (AX3037).

---

Removed Features

These features existed in earlier versions of Axiom but have been removed. Each word keeps a grammar rule whose only job is to report AX2004 and say what to write instead.

begin — Removed

(begin a b c) was the sequencing form. Brace blocks replaced it: { a b c } sequences and answers its last expression, and a fn body already sequences, so the wrapper is usually just deletable.

It is reserved rather than left as an ordinary name. Until 2026-08-26 it was one, so (begin 1 2 42) fell through to an application and drew AX3001 undefined variable begin — a diagnostic that names no replacement and reads like a typo. It answers AX2004 now, like its five siblings.

union — Removed

C interoperability is no longer a goal, and an untagged union cannot be pattern-matched safely — its variants are not distinguishable at run time. Use data for a tagged sum or struct for a product.

(This sentence used to end "has no meaning under linear types". Linear types were removed on 2026-08-25 for enforcing nothing, so the justification was resting on a feature the language does not have.)

linear — Removed

Refused rather than implemented. linear T parsed to the nominal type constructor Linear T and enforced nothing else: no use was counted, so a value could be consumed twice or never, and Linear T was a real barrier against T (AX3004) and nothing more. A marker that reads as an ownership guarantee and supplies none is worse than no marker, because a reader spends trust on it — the same ground deriving was refused on.

Delete the marker and use the type. Reclamation is the reference counting every heap block carries (docs/memory-model.md MM-LIFE-2b/2c), and __axiom_arena_mark / __axiom_arena_reset_keeping is the explicit fallback for a program that wants to choose the point.

consume — Removed

Refused rather than implemented. (consume e) was a parse-time identity that kept the Linear wrapper: the checker typed it as its operand, the IR lowered it to its operand, and consuming twice was accepted. The form reclaimed nothing. Delete the wrapper and keep its argument — (consume e) always meant e.

trait and impl — Removed

An interface is a capability record now — a parameterised struct whose fields are functions, and an instance is an ordinary value of it. Capability Records is the whole replacement, with a compiled example. Both words report AX2004 and say what to write:

(trait (Eq a) where
  (eq :: (-> a a Bool)))

(:: main Int)
(fn (main) 0)
; error[AX2004]: `trait` is no longer part of Axiom

(impl (Eq Int) where
  ((eq (lambda (x y) (== x y)))))

(:: main Int)
(fn (main) 0)
; error[AX2004]: `impl` is no longer part of Axiom

Dispatch is spelled ((c.eq) x y) — an application, not a resolution rule — and rendering needs no record at all, because the compiler renders every type from its static type (Printing and Formatting).

They are reserved rather than freed, for the sharper of AX2004's two reasons: an ordinary identifier named impl would make (impl (Eq Int) where ...) a declaration-macro invocation, and the reader would be told that no macro named impl exists — a true sentence naming neither the construct they wrote nor what replaced it.

Three things went with the pair and have no replacement, because a record needs none: supertraits, default method bodies, and the effect list a trait/impl header accepted and discarded without checking. A record's members are ordinary functions, so they declare their own effects the way every other function does. where went too — it was a keyword only inside these two forms, and it is an ordinary identifier again.

region — returned

region sat on this list from 2026-08-10 to 2026-09-03, and the advice this section gave — "delete the wrapper; lifetimes are inferred" — described a region-inference sketch that was withdrawn the same month (docs/memory-model.md MM-ALLOC-18, §3.4). Inference never replaced the annotation, so the keyword is back as a scope the program brackets: see Regions. A (region ...) at the top level is not a declaration and reports AX3027 like any other expression head.

foreign — Removed

foreign never worked: it emitted a call to a symbol the module never declared, so a program that used one passed check and then failed inside opt or the linker. It was refused rather than repaired, and the FFI that replaced it is the extern block — a different feature with a different contract, not this one renamed (ffi.md). For the kernel, reach the standard library instead, which is written in Axiom over __syscall0-__syscall6 and needs no FFI at all.

Struct layout modifiers went with it. packed, repr(C) and align(N) appeared in this document and in the formatter; the parser rejected all three.

---

The REPL

The REPL compiles expressions to native code — it doesn't interpret them. This means you get real performance even in interactive mode.

axiom repl

REPL Commands

Command	Aliases	What it does
:help	:h	Show all commands
:quit	:q, :exit	Exit the REPL
:type <expr>	:t <expr>	Show the type of an expression
:load <file>	:l <file>	Load a file into the REPL
:reset	:r	Clear all definitions
:defs	:d	Show all definitions in scope
:llvm <expr>	—	Show the generated LLVM IR
:time <expr>	—	Time how long an expression takes

Example Session

The banner is two lines, there is no prompt, and every line of output goes to stdout. The loop reads a line, answers it, and reads the next one, so a piped session and a typed one produce the same bytes.

$ axiom repl
Axiom 0.7.5 - REPL
Type :help for commands, :quit to exit

(:: add (-> Int Int Int))
OK: add defined
(fn (add x y) (+ x y))
OK: add defined
(add 3 4)
type : Int
result 7
:type (add 3 4)
(add 3 4) : Int
:defs
Definitions in scope:
  add
  add
:llvm (+ 1 2)
Generated LLVM IR:
target triple = "arm64-apple-macosx14.0.0"
...

The input lines are shown interleaved for readability; the REPL echoes nothing it was given.

What pins this, and the one line nothing pins. The session is held by scripts/check-repl-selfhost.sh, which drives the loop and compares its bytes — except the banner, which that gate never sees, because it runs the REPL as repl --no-banner. The version inside the banner is held instead by scripts/check-version.sh, which names this file as one of its sites; scripts/lib/version-sites.sh expects exactly one such banner here, so a second copy of it in this document would fail the version gate rather than duplicate harmlessly.

The REPL accumulates definitions — functions you define persist across inputs. Nothing else persists: there is no line editing, no arrow-key history and no history file, because the loop reads plain lines rather than driving a terminal. :help's own text still advertises ? and arrow keys; only a line beginning with : reaches the command dispatcher, so ? is read as an expression and answered with a parse error. The editor-grade interface is the LSP's business (self_host/repl.ax records the divergence).

---

CLI Commands

Checking and Building

# Check syntax and types (no code generation)
axiom check source.ax

# Compile to a native executable
axiom build --input source.ax --output program

# Emit LLVM IR to stdout
axiom emit-llvm source.ax

# Emit LLVM IR to a file
axiom emit-llvm source.ax -o output.ll

# Compile and run immediately
axiom run source.ax

# Lower `parallel` to the platform's threads rather than to forked
# processes (build, run, test; darwin and linux); see the `parallel`
# section under Let Bindings for what that buys and costs
axiom build --threads --input source.ax --output program

Choosing a Memory Manager

# Default: an mmap-backed bump allocator, with per-block reference
# counts since 2026-08-15 - a block whose count reaches zero is walked
# and re-issued from a size class, so a dead value is freed with no
# reclamation written in the source.
axiom build --input source.ax --output program

The build is freestanding — it does not call libc.

There is no tracing collector. The retired Rust compiler had one behind a --gc flag; it was not ported, and --gc is now refused by name rather than silently ignored (see the self-hosting record). What reclaims instead is reference counting: every heap block carries a count and a shape word, and a thousand build-and-drop iterations move the allocator's bump by 384 bytes where they moved it by 80,304 (tests/stdlib/359-arc-str-bytes.ax). Every ownership event memory-model.md MM-LIFE-2c specifies now emits: events 2 and 3, the two that needed an escape analysis, shipped on 2026-08-21 (tests/stdlib/372-arc-owned-results.ax), so peak memory tracks live data rather than total allocation. Where a program wants reclamation at a point of its own choosing, __axiom_arena_mark, __axiom_arena_reset and __axiom_arena_reset_keeping roll the allocator's waterline back — which is how the language server holds flat memory across an editing session.

The three carry a contract the compiler cannot check: after a reset, nothing allocated since the matching mark may be read again. What the allocator does guarantee around them is worth stating, because the one useful pattern depends on it:

• memAlloc answers zeroed memory always, including memory a reset has reclaimed and handed out again.
• memAlloc also answers a leaf: a block it hands out is declared to hold no references, because a byte count is all it was told. (memAllocMapped bytes map) is the same allocation with bit i of map naming payload word i as a handle to another counted block, so releasing this block releases that one too. Str's header is the first user — word 2 owns the bytes — and it is what makes a dead string free its buffer rather than just its header. The map is clamped to the block, so it can name the wrong word of your own block and never a word outside it.
• A reset writes nothing to what it reclaims. Memory above the restored waterline keeps its contents until it is handed out again.
• (__axiom_arena_reset_keeping mark addr bytes) reclaims to mark and carries the bytes at addr across the reclaim, answering their new address. This is how a value is kept: doing it as a reset followed by an ordinary copy is unsound, because the copy's destination is scrubbed on allocation and the scrub can run over the source.

A container can own what it holds, and be freed. Since 2026-08-24 each of the three has an owning constructor beside its ordinary one - vecNewRef, mapNewRefVals, and internNew, which is owning outright because an interner has no other use - and a Free that hands the whole structure back:

(let ((v vecNewRef))
  {
    (vecPush v (strDup "hello"))   ; the vector takes a share
    (vecFree v)                    ; header, data block, and the string
  })

The two constructors differ in ONE WORD at allocation: the data block of a vecNewRef carries the array form (Mem.memMarkArray cap), which says its first cap payload words are handles, so releasing the block releases them all. vecNew's data block is a leaf and makes no claim about its contents. For the Ints a compiler's vectors are full of that is exactly right and free - the store emits no instruction at all. For a REFERENCE it is not a borrow: the store still takes a share (memory-model.md MM-LIFE-2g) and nothing hands it back, so the element is immortal. Closing that is what the owning constructor is for. Growth, overwriting and removal all hand back what they displace, and vecPop zeroes the slot it vacates - the popped value's share becomes the caller's. memory-model.md MM-LIFE-2h states the encoding and the two obligations that come with it; MM-LIFE-2i is the acceptance property and its measurement.

A fourth form turns a mark into a recovery point. (__axiom_recover mark thunk) runs thunk — a (-> Int Int), called with 0 — and answers what it answered. If instead the program runs out of memory, performs an effect with no handler in dynamic extent, or divides by zero anywhere inside that extent, the arming call answers 70, 71 or 72 and the program carries on; outside a recovery point those three still write their sentence to fd 2 and exit, exactly as before. Points nest and an abort takes the innermost armed one.

The abort restores the stack pointer, resets the arena to mark, and restores every evidence slot — that last one is why this is sound where calling __axiom_arena_reset by hand across a live handle is not (memory-model.md MM-ALLOC-16b, MM-ALLOC-23). Nothing runs on the way out: there are no destructors to call and no landing pads. It is not a catch and cannot contain a memory-safety fault — a SIGSEGV is not a trap and asks nothing. error-model.md ERR-REC-6 states the whole contract; tests/stdlib/403-recover-div.ax is the smallest example.

Using the AI-Optimized Format

For machine-readable output, always use --diagnostic-format=ai:

axiom --diagnostic-format=ai check source.ax
axiom --diagnostic-format=ai build --input source.ax --output program
axiom --diagnostic-format=ai symbols source.ax

See docs/diagnostics.md for the full AXDL and AXSYM notation reference.

Symbol Listing

# List every top-level symbol and its type
axiom symbols source.ax

# Also include built-in operators
axiom symbols source.ax --builtins

# Also print each function's resolved call edges as `#calls=`
axiom symbols source.ax --diagnostic-format=ai --calls

--calls prints the graph the effect fixpoint already walks: the edges inferEffects resolved in order to derive each #effects= row. It is opt-in because it would otherwise appear on every row of every symbols golden. scripts/check-agent-calls.sh gates the relationship between the two keys - no callee's effect escapes its caller, every inferred effect has an edge accounting for it, and every IO reaches a syscall or an extern. See agent-harness.md §3.5.

The default rendering is an aligned human table. --diagnostic-format=ai gives AXSYM instead, one line per symbol; --diagnostic-format=json has no symbol renderer, says so on the first line, and falls back to AXSYM.

Diagnostic Lookup

# Look up a diagnostic code
axiom explain AX3001

# List all known diagnostic codes
axiom explain --list

---

Testing

A test is a top-level function whose name begins with test and which takes no parameters. There is no attribute to write, nothing to register and no manifest — axiom test reads the file and finds them.

; tests/testrunner/pass-tests.ax is this repository's own
(import Test)

(import Vec)

(:: testVecGrowsAndKeepsItsElements Int)

;@axiom:effect(io)
(fn (testVecGrowsAndKeepsItsElements)
  (let ((v vecNew))
    {
      (vecPush v 41)
      (vecPush v 1)
      (assertEq "length after two pushes" 2 (vecLen v))
      (assertEq "sum" 42 (vecSum v))
      0
    }))

$ axiom test tests/testrunner/pass-tests.ax
ok   testVecGrowsAndKeepsItsElements
ok   testMapRoundTrips
ok   testStrSlicesShareBytes
ok   testPathSplitsIntoItsParts
ok   testAssertNeSeparatesTwoValues

5 test(s), 0 failed

Discovery, and the two anti-silence rules

A directory runs every .ax file directly inside it, in name order. --filter TEXT runs only the tests whose name contains TEXT.

Two rules exist so that nothing is skipped in silence, which is a runner's characteristic defect — a skipped test reads exactly like a passing one:

• A file that declares no test is a failure, not an empty success.
• A test-named function that takes parameters is refused by name, rather than passed over (tests/testrunner/arity-tests.ax).

A --filter that matches nothing is a failure for the same reason an empty file is. The gate is scripts/check-test-runner.sh, whose fixtures are tests/testrunner/.

Assertions Take a Label First

stdlib/Test.ax is the assertion surface: assertEq, assertNe, assertStrEq, assertTrue, assertFalse, and testFail for the branch that must not be reached. Every one of them takes a label first, and the reason is a capability the macro system does not have: Axiom's macros cannot stringify an expression (macro-system.md), so there is no way to print the comparison that failed. The label is what the failure has to say instead.

One Failure Ends One Test

A failed assertion ends the test it is in, and no other. It performs an operation of the Assert effect, which with no handler in dynamic extent is the unhandled-effect trap, and axiom test arms one recovery point per test — so the three ways an Axiom program can stop without returning all end exactly one test and answer the runner with a status (error-model.md ERR-REC-6 is the specification):

ok   testTheFirstOnePasses
     deliberate: want 3, got 4
FAIL testAFailedAssertionEndsTheTest - a failed assertion, or an unhandled effect (status 71)
FAIL testADivisionByZeroIsContained - division by zero (status 72)
FAIL testAnUnhandledEffectIsContained - a failed assertion, or an unhandled effect (status 71)
ok   testTheLastOneStillRuns

5 test(s), 3 failed

That last line is the point of the mechanism: the test declared after all three failures still ran (tests/testrunner/mixed-tests.ax). A memory-safety fault is the one thing this does not contain, and no language contains it.

Marking a Test Expected to Fail

;@axiom:expect, written above a test's fn (or its :: signature, when that is where it ends up), flips the verdict: a tagged test that fails is reported xfail rather than FAIL, and does not count against the run, while a tagged test that does not fail is reported FAIL — with its own message — and does. The flip is keyed on the status the recovery point answers, not on the Assert effect specifically, so a tagged test that ends in a division by zero is xfail too:

ok   testANormalTestIsUnaffected
     deliberate: want 1, got 2
xfail testXFailReportsTheFailureAsExpected - a failed assertion, or an unhandled effect (status 71), as expected
xfail testXFailAlsoCatchesADivisionByZero - division by zero (status 72), as expected
FAIL testXFailButItPassesAnyway - expected to fail, but passed
     still deliberate: want 1, got 2
xfail testXFailTaggedOnTheSignature - a failed assertion, or an unhandled effect (status 71), as expected

5 test(s), 1 failed

The tag cannot be used to silence a broken test: testXFailButItPassesAnyway above is tagged and still reported as a failure, because its assertion stopped failing (tests/testrunner/xfail-tests.ax, scripts/check-test-runner.sh).

---

Compiler Pipeline

Source (.ax) → Lexer → Parser → Imports → Macro Expansion → Type Checker → LLVM IR → opt → llc → cc → Executable

Import resolution is the stage between the parser and the expander, and what it produces is one merged declaration list, each entry remembering the module it came from — which is what lets a bare name resolve across files and a diagnostic still name the file it came from. Macro expansion then runs to a fixpoint before any body is walked, and the type checker is two passes: collect declarations, then check bodies.

There is no separate IR stage: codegen.ax writes LLVM IR text straight from the checked AST. The retired Rust compiler had a three-address IR crate between the two; it was not ported (the self-hosting record).

Compiler Structure

The compiler is written in Axiom, in self_host/.

Module	Purpose
core.ax	Tokens and spans
lexer.ax	Tokenizer
parser.ax	S-expression parser and AST
expand.ax	Macro expansion — to a fixpoint, with the syntax/* query vocabulary — hygiene, expansion diagnostics
typecheck.ax	Name resolution, type checking, effects, AXTAG validation
namespace.ax	The declaration namespace: how a bare name reaches a definition, and which names may leave a module
codegen.ax	Import resolution, name mangling, LLVM emission
diag.ax	Diagnostics, AXDL/JSON rendering, source maps
render.ax	The human diagnostic renderer
style.ax	The one palette table every coloured render reads — ANSI colour for the human renderer, and for nothing else
driver.ax	build: opt, llc, cc, and blaming the right one when a stage fails; --crate running cargo and axiom-bindgen; grounding externs; the crate/archive linking the FFI needs
rustbind.ax	The Rust binding --emit-rust-binding writes for an Axiom archive (ffi.md §10)
main.ax	CLI entry point and subcommand dispatch; format.ax, repl.ax, symbols.ax, explain.ax, lsp.ax are the tools
build.ax	One string literal: the build id scripts/build-stamped.sh rewrites in a copy of this directory, so a shipped binary names the tree it came from
Host.<target>.ax	Host triple and syscall ABI, selected when the compiler is compiled — a freestanding binary has no uname to ask

---

Cross-Compilation

Use --target to select the platform:

axiom --target=linux-x86_64 emit-llvm main.ax -o main.ll

Supported targets: darwin-aarch64, darwin-x86_64, freebsd-x86_64, linux-aarch64, linux-x86_64, windows-x86_64. Defaults to the host.

What puts a name on that list is stated once, in README's Targets section: a CI leg executes what the compiler emits there. This line is a copy of the README's, and scripts/check-doc-drift.sh requires the two to agree.

Being on this list does not mean a release carries a prebuilt archive for it. Supported and shipped are separate questions, and since 2026-08-30 linux-x86_64 answers them differently: its CI leg runs the whole gate battery on every change, and release.yml builds only linux-aarch64 and darwin-aarch64. On a host with no archive scripts/install.sh says so and points at scripts/bootstrap-from-seed.sh instead of failing on a download, and scripts/check-release-targets.sh holds the release matrix and that refusal list to each other.

freebsd-x86_64 joined the list on 2026-08-30, when its leg had been seen green on 13 of the previous 15 runs and its continue-on-error was removed: Tests (freebsd-x86_64) boots FreeBSD 14.4 in a VM and runs the bootstrap, the whole stdlib corpus and the syscall-table gates there, and it is blocking. The corpus is the half that is easy to under-read: 109 cases execute on that kernel, 470-parallel, 471-parallel-trap and 476-par-pool among them, which is what makes parallel's process lowering measured on FreeBSD rather than merely assembled (scripts/check-parallel.sh section 7 holds the leg to it). freebsd-aarch64 did NOT join and is the one FreeBSD target that is not supported — it has the same seed and the same syscall table but no leg, because an aarch64 guest is TCG-emulated on every runner GitHub offers (measured at a 300-minute budget and dropped). Neither FreeBSD target ships an archive: a freebsd-x86_64 host gets the build-from-source paragraph linux-x86_64 gets, a freebsd-aarch64 host the not-supported one. FreeBSD 12 is the floor the syscall numbers need; the triple pins 14.

windows-x86_64 joined the list on 2026-08-30: Tests (windows-x86_64) links and EXECUTES a hello world on windows-latest from modules the Linux cross job emitted, its imports held to an allowlist, and the leg is blocking. The scope of that word is one program — the FreeBSD leg runs the whole stdlib corpus, this one runs hello.exe — and README's Targets section states the difference rather than letting supported cover both silently. Supported as a target is not supported as a host: the compiler does not run on Windows, and scripts/install.sh refuses a Windows host outright. It is the one target without a syscall ABI, so the emitted runtime and stdlib/Sys/Platform.windows.ax reach kernel32 by call (Sys.Platform.usesSyscallAbi is 0 there, and Sys.ax calls the platform module's own platformWriteFd/platformReadFd/platformExitWith instead of __syscallN), the program enters at mainCRTStartup with no C runtime, and a __syscallN the program reaches anyway exits 74 after axiom: no syscall ABI on this target.

axiom build --target=windows-x86_64 --input p.ax --output p links p.exe with lld-link (/subsystem:console /entry:mainCRTStartup), which ships with LLVM's lld; --link-search DIR is translated to /libpath:DIR and --link-lib NAME to NAME.lib. The runtime's kernel32 imports are grounded like any extern block's, so a kernel32.lib must sit on a search directory: the Windows SDK's (Lib\<ver>\um\x64), or one generated anywhere with llvm-dlltool -m i386:x86-64 -d kernel32.def -l kernel32.lib from a .def naming the symbols on scripts/platform-allow.windows.txt - which is what the gates and the CI leg do. --emit-staticlib is refused for this target. Hosting the compiler itself on Windows is a later phase; scripts/install.sh and scripts/bootstrap-from-seed.sh say so.

---

Optimisation

Axiom has while with mut and set (see Mutable Bindings and while), used 316 times in the compiler's own sources (grep -o '(while ' self_host/*.ax | wc -l). Iteration may also be written as recursion. A self tail call runs in constant stack at every --opt level, including 0 — the loop is built by Axiom's own codegen, not by LLVM (docs/memory-model.md MM-EXEC-6b). What still needs --opt 1 (the default) and above is mutual tail recursion and a tail call sitting in a let body, which only LLVM's passes flatten (MM-EXEC-6c):

axiom build --input main.ax --output main --opt 2

Use --opt 2 for anything that iterates over a large input.

Iteration Has Three Spellings, and Only One Is Bounded

	Depth at --opt 0
while	Unbounded — it is a real loop. 10⁷ iterations in constant stack (tests/selfhost/500-while-mut.ax)
Self tail recursion	Unbounded — the loop is built by Axiom's own codegen at every --opt level, in every tail position: a { } block's last expression, an if or cond or match arm, and a let body (memory-model.md MM-EXEC-6b; tests/stdlib/467-mutual-tail.ax term 6 runs ten million through a let body at --opt 0)
Mutual tail recursion	Unbounded when the two prototypes match and nothing is owed after the call — the emitter marks it musttail, LLVM's guaranteed tail call, at every --opt level (MM-EXEC-6c; 467-mutual-tail.ax terms 1–3 under a 512 KiB stack, scripts/check-tail-calls.sh). Bounded for a callee of a different arity, or a call handing over an owned temporary such as (od (+ i 1) (strConcat s "x")): those stay plain calls and are flattened only by LLVM at --opt 1+, when at all
Non-tail recursion	Bounded by the machine stack: measured on an 8176 KiB stack, 174,000–175,000 frames at --opt 0 and 260,000–262,000 at --opt 1, beyond which the process dies with SIGSEGV, status 139 (memory-model.md MM-EXEC-6d)

So the shape to avoid at scale is a fold whose combining step happens after the recursive call:

; Bounded: the `+` runs after the call, so every level keeps a frame.
(fn (count v i hi)
  (if (>= i hi) 0 (+ (vecGet v i) (count v (+ i 1) hi))))

; Unbounded: an accumulator makes the call a tail call.
(fn (count v i hi acc)
  (if (>= i hi) acc (count v (+ i 1) hi (+ acc (vecGet v i)))))

--opt 1 and above are worth using for anything hot. They are no longer needed for the correctness of mutual tail recursion between functions of one arity: since 2026-09-03 that call is a musttail, and llc either jumps or refuses the module. What still needs the optimiser — and gets no guarantee from it — is a mutual call across arities, or one that hands the callee a temporary the caller must release afterwards (MM-EXEC-6c names both, with the measurement).

Link-time optimisation, and why there is no flag for it

Every Axiom program is emitted as one LLVM module — user code, every imported stdlib module, and the runtime allocator — and opt runs over that module, so what a C toolchain calls link-time optimisation (inlining and dead-code elimination across translation units) is the ordinary optimisation here: there is only one unit. The emitter also prunes every define nothing reaches before opt sees the module (pruneDeadDefs in self_host/codegen.ax; scripts/check-dead-code.sh holds that a hello world's binary names nothing a walk from main cannot reach).

Two things were measured on 2026-09-03 before deciding not to add a link flag:

• -Wl,-dead_strip at the cc line (the darwin spelling; --gc-sections with -function-sections is the ELF one) removes 10 runtime symbols and 752 bytes from a 34,896-byte hello world and 32 bytes from the 1,955,712-byte compiler — the IR-level prune has already done the work, and a flag whose whole effect is ten unreferenced runtime helpers is not worth a byte-layout change on every target.
• Cross-language LTO over extern is the boundary the single module cannot cross, and it is reachable: a Rust crate built with rustc --emit=llvm-bc links into the Axiom module with llvm-link, one opt -O2 over the union inlines the Rust function into the Axiom loop (call i64 @adder_add 2 → 0), and the result links against the crate's archive for the rest and answers. Two facts gate a driver flag: a staticlib built with -C linker-plugin-lto carries no bitcode member at all (0 of 393 objects), so the bitcode has to be asked for as its own artifact; and the inliner refuses the merged callee until its "target-cpu"/ "target-features" attributes are stripped — rustc stamps apple-m1 on every function and Axiom's module stamps nothing, and LLVM will not inline across that (the same probe with the attribute removed inlines). Both are mechanical, neither is built, and docs/ffi.md's C-ABI contract is unchanged either way.

What the Vectorizer Does With an Axiom Loop

Axiom emits LLVM IR and the driver hands it to opt, so SIMD is automatic exactly where LLVM's loop vectorizer accepts the loop the emitter wrote — and only at --opt 2 and above: LLVM enables the loop and SLP vectorizers at speedup level 2, and the default --opt 1 runs neither. Measured 2026-09-03 (scripts/check-simd.sh holds the fixtures and the IR facts; the timings are best of five with the arms interleaved on a machine at load average 9):

Loop	At --opt 2	LLVM's reason, from --pass-remarks-output
(for x xs (set acc (+ acc x))) over a (Vec Int)	vectorized, width 2, interleave 4; 3.1x over --opt 1	no store in the loop, so the header reads hoist and the range check folds against the hoisted bound
(for i 0 n (if (== (strByte s i) 97) ...)) over a String	vectorized, width 16; 1.9x	same shape, byte elements
(for i 0 n (vecSet v i (+ (vecGet v i) 1))) in place	not vectorized (1.09x, from other passes)	Control flow cannot be substituted for a select, call instruction cannot be vectorized, Cannot vectorize early exit loop with complex writes to memory
the same map with * 3 written over raw words, nothing checked	not vectorized	the cost-model indicates that vectorization is not beneficial: an i64 multiply has no vector instruction on baseline NEON or SSE2; with + 1 the identical loop vectorizes at width 2
web/bench/collatz.ax's while	not vectorized, correctly	Cannot vectorize uncountable loop: the trip count is data-dependent

Read the third row as the shape of the whole problem. Every memory access is a load/store through an integer address, so a store into one vector's data block may, as far as LLVM knows, have changed another vector's length word — the length, data pointer and ownership flag are re-read every iteration, the range check cannot fold, and its trap is an exit inside the loop. Tagging the header and element accesses by hand with scalar TBAA (a data block never overlaps a header block) folds the trap but does not get the loop vectorized: the data-pointer read sits inside the check's branch, where LICM will not speculate a load through an integer address; the ownership branch keeps an axiom_release call in the body; and vecSet's silent out-of-range skip is a predicated store, which neither baseline has a masked-store instruction for, so the cost model declines even once the loop is legal. Write loops are the open half, and the memory-model argument for them is not a flag.

What did change on 2026-09-03 is the trap itself. The six trap functions (__axiom_index_out_of_range and its siblings) are emitted noreturn cold. Before that, every inlined vecGet carried the trap's two syscalls and @__axiom_backtrace call into its caller — 1,518 copies inside the compiler's own optimised IR at --opt 2, 1,685 at --opt 1, one in every hot function that indexes a vector — and a trap call that returned into the loop was an exit the vectorizer refused to reason about. Now the inliner leaves the cold callee as a call, the block after it is unreachable, the compiler binary is 6.9% smaller for it (2,153,352 → 2,004,600 bytes), and three more of its loops vectorize (98 → 101). nounwind was measured beside it and moved nothing.

To see what LLVM decides about your own loop:

axiom emit-llvm main.ax -o main.ll
opt -O2 -S main.ll -o main.O2.ll \
  --pass-remarks-output=main.yaml --pass-remarks-filter=loop-vectorize
grep -B2 -A2 'Function: *yourFunction' main.yaml

A Vectorized remark names the width and interleave count; a MissedDetails remark is preceded by the analysis remarks that say why. The compiler's own IR reports 101 vectorized loops this way, out of a few thousand — CantVectorizeLibcall (a call in the body) and UnsupportedUncountableLoop (a while whose bound is not a counter) are the two reasons that account for most of the rest.

---

Tips and Patterns

Writing a Function with I/O

(import IO)

(:: main Int)
;@axiom:effect(io)
(fn (main)
  {
    (println "Hello from Axiom!")
    0
  })

Using let for Intermediate Values

(fn (compute n)
  (let ((x (+ n 1))
        (y (* x 2)))
    (+ x y)))

Pattern Matching on ADTs

(data Maybe (a)
  (Nothing)
  (Just a))

(:: safeDiv (-> Int Int (Option Int)))
(fn (safeDiv a b)
  (match b
    ((0) (None))
    (_ (Some (/ a b)))))

Building a List

(data List (a)
  (Nil)
  (Cons a (List a)))

(:: sum (-> (List Int) Int))
(fn (sum lst)
  (match lst
    ((Nil) 0)
    ((Cons h t) (+ h (sum t)))))

(:: main Int)
(fn main
  (sum (Cons 1 (Cons 2 (Cons 3 (Nil))))))   ; => 6

Using the Standard Library

(import IO)
(import Str)
(import Fmt)

(:: main Int)
;@axiom:effect(io)
(fn (main)
  (let ((total (+ 1 2)))
    {
      (println 42)
      (println "sum={total}")
      0
    }))

---

Further Reading

• The Memory Model — the normative specification: representation, allocation, mutation, lifetimes; reference counting is the chosen reclamation strategy
• The Macro System — the normative specification: expansion, hygiene, budgets, and what derive will be built on
• Macros — what expansion guarantees, what it does not, and the probes behind each claim
• The Error Model — Result, the Error record, and stdlib/Err.ax
• The Rust FFI — extern blocks, --emit-staticlib, and what crosses the boundary
• Diagnostics & Agent Notations — AXDL, AXSYM, NID, AXTAG reference
• Contributing — the gates, the conventions, and the two documents retired into history
• README — project overview and installation guide