Foreword

For a long time, programming languages competed to be expressive and ergonomic. They were designed for humans. Before 2020 this made sense, because humans wrote nearly all the code, and languages grew around what humans found natural, flexible, or satisfying.

Today, AI systems write a large share of real software. Sometimes they draft functions, and sometimes whole modules. Humans are starting to act less as typists and more as reviewers, managers, and co-authors.

But as IBM famously said in 1979: "A computer can never be held accountable, therefore a computer must never make a management decision". AI can speed up writing code, but that speed brings added risk.

Aela is designed for this shift by designing for auditability and verifiability.

When machines write more code than humans, the language itself has to provide more guardrails. The fewer ways there are to write something, the easier it is to understand it, check it, and keep it working. Aela follows this idea in its type system, its memory model, and its checks. It is built for a partnership between human oversight and machine-written code, based on constraints, clarity, and behavior you can prove.

Chapter 1. Basics

Hello, World In Other Languages

To start, here is "Hello, World!" in some familiar languages.

hello.c

#include <stdio.h>
int main(void) {
  printf("Hello, World!\n");
  return 0;
}

hello.cpp

#include <print>
int main() {
  std::println("Hello, World!");
}

hello.rs

fn main() {
  println!("Hello, World!");
}

main.adb

with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
begin
   Put_Line("Hello, World!");
end Main;

Hello, Aela!

hello.ae

fn main() -> i32 {
  println("Hello, World!");
  return 0;
}

fn main() -> i32 is where the program starts. Every program has a main function, and here it returns an i32.
The number that main returns is the program's exit status. By custom, 0 means that everything went well.
println writes a string to standard output and then a newline. It is a builtin function, so you do not need to import anything to use it. There is also print, which does not add a newline.
Every statement ends with a semicolon, and blocks go between { and }.

A function in Aela always writes its return type. If you leave out -> i32, the program does not compile. This version is wrong on purpose, and the compiler rejects it:

Aela

fn main() {
  println("Hello, World!");
}

The compiler stops with error E0361 ("main returns the exit status") and shows the right form, fn main() -> i32. A function must also return a value on every path. If you write -> i32 but forget the return 0;, you get error E0399.

Building and Running

The compiler is called aec. Give it the source file and, if you like, a name for the program with -o:

Shell

aec hello.ae -o hello
./hello

The output is:

Text

1Hello, World!

If you leave out -o, the program is named after the file, so aec hello.ae also makes ./hello. Every error the compiler reports has a code, such as E0399. To read more about an error, run aec explain E0399.

Putting Values Into Strings

To print a value, put it inside a string with \( ... ). Any expression can go between the parentheses.

Aela

fn main() -> i32 {
  let name = "Aela";
  let year = 2025;
  println("Hello, \(name)!");        // Hello, Aela!
  println("Next year is \(year + 1)."); // Next year is 2026.
  return 0;
}

println takes only a string. To print a number on its own, put it in a string too: println("\(year)"). This is the only way to build a string from parts. There is no printf style format string, and you cannot join strings with +. Chapter 2 says more about this.

Comments

Aela

//! A comment that starts with //! describes the whole file.
/// A comment that starts with /// describes the next declaration.
/// The command `aec doc` shows these comments.
fn main() -> i32 {
  // A normal comment runs to the end of the line.
  /* A block comment can span
     more than one line. Block comments do not nest. */
  println("comments");
  return 0;
}

Exit Status and Arguments

Since the result of main is the exit status, a program can report a problem by returning a number other than zero.

status.ae

fn main() -> i32 {
  println("Something went wrong.");
  return 3;
}

Shell

aec status.ae -o status
./status
echo $?

This prints "Something went wrong." and then 3.

main can also take the program's command line arguments, as an array of strings. The first element, args[0], is the name the program was started with.

greet.ae

fn main(args: string[]) -> i32 {
  println("Program: \(args[0])");
  println("Arguments: \(args.len - 1)");
  for (let i: i64 in 1..args.len) {
    println("  \(args[i])");
  }
  return 0;
}

Shell

aec greet.ae -o greet
./greet one two

The output is:

Text

Program: ./greet
Arguments: 2
  one
  two

There are a few more forms of main, for programs that use async code or failures, but these two are all you need for now. A main with some other form, such as one that returns i64, is error E0361. Loops like the for loop above are covered in Chapter 4.

Chapter 2. Variables, Types, and Basic Expressions

Almost every real program needs to store values, compute with them, and print the results. This chapter shows how each language handles:

declaring a variable
giving it a first value
deciding whether it can change
basic expressions, such as arithmetic and comparisons

Aela's rule for first values is simple. A variable that is declared without a value starts at the zero value of its type. There is no way to read memory that was never set. This removes one of the most common bugs in C and C++.

Let's compare.

C

#include <stdio.h>
int main(void) {
  int a; // not initialized: its value is unknown
  int b = 2;
  int c = a + b; // undefined behavior
  printf("c = %d\n", c);
  return 0;
}

Local variables are not initialized for you. int a; holds whatever bits were already on the stack.
Reading a variable that was never set is undefined behavior. The program may print any number, or the compiler may change the code in surprising ways.
This is a major source of bugs that are hard to reproduce.

C++

#include <print>
int main() {
  int a; // still not initialized, just like C
  int b = 2;
  int c = a + b; // undefined behavior
  std::println("c = {}", c);
}

Basic types such as int behave just like in C. They are not initialized for you.
C++ can set a value to zero with int a{};, but this is not the default, and it is easy to forget.

Rust

fn main() {
  let a: i32; // declared, but not set
  let b = 2;
  let c = a + b; // compile error E0381
  println!("c = {c}");
}

Rust does not let you read a variable before it is set.
This code does not compile. The error is E0381: "used binding a isn't initialized".
Rust removes this whole class of bugs, but you must give every variable a value before you use it.

Ada

with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
   A : Integer;           -- not initialized
   B : Integer := 2;
   C : Integer := A + B;  -- reads A before it is set
begin
   Put_Line("C = " & Integer'Image(C));
end Main;

A variable declared without := is not initialized.
Reading it is a "bounded error". The program may raise an exception, or it may use some unknown value.
Ada encourages you to initialize variables, but does not force you to. SPARK's analysis tools do reject code like this.

Aela

fn main() -> i32 {
  var a: i32;      // no value given, so a starts at 0
  let b: i32 = 2;
  let c = a + b;
  println("c = \(c)");   // c = 2
  return 0;
}

Every variable has a value. If you do not give one, the variable starts at the zero value of its type.
There is no undefined behavior from reading a variable.
let c = a + b; does not write a type. The compiler works it out from the value, so c is an i32.

Zero Values

Each type has a zero value. This program prints the zero value of several types.

Aela

struct Point {
  x: i64;
  y: i64;
}
fn main() -> i32 {
  var count: i64;
  var ratio: f64;
  var done: bool;
  var name: string;
  var maybe: i64?;
  var items: i64[];
  var p: Point;
  println("\(count) \(ratio) \(done) [\(name)] \(maybe) \(items) \(p)");
  // 0 0.0 false [] none [] Point { x: 0, y: 0 }
  return 0;
}

Type	Zero value
integers	`0`
floats	`0.0`
`bool`	`false`
`char`	the character with code 0
`string`	`""`, the empty string
arrays such as `T[]`	`[]`, an empty array
optionals such as `T?`	`none`
structs	a struct with every field at its zero value

Aela has no null pointer. A value that may be missing has an optional type, such as i64?, and its zero value is none. A few kinds of values have no zero value at all, such as references and function values. You must always give those a value when you declare them.

`let` and `var`

Aela has two ways to declare a variable:

let declares a name whose value never changes.
var declares a variable that you can change later.

Aela

fn main() -> i32 {
  let limit = 3;
  var total = 0;
  total = total + 10;
  total += 5;
  println("\(limit) \(total)");   // 3 15
  return 0;
}

Assigning a new value to a let is a compile error. The compiler rejects this program with error E0413 ("cannot assign to immutable binding 'count'"):

Aela

fn main() -> i32 {
  let count = 1;
  count = 2;
  return 0;
}

A good habit is to use let by default, and var only when the value needs to change.

Writing the Type

You can write a variable's type after its name, or you can leave it out. When you leave it out, the variable takes the type of its value. A whole number like 5 is an i64, and a number with a decimal point like 2.5 is an f64.

Aela

let rate: f64 = 1.5;     // a global: it must have a type
var calls: i64 = 0;
fn main() -> i32 {
  let a = 5;             // i64
  let b: i32 = 5;        // i32, because the type is written
  let c = 2.5;           // f64
  calls += 1;
  println("\(a) \(b) \(c) \(rate) \(calls)");   // 5 5 2.5 1.5 1
  return 0;
}

Variables declared outside of any function are globals. A global must always have a written type. Leaving it out is error E0303.

One Name, One Meaning

Many languages let you declare a new variable with the same name as one that is already visible. This is called shadowing. Aela does not allow it, because it makes code harder to read. The compiler rejects this program with error E0203 ("shadowing is not allowed"):

Aela

fn main() -> i32 {
  let x = 10;
  if (x > 5) {
    let x = 20;
    println("\(x)");
  }
  return 0;
}

Two blocks that come one after the other may each use the same name, because the two names are never visible at the same time.

Basic Types

Type	Values
`i8 i16 i32 i64`	signed integers of 8, 16, 32 and 64 bits
`u8 u16 u32 u64`	unsigned integers of 8, 16, 32 and 64 bits
`i128 u128`	integers of 128 bits
`f32 f64`	floating point numbers
`bool`	`true` and `false`
`char`	one Unicode character, such as `'a'` or `'é'`
`string`	text, stored as UTF-8 bytes, that cannot be changed
`Duration`	a span of time, such as `250ms` or `1.5s`

Number literals can be written in several ways:

Aela

fn main() -> i32 {
  let million = 1_000_000;      // _ makes long numbers easier to read
  let mask: u32 = 0xFF;         // hexadecimal
  let bits = 0b1010;            // binary
  let small = 42u8;             // the suffix u8 makes this a u8
  let tiny = 2.5e-3;            // a float with an exponent
  let wait = 1.5s;              // a Duration
  let letter = 'é';             // a char
  println("\(million) \(mask) \(bits) \(small) \(tiny) \(wait) \(letter)");
  // 1000000 255 10 42 0.0025 1.5s é
  return 0;
}

A literal must fit the type it is given. let x: u8 = 300; is error E0312, because a u8 holds only 0 to 255.

No Hidden Conversions

In C, an int turns into a long or a double on its own when needed. In Aela, no value ever changes type unless you ask for it. This holds even between two integer types. The compiler rejects this program with error E0301 ("expected i64, found i32"):

Aela

fn main() -> i32 {
  let small: i32 = 5;
  let big: i64 = small;
  return 0;
}

The two sides of an operator must also have the same type. Adding an i32 to an i64 is error E0305 ("mixed operand types"):

Aela

fn main() -> i32 {
  let a: i32 = 5;
  let b: i64 = 10;
  let c = a + b;
  return 0;
}

To change a value's type, use as:

Aela

fn main() -> i32 {
  let a: i32 = 5;
  let b: i64 = 10;
  let c = (a as i64) + b;          // 15, an i64
  let half = 7 as f64 / 2.0;       // 3.5
  let whole = 3.99 as i64;         // 3: the fraction is cut off
  let code = 'A' as u32;           // 65
  println("\(c) \(half) \(whole) \(code)");   // 15 3.5 3 65
  return 0;
}

An integer cast never changes a number without telling you. When you cast to an integer type that may not hold the value, such as a smaller one, the value is checked. If it does not fit, the program stops with a trap:

Aela

fn main() -> i32 {
  let n: i64 = 1000;
  let ok = n as i32;               // 1000 fits in an i32
  println("\(ok)");                // 1000
  let bad = n as u8;               // 1000 does not fit in a u8
  println("\(bad)");               // never reached
  return 0;
}

This program prints 1000, then stops with trap: integer out of range for its cast and exit status 1. If you really want only the low bits of the number, you write that out: std::low_bits(n) as u8 gives 232.

Arithmetic

The arithmetic operators are +, -, *, / and %. Multiplication and division happen before addition and subtraction, as in math. Parentheses change the order.

Aela

fn main() -> i32 {
  let a = 7;
  let b = 2;
  println("\(a + b) \(a - b) \(a * b) \(a / b) \(a % b)");   // 9 5 14 3 1
  println("\(-7 / 2) \(-7 % 2)");                            // -3 -1
  println("\(2 + 3 * 4) \((2 + 3) * 4)");                    // 14 20
  return 0;
}

Dividing two integers gives an integer. The result is rounded toward zero, so 7 / 2 is 3 and -7 / 2 is -3.
% gives the remainder. It has the same sign as the number on the left.
Dividing by zero stops the program with trap: division by zero. Dividing by the literal 0 is caught when the program compiles (error E0311).

Overflow

In C, if a signed integer gets too big for its type, the behavior is undefined. In Aela, +, - and * check every result. If the result does not fit the type, the program stops.

Aela

fn main() -> i32 {
  let big: u8 = 250;
  let more: u8 = 10;
  let sum = big + more;      // 260 does not fit in a u8
  println("\(sum)");         // never reached
  return 0;
}

This program stops with trap: arithmetic overflow and exit status 1. The trap report also names the function and line where it happened.

Sometimes you want a number to wrap around, as in a hash function or a checksum. For that, Aela has separate operators: +%, -% and *%. They keep the low bits of the result and never stop the program.

Aela

fn main() -> i32 {
  let big: u8 = 250;
  let more: u8 = 10;
  println("\(big +% more)");          // 4
  println("\((127 as i8) +% 1)");     // -128
  return 0;
}

Because wrapping has its own operators, a reader can tell at a glance where the code expects it. A plain + always means that overflow would be a bug.

Floats

Floats use +, -, * and /, and follow the usual IEEE 754 rules. They never trap. Dividing by zero gives inf, and 0.0 / 0.0 gives NaN. There is no % on floats.

Aela

fn main() -> i32 {
  let x = 0.1 + 0.2;
  let y: f64 = 1.0 / 3.0;
  println("\(x) \(y)");        // 0.30000000000000004 0.3333333333333333
  return 0;
}

Comparisons and Logic

The comparison operators are ==, !=, <, <=, > and >=. Their result is a bool. To combine bool values, use && (and), || (or) and ! (not). && and || stop early when the answer is already known.

Aela

fn main() -> i32 {
  let age = 30;
  let member = true;
  let adult = age >= 18;
  let discount = adult && !member;
  println("\(adult) \(discount) \(age == 30 || age > 100)");   // true false true
  return 0;
}

The bit operators are &, |, ^, ~, << and >>. Be careful: as in C, &, | and ^ bind more loosely than comparisons. So flags & 2 == 2 means flags & (2 == 2). In C this compiles and does the wrong thing. In Aela it is a compile error, because it mixes an integer with a bool. The compiler rejects this program with error E0305 and tells you to add parentheses:

Aela

fn main() -> i32 {
  let flags = 6;
  if (flags & 2 == 2) {
    println("set");
  }
  return 0;
}

The fix is to write (flags & 2) == 2.

Assignment

x = v stores a new value in a var. There are also short forms that combine an operator with assignment: +=, -=, *=, /=, %=, and the same for the bit operators. x += 5 means x = x + 5.

In Aela, an assignment is a statement and has no value. You cannot chain assignments, and you cannot assign inside a condition. The compiler rejects this program with error E0304 ("an assignment has no value"):

Aela

fn main() -> i32 {
  var x = 1;
  var y = 2;
  y = x = 5;
  return 0;
}

This also means the classic C bug if (x = 5), where = was written instead of ==, cannot happen in Aela.

Strings in Expressions

Strings have no operators. You cannot join them with +, and you cannot compare them with ==. Both are error E0309. The compiler rejects this program:

Aela

fn main() -> i32 {
  let first = "Ada";
  let last = "Lovelace";
  let full = first + " " + last;
  return 0;
}

To build a string, use interpolation. To compare two strings, use str::eq from the module std/string. The field len gives a string's length in bytes.

Aela

import str from "std/string";
fn main() -> i32 {
  let first = "Ada";
  let last = "Lovelace";
  let full = "\(first) \(last)";
  println(full);                             // Ada Lovelace
  println("\(full.len)");                    // 12
  println("\(str::eq(first, "Ada"))");       // true
  return 0;
}

Summary

Language	A variable declared without a value	Reading it
C	not initialized	undefined behavior
C++	not initialized	the same as C
Rust	must be set before use	compile error
Ada	not initialized	bounded error
Aela	starts at its zero value	always gives a known value

Aela also has a few rules that keep expressions predictable:

let never changes, and var can.
A name cannot be declared twice where both are visible.
Values never change type on their own. You convert them with as, and a conversion that would lose a value stops the program.
Integer overflow stops the program. Wrapping has its own operators.
An assignment is a statement, not a value.

These rules mean that what you read in the code is what the program does.

Chapter 3. Conditions and Branching

Programs make decisions with control flow. The most common form is the if statement, which runs some code only when a condition is true.

All the languages in this chapter have an if statement, but they have different rules for:

what kinds of values can be used as a condition
whether numbers, strings or pointers count as true or false
whether an assignment can be written where a comparison was meant

Aela keeps the rules simple. A condition must be a bool, and an assignment cannot be used as a condition.

Let's compare.

C

#include <stdio.h>
int main(void) {
  int x = 5;
  if (x > 0) {
    printf("x is positive\n");
  }
}

C Gotchas

1. Any number can be a condition

C

1if (x) { /* true when x != 0 */ }

This is short to write, but it means that almost any value can be used as a condition, even when that was not what you meant.

2. Assignment inside a condition

C

if (x = 5) {
  printf("Oops!\n");
}

This sets x to 5 and then checks whether 5 is not zero, so the condition is always true. It is a classic bug.

The language allows it. Most compilers only warn about it when you turn on extra warnings.

C++

#include <print>
int main() {
  int x = 5;
  if (x > 0) {
    std::println("x is positive");
  }
}

Numbers and pointers can still be used as conditions.
An assignment inside a condition is still allowed, and still dangerous.

C++17 added a way to declare a variable inside the if:

C++

1if (int y = x; y > 0) { /* ... */ }

This is useful, but it does not stop the old mistakes.

Rust

fn main() {
  let x = 5;
  if x > 0 {
    println!("x is positive");
  }
}

A condition must be a bool.
A number does not count as true or false, so if x {} is an error.
An assignment has no useful value, so if x = 5 {} is an error too.

Ada

with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
   X : Integer := 5;
begin
   if X > 0 then
      Put_Line("x is positive");
   end if;
end Main;

A condition must be a Boolean.
A number does not count as true or false.
Assignment is a statement, so it cannot appear inside an if condition.

In this way Ada is much more like Rust and Aela than like C.

Aela

positive.ae

fn main() -> i32 {
    let x = 5;
    if (x > 0) {
        println("x is positive");
    }
    return 0;
}

The condition goes inside parentheses, and the code to run goes inside braces. println is built in, so this program needs no import.

A condition must be a `bool`

You cannot use a number as a condition. This program does not compile:

Aela

fn main() -> i32 {
    let x = 5;
    if (x) {
        println("x is not zero");
    }
    return 0;
}

The compiler stops with error[E0301]: a condition must be a bool, found i64. The same error appears if you try to use a string as a condition.

To fix it, write the comparison you mean. Here are the usual checks for a number, a string and an optional value:

Aela

fn main() -> i32 {
    let x = 5;
    if (x != 0) {
        println("x is not zero");
    }
    let name = "";
    if (name.len == 0) {
        println("no name");
    }
    let age: i64? = none;
    if (age == none) {
        println("no age");
    }
    return 0;
}

Aela has no null. A value that may be missing has an optional type, such as i64?, and it is either a value or none. We will see a better way to check optionals later in this chapter.

An assignment is not a condition

In Aela an assignment is a statement. It does not produce a value, so it cannot be used inside a condition. This program does not compile:

Aela

fn main() -> i32 {
    var x = 0;
    if (x = 5) {
        println("Oops!");
    }
    return 0;
}

The compiler stops with error[E0304]: an assignment has no value: write it as a statement of its own. The C bug from earlier cannot happen.

Operators in conditions

The comparison operators are ==, !=, <, <=, > and >=. They give a bool. The logical operators are && (and), || (or) and ! (not). They take bool values only.

Aela

fn main() -> i32 {
    let age = 30;
    let member = true;
    let xs: i64[] = [];
    if (age >= 18 && member) {
        println("welcome");
    }
    if (!member || age < 18) {
        println("sorry");
    }
    if (xs.len > 0 && xs[0] == 1) {
        println("starts with 1");
    }
    return 0;
}

This prints only welcome.

&& and || stop early. If the left side of && is false, the right side is never run. In the last if, this is what keeps xs[0] from being read when the array is empty.

Both sides of a comparison must have the same type. Aela does not convert between types for you, not even between i32 and i64. Use as to convert, as in (n as i64) > limit.

Strings have no == operator. This program does not compile:

Aela

fn main() -> i32 {
    let a = "cat";
    let b = "cat";
    if (a == b) {
        println("same");
    }
    return 0;
}

The compiler stops with error[E0309]: strings have no comparison operators: use str::eq(a, b) or str::cmp(a, b). Use the function str::eq from std/string instead:

Aela

import str from "std/string";
fn main() -> i32 {
    let a = "cat";
    let b = "cat";
    if (str::eq(a, b)) {
        println("same");    // same
    }
    return 0;
}

One more thing to watch for. The bit operators &, | and ^ bind more loosely than comparisons, as they do in C. So x & 1 == 0 means x & (1 == 0). In C this compiles and gives a wrong answer. In Aela it is error[E0305], because it mixes an integer and a bool. Write (x & 1) == 0 instead.

Example: A Three-Way Branch

Here is a full "positive, zero or negative" decision. Each else if is tried only when the conditions above it were false, and the final else runs when none of them were true.

three_way.ae

fn describe(x: i64) -> void {
    if (x > 0) {
        println("positive");
    } else if (x == 0) {
        println("zero");
    } else {
        println("negative");
    }
}
fn main() -> i32 {
    describe(7);     // positive
    describe(0);     // zero
    describe(-3);    // negative
    return 0;
}

C and C++

The structure is the same, but with the hazards we discussed above.

Rust

The structure is the same, but there are no parentheses around the conditions.

Ada

The structure is the same, but Ada writes elsif and ends the whole statement with end if;.

`if` Is Not an Expression

In Rust you can write let size = if x > 5 { "big" } else { "small" };. Aela does not allow this. In Aela if is only a statement, and using it as a value is a syntax error (error[E0102]: expected an expression).

When you need a value that depends on a condition, use match, which is the subject of the next section:

Aela

fn main() -> i32 {
    let x = 7;
    let size = match (x > 5) { true => "big", false => "small" };
    println(size);    // big
    return 0;
}

`match`

A match compares one value against a list of patterns. The arms are tried in order, and the first arm that matches is the one that runs. It is like switch in C, but there is no fallthrough from one arm into the next, and the compiler checks that every possible value is handled.

classify.ae

fn classify(n: i64) -> string {
    match (n) {
        0 => { return "zero"; },
        1 | 2 | 3 => { return "small"; },
        4..=9 => { return "medium"; },
        x if x < 0 => { return "negative \(x)"; },
        _ => { return "large"; }
    }
}
fn main() -> i32 {
    println(classify(0));     // zero
    println(classify(2));     // small
    println(classify(7));     // medium
    println(classify(-4));    // negative -4
    println(classify(50));    // large
    return 0;
}

These are the patterns you can use:

a literal: an integer, a character, a string, true or false
a range of integers or characters: 4..9 leaves out 9, and 4..=9 includes it
an enum variant, such as Light::Red
a name, such as x, which matches any value and gives it that name inside the arm
_, which matches any value
two or more patterns joined with |, which matches if any of them match

You can add a guard to an arm with if, as in x if x < 0. The arm only matches when the guard is true.

A match can also give a value. Then each arm is an expression instead of a block:

lights.ae

enum Light { Red, Yellow, Green }
fn main() -> i32 {
    let light = Light::Yellow;
    let advice = match (light) {
        Light::Red => "stop",
        Light::Yellow => "slow down",
        Light::Green => "go",
    };
    println(advice);    // slow down
    let c = 'q';
    let kind = match (c) { 'a'..='z' => "lower", 'A'..='Z' => "upper", _ => "other" };
    println(kind);      // lower
    let word = "bye";
    let code = match (word) { "hi" => 1, "bye" => 2, _ => 0 };
    println("\(code)"); // 2
    return 0;
}

Every case must be handled

A match must cover every possible value. For an enum, that means every variant. For a number or a string, it usually means adding a _ arm at the end. An arm with a guard does not count, because the guard might be false.

This program forgets Light::Yellow, so it does not compile:

Aela

enum Light { Red, Yellow, Green }
fn main() -> i32 {
    let light = Light::Green;
    match (light) {
        Light::Red => { println("stop"); },
        Light::Green => { println("go"); },
    }
    return 0;
}

The compiler stops with error[E0329]: match does not handle the variant (add an arm, or _ =>): 'Yellow'. This is very helpful when you add a new variant to an enum later. The compiler will point to every match that needs a new arm.

Tuples and structs cannot be used as patterns. Enum variants that carry fields can be matched, and a pattern can give names to their fields.

`if (let ...)`: Checking an Optional

Earlier we checked an optional value with age == none. That tells you whether a value is there, but it does not let you use the value. Aela does not let you compare or do math on an optional directly. For example, age > 18 with age: i64? is error[E0314].

Instead, use if (let ...). If the optional holds a value, the first block runs, and the new name holds that value. If the optional is none, the else block runs.

find.ae

fn find(xs: &i64[], want: i64) -> i64? {
    for (let i: i64, let x: i64 in xs) {
        if (x == want) { return i; }
    }
    return none;
}
fn main() -> i32 {
    let xs: i64[] = [10, 20, 30];
    if (let i = find(&xs, 20)) {
        println("found at \(i)");     // found at 1
    } else {
        println("missing");
    }
    if (let i = find(&xs, 99)) {
        println("found at \(i)");
    } else {
        println("missing");           // missing
    }
    println("\(find(&xs, 99) ?? -1)");    // -1
    return 0;
}

The name i can only be used inside the first block, and it cannot be changed. The last line shows the ?? operator. It gives the value if there is one, and the value on its right if there is not.

You can chain these checks with else if (let ...):

Aela

fn main() -> i32 {
    let first: string? = none;
    let second: string? = "bo";
    if (let a = first) {
        println("first: \(a)");
    } else if (let b = second) {
        println("second: \(b)");    // second: bo
    } else {
        println("neither");
    }
    return 0;
}

Rust has the same idea, written if let Some(i) = find(...). C has no optionals, so the usual way is to return a special value such as -1 or NULL and hope that every caller checks for it.

Summary

Language	Condition must be a bool?	Numbers count as true or false?	Assignment allowed in `if`?	Checks that every case is handled?
C	No	Yes	Yes	No
C++	No	Yes	Yes	No
Rust	Yes	No	No	Yes, in `match`
Ada	Yes	No	No	Yes, in `case`
Aela	Yes	No	No	Yes, in `match`

Aela's rules stop several kinds of bugs that are common in C and C++, and the syntax still looks familiar.

Chapter 4. Loops

A loop repeats some work until a condition tells it to stop. Every language has some kind of while or for loop, but they differ in how safe and clear they are, and in how much the compiler can check.

This chapter shows ordinary loops first. Proving things about loops comes later, as an advanced topic.

Part 1 — Ordinary Loops

We start with the simplest form, a while loop that counts from 0 to 2.

C

int i = 0;
while (i < 3) {
  printf("%d\n", i);
  i = i + 1;
}

Any number can be a condition, so while (i) compiles.
An assignment can be a condition, so while (i = 5) compiles and never ends.
A variable declared without a value holds whatever was in memory before.

C++

C++ has the same rules, and the same pitfalls, as C.

C++

int i = 0;
while (i < 3) {
  std::println("{}", i);
  i++;
}

Rust

let mut i = 0;
while i < 3 {
  println!("{i}");
  i += 1;
}

The condition must be a bool.
A number does not count as true or false.
An assignment cannot be used as a condition.

Ada

with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
   I : Integer := 0;
begin
   while I < 3 loop
      Put_Line(Integer'Image(I));
      I := I + 1;
   end loop;
end Main;

The condition must be a Boolean.
A number does not count as true or false.
An assignment cannot be used as a condition.

Aela

Aela follows the same model as Rust and Ada:

count.ae

fn main() -> i32 {
    var i = 0;
    while (i < 3) {
        println("\(i)");
        i = i + 1;
    }
    return 0;
}

This prints 0, 1 and 2, each on its own line. i is declared with var because the loop changes it. A let cannot be changed. "\(i)" puts the value of i into a string, because println only takes a string.

The rules from the last chapter apply to loops too:

The condition must be a bool. while (i) is error[E0301]: a condition must be a bool, found i64.
An assignment cannot be a condition. while (i = 5) is error[E0304].

Aela also never gives you a variable full of leftover memory. A variable declared without a value starts at its type's zero value:

Aela

fn main() -> i32 {
    var n: i64;
    var s: string;
    println("\(n) [\(s)]");    // 0 []
    return 0;
}

`break` and `continue`

break leaves the loop at once. continue skips the rest of the body and goes on with the next round of the loop. A common pattern is a while (true) loop that ends with a break:

break.ae

fn main() -> i32 {
    var i = 0;
    while (true) {
        i += 1;
        if (i % 2 == 0) { continue; }
        if (i > 7) { break; }
        print("\(i) ");
    }
    println("");    // 1 3 5 7
    for (let row: i64 in 0..3) {
        for (let col: i64 in 0..3) {
            if (col > row) { break; }
            print("\(row)\(col) ");
        }
    }
    println("");    // 00 10 11 20 21 22
    return 0;
}

print is like println, but it does not add a new line.

break and continue always act on the innermost loop. In the second part of the example, break ends only the inner loop over col, and the outer loop goes on. Aela has no loop labels, so you cannot break out of two loops at once. If you need that, put the loops in a function and use return. Using break or continue outside a loop is error[E0125].

No `while (let ...)`

The last chapter showed if (let x = o) for optional values. Rust also has while let, but Aela does not. while (let m = next(n)) is a syntax error (error[E0102]: expected an expression).

Write a while (true) loop with an if (let ...) inside it instead:

doubling.ae

fn next_double(n: i64) -> i64? {
    if (n >= 50) { return none; }
    return n * 2;
}
fn main() -> i32 {
    var n = 1;
    while (true) {
        if (let m = next_double(n)) {
            n = m;
            print("\(n) ");
        } else {
            break;
        }
    }
    println("");    // 2 4 8 16 32 64
    return 0;
}

Basic `for` Loops

Now we look at loops over ranges and collections.

C (a range through an index)

C

for (int i = 0; i < 3; i++) {
  printf("%d\n", i);
}

It is easy to write a loop that never ends by mistake.
An assignment is allowed in the condition.
Off-by-one errors are common, such as writing <= where < was meant.

C++

#include <print>
#include <vector>
int main() {
    for (int i : {0, 1, 2}) {
        std::println("{}", i);
    }
}

Rust (iterator style)

Rust

for i in 0..3 {
  println!("{i}");
}

It is safer, because the range is written directly.
It removes many indexing mistakes.

Ada

for I in 0 .. 2 loop
   Put_Line(Integer'Image(I));
end loop;

Range loops are built in.
The loop counter cannot be changed inside the loop.

Aela

Aela loops over a range like this:

ranges.ae

fn main() -> i32 {
    for (let i: i64 in 0..3) {
        println("\(i)");
    }
    for (let i: i64 in 1..=3) {
        print("\(i) ");
    }
    println("");    // 1 2 3
    let n = 4;
    for (let i: i64 in -2..n) {
        print("\(i) ");
    }
    println("");    // -2 -1 0 1 2 3
    for (let i: i64 in 5..5) {
        println("never printed");
    }
    return 0;
}

The first loop prints 0, 1 and 2, each on its own line.

a..b counts from a up to b, but does not include b.
a..=b includes b.
The ends of a range can be any expressions, not just numbers.
A range that is empty, such as 5..5, runs the body zero times. So does a range like 3..1. Ranges never count down.
The counter is declared with let and its type, and over a range the type must be i64. Writing let i: i32 is error[E0126]: a range loop counter is an i64. Leaving out let and the type is error[E0101].
The counter cannot be changed inside the loop. i = 5; in the body is error[E0413].
There is no C-style three-part for loop. Use a range, or a while loop.

Arrays

A for loop can also walk over the elements of an array. If you add a second name in front, the first one holds the index:

arrays.ae

fn main() -> i32 {
    let names: string[] = ["ada", "bo", "cy"];
    for (let name: string in &names) {
        println(name);
    }
    for (let i: i64, let name: string in &names) {
        println("\(i): \(name)");
    }
    println("\(names.len)");     // 3
    return 0;
}

This prints:

Shell

ada
bo
cy
0: ada
1: bo
2: cy
3

You can write names or &names after in. Either way the loop only reads the elements, and the array is still there after the loop. The element's type must match the array's type. for (let x: i32 in &xs) with xs: i64[] is error[E0301]: the elements are i64, found i32. The index is always an i64.

The loop variable is a read-only view of each element. To change the elements, loop over the indexes, or over references to the elements:

change.ae

fn main() -> i32 {
    var xs: i64[] = [1, 2, 3];
    for (let i: i64 in 0..xs.len) {
        xs[i] = xs[i] * 10;
    }
    println("\(xs)");    // [10, 20, 30]
    for (let p: &xs::&i64 in mut &xs) {
        *p += 1;
    }
    println("\(xs)");    // [11, 21, 31]
    return 0;
}

In the second loop, mut &xs lends the array to the loop so that it can be changed. Each p is a reference to one element, and *p is the element itself. The type &xs::&i64 means "a reference to an i64 inside xs".

Strings

A string in Aela is a list of bytes in UTF-8. A for loop over a string gives you its bytes, as u8 values. To get characters, use str::chars from std/string:

strings.ae

import str from "std/string";
fn main() -> i32 {
    let word = "añb";
    for (let i: i64, let b: u8 in word) {
        print("\(i):\(b) ");
    }
    println("");    // 0:97 1:195 2:177 3:98
    let chars: char[] = str::chars(word);
    for (let c: char in &chars) {
        print("[\(c)]");
    }
    println("");    // [a][ñ][b]
    return 0;
}

The word has three characters, but four bytes, because ñ takes two bytes in UTF-8. Writing for (let c: char in word) is error[E0301], and the message tells you to use str::chars.

Summary of Ordinary Loops

Language	Numbers count as true or false?	Assignment in a condition?	Range loops built in?
C	Yes	Yes	No
C++	Yes	Yes	Partly
Rust	No	No	Yes
Ada	No	No	Yes
Aela	No	No	Yes

In ordinary use, Aela behaves most like Rust and Ada. Conditions are strict bool values, there are no hidden conversions, and the flow of the program is easy to predict.

Part 2 — Verified Loops (Aela and SPARK Ada)

Now that we have seen ordinary loops, we look at an optional feature. In Aela you can ask the compiler to prove facts about a loop, before the program ever runs.

Both Aela and Ada in SPARK mode can check loops with invariants and variants. An invariant is a fact that must be true every time around the loop. A variant is a number that must get smaller every time around the loop, which proves that the loop ends. This part is advanced, and you can skip it on a first reading.

Why invariants?

An invariant says what is always true about the loop's variables. The checker makes sure that:

it is true when the loop is first reached
each round of the loop keeps it true
it is still true after the loop ends, so the code after the loop can rely on it

A variant proves that the loop really ends. It must never go below zero, and it must get smaller every round.

SPARK Ada example (for reference)

Ada

while I < N loop
 pragma Loop_Invariant (0 <= I and then I <= N);
 pragma Loop_Variant   (Decreases => N - I);
 I := I + 1;
end loop;

This is the kind of tool used in systems where safety matters most, such as aircraft, medical devices and railways.

Aela example (the same idea, shorter)

In Aela, you write #invariant and #variant lines right before a while or for loop. They describe that loop. A function can also have #requires, which says what must be true when the function is called.

count_up.ae

#requires 0 <= n;
fn count_up(n: i64) -> i64 {
    var i: i64 = 0;
    #invariant 0 <= i && i <= n;
    #variant n - i;
    while (i < n) {
        i = i + 1;
    }
    return i;
}
fn main() -> i32 {
    println("\(count_up(3))");    // 3
    return 0;
}

These lines are only checked when you build with --verify:

Shell

1aec count_up.ae --verify -o count_up && ./count_up

A normal build without --verify skips them. Either way, nothing extra goes into the program, so the checks cost nothing when it runs.

With --verify, the compiler proves that:

i stays between 0 and n
the loop ends, because n - i gets smaller every round and never goes below zero
every call to count_up passes an n that is not negative

If a proof fails, the program does not compile. For example, #variant i; in the loop above is wrong, because i gets bigger, not smaller. With --verify this is error[E0807]: the loop variant (#variant) is not proven to decrease. An invariant that is false when the loop starts, such as #invariant i < 0;, is error[E0806]: the loop invariant is not proven on entry.

There are limits to what the checker understands. A specification must be made of comparisons joined by &&. Each side may use variables, lengths such as xs.len, constants, + and -. Calls, * and || are not allowed, and using them is error[E0802]. A #variant must be even simpler, such as n - i or xs.len - i. These limits keep the checker fast and predictable.

What `--verify` checks for you

--verify does more than check the lines you write. It also proves that every array index is in range, and that plain +, - and * cannot overflow.

Here is a loop that adds up an array:

total.ae

fn total(xs: &i64[]) -> i64 | Overflow {
    var t: i64 = 0;
    var i: i64 = 0;
    #invariant 0 <= i && i <= xs.len;
    #variant xs.len - i;
    while (i < xs.len) {
        (t += xs[i])?;
        i += 1;
    }
    return t;
}
fn main() -> i32 | Overflow {
    let xs: i64[] = [1, 2, 3, 4];
    println("\(total(&xs)?)");    // 10
    return 0;
}

With --verify, the compiler proves that:

xs[i] is always in range, so the program never stops with an index error
i += 1 cannot overflow, because i is less than xs.len
the loop ends, because xs.len - i gets smaller every round

The sum itself could still overflow if the numbers were very large, and the compiler cannot rule that out without knowing the numbers. So the addition is written (t += xs[i])?. If it overflows, the function fails with Overflow instead of stopping the program. The | Overflow in the function's type says that this can happen, and total(&xs)? in main passes the failure on.

Now suppose we make the classic off-by-one mistake and write <= instead of <:

Aela

fn total(xs: &i64[]) -> i64 | Overflow {
    var t: i64 = 0;
    var i: i64 = 0;
    while (i <= xs.len) {
        (t += xs[i])?;
        i += 1;
    }
    return t;
}
fn main() -> i32 | Overflow {
    let xs: i64[] = [1, 2, 3, 4];
    println("\(total(&xs)?)");
    return 0;
}

A normal build compiles this, and the program stops at run time with trap: index out of bounds. With --verify, the program does not compile. The error is error[E0809]: an index that may be out of bounds, and it points at xs[i]. The bug is found before the program runs.

A range loop is even simpler, because the compiler already knows the bounds of the counter. This version needs no invariant at all, and it passes --verify too:

Aela

fn total(xs: &i64[]) -> i64 | Overflow {
    var t: i64 = 0;
    for (let i: i64 in 0..xs.len) {
        (t += xs[i])?;
    }
    return t;
}
fn main() -> i32 | Overflow {
    let xs: i64[] = [1, 2, 3, 4];
    println("\(total(&xs)?)");    // 10
    return 0;
}

Summary (Verification Features)

Language	Loop invariants?	Proves loops end?	Proofs at compile time?
C	No	No	No
C++	No	No	No
Rust	No	No	No
Ada with SPARK	Yes	Yes	Yes
Aela	Yes	Yes	Yes

With --verify, Aela can prove facts about loops, as SPARK Ada can. The checker is simpler than SPARK's, but it is built into the compiler, and it costs nothing when the program runs.

Chapter 5. Functions

Functions are the main way to group logic and reuse code. A function takes inputs, called parameters. It can give back a value, called its result. Its body has its own scope, so the names declared inside it are not visible outside.

Languages differ in what a function may do to the values it is given, and in how it reports that something went wrong. This chapter starts with the simplest case, a function that adds two integers, and then looks at those differences.

Part 1. Ordinary Functions

C

#include <stdio.h>
int add(int a, int b) {
  return a + b;
}
int main(void) {
  printf("%d\n", add(2, 3));
  return 0;
}

There is no type inference.
A declaration in a header can disagree with the definition, and the compiler may not notice.
C converts between number types without asking. Passing a long where an int is expected silently cuts the value down.

C++

C++ has the same rules as C, and adds overloading, so two functions can share a name if their parameter types differ.

C++

#include <print>
int add(int a, int b) {
  return a + b;
}
int main() {
  std::println("{}", add(2, 3));
}

Rust

fn add(a: i32, b: i32) -> i32 {
    a + b
}
fn main() {
    println!("{}", add(2, 3));
}

The last expression of a block is its value when it has no semicolon, so a + b is the result.
Types are inferred for let, but never for parameters or results.

Ada

with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
   function Add (A, B : Integer) return Integer is
   begin
      return A + B;
   end Add;
begin
   Put_Line (Integer'Image (Add (2, 3)));
end Main;

Ada has strong static typing.
Parameter and result types are always written out.

Aela

add.ae

fn add(a: i32, b: i32) -> i32 {
    return a + b;
}
fn main() -> i32 {
    println("\(add(2, 3))");    // 5
    return 0;
}

The rules for an Aela function are simple and strict.

Every parameter has a written type.
The result type is always written. A function that gives back nothing is written -> void.
The result is given with return. There is no "last expression" rule as in Rust.
A function with a result must return a value on every path through its body.
There are no implicit conversions. An i64 is not accepted where an i32 is expected.
There is no overloading. Each function name means one function.

println takes a string. To print a number, put it inside a string with \( ). Any value can be printed this way.

The compiler checks that every path returns. This program does not compile, because sign(0) would reach the end of the body without a value.

Aela

fn sign(n: i64) -> string {
    if (n < 0) { return "negative"; }
    if (n > 0) { return "positive"; }
}
fn main() -> i32 {
    println(sign(4));
    return 0;
}

The compiler reports error[E0399]: this function can reach the end of its body without returning a value. Adding return "zero"; at the end fixes it.

The next program does not compile either. The variable x is an i64, and add wants an i32.

Aela

fn add(a: i32, b: i32) -> i32 {
    return a + b;
}
fn main() -> i32 {
    let x: i64 = 2;
    println("\(add(x, 3))");
    return 0;
}

The error is error[E0301]: expected i32, found i64. If you really want the conversion, write it with as, as in add(x as i32, 3). A conversion with as is checked when the program runs. If the value does not fit in an i32, the program stops with a trap.

Default values and variadic parameters

A parameter can have a default value. A call may then leave it out. The last parameter can also collect any number of extra arguments into an array. You write it with ... before its name.

Aela

fn greet(name: string, greeting: string = "hello") -> void {
    println("\(greeting), \(name)");
}
fn sum(first: i64, ...rest: i64[]) -> i64 {
    var total = first;
    for (let x: i64 in rest) { total += x; }
    return total;
}
fn main() -> i32 {
    greet("ada");                   // hello, ada
    greet("bob", "hi");             // hi, bob
    println("\(sum(1, 2, 3, 4))");  // 10
    return 0;
}

Only parameters at the end can be left out. Aela has no named arguments.

Part 2. Passing Data, References and `mut &`

Languages differ in how a function gets the values passed to it. In C everything is copied, and a function that wants to change the caller's variable must be given a pointer. Nothing in C stops two pointers from pointing at the same thing, or stops a pointer from outliving the value it points to.

Aela has three ways to pass a value.

parameter	the call writes	what the function gets
`p: T`	`f(x)`	the value itself
`p: &T`	`f(&x)`	a shared reference that can only read `x`
`mut p: &T`	`f(mut &x)`	an exclusive reference that can change `x`

When you pass a value itself, numbers are copied. Strings are shared, which is safe because a string can never change. Structs and arrays are moved into the call, so the caller cannot use them afterwards. Chapter 6 shows moves in more detail.

The call site always shows what is going on. If you see mut &x in a call, you know the function may change x. If you see &x, you know it will not.

Aela

fn total(xs: &i64[]) -> i64 {
    var t: i64 = 0;
    for (let x: i64 in xs) { t += x; }
    return t;
}
fn add_to_all(mut xs: &i64[], k: i64) -> void {
    for (let i: i64 in 0..xs.len) { xs[i] += k; }
}
fn main() -> i32 {
    var scores: i64[] = [3, 5, 7];
    println("\(total(&scores))");       // 15
    add_to_all(mut &scores, 10);
    println("\(scores)");               // [13, 15, 17]
    return 0;
}

Here is the classic "increment" function. Through a reference to a number, *x reads the number and *x = ... writes it.

Aela

fn increment(mut x: &i64) -> void {
    *x = *x + 1;
}
fn main() -> i32 {
    var value: i64 = 10;
    increment(mut &value);
    println("\(value)");    // 11
    return 0;
}

The compiler checks both sides of the call.

Writing increment(&value) is an error, because the function asks for an exclusive reference. The compiler reports E0416.
If value were declared with let, then mut &value would be an error, because a let can never change. The compiler reports E0414.

A variable may have many shared references at once, or exactly one exclusive reference, but never both. This program breaks that rule, because it passes xs to be changed and to be read in the same call.

Aela

fn copy_into(mut dst: &i64[], src: &i64[]) -> void {
    for (let x: i64 in src) { dst.push(x); }
}
fn main() -> i32 {
    var xs: i64[] = [1, 2];
    copy_into(mut &xs, &xs);
    return 0;
}

The compiler rejects it with error[E0407]: cannot borrow while it is mutably borrowed: 'xs'. In C, the same function would add elements to the array while it is reading it, which can loop forever or read freed memory.

There is one more use of mut on a parameter. Writing mut n: i64 (with no &) makes the parameter a local variable that the function may change. It is the function's own copy, so the caller does not see the change.

Aela

fn countdown(mut n: i64) -> void {
    while (n > 0) {
        print("\(n) ");
        n -= 1;
    }
    println("go");
}
fn main() -> i32 {
    let start: i64 = 3;
    countdown(start);           // 3 2 1 go
    println("\(start)");        // 3
    return 0;
}

Without mut, a parameter works like a let and cannot be assigned.

Part 3. Failures as Values

Sometimes a function cannot do its job. The input may be bad, or a file may be missing. Languages handle this in different ways.

In C, a function usually returns a special value such as -1, and sets errno. Nothing forces the caller to check it.

C

#include <stdio.h>
#include <stdlib.h>
int main(void) {
  FILE *f = fopen("missing.txt", "r");
  if (f == NULL) {
    perror("fopen");
    return 1;
  }
  fclose(f);
  return 0;
}

C++ and many other languages use exceptions. An exception can come out of any call, and nothing in the function's signature says so.

Rust returns a Result, and the ? operator passes an error on to the caller.

Rust

fn halve(x: i64) -> Result<i64, String> {
    if x < 0 {
        return Err(format!("negative: {}", x));
    }
    Ok(x / 2)
}
fn quarter(x: i64) -> Result<i64, String> {
    Ok(halve(halve(x)?)?)
}
fn main() {
    match quarter(-8) {
        Ok(v) => println!("{}", v),
        Err(e) => println!("{}", e),
    }
}

Aela works in a similar way to Rust. A function lists the failures it can return after its result type, separated by |. A failure is a value with its own type, declared with failure. The function returns one with fail.

Aela

failure Negative { value: i64; }
fn checked_sqrt(n: i64) -> i64 | Negative {
    if (n < 0) { fail Negative { value: n }; }
    var r: i64 = 0;
    while ((r + 1) * (r + 1) <= n) { r += 1; }
    return r;
}
fn sum_of_roots(a: i64, b: i64) -> i64 | Negative {
    return checked_sqrt(a)? + checked_sqrt(b)?;
}
fn main() -> i32 {
    match (sum_of_roots(16, 9)) {
        v => { println("ok: \(v)"); },                          // ok: 7
        e: Negative => { println("negative: \(e.value)"); }
    }
    match (sum_of_roots(16, -4)) {
        v => { println("ok: \(v)"); },
        e: Negative => { println("negative: \(e.value)"); }     // negative: -4
    }
    return 0;
}

The caller of a function that can fail must handle the failure in one of three ways.

f(x)? gives the value, or returns the failure from the calling function as well.
return f(x); gives back the value or the failure just as it is.
match (f(x)) { ... } has one arm for the value and one arm for each failure. A failure arm is written name: FailureType.

There are no exceptions in Aela, and nothing unwinds the stack. A failure is just a value that a function returns, so you can always see from a signature what can go wrong.

Ignoring a failure is a compile error. This program stores the result without handling it.

Aela

failure Negative { value: i64; }
fn checked_sqrt(n: i64) -> i64 | Negative {
    if (n < 0) { fail Negative { value: n }; }
    return n;
}
fn main() -> i32 {
    let r = checked_sqrt(9);
    println("\(r)");
    return 0;
}

The compiler reports error[E0502]: the result of a call that can fail must be handled with ?, match or return.

Using ? also has a rule. The calling function must list the same failure in its own signature. A function declared -> i64 with no failures cannot use ? on checked_sqrt. The compiler reports E0503 there.

A few failures are built into the language. Arithmetic, division and indexing normally stop the program with a trap when something goes wrong. If you add ?, they return a failure instead. For example, (a + b)? fails with Overflow, and (a / b)? fails with DivByZero.

Aela

fn mean(xs: &i64[]) -> i64 | Overflow | DivByZero {
    var total: i64 = 0;
    for (let x: i64 in xs) { (total += x)?; }
    return (total / xs.len)?;
}
fn report(xs: &i64[]) -> string {
    return match (mean(xs)) {
        v => "mean \(v)",
        _: Overflow => "too big",
        _: DivByZero => "no values"
    };
}
fn main() -> i32 {
    let some: i64[] = [4, 8, 9];
    let empty: i64[] = [];
    println(report(&some));     // mean 7
    println(report(&empty));    // no values
    return 0;
}

This example uses match as an expression. Each arm gives a value, and _: Overflow means "this failure, without giving it a name".

main may list failures too. If a failure leaves main, the program prints a report and exits with status 70.

Aela

failure Negative { value: i64; }
fn halve(x: i64) -> i64 | Negative {
    if (x < 0) { fail Negative { value: x }; }
    return x / 2;
}
fn main() -> i32 | Negative {
    println("\(halve(4)?)");
    println("\(halve(-3)?)");
    return 0;
}

If this file is called halve.ae, the program prints the following.

Text

2
failure: Negative { value: -3 }
  at halve (halve.ae:4)
  at main (halve.ae:10)

For a real bug, where the program should simply stop, use std::trap("message") instead of a failure. Aela has no panic.

Part 4. Pure Functions

A function marked pure fn has no side effects. It cannot print, read or write files, or use a global var. It can only call other pure functions and the builtins that have no effects. It cannot take a mut & parameter, and it cannot fail. The compiler checks all of this, so the word pure is a promise you can rely on.

Aela

pure fn square(x: i64) -> i64 {
    return x * x;
}
pure fn sum_of_squares(a: i64, b: i64) -> i64 {
    return square(a) + square(b);
}
fn main() -> i32 {
    println("\(sum_of_squares(3, 4))");    // 25
    return 0;
}

This one does not compile, because a pure function may not print.

Aela

pure fn square(x: i64) -> i64 {
    println("squaring");
    return x * x;
}
fn main() -> i32 {
    println("\(square(3))");
    return 0;
}

The error is error[E0903]: a pure function can only call pure functions and effect-free builtins: 'println'.

A pure function can still trap, for example on overflow.

Part 5. Function Values and Closures

In C, you can pass a function to another function through a function pointer.

C

#include <stdio.h>
int twice(int x) { return x * 2; }
int apply(int (*f)(int), int x) {
  return f(x);
}
int main(void) {
  printf("%d\n", apply(twice, 21));
  return 0;
}

In Aela, a function is a value. You can pass it, store it in a variable or an array, return it, and call it later. The type of a function value is written like a signature without names, for example fn(i64) -> i64.

Aela

fn double(x: i64) -> i64 { return x * 2; }
fn square(x: i64) -> i64 { return x * x; }
fn apply_twice(f: fn(i64) -> i64, x: i64) -> i64 {
    return f(f(x));
}
fn main() -> i32 {
    println("\(apply_twice(double, 3))");   // 12
    println("\(apply_twice(square, 3))");   // 81
    let ops: (fn(i64) -> i64)[] = [double, square];
    for (let op: fn(i64) -> i64 in ops) {
        print("\(op(5)) ");
    }
    println("");                            // 10 25
    return 0;
}

An array of function values needs parentheses around the function type, as in (fn(i64) -> i64)[]. Without them, the [] would belong to the result type.

You can also write a function where a value is expected. This is a function expression. It can use the variables around it, and then it is called a closure. A function expression may leave out its result type. The compiler then takes it from the first return, or uses void if there is none.

Aela

fn main() -> i32 {
    let step: i64 = 3;
    let add_step = fn(x: i64) -> i64 { return x + step; };
    println("\(add_step(10))");             // 13
    var log: string = "";
    let note = fn(word: string) -> { log = "\(log)\(word) "; };
    note("one");
    note("two");
    println(log);                           // one two
    return 0;
}

How a closure sees a variable depends on the variable's type.

Numbers, bools, chars and enums are copied when the closure is made. The closure cannot change its copy.
Strings, structs, arrays and optionals are shared with the function around the closure. A change made by either side is seen by the other. That is why note can add to log.

A closure may outlive the function that made it. Here each call of tick adds to an array that only the closure can still reach.

Aela

fn make_counter() -> fn() -> i64 {
    var hits: i64[] = [];
    return fn() -> i64 {
        hits.push(1);
        return hits.len;
    };
}
fn main() -> i32 {
    let tick = make_counter();
    tick();
    tick();
    println("\(tick())");                   // 3
    return 0;
}

A closure written directly as an argument, for a function that only calls it, may also change a number around it. The compiler knows that such a closure runs only during that call.

Aela

fn each(xs: &i64[], f: fn(i64) -> void) -> void {
    for (let x: i64 in xs) { f(x); }
}
fn main() -> i32 {
    let xs: i64[] = [1, 2, 3, 4];
    var total: i64 = 0;
    each(&xs, fn(x: i64) -> void { total += x; });
    println("\(total)");                    // 10
    return 0;
}

A closure that is stored in a variable cannot do this. This program is rejected with E0435, because bump holds a copy of count.

Aela

fn main() -> i32 {
    var count: i64 = 0;
    let bump = fn() -> { count += 1; };
    bump();
    println("\(count)");
    return 0;
}

Some functions cannot be used as values. These are generic functions, methods, builtins such as println, and async functions. To pass one of them, wrap it in a small function expression.

Part 6. Verified Functions

Some languages let you state what a function needs and what it promises, and then prove it before the program runs. SPARK, a subset of Ada, is the best known example.

Ada

function Add_One (N : Integer) return Integer
  with Pre  => N >= 0 and N < 1000,
       Post => Add_One'Result = N + 1;

The SPARK tools prove that every caller meets the precondition (Pre), and that the function always meets the postcondition (Post).

Aela has a built-in verifier that works in the same spirit. You write specifications on the lines just before a function or a loop.

specification	where it goes	what it states
`#requires`	before a function	what must be true when the function is called
`#ensures`	before a function	what is true of `result` when the function returns
`#let`	before a function	a name for a value, used only in specifications
`#invariant`	before a loop	what is true each time the loop starts a new round
`#variant`	before a loop	a number that stays at 0 or more and gets smaller each round, so the loop ends

The checks run when you build with aec --verify. A normal build does not check the specifications.

Aela

#requires n >= 0 && n < 1000;
#ensures result == n + 1;
fn add_one(n: i64) -> i64 {
    return n + 1;
}
#requires 0 <= n && n < 1000000;
#ensures result == n;
fn count_up(n: i64) -> i64 {
    var i: i64 = 0;
    #invariant 0 <= i && i <= n;
    #variant n - i;
    while (i < n) {
        i += 1;
    }
    return i;
}
fn main() -> i32 {
    println("\(add_one(41)) \(count_up(5))");   // 42 5
    return 0;
}

With aec --verify, the compiler proves the following facts about this program.

Every call of add_one passes a number from 0 to 999.
Each return meets its #ensures.
The invariant holds when the loop starts and after each round.
The variant n - i never goes below 0 and gets smaller each round, so the loop ends.
No + in the program can overflow.

The last point is worth noting. With --verify, every plain +, - and * must be proven not to overflow, and every index must be proven to be in range. This is why add_one needs its #requires.

If a call breaks a precondition, the verified build fails. This program builds normally, but it is rejected by aec --verify.

Aela

#requires n >= 0 && n < 1000;
fn add_one(n: i64) -> i64 {
    return n + 1;
}
fn main() -> i32 {
    println("\(add_one(5000))");
    return 0;
}

The error is error[E0804]: the precondition (#requires) is not proven for this call to 'add_one'.

Here is a loop over an array. #let gives the array's length a name, and (t += xs[i])? turns a possible overflow into a failure instead of something that must be proven impossible.

Aela

fn total(xs: &i64[]) -> i64 | Overflow {
    #let size = xs.len;
    var t: i64 = 0;
    var i: i64 = 0;
    #invariant 0 <= i && i <= size;
    #variant size - i;
    while (i < xs.len) {
        (t += xs[i])?;
        i += 1;
    }
    return t;
}
fn main() -> i32 | Overflow {
    let xs: i64[] = [1, 2, 3];
    println("\(total(&xs)?)");      // 6
    return 0;
}

The verifier is simpler than SPARK's. It uses one fixed method that always finishes quickly, so whether a program verifies never depends on guesswork. In return, a specification may only compare variables, array lengths and constants, joined with +, - and &&. Multiplication, || and function calls are not allowed in a specification. The compiler rejects them with E0802 instead of quietly ignoring them. With --verify, a recursive function also needs a #variant before it, to prove that the recursion ends.

Summary

Language	Types written?	How errors are reported	Checked side effects	Contracts
C	Yes	special values, `errno`	No	No
C++	Yes	exceptions, special values	No	No
Rust	Yes	`Result` and `?`	No	No
Ada	Yes	exceptions	No	Yes, with SPARK
Aela	Yes	failures in the signature, `?`	Yes, with `pure fn`	Yes, linear ones, with `--verify`

In this chapter we learned the following.

A function writes all its parameter types and its result type, and returns a value on every path.
There are no implicit conversions and no overloading. Parameters may have defaults, and the last one may collect extra arguments.
A value can be passed as itself, as a shared reference &x, or as an exclusive reference mut &x. The call site always shows which.
A function lists its failures after |. A caller handles them with ?, return or match, and the compiler makes sure it does.
pure fn is a checked promise that a function has no side effects.
Functions are values, and closures can use the variables around them.
#requires, #ensures, #invariant and #variant state facts that aec --verify proves before the program runs.

Chapter 6. Types, Structs, and Enums

Up to now, we have focused on control flow and functions. In this chapter, we learn how Aela represents data.

We go in small steps.

Basic types
Structs, which group named fields into one value
Methods, which are functions attached to a struct
Ownership and references, which decide who may use a value and when
Enums, which describe a value that can take one of several forms
Interfaces, which let different structs share a set of methods
Type aliases

Aela borrows ideas from C, C++, Rust and Ada, and tries to keep the rules few and consistent.

1. Basic Types

Aela has the usual primitive types.

type	values
`i8 i16 i32 i64`	signed integers
`u8 u16 u32 u64`	unsigned integers
`f32 f64`	floating point numbers
`bool`	`true` and `false`
`char`	one Unicode character, such as `'a'`
`string`	text, stored as UTF-8 bytes

Aela

fn main() -> i32 {
    let i: i32 = 10;
    let j: i64 = 10;
    let f: f32 = 1.5;
    let g: f64 = 1.5;
    let b: bool = true;
    let c: char = 'a';
    let s: string = "hello";
    let n = 42;                 // i64, from the value
    var count: i64;             // starts at 0
    println("\(i) \(j) \(f) \(g) \(b) \(c) \(s) \(n) \(count)");
    // 10 10 1.5 1.5 true a hello 42 0
    return 0;
}

Here are the main rules.

You may leave out the type of a local variable when its value shows the type. A whole number on its own is an i64, and a number with a decimal point is an f64.
A variable never holds garbage. A var declared without a value starts at its type's zero value. That is 0 for numbers, false for bool, and "" for a string.
There are no implicit conversions between types.

This program does not compile, because an i32 is not an i64.

Aela

fn main() -> i32 {
    let small: i32 = 7;
    let big: i64 = small;
    return 0;
}

The error is error[E0301]: expected i64, found i32. You convert with as.

Aela

fn main() -> i32 {
    let small: i32 = 7;
    let big: i64 = small as i64;
    let r = big * 1000;
    println("\(r)");            // 7000
    return 0;
}

Integer arithmetic is checked. If +, - or * overflows, the program stops with a trap instead of giving a wrong answer. Chapter 5 showed how (a + b)? turns this into a failure instead.

2. Structs

A struct groups several values, called fields, into one value. Each field has a name and a type.

In C, a struct is a plain block of memory. A local struct that you do not fill in holds whatever bytes were there before.

C

#include <stdio.h>
struct Point {
  int x;
  int y;
};
int main(void) {
  struct Point p;   /* p.x and p.y are not set yet */
  p.x = 1;
  printf("%d\n", p.x);
  return 0;
}

Rust makes you give every field a value when you create a struct.

Rust

struct Point {
    x: i64,
    y: i64,
}
fn main() {
    let p = Point { x: 1, y: 2 };
    println!("{} {}", p.x, p.y);
}

In Aela, a struct is declared with struct. Each field ends with a semicolon.

Aela

struct Point {
    x: i64;
    y: i64;
}
fn main() -> i32 {
    var p = Point { x: 1, y: 2 };
    p.x = 10;
    println("\(p.x) \(p.y)");   // 10 2
    println("\(p)");            // Point { x: 10, y: 2 }
    var origin: Point;
    println("\(origin)");       // Point { x: 0, y: 0 }
    return 0;
}

You create a struct value with Name { field: value, ... }. The name of the type is always written.
A literal must give every field a value, unless the field has a default (error E0389 otherwise). A variable declared without a value, such as var origin: Point;, starts as the zero value of its type, here the point (0, 0).
You read a field with p.x. To change a field, the variable must be a var.
Any struct can be printed with \( ). It prints its name and all its fields.

A field can also have a default value, which is used when the field is left out. A literal can copy the fields it does not name from another value of the same type, with ....

Aela

struct Settings {
    name: string;
    retries: i64 = 3;
    verbose: bool = false;
}
fn main() -> i32 {
    let s = Settings { name: "backup" };
    println("\(s)");    // Settings { name: "backup", retries: 3, verbose: false }
    let t = Settings { ...s, verbose: true };
    println("\(t)");    // Settings { name: "backup", retries: 3, verbose: true }
    return 0;
}

Aela has no inheritance. To build a bigger type from smaller ones, put one struct inside another as a field.

3. Methods

An impl block gives a struct its methods. A method is a function whose first parameter, the receiver, is the struct it is called on. By habit it is named self.

Aela

struct Point {
    x: i64;
    y: i64;
}
impl Point {
    fn length_squared(self: &Point) -> i64 {
        return self.x * self.x + self.y * self.y;
    }
    fn move_by(mut self: &Point, dx: i64, dy: i64) -> void {
        self.x += dx;
        self.y += dy;
    }
}
fn main() -> i32 {
    var p = Point { x: 3, y: 4 };
    println("\(p.length_squared())");   // 25
    p.move_by(1, 1);
    println("\(p)");                    // Point { x: 4, y: 5 }
    return 0;
}

The type of the receiver says how the method uses the value.

receiver	what the method gets
`self: &Point`	a shared reference, so it can only read
`mut self: &Point`	an exclusive reference, so it can change
`self: Point`	the value itself, which moves into the call

At the call you just write p.move_by(1, 1). The compiler takes the right kind of reference for you, and applies the same rules as for any other reference. For example, you cannot call move_by on a let.

A method call is resolved when the program is compiled, so it costs the same as a plain function call. Aela has no static methods such as Point::new(). Use a plain function to make a new value, or declare a variable without one (var p: Point;) to start at the zero value.

4. Ownership and References

This section explains how Aela keeps memory safe without a garbage collector.

One owner

A struct or an array has exactly one owner. Assigning it to another variable, or passing it to a parameter of type Point, moves it. After a move, the old name can no longer be used.

Aela

struct Point {
    x: i64;
    y: i64;
}
fn main() -> i32 {
    let p = Point { x: 1, y: 2 };
    let q = p;              // p moves into q
    println("\(p.x)");
    return 0;
}

This program does not compile. The compiler reports error[E0401]: use of moved value 'p'.

If you want two separate values, make a copy with std::copy. If a function only needs to look at a value, pass it a reference with &, and the caller keeps it.

Aela

struct Point {
    x: i64;
    y: i64;
}
fn show(p: &Point) -> void {
    println("(\(p.x), \(p.y))");
}
fn consume(p: Point) -> i64 {
    return p.x + p.y;
}
fn main() -> i32 {
    let p = Point { x: 1, y: 2 };
    let q = std::copy(p);       // a second, separate Point
    show(&p);                   // (1, 2)
    show(&p);                   // (1, 2): a borrow does not move p
    println("\(consume(q))");   // 3: q moves into the call
    return 0;
}

When the owner of a struct or array goes out of scope, the compiler frees the value. There is no garbage collector, and you never call free or delete. Structs and arrays do not have reference counts. Strings are different. A string never changes, so it can be shared, and it is freed when the last user lets go of it.

Numbers, bools and chars are always copied, so they never move.

Borrowing

A reference lets you use a value without owning it. This is called borrowing. Chapter 5 showed the two kinds.

&x is a shared reference. It can only read.
mut &x is an exclusive reference. It can change x.

A variable may have many shared references, or one exclusive reference, but never both at the same time. While a variable is borrowed, it also cannot be changed or moved through its own name.

Aela

struct Counter { count: i64; }
fn bump(mut c: &Counter) -> void {
    c.count += 1;
}
fn main() -> i32 {
    var ctr = Counter { count: 0 };
    let r = &ctr;               // a shared borrow that lives to the end of main
    bump(mut &ctr);
    println("\(r.count)");
    return 0;
}

This program does not compile. The compiler reports error[E0408]: cannot borrow mutably while it is borrowed: 'ctr'. The shared reference r is still in use, so ctr cannot be lent out to be changed.

Where a reference comes from

In C++, a reference into a vector can be left pointing at freed memory when the vector grows.

C++

#include <iostream>
#include <string>
#include <vector>
struct User {
  int id;
  std::string name;
};
int main() {
  std::vector<User> users = {{1, "ada"}};
  User& u = users[0];
  users.push_back({2, "bob"});   // may move every element to new memory
  std::cout << u.name << "\n";   // u may now refer to freed memory
}

Rust prevents this with lifetimes, which are names such as 'a that you sometimes write in signatures. Aela prevents it in a different way. Every reference names the variable it borrows from, which is called its root. When a function returns a reference, its result type names the parameter the reference comes from.

Aela

struct User { id: i64; name: string; }
fn first_user(users: &User[]) -> &users::&User {
    return &users[0];
}
fn main() -> i32 {
    let users: User[] = [User { id: 1, name: "ada" }, User { id: 2, name: "bob" }];
    let u = first_user(&users);     // u borrows from users
    println(u.name);                // ada
    return 0;
}

The type &users::&User means "a reference to a User, borrowed from the parameter users". So the caller knows that u borrows from its array. If the program tries to grow the array while u is alive, the compiler rejects it.

Aela

struct User { id: i64; name: string; }
fn first_user(users: &User[]) -> &users::&User {
    return &users[0];
}
fn main() -> i32 {
    var users: User[] = [User { id: 1, name: "ada" }];
    let u = first_user(&users);
    users.push(User { id: 2, name: "bob" });
    println(u.name);
    return 0;
}

The error is error[E0410]: cannot modify a value while it is borrowed: 'users'.

There is nothing to infer and no lifetime names to learn. The checker follows each reference back to its root in one pass over the code. A reference also cannot be stored in a global, and it cannot outlive the block of the variable it borrows from.

Aela also has arenas and regions, for programs that make many small linked objects. Inside a region, new creates an object. They are a more advanced topic and are not covered in this chapter.

5. Enums

An enum describes a value that is exactly one of several named forms, called variants.

Plain enums

An enum whose variants carry no data is a plain enum. It is stored as a small integer. Variants are numbered from 0 in the order they are written, and they can be compared in that order.

Aela

enum Color { Red, Green, Blue }
fn describe(c: Color) -> string {
    match (c) {
        Color::Red => { return "warm"; },
        Color::Green | Color::Blue => { return "cool"; }
    }
}
fn main() -> i32 {
    let c = Color::Blue;
    var d: Color;                   // the first variant, Red
    println("\(c) \(d) \(c as i64) \(c > d)");  // Blue Red 2 true
    println(describe(c));           // cool
    return 0;
}

An enum value prints as the name of its variant. The zero value of a plain enum is its first variant.

Enums with data

A variant may carry fields. Then the enum is a tagged union, also called a sum type. In C you would build this by hand, with a tag and a union, and nothing stops you from reading the wrong member.

C

#include <stdio.h>
enum ShapeKind { CIRCLE, RECT };
struct Shape {
  enum ShapeKind kind;
  union {
    double radius;
    struct { double width, height; } rect;
  } u;
};
int main(void) {
  struct Shape s = { .kind = RECT, .u.rect = { 2.0, 3.0 } };
  printf("%f\n", s.u.radius);   /* compiles, but reads the wrong member */
  return 0;
}

Rust has enums with data built in, and so does Aela. Ada has a similar idea, called a variant record.

Rust

enum Shape {
    Circle { radius: f64 },
    Rect { width: f64, height: f64 },
}
fn area(s: &Shape) -> f64 {
    match s {
        Shape::Circle { radius } => 3.14159 * radius * radius,
        Shape::Rect { width, height } => width * height,
    }
}
fn main() {
    println!("{}", area(&Shape::Rect { width: 2.0, height: 3.0 }));
}

In Aela, a variant's fields are written like a function's parameters, with a name and a type. A value is created like a struct, with the field names.

Aela

enum Shape {
    Circle(radius: f64),
    Rect(width: f64, height: f64),
    Empty,
}
fn area(s: &Shape) -> f64 {
    match (*s) {
        Shape::Circle { radius } => { return 3.14159 * radius * radius; },
        Shape::Rect { width, height } => { return width * height; },
        Shape::Empty => { return 0.0; }
    }
}
fn main() -> i32 {
    let shapes: Shape[] = [
        Shape::Circle { radius: 1.0 },
        Shape::Rect { width: 2.0, height: 3.0 },
        Shape::Empty,
    ];
    for (let s: &shapes::&Shape in &shapes) {
        println("\(*s) has area \(area(s))");
    }
    // Shape::Circle { radius: 1.0 } has area 3.14159
    // Shape::Rect { width: 2.0, height: 3.0 } has area 6.0
    // Shape::Empty has area 0.0
    return 0;
}

The only way to read a variant's fields is to match on the value. A pattern such as Shape::Rect { width, height } checks the variant and gives names to its fields. So you can never read the wrong field.
*s is the value that the reference s points to.
A match must handle every variant, or have a _ arm for the rest.

The last rule is very useful when a program grows. If you add a variant, every match that does not handle it stops compiling. Here the Empty arm is missing.

Aela

enum Shape {
    Circle(radius: f64),
    Rect(width: f64, height: f64),
    Empty,
}
fn area(s: &Shape) -> f64 {
    match (*s) {
        Shape::Circle { radius } => { return 3.14159 * radius * radius; },
        Shape::Rect { width, height } => { return width * height; }
    }
}
fn main() -> i32 { return 0; }

The compiler reports error[E0329]: match does not handle the variant (add an arm, or _ =>): 'Empty'.

When you only care about one variant, if (let ...) is shorter than a match. In a pattern, .. stands for the fields you do not name.

Aela

enum Shape {
    Circle(radius: f64),
    Rect(width: f64, height: f64),
    Empty,
}
fn main() -> i32 {
    let s = Shape::Rect { width: 2.0, height: 5.0 };
    if (let Shape::Rect { width, .. } = s) {
        println("a rectangle \(width) wide");   // a rectangle 2.0 wide
    }
    return 0;
}

A variant may hold values of its own enum, so a tree needs nothing special. Here is a small expression tree.

Aela

enum Expr {
    Num(value: i64),
    Add(left: Expr, right: Expr),
    Mul(left: Expr, right: Expr),
}
fn eval(e: &Expr) -> i64 {
    match (*e) {
        Expr::Num { value } => { return value; },
        Expr::Add { left, right } => { return eval(&left) + eval(&right); },
        Expr::Mul { left, right } => { return eval(&left) * eval(&right); }
    }
}
fn main() -> i32 {
    // 1 + 2 * 3
    let e = Expr::Add {
        left: Expr::Num { value: 1 },
        right: Expr::Mul { left: Expr::Num { value: 2 }, right: Expr::Num { value: 3 } },
    };
    println("\(eval(&e))");     // 7
    return 0;
}

An enum with data owns its fields, just like a struct. It moves, and it is freed with its fields. Enums cannot have methods yet, and there is no == on enums with data. Use match, if (let ...) or the builtin equal to compare them.

6. Interfaces

An interface names a set of methods. A struct that has those methods can say that it implements the interface, with impl Type as Interface. This is close to a trait in Rust.

Aela

interface Shape {
    fn area(self: &Self) -> f64;
    fn name(self: &Self) -> string;
}
struct Circle { radius: f64; }
struct Square { side: f64; }
impl Circle as Shape {
    fn area(self: &Circle) -> f64 { return 3.14159 * self.radius * self.radius; }
    fn name(self: &Circle) -> string { return "circle"; }
}
impl Square as Shape {
    fn area(self: &Square) -> f64 { return self.side * self.side; }
    fn name(self: &Square) -> string { return "square"; }
}
fn main() -> i32 {
    let shapes: Shape[] = [Circle { radius: 1.0 }, Square { side: 2.0 }];
    for (let s: &shapes::&Shape in &shapes) {
        println("\(s.name()): \(s.area())");
    }
    // circle: 3.14159
    // square: 4.0
    return 0;
}

Inside an interface, Self stands for the struct that implements it.
A Circle can be stored where a Shape is expected. The value keeps a small tag that says which struct it really is.
A method call on a Shape checks the tag and calls the right struct's method directly. There are no vtables.
An interface method cannot list failures.

If a struct leaves out one of the methods, the impl is rejected. For example, an impl Square as Shape with only area gives error[E0365]: Square does not implement Shape: no method name.

An interface can also limit a type parameter of a generic function. Here T: Shape means "any type that implements Shape". Each call is then compiled for the real type, so the method calls need no tag check at all.

Aela

interface Shape {
    fn area(self: &Self) -> f64;
}
struct Square { side: f64; }
impl Square as Shape {
    fn area(self: &Square) -> f64 { return self.side * self.side; }
}
fn largest(T: Shape; xs: &T[]) -> f64 {
    var best: f64 = 0.0;
    for (let x: &xs::&T in xs) {
        if (x.area() > best) { best = x.area(); }
    }
    return best;
}
fn main() -> i32 {
    let squares: Square[] = [Square { side: 2.0 }, Square { side: 3.0 }];
    println("\(largest(&squares))");    // 9.0
    return 0;
}

Only structs can implement an interface for now.

7. Type Aliases

A type alias gives a second name to a type. It does not create a new type, so the alias and the original mix freely.

Aela

type Meters = f64;
type Names = string[];
fn total_length(parts: &Meters[]) -> Meters {
    var t: Meters = 0.0;
    for (let p: f64 in parts) { t += p; }
    return t;
}
fn main() -> i32 {
    let parts: f64[] = [1.5, 2.0, 0.5];
    let team: Names = ["ada", "bob"];
    println("\(total_length(&parts)) \(team.len)");    // 4.0 2
    return 0;
}

Aliases make long types easier to read. They are most useful for function types, such as type Handler = fn(i64) -> void;. A type alias can also add bounds to a number. This is called a refinement type, and it is covered in Chapter 10.

8. Putting It Together

This small to-do list uses most of the chapter. It has a struct with methods, an enum with data, a failure, and both kinds of reference.

Aela

enum Status {
    Open,
    Done(note: string),
}
struct Task {
    title: string;
    status: Status;
}
struct TodoList {
    tasks: Task[];
}
failure NoSuchTask { index: i64; }
impl TodoList {
    fn add(mut self: &TodoList, title: string) -> void {
        self.tasks.push(Task { title, status: Status::Open });
    }
    fn finish(mut self: &TodoList, i: i64, note: string) -> void | NoSuchTask {
        if (i < 0 || i >= self.tasks.len) { fail NoSuchTask { index: i }; }
        self.tasks[i].status = Status::Done { note };
    }
    fn open_count(self: &TodoList) -> i64 {
        var n: i64 = 0;
        for (let t: &self::&Task in &self.tasks) {
            match (t.status) {
                Status::Open => { n += 1; },
                Status::Done { .. } => {}
            }
        }
        return n;
    }
}
fn main() -> i32 | NoSuchTask {
    var list = TodoList { tasks: [] };
    list.add("write chapter");
    list.add("test examples");
    list.finish(1, "all pass")?;
    match (list.finish(7, "oops")) {
        _ => {},
        e: NoSuchTask => { println("no task \(e.index)"); }    // no task 7
    }
    println("\(list.open_count()) open");                      // 1 open
    println("\(list.tasks[1])");
    // Task { title: "test examples", status: Status::Done { note: "all pass" } }
    return 0;
}

Task { title, status: Status::Open } is short for Task { title: title, status: Status::Open }.
add and finish change the list, so their receiver is mut self: &TodoList. open_count only reads it.
finish returns nothing, but it can fail. Its result type is void | NoSuchTask.
The for loop takes a shared reference to each task, so nothing is copied.
list is freed when main ends, together with every task and string inside it.

Summary

Feature	C	C++	Rust	Aela
Fields always set	No	No	Yes	Yes, to given values or defaults
Methods	No	Yes	Yes, in `impl`	Yes, in `impl`
Inheritance	No	Yes	No	No
Enums with data	By hand	`std::variant`	Yes	Yes
Every case handled	No	No	Yes	Yes
Freeing memory	`free`	destructors	ownership	ownership
Safe references	No	No	Yes, with lifetimes	Yes, each reference names its root

In this chapter we learned the following.

The basic types, and that there are no implicit conversions between them.
Structs, which group named fields. Every field starts with a value.
Methods in impl blocks, where the receiver says whether the method reads or changes the value.
A struct or array has one owner. It moves on assignment, std::copy makes a separate copy, and it is freed when its owner goes out of scope.
Shared references & and exclusive references mut &, and the rule that you cannot have both at once.
Every reference names the variable it borrows from, so there are no lifetime annotations.
Plain enums, enums with data, and match, which must handle every variant.
Interfaces, which let different structs be used through the same methods.
Type aliases, which give a type a second name.

Chapter 7. Modules, Imports, and Exports

Most real programs are split into many files. Each language has its own way to let one file use the code in another:

C and C++: a file includes a header, and the header's names become visible. A header can include other headers, so a single line can bring in many names you never asked for.
Rust: items are private by default and pub makes them public. use brings names into scope, and a prelude brings in some names without any use at all. pub use can re-export a name from somewhere else.
Ada: packages have a clear public part. with makes a package available, and use makes its names visible without the package prefix.

Aela's module system follows a few simple rules:

Every file is a module.
Everything in a file is private unless it is marked export.
A name from another file can only be used if you import it.
There is no way to import every name of a module at once.
Re-exporting a name is something you write on purpose.

Let's start with a small program.

1. The Most Basic Import

You do not need an import to print. println is a builtin, and builtins are visible in every file:

Aela

fn main() -> i32 {
    println("Hello, Aela!");
    return 0;
}

The standard library is different. Its modules must be imported. Here we import the string module, std/string, and give it the local name str:

Aela

import str from "std/string";
fn main() -> i32 {
    println(str::to_upper("hello, aela"));     // HELLO, AELA
    return 0;
}

Here is what this shows:

"std/string" is the path of the module.
str is the name we chose for the module in this file.
We call its functions with the prefix str::, as in str::to_upper.
Nothing else from std/string comes into this file. The name to_upper alone means nothing here.

This is the basic rule of the chapter. A name from another module is only visible if you import it.

2. Exporting from Modules

A module decides which of its names other files may use. It does this with the word export.

Here is a small module in a file named math.ae:

math.ae

export fn add(a: i32, b: i32) -> i32 {
    return a + b;
}
fn double(a: i32) -> i32 {
    return a * 2;
}

add is exported, so other files may import it. double is not exported, so only code inside math.ae can call it.

export can go in front of a function, a struct, an enum, a failure, an interface, a type alias, a C function (extern fn) or a global variable.

If another file tries to import double, the program does not compile. This example is meant to fail:

Aela

import { double } from "math.ae";
fn main() -> i32 {
    println("\(double(4))");
    return 0;
}

The compiler says:

text

error[E0205]: 'double' is not exported by math.ae (write export before its declaration there)

Other languages make different choices:

C makes every function in a file visible to the linker unless you mark it static.
C++ works the same way, and namespaces only group names. They do not hide them.
Rust makes items private to their module by default, and pub makes them public. In this way it is close to Aela.
Aela makes a name visible to other files only when it is marked export.

3. Importing Specific Names

You can import just the names you need. Put them in braces:

Aela

import { add } from "math.ae";
fn main() -> i32 {
    println("\(add(2, 3))");     // 5
    return 0;
}

Now add can be used without a prefix. The import line at the top of the file tells the reader exactly where add comes from.

You can also give an imported name a different local name. Write the original name, a colon, and the new name:

Aela

import { add: plus } from "math.ae";
fn main() -> i32 {
    println("\(plus(2, 3))");     // 5
    return 0;
}

This is useful when two modules export the same name, as we will see in section 7.

The path is relative to the file that has the import. You may leave out the .ae at the end, so "math" also finds math.ae. A file is loaded only once, however many files import it.

4. Module Namespace Imports

Instead of importing single names, you can import the whole module under one name:

Aela

import math from "math.ae";
fn main() -> i32 {
    println("\(math::add(2, 3))");     // 5
    return 0;
}

Here math is the name of the module in this file, and every export of math.ae is reached as math::name.

This is often the clearest choice when you use many names from one module. Each use shows where the name comes from.

The module::name form works everywhere a name can appear: in calls such as math::add(1, 2), in types such as geo::Point, in struct literals such as geo::Point { x: 0, y: 0 }, and in enum variants such as geo::Color::Red.

Importing a module this way does not make its names visible without the prefix. This example is meant to fail:

Aela

import math from "math.ae";
fn main() -> i32 {
    println("\(add(2, 3))");
    return 0;
}

The compiler even tells you how to fix it:

text

error[E0207]: 'add' is declared in math.ae: import it: import { add } from "math.ae";

5. Re-Exporting: The Facade Module

Sometimes a library is spread over many files, but you want users to import it from one place. This is called a facade module. In Aela you build one by importing names and then exporting them again.

Here is the layout:

Shell

math/
  index.ae
  src/
    add.ae
    mul.ae
    sub.ae
main.ae

Each file in src holds one function:

math/src/add.ae

1export fn add(a: i64, b: i64) -> i64 { return a + b; }

math/src/mul.ae

1export fn mul(a: i64, b: i64) -> i64 { return a * b; }

math/src/sub.ae

1export fn sub(a: i64, b: i64) -> i64 { return a - b; }

The file index.ae is the public face of the library. It imports each function and exports it again with export name;:

math/index.ae

import { add } from "src/add.ae";
import { mul } from "src/mul.ae";
import { sub } from "src/sub.ae";
export add;
export mul;
export sub;

The paths in index.ae are relative to index.ae itself, so "src/add.ae" means math/src/add.ae.

Now a program can use the library through index.ae in either style:

main.ae

import math from "math/index.ae";
import { add, sub } from "math/index.ae";
fn main() -> i32 {
    println("\(math::mul(3, 4)) \(add(1, 2)) \(sub(9, 4))");     // 12 3 5
    return 0;
}

This pattern has some good points:

Every name that the library makes public is listed in one file.
A helper inside src stays private unless index.ae exports it.
You can move code between the files in src without changing the programs that use the library.

In C and C++, a header that includes other headers also passes on their names, but this happens silently. In Rust, pub use does the same job as Aela's export name;.

6. No Glob Imports

Some languages let you bring every name of a module into scope with one line:

use std::io::*; in Rust
using namespace std; in C++
import * as X from "..." in JavaScript, which puts everything under one name

Aela has no import of this kind. The module form, import math from "math.ae", keeps every name behind the math:: prefix, so it is not a glob import. If you try to write one, the parser rejects it. This example is meant to fail:

Aela

import * from "math.ae";
fn main() -> i32 {
    return 0;
}

text

1error[E0101]: expected 'identifier'

This rule has a simple benefit. For any name in a file, you can find where it comes from. It is declared in the file, or it is listed in an import line at the top, or it has a module prefix such as math::, or it is a builtin.

7. Importing Types, Constants, and More

Structs, enums, global variables and functions are all exported and imported the same way. Here is a module with a constant, a struct and a function:

geometry.ae

export let PI: f64 = 3.14159;
export struct Circle {
    r: f64;
}
export fn area(c: &Circle) -> f64 {
    return PI * c.r * c.r;
}

You can import the names you need:

main.ae

import { PI, Circle, area } from "geometry.ae";
fn main() -> i32 {
    let c = Circle { r: 1.0 };
    println("\(PI) \(area(&c))");     // 3.14159 3.14159
    return 0;
}

Or you can import the module and use the prefix:

main2.ae

import geometry from "geometry.ae";
fn main() -> i32 {
    let c = geometry::Circle { r: 1.0 };
    println("\(geometry::PI) \(geometry::area(&c))");     // 3.14159 3.14159
    return 0;
}

A global needs a written type, as in let PI: f64 = .... A let global cannot be changed. A var global can be.

Two modules with the same name

Suppose two modules both export a struct named Point:

geo.ae

1export struct Point { x: i64; y: i64; }

grid.ae

1export struct Point { row: i64; col: i64; }

You cannot import both under the name Point. This example is meant to fail:

bad.ae

import { Point } from "geo.ae";
import { Point } from "grid.ae";
fn main() -> i32 {
    return 0;
}

text

error[E0202]: duplicate definition of 'Point': two imports of this file give the name to different declarations

The fix is to give one of them a new local name:

main.ae

import { Point } from "geo.ae";
import { Point: Cell } from "grid.ae";
fn main() -> i32 {
    let p = Point { x: 1, y: 2 };
    let c = Cell { row: 3, col: 4 };
    println("\(p)");     // geo::Point { x: 1, y: 2 }
    println("\(c)");     // grid::Point { row: 3, col: 4 }
    return 0;
}

When two files declare the same name, Aela prints each one with its module name in front, as you can see in the output. That way you can always tell them apart.

Fields and methods across packages

Inside your own program, every file can use all the fields and methods of your structs. Rules for fields and methods matter when you write a package that other people use. Then a field or method needs export too, or the other package cannot use it. The MODULES page in the Aela docs explains this in detail.

8. Side-by-Side Comparison Table

Feature	C	C++	Rust	Ada	Aela
How names enter scope	`#include`	`#include`, `using`	`use`, and the prelude	`with` and `use`	`import`
Private by default?	No (use `static`)	No (use `static` or an unnamed namespace)	Yes (`pub` exports)	Yes (only the package spec is public)	Yes (`export` exports)
Can re-export?	A header can include another	A header can include another	`pub use`	Yes, with renaming	`export name;`
Glob imports?	Yes, `#include` brings in everything	`using namespace`	`use x::*`	`use`	No
Names visible without an import	Whatever the headers bring	Whatever the headers bring	The prelude	The package `Standard`	Only the builtins

Aela is closest to Ada in spirit. Both make the public part of a module clear, and both make you name what you use.

9. A Complete Example

Here is a small program built from three files:

Shell

shapes/
  circle.ae
  index.ae
main.ae

The file circle.ae holds the real code:

shapes/circle.ae

export let PI: f64 = 3.14159;
export struct Circle {
    r: f64;
}
export fn area(c: &Circle) -> f64 {
    return PI * c.r * c.r;
}

The file index.ae is the facade. It decides what the shapes library makes public:

shapes/index.ae

import { PI, Circle, area } from "circle.ae";
export PI;
export Circle;
export area;

The program imports the library as one module:

main.ae

import shapes from "shapes/index.ae";
fn main() -> i32 {
    let c = shapes::Circle { r: 2.0 };
    println("pi = \(shapes::PI)");               // pi = 3.14159
    println("area = \(shapes::area(&c))");       // area = 12.56636
    return 0;
}

To build and run it, give the compiler the program's main file. It finds the other files through the imports:

Shell

1aec main.ae -o shapes_demo && ./shapes_demo

Every name in main.ae is easy to trace. shapes comes from the import line, and everything else has the shapes:: prefix or is a builtin like println.

Chapter 7 Summary

In this chapter we learned that:

every file is a module, and its names are private unless marked export
import { a, b } from "file.ae"; brings in single names, and { a: x } renames one
import m from "file.ae"; brings in a module, and its names are used as m::name
standard library modules are imported the same way, for example import str from "std/string";
export name; re-exports an imported name, which lets you build a facade module
there are no glob imports, and only the builtins are visible without an import
the compiler explains what is wrong when a name is missing, private or imported twice

These rules make it easy to see where every name comes from, even in a large program.

Chapter 8. Vectors, Maps and Strings

So far you have learned how Aela represents values, how functions work, and how code is organized into modules. Now we turn to a practical topic. How do you store and work with collections of data in Aela?

This chapter has four parts:

Arrays. Aela's built-in arrays can grow and shrink, so they do the job of a vector.
Library containers. The module std/containers adds Vec, Map, Set and OrderedMap.
Strings. Text is a built-in type, and the module std/string has the functions to work with it.
Using them together. A short program that counts words.

1. Arrays

You have already seen an Aela array. The main function can receive the program's command-line arguments as an array of strings:

Aela

fn main(args: string[]) -> i32 {
    // ...
    return 0;
}

string[] is an array of strings. In general, the type T[] is an array of values of type T:

the values are stored one after another in memory
you read and write an element with xs[i], counting from 0
the field xs.len gives the number of elements
an index outside the array stops the program with a trap

Unlike a C array, an Aela array knows its own length, and it can grow. In other languages you would reach for a library type to get this:

C++

std::vector<int> v;
v.push_back(10);

Rust

let mut v: Vec<i32> = Vec::new();
v.push(10);

In Aela the built-in array already does this, as section 1.3 shows.

1.1 Printing command-line arguments

Aela

fn main(args: string[]) -> i32 {
    let n = args.len;
    var i = 0;
    while (i < n) {
        println("args[\(i)] = \(args[i])");
        i += 1;
    }
    return 0;
}

If you build this program as ./args and run ./args one two, it prints:

text

args[0] = ./args
args[1] = one
args[2] = two

The first element, args[0], is the name the program was started with.

A for loop is shorter. If you write two variables, the first one is the index and the second one is the element:

Aela

fn main(args: string[]) -> i32 {
    for (let i: i64, let a: string in &args) {
        println("args[\(i)] = \(a)");
    }
    return 0;
}

The & in &args means the loop only reads the array. The array is still there after the loop.

1.2 Arrays of numbers

Here is a function that adds up an array of numbers:

Aela

fn sum(nums: &i32[]) -> i32 {
    var total: i32 = 0;
    for (let n: i32 in nums) {
        total += n;
    }
    return total;
}
fn main() -> i32 {
    let xs: i32[] = [3, 4, 5];
    println("\(sum(&xs))");     // 12
    return 0;
}

The parameter type &i32[] means that sum borrows the array. It can read the array, but it does not take it away from the caller. The call writes &xs to match.

1.3 Growing and shrinking

Three builtin methods change the length of an array, and one field reads it:

xs.push(v) adds v at the end
xs.pop() removes the last element and gives it back
xs.clear() removes every element
xs.len tells you how many elements there are

Aela

fn main() -> i32 {
    var xs: i64[] = [];
    xs.push(10);
    xs.push(20);
    xs.push(30);
    println("\(xs) \(xs.len)");      // [10, 20, 30] 3
    let last = xs.pop();
    println("\(last) \(xs)");        // 30 [10, 20]
    xs[0] = 5;
    println("\(xs[0]) \(xs.len)");   // 5 2
    xs.clear();
    println("\(xs)");                // []
    return 0;
}

A few things to notice:

An empty array literal needs a type, so we wrote var xs: i64[] = [];.
To change an array, it must be a var.
xs.pop() on an empty array stops the program with a trap. xs.pop()? gives the failure Empty instead.
An array prints with \(xs), just like a number does.

1.4 An array has one owner

An array belongs to one variable at a time. let ys = xs; does not copy the array. It moves it, and after that xs can no longer be used. This example is meant to fail:

Aela

fn main() -> i32 {
    var xs: i64[] = [1, 2, 3];
    let ys = xs;
    println("\(xs.len)");
    return 0;
}

text

1error[E0401]: use of moved value 'xs'

When you really want a second array, ask for a copy with std::copy:

Aela

fn main() -> i32 {
    var xs: i64[] = [1, 2, 3];
    var ys = std::copy(xs);
    ys.push(4);
    println("\(xs) \(ys)");     // [1, 2, 3] [1, 2, 3, 4]
    return 0;
}

There is also a fixed-length array, written T[N], such as u8[4]. It always has exactly N elements, so push and pop do not work on it.

2. Library Containers

The module std/containers has four types. You import the ones you need:

Aela

import { Vec, Map, Set, OrderedMap } from "std/containers";
fn main() -> i32 {
    return 0;
}

Vec(T) is an array with methods.
Map(K, V) is a hash map. It stores values of type V under keys of type K, and the entries have no order.
Set(T) is a set of values, with no order.
OrderedMap(K, V) is a map that remembers the order in which keys were added.

All four are used through methods, such as m.put(k, v) and v.push(x). An empty one is made with an empty struct literal, such as Map {}.

2.1 `Vec(T)`

A built-in array is enough for most programs. Vec(T) wraps an array and adds useful methods. Its field items is the array itself, so you can still index it and loop over it.

Aela

import { Vec } from "std/containers";
fn main() -> i32 {
    var v: Vec(string) = Vec {};
    v.push("xyz");
    v.push("abc");
    v.push("def");
    println("\(v.len())");                      // 3
    println("\(v.get(0) ?? "?")");              // xyz
    println("\(v.get(100) == none)");           // true
    if (let x = v.last()) { println(x); }       // def
    v.insert(0, "first");
    println("\(v.items)");                      // ["first", "xyz", "abc", "def"]
    println("\(v.contains("abc")) \(v.index_of("abc"))");     // true 2
    let gone = v.remove(1);
    println("\(gone) \(v.items)");              // xyz ["first", "abc", "def"]
    if (let x = v.pop()) { println(x); }        // def
    v.reverse();
    for (let s: string in &v.items) { print("\(s) "); }
    println("");                                // abc first
    return 0;
}

Some of these methods give back an optional value, of type T?. This means the result is either a value or none:

v.get(i) gives element i, or none if i is past the end
v.first() and v.last() give the first or last element, or none if the Vec is empty
v.pop() removes and gives back the last element, or none if the Vec is empty

There are two common ways to use an optional. a ?? b gives the value of a, or b if a is none. if (let x = o) { ... } runs the block only when o has a value, and inside the block x is that value.

Other methods include insert, remove, swap, truncate, extend, clear and is_empty. Run aec doc std/containers to see them all.

2.2 `Map(K, V)`

A map stores values under keys. Here is a map from strings to strings:

Aela

import { Map } from "std/containers";
fn main() -> i32 {
    var colors: Map(string, string) = Map {};
    colors.put("sky", "blue");
    colors.put("grass", "green");
    colors.put("sky", "gray");                  // replaces "blue"
    println("\(colors.len())");                 // 2
    println(colors.get("sky") ?? "unknown");    // gray
    println(colors.get("sun") ?? "unknown");    // unknown
    println("\(colors.has("grass"))");          // true
    if (let c = colors.get("grass")) {
        println("grass is \(c)");               // grass is green
    }
    colors.remove("grass");
    println("\(colors.has("grass"))");          // false
    return 0;
}

These are the main methods:

m.put(key, value) stores value under key. If the key was already there, the old value is replaced.
m.get(key) gives a copy of the value, or none if the key is not in the map.
m.has(key) tells you whether the key is in the map.
m.remove(key) takes the key and its value out of the map.
m.len() gives the number of entries.

A key can be almost any value: a number, a string, an enum, or even a struct or an array. Aela compares keys by their contents.

A Map has no m[key] syntax. You always use the methods. This example is meant to fail:

Aela

import { Map } from "std/containers";
fn main() -> i32 {
    var m: Map(string, string) = Map {};
    m["k"] = "v";
    return 0;
}

text

1error[E0349]: value cannot be indexed

2.3 Looping over a map

A Map keeps its entries in slots. To visit every entry, you loop over the slot numbers from 0 to m.cap(). You skip the empty slots with m.full(s), and you read an entry with m.entry(s). Each entry has a key and a val:

Aela

import { Map } from "std/containers";
fn main() -> i32 {
    var ages: Map(string, i64) = Map {};
    ages.put("ada", 36);
    ages.put("alan", 41);
    for (let s: i64 in 0..ages.cap()) {
        if (ages.full(s)) {
            let e = ages.entry(s);
            println("\(e.key) = \(e.val)");
        }
    }
    return 0;
}

A Map has no order, so the entries may come out in any order.

2.4 `OrderedMap(K, V)`

When the order matters, use an OrderedMap. It keeps its keys in the order they were added. m.keys() gives the keys as an array, and m.vals() gives the values in the same order:

Aela

import { OrderedMap } from "std/containers";
fn main() -> i32 {
    var stock: OrderedMap(string, i64) = OrderedMap {};
    stock.put("pears", 4);
    stock.put("apples", 7);
    stock.put("plums", 2);
    for (let i: i64, let k: string in stock.keys()) {
        println("\(k): \(stock.vals()[i])");
    }
    // pears: 4
    // apples: 7
    // plums: 2
    return 0;
}

It also has put, get, has, remove and len, just like Map. A Map is a little faster, so use it when you do not need the order.

2.5 `Set(T)`

A set holds each value at most once. s.add(x) gives true if x was new, and false if it was already there:

Aela

import { Set } from "std/containers";
fn main() -> i32 {
    var seen: Set(string) = Set {};
    println("\(seen.add("ada"))");      // true
    println("\(seen.add("ada"))");      // false
    println("\(seen.has("ada")) \(seen.len())");     // true 1
    return 0;
}

3. Strings

string is a built-in type. You do not need an import to make strings, join them with interpolation, or print them. For searching, splitting and trimming, you import std/string.

3.1 String basics

Aela

import str from "std/string";
fn main() -> i32 {
    let greeting: string = "héllo";
    println("\(greeting.len)");                   // 6
    println("\(greeting[0])");                    // 104
    println(greeting[0..1]);                      // h
    println(greeting[3..]);                       // llo
    println("\(str::eq(greeting, "héllo"))");     // true
    return 0;
}

Here is what this shows:

A string is a sequence of bytes in UTF-8.
s.len counts bytes, not characters. The letter é takes two bytes, so "héllo" has a length of 6.
s[i] is the byte at position i, as a u8. The letter h is byte 104.
s[a..b] is the part of the string from byte a up to, but not including, byte b. s[a..] goes to the end. This does not copy the bytes.
str::eq(a, b) tells you whether two strings are equal.

Strings cannot be changed. Every function that seems to change a string really makes a new one.

Two operators that you may expect do not work on strings. There is no ==, so you use str::eq to compare and str::cmp to put strings in order. There is no +, so you join strings with interpolation. This example is meant to fail:

Aela

fn main() -> i32 {
    let a = "x";
    let s = a + "y";
    return 0;
}

text

error[E0309]: strings have no + operator: use interpolation, for example "\(a)\(b)"

3.2 String interpolation

Inside a string in double quotes, \(expr) puts in the value of any expression:

Aela

fn main() -> i32 {
    let name = "Aela";
    let version = 2.1;
    println("Welcome to \(name) v\(version)!");     // Welcome to Aela v2.1!
    let a = 3;
    let b = 4;
    println("\(a) + \(b) = \(a + b)");              // 3 + 4 = 7
    let xs: i64[] = [1, 2, 3];
    println("xs = \(xs), length \(xs.len)");        // xs = [1, 2, 3], length 3
    let file = "config.ae";
    let message = "Error:
  Could not open file: \(file)";
    println(message);
    // Error:
    //   Could not open file: config.ae
    return 0;
}

The expression inside \( ) is checked by the compiler like any other code. Any value can be put into a string this way: numbers, strings, arrays, structs, optionals and enums.

The last example shows that a string in double quotes may span several lines. The line breaks are kept.

3.3 Raw strings

A string in backticks is a raw string. It keeps every character exactly as written, including backslashes and line breaks. This makes it handy for help text and Windows paths:

Aela

fn main() -> i32 {
    let usage = `Usage:
  foo [flags] [file]
Options:
  -h   Help
  -i   Interactive mode`;
    println(usage);
    let path = `C:\temp\new`;
    println(path);                    // C:\temp\new
    return 0;
}

Because a raw string keeps every character, interpolation does not work inside it:

Aela

fn main() -> i32 {
    let name = "Aela";
    println(`Hello, \(name)`);      // Hello, \(name)
    return 0;
}

When you need both line breaks and interpolation, use a string in double quotes, as in section 3.2.

3.4 The `std/string` module

The module std/string has the functions for working with text. It is usually imported under the name str:

Aela

import str from "std/string";
fn main() -> i32 {
    let s = "  Hello, World  ";
    let t = str::trim(s);
    println("[\(t)]");                              // [Hello, World]
    println("[\(str::trim_start(s))]");             // [Hello, World  ]
    println("[\(str::trim_end(s))]");               // [  Hello, World]
    println(str::to_upper(t));                      // HELLO, WORLD
    println(str::to_lower(t));                      // hello, world
    println(str::slice(t, 0, 5));                   // Hello
    println(str::replace(t, "World", "Aela"));      // Hello, Aela
    println("\(str::contains(t, "World"))");        // true
    println("\(str::starts_with(t, "Hell"))");      // true
    if (let at = str::find(t, ",")) {
        println("comma at \(at)");                  // comma at 5
    }
    let parts: string[] = str::split("a,b,c", ",");
    println("\(parts)");                            // ["a", "b", "c"]
    println(str::join(&parts, " + "));              // a + b + c
    println("\(str::char_count("héllo"))");         // 5
    return 0;
}

A few notes:

str::find gives the byte position of the first match, or none if there is no match. That is why we use if (let at = ...).
str::slice(s, start, end) takes an end position. str::substr(s, start, n) takes a length instead.
str::char_count counts characters, not bytes, so "héllo" has 5.
Other useful functions are str::lines, str::fields (which splits on white space), str::ends_with, str::repeat, str::pad_start and str::chars. Run aec doc std/string to see them all.

To turn text into a number, use str::parse_int. It fails if the text is not a whole number, so you handle the failure with match:

Aela

import str from "std/string";
fn main() -> i32 {
    let n: i64 = match (str::parse_int("123")) { v => v, e: str::BadInt => -1 };
    let m: i64 = match (str::parse_int("12ab")) { v => v, e: str::BadInt => -1 };
    println("\(n) \(m)");       // 123 -1
    return 0;
}

The page FAILURES.md in the Aela docs explains failures in detail.

3.5 Building a string piece by piece

When you build a long string out of many small pieces, use str::Builder. You add the pieces one at a time, and at the end to_string() gives you the whole string. This is faster than making a new string for every piece:

Aela

import str from "std/string";
fn main() -> i32 {
    var b = str::Builder {};
    b.add("hello");
    b.add(" ");
    b.add("world");
    b.add_char('!');
    b.add_int(42);
    println(b.to_string());     // hello world!42
    println("\(b.len())");      // 14
    return 0;
}

add adds a string, add_char adds one character, and add_int adds a number. len() gives the number of bytes so far.

4. Using Them Together

Let's count the words in a piece of text. We split the text into words with str::fields, count each word in an OrderedMap, and build the result with a Builder. We use an OrderedMap so that the words come out in the order they first appear.

Aela

import str from "std/string";
import { OrderedMap } from "std/containers";
fn count_words(text: string) -> OrderedMap(string, i64) {
    var counts: OrderedMap(string, i64) = OrderedMap {};
    let words: string[] = str::fields(str::to_lower(text));
    for (let w: string in &words) {
        counts.put(w, (counts.get(w) ?? 0) + 1);
    }
    return counts;
}
fn main() -> i32 {
    let counts = count_words("The cat and the dog and THE bird");
    var b = str::Builder {};
    for (let i: i64, let w: string in counts.keys()) {
        if (i > 0) { b.add(", "); }
        b.add(w);
        b.add("=");
        b.add_int(counts.vals()[i]);
    }
    println(b.to_string());     // the=3, cat=1, and=2, dog=1, bird=1
    return 0;
}

The line counts.put(w, (counts.get(w) ?? 0) + 1); does the counting. counts.get(w) gives the count so far, or none for a new word. ?? 0 turns none into 0. Then we add 1 and store the new count.

This small program uses every part of the chapter:

an array of strings, string[], from str::fields
a for loop with an index
a map from words to counts
optional values with ??
a Builder to make the output

Chapter 8 Summary

In this chapter we learned:

Arrays (`T[]`)

T[] is a built-in array that can grow
xs[i] reads or writes an element, and an index out of range is a trap
push, pop and clear are builtin methods of an array, and len is a field
an array has one owner, and std::copy makes a second array

Library containers (`std/containers`)

Vec(T) is an array with methods
Map(K, V) is a hash map with put, get, has and remove
OrderedMap(K, V) is a map that keeps the order of its keys
Set(T) holds each value at most once
methods that may find nothing give back an optional, such as V?

Strings

string is built in, made of UTF-8 bytes, and cannot be changed
"\(expr)" puts a value into a string, and backticks make a raw string
strings are compared with str::eq and joined with interpolation, not with == and +
std/string has the functions for trimming, splitting, searching and more
str::Builder builds a long string piece by piece

These tools are the backbone of practical Aela programs. You use them to read input, store and transform data, and prepare text for output.

Chapter 9. Packages

By now you have written Aela programs that span several files and modules. You have organized code into modules, used containers from the standard library, and learned how imports and exports work.

This is where you will want to start thinking about packages. A package is how a small program grows into a larger piece of software. You will want packages when:

you want to break features into separate parts,
you want to reuse code in more than one program,
you want a build that does the same thing every time,
you want your code to have a clear boundary, so that others can use it without reaching into its details.

1. What Is a Package?

A package is a directory with a file named index.json in it. This file is the package's manifest. It says:

the package's name and version,
which file is the program's entry point (the file with main),
which other packages it depends on,
and, if needed, which C sources to compile and which limits the program must stay within.

A typical layout looks like this:

text

myapp/
  index.json
  src/
    main.ae
    lexer.ae
    parser.ae

The compiler builds a package with aec build. The program goes into a build directory inside the package.

If modules are the chapters, a package is the book.

2. Your First Package

Make a directory named hello with two files in it. The manifest is small:

index.json

{
  "name": "hello",
  "version": "0.1.0",
  "entry": "src/main.ae"
}

The entry file is an ordinary Aela program:

src/main.ae

fn main() -> i32 {
    println("hello from a package");
    return 0;
}

Now build and run it from inside the hello directory:

Shell

aec build
./build/hello

The program prints hello from a package.

Here is what the manifest's keys mean:

name is the only key you must give. It starts with a letter, followed by letters, digits, - and _.
version has the form major.minor.patch, such as 0.1.0.
entry is the file with main. If you leave it out, it is src/main.ae.
output is where the program goes. If you leave it out, it is build/<name>.

aec build takes the package's directory as an argument, so aec build hello works from the directory above it. It also takes the compiler's usual options, such as --release and --verify.

The manifest is JSON, but it may also have comments (// and /* */) and trailing commas. If a value has the wrong shape, the error message names the exact place in the file.

3. How Other Languages Do It

C has no package system. You share code by writing a header file, and the build tool (a Makefile or a shell command) has to know which files to compile:

geometry.h

#ifndef GEOMETRY_H
#define GEOMETRY_H
struct vector2 { long x, y; };
long dot(const struct vector2 *a, const struct vector2 *b);
#endif

Shell

1cc -o app main.c geometry.c

Nothing in the C code says where geometry.c lives or which version of it you need. That knowledge sits in the build files, and it is easy to get wrong.

Rust has Cargo. Each package has a Cargo.toml file, and dependencies usually name a version range:

toml

[package]
name = "app"
version = "0.1.0"
[dependencies]
geometry = { path = "../geometry" }
rand = "0.8"

Here rand = "0.8" means "any 0.8.x release". Cargo picks the newest one it can find and writes the choice into a lock file. Node and Python tools work in a similar way.

Aela's manifest plays the same role as Cargo.toml. A dependency in Aela names a directory, and there are no version ranges. You always build against exactly the code in that directory.

4. A Library Package

Let's write a small geometry library as a package of its own. It has two modules.

text

geometry/
  index.json
  src/
    geometry.ae
    vector2.ae

index.json

{
  "name": "geometry",
  "version": "0.1.0",
  "entry": "src/geometry.ae"
}

The module vector2.ae holds a struct, a method and a function:

src/vector2.ae

export struct Vector2 {
    export x: i64;
    export y: i64;
}
impl Vector2 {
    export fn add(self: &Vector2, other: &Vector2) -> Vector2 {
        return Vector2 { x: self.x + other.x, y: self.y + other.y };
    }
}
export fn dot(a: &Vector2, b: &Vector2) -> i64 {
    return a.x * b.x + a.y * b.y;
}

The entry file, geometry.ae, is the face of the package. It re-exports the names from vector2.ae and adds one function of its own:

src/geometry.ae

//! Small 2D geometry helpers.
import { Vector2, dot } from "vector2.ae";
export Vector2;
export dot;
/// The squared length of a vector.
export fn length2(v: &Vector2) -> i64 {
    return dot(v, v);
}

A library's entry file does not need a main. Other packages import it.

Notice the word export in front of the fields x and y and in front of the method add. Inside a package, every file can use every field and method of the package's structs. Other packages can only use the fields and methods marked export. Section 6 shows what happens when they try to use the others.

You can read the library's documentation with aec doc. It prints the //! and /// comments next to each exported declaration:

Shell

1aec doc geometry/src/geometry.ae

5. Depending on Another Package

Now write a program that uses the library. Put it next to the geometry directory:

text

app/
  index.json
  src/
    main.ae
geometry/
  ...

The program's manifest lists the dependency. url is the path to the other package's directory, relative to this package:

index.json

{
  "name": "app",
  "version": "0.1.0",
  "entry": "src/main.ae",
  "dependencies": [
    { "name": "geometry", "url": "../geometry" }
  ]
}

In the code, the dependency's name is used like a module path. import geometry from "geometry" imports the dependency's entry file under the name geometry:

src/main.ae

import geometry from "geometry";
fn main() -> i32 {
    let a = geometry::Vector2 { x: 3, y: 4 };
    let b = geometry::Vector2 { x: 1, y: 2 };
    let c = a.add(&b);
    println("\(c.x) \(c.y)");                   // 4 6
    println("\(geometry::length2(&a))");        // 25
    return 0;
}

You can also import single names, just as you do with a file:

src/main.ae

import { Vector2, length2 } from "geometry";
fn main() -> i32 {
    let a = Vector2 { x: 3, y: 4 };
    println("\(length2(&a))");                  // 25
    return 0;
}

Build it from inside app:

Shell

aec build
./build/app

To see what a build will use without building it, run aec manifest. For this package it prints:

text

target: macos-arm64
package app 0.1.0 (./)
  entry: src/main.ae
  output: build/app
  depends on geometry (../geometry/)
dependency geometry 0.1.0 (../geometry/)

The first line is the machine you build for. On Linux it will say linux-x64 or linux-arm64.

A few rules about dependencies:

import x from "x" imports the entry file of the dependency named x. import { lock } from "sync/lock.ae" imports one file inside the dependency sync.
A package sees only its own dependencies. If app depends on geometry, and geometry depends on some other package, app cannot import that other package unless it lists it too.
No dependency may be named std, and two dependencies may not have the same name.
Today, url must be a local path. A remote address such as git+https://... is rejected with error E0219, because the compiler does not download packages yet.

6. The Package Boundary

A package draws a line around its code. Inside the line, all files can use everything. Outside it, other packages see only what is exported.

This matters most for struct fields. Here is a small counter package. The field count is not exported, so only the counter package itself can read or change it:

index.json

1{ "name": "counter", "entry": "src/counter.ae" }

src/counter.ae

export struct Counter {
    count: i64 = 0;
}
impl Counter {
    export fn bump(mut self: &Counter) -> void { self.count += 1; }
    export fn value(self: &Counter) -> i64 { return self.count; }
}

Another package, named user, depends on it. Its manifest has no entry, so the entry is src/main.ae:

index.json

{
  "name": "user",
  "dependencies": [ { "name": "counter", "url": "../counter" } ]
}

src/main.ae

import { Counter } from "counter";
fn main() -> i32 {
    var c: Counter = Counter {};
    c.bump();
    c.bump();
    println("\(c.value())");        // 2
    return 0;
}

The program can make a Counter with Counter {} because every field that is not exported has a default value (= 0). If a hidden field had no default, only the counter package could make new counters (error E0231).

The next version of src/main.ae tries to set the count directly. It is meant to fail, and aec build stops with error E0230:

src/main.ae

import { Counter } from "counter";
fn main() -> i32 {
    var c: Counter = Counter {};
    c.count = 100;
    println("\(c.value())");
    return 0;
}

text

src/main.ae:5:5: error[E0230]: a field of Counter is not exported by its package: 'count'

So a package can keep promises about its own data. Here, the only way to change a counter is to call bump, and bump adds one each time.

7. Several Programs from One Package

Sometimes one source tree builds more than one program. A command-line tool and a small helper tool might share most of their code. For this, the manifest has products in place of entry:

text

tools/
  index.json
  src/
    shared.ae
    hi.ae
    bye.ae

index.json

{
  "name": "tools",
  "version": "0.1.0",
  "products": [
    { "name": "hi", "entry": "src/hi.ae" },
    { "name": "bye", "entry": "src/bye.ae", "options": [ "--release" ] }
  ]
}

src/shared.ae

export fn greet(word: string) -> void {
    println("\(word), world");
}

src/hi.ae

import { greet } from "shared.ae";
fn main() -> i32 {
    greet("hi");
    return 0;
}

src/bye.ae

import { greet } from "shared.ae";
fn main() -> i32 {
    greet("bye");
    return 0;
}

aec build builds both programs, build/hi and build/bye. To build only one of them, name it:

Shell

1aec build --product bye

Each product has a name and an entry. It may also have an output path and a list of compiler options, which apply to that product alone. All products share the rest of the manifest, such as the dependencies.

8. C Code in a Package

A package can also include C sources. The compiler builds them with the system's C compiler and links them into the program. Aela code calls a C function after declaring it with extern fn.

text

fast/
  index.json
  c/
    sum.c
  src/
    main.ae

index.json

{
  "name": "fast",
  "sources": { "shared": [ "c/sum.c" ] },
  "compile": { "flags": { "shared": [ "-O2" ] } }
}

c/sum.c

long sum_to(long n) {
    long t = 0;
    for (long i = 1; i <= n; i++) t += i;
    return t;
}

src/main.ae

extern fn sum_to(n: i64) -> i64;
fn main() -> i32 {
    println("\(sum_to(100))");      // 5050
    return 0;
}

shared means "on every platform". You can also give lists for one platform only, such as darwin (macOS) or linux. There is a link key for linker flags, such as -lm. The compiler also writes build/compile_commands.json, which editors and C tools such as clangd can read.

A package with no C sources needs no C compiler at all.

Keep in mind that the compiler cannot check C code. Whatever the C function does is trusted. The extern fn line is the place to review carefully.

9. Budgets

Most languages build a program first and let you find out later that it is too large for the device it must run on.

In Aela, a package can state its limits up front. You write them as budgets on a target. A target is a machine you build for. After linking, aec build measures the program, and the build fails if the program is over a budget.

index.json

{
  "name": "hello",
  "version": "0.1.0",
  "entry": "src/main.ae",
  "targets": [
    {
      "name": "tiny",
      "arch": "arm64",
      "board": "linux",
      "budgets": {
        "flash_bytes": 65536,
        "ram_bytes": 32768
      }
    }
  ]
}

This target builds a Linux program for 64-bit ARM. Build for it by name:

Shell

1aec build --target tiny

The build prints how much of each budget the program uses:

text

budgets of tiny (build/hello):
  flash (text + rodata + data): 44204 B (43 KiB) / 64 KiB (67%)
  RAM (data + bss): 14336 B (14 KiB) / 32 KiB (43%)

The exact sizes depend on the compiler version. If you lower flash_bytes to 16384, the same build fails with error E0221:

text

budgets of tiny (build/hello):
error[E0221]: flash (text + rodata + data): 44204 B (43 KiB) / 16 KiB (269%): over budget by 27 KiB
  RAM (data + bss): 14336 B (14 KiB) / 32 KiB (43%)

The two budgets that are measured today are:

flash, which is everything stored in the program file: the code, the constants, and the starting values of global data;
RAM, which is the global data the program needs while it runs.

A manifest can also give stack_bytes, heap_bytes and cpu budgets. The compiler reads and checks these values, but it reports them as "not measured yet". The sizes are read from ELF files, the format Linux uses, so a budget is only checked when you build for Linux. For a macOS or Windows program, the build says that the budgets were not checked. Without --target, the build is for your own machine and no budget is checked.

Why would you want limits like this? Because they turn a surprise at the end of a project into a decision at the start. If the build fails, you have to ask useful questions. Do we need this dependency? Can this code be simpler? Is this table larger than it needs to be? A continuous integration server can run the same build and catch the problem on the day it appears.

10. Where a Program Came From

Every program that aec build makes carries a record of what it was built from. The record is stored in a part of the file the program never loads, so it costs no memory at run time. aec provenance prints it:

Shell

1aec provenance build/app

The record names the package, the target, the compiler, and every file the build read, each with its SHA-256 hash. For the app package from section 5, the file lines look like this:

text

file: 2f72462f1e32eb6e3fe4dc6a2685529cd81752265bbcb387316d43a87dd9f6d3 geometry/index.json
file: f0c93cb2e26577d6df2d8aeb616ecd8cb0854269a310149b7f94e92a0fd07346 geometry/src/geometry.ae
file: 7edbea70aba1865675ca92076e03428a1f3e000611938a057970f2041722220e geometry/src/vector2.ae
file: 1930cc5900733a0f2af40be0fa1c143e4c0dff90791882ee018a4f17ab2cfd0a index.json
file: 328c4452ab273586cd23a38650ca72e530d0d2a9f938a499c46fa74f49d4432b src/main.ae

The names in the record do not depend on where the build ran. So if two people build the same package with the same compiler, they get the same program, and they can compare the records to prove it. For software that must run for many years, this is very useful. Years later, you can still tell exactly which code is inside a device.

11. What Is Not There Yet

The package system is still growing. These parts are not available today:

downloading remote dependencies, and checking their sha256 hashes,
version constraints and a lock file,
aec test for a whole package,
measuring the stack, heap and CPU budgets,
embedded targets such as armv7m in the compiler's backend.

The manifest has a few more keys that this chapter did not cover. include and exclude limit which files a package may load. repo records where a package is published. Run aec docs packages to read about them.

Chapter Summary

A package is a directory with an index.json manifest. aec build builds it, and the program goes into build/.
The manifest names the package, its entry file, and its dependencies. A dependency is the path to another package's directory.
import geometry from "geometry" imports a dependency's entry file. A package sees only the dependencies it lists itself.
Other packages see only the fields and methods marked export. This lets a package protect its own data.
One package can build several programs with products, and it can include C sources.
Targets with budgets make size limits part of the build. Flash and RAM are measured today.
Every program records the exact files it was built from, and aec provenance prints that record.

Chapter 10. Parametric and Value-Aware Types

In Aela, a type can depend on other types, and it can also depend on values that are known when the program is compiled. The compiler and the verifier can then reason about the shapes and sizes of your data before the program ever runs.

You have already used these ideas in earlier chapters, even if we did not name them:

Map(string, i64) and Vec(string) from std/containers,
optional values like i64?,
growable arrays like string[],
fixed-size arrays like u8[32].

This chapter explains what is going on. There are four parts:

Type parameters let a struct or a function work with many types.
Value parameters let a type depend on a number known at compile time, such as the length of an array.
Refinement types limit an integer to a range, such as 0 to 100.
Specifications (#requires, #ensures, #invariant and #variant) state facts about your code, and aec --verify proves them.

Together they are a small, practical form of what language designers call dependent types. They are aimed at programs that must not fail, not at writing mathematical proofs.

1. Type Parameters: Families of Types

Most typed languages let you write code once and use it with many types. In C++ these are templates, and in Rust they are generics:

C++

template <typename T, typename U>
struct Pair {
    T first;
    U second;
};
template <typename T, typename U>
Pair<U, T> swap_pair(const Pair<T, U>& p) {
    return Pair<U, T>{p.second, p.first};
}

Rust

struct Pair<T, U> {
    first: T,
    second: U,
}
fn swap<T, U>(p: Pair<T, U>) -> Pair<U, T> {
    Pair { first: p.second, second: p.first }
}

Here is the same thing in Aela:

Aela

struct Pair(T, U) {
    first: T;
    second: U;
}
fn swap(T, U; p: Pair(T, U)) -> Pair(U, T) {
    return Pair { first: std::copy(p.second), second: std::copy(p.first) };
}
fn main() -> i32 {
    let p = Pair { first: 42, second: "answer" };   // Pair(i64, string)
    let q = swap(p);                                // Pair(string, i64)
    println("\(q.first) \(q.second)");              // answer 42
    let r: Pair(bool, f64) = Pair { first: true, second: 1.5 };
    println("\(r)");                                // Pair { first: true, second: 1.5 }
    return 0;
}

There are a few things to notice:

struct Pair(T, U) declares a struct with two type parameters. Pair alone is not a type. Pair(i64, string) is a type.
In a function, the type parameters come first, followed by a ;, and then the normal parameters: fn swap(T, U; p: Pair(T, U)).
A call never writes the types. The compiler works them out from the arguments. swap(p) gets T = i64 and U = string from the type of p.
A struct literal gets its types from the type you wrote for the variable, as with r, or else from the values of its fields, as with p.
Reading a T out of a field needs std::copy(...), because a T might be a struct or an array, and those move rather than copy.

A generic struct can have methods. The impl block names the struct with its parameters:

Aela

struct Stack(T) {
    items: T[];
}
impl Stack(T) {
    fn push1(mut self: &Stack(T), x: T) -> void { self.items.push(x); }
    fn size(self: &Stack(T)) -> i64 { return self.items.len; }
    fn top(self: &Stack(T)) -> T? {
        if (self.items.len == 0) { return none; }
        return std::copy(self.items[self.items.len - 1]);
    }
}
fn main() -> i32 {
    var words: Stack(string) = Stack { items: [] };
    words.push1("alpha");
    words.push1("beta");
    var numbers: Stack(i64) = Stack { items: [] };
    numbers.push1(7);
    println("\(words.size()) \(words.top() ?? "empty")");      // 2 beta
    println("\(numbers.size()) \(numbers.top() ?? 0)");        // 1 7
    return 0;
}

The containers in the standard library are built the same way. Map(K, V) is a generic struct with two type parameters:

Aela

import { Map } from "std/containers";
fn main() -> i32 {
    var ages: Map(string, i64) = Map {};
    ages.put("ada", 36);
    ages.put("alan", 41);
    println("\(ages.get("alan") ?? 0) \(ages.len())");     // 41 2
    return 0;
}

How generic code is compiled

As in C++ and Rust, the compiler makes a separate copy of a generic function or struct for each set of types that the program uses. Stack(string) and Stack(i64) above become two different structs with their own methods. This means type parameters cost nothing at run time. A Stack(u8) stores its bytes packed together, just as a plain u8[] would.

What you can do with a `T`

The compiler checks a generic function once, with T unknown. So in the body, a value of type T can only do things that every type can do. You can move it, store it, pass it, return it, copy it with std::copy(x), print it with "\(x)", compare it with std::equal(&a, &b) and hash it with std::hash(&x).

You cannot use operators on a T, not even == or >. The next example is meant to fail. The compiler rejects it with error E0348, because it cannot know that every T has a >:

Aela

fn bigger(T; a: T, b: T) -> T {
    if (a > b) { return a; }
    return b;
}
fn main() -> i32 { return 0; }

text

error[E0348]: a type parameter's values can only be moved, stored, passed, returned and printed

C++ templates are different here. C++ checks a template only when you use it, so a mistake shows up deep inside the template, in terms of the type you passed in. Aela, like Rust, checks the generic code itself.

Asking for more: interface constraints

To call methods on a T, say which interface it must implement. T: Shape means "any type that implements Shape". Rust writes the same idea as T: Shape too.

Aela

interface Shape {
    fn area(self: &Self) -> i64;
}
struct Square { side: i64; }
struct Rect { w: i64; h: i64; }
impl Square as Shape {
    fn area(self: &Square) -> i64 { return self.side * self.side; }
}
impl Rect as Shape {
    fn area(self: &Rect) -> i64 { return self.w * self.h; }
}
fn largest(T: Shape; xs: &T[]) -> i64 {
    var best: i64 = 0;
    for (let x: &xs::&T in xs) {
        if (x.area() > best) { best = x.area(); }
    }
    return best;
}
fn main() -> i32 {
    let squares: Square[] = [Square { side: 3 }, Square { side: 5 }];
    let rects: Rect[] = [Rect { w: 2, h: 10 }, Rect { w: 4, h: 4 }];
    println("\(largest(&squares)) \(largest(&rects))");    // 25 20
    return 0;
}

Each call must pass a T that implements Shape. Because there is one compiled copy per type, x.area() is a direct call to Square's or Rect's method.

What cannot be generic

Not everything can take type parameters:

Enums cannot be generic. There is no enum Result(T, E), and if you write one, the parser stops with error E0101. Use a generic struct instead.
Type aliases cannot be generic either.
You cannot write the type arguments at a call, as in last(i64; xs). They always come from the arguments.
A type argument cannot be a reference. Pair(&i64, string) is error E0340.

2. Value Parameters: Types Shaped by Numbers

Now we go one step further. In Aela, a type can also depend on a value that is known when the program is compiled.

The simplest case is the fixed-size array. T[N], where N is a constant, always has exactly N elements:

Aela

fn main() -> i32 {
    let key: u8[32];                    // exactly 32 bytes, all zero
    let block: i64[4] = [1, 2, 3, 4];   // exactly 4 elements
    println("\(key.len) \(block[3])");  // 32 4
    return 0;
}

The length is part of the type, so the compiler can hold you to it:

An array literal must have exactly the right number of elements. let block: i64[4] = [1, 2, 3]; is error E0346.
push, pop and clear do not work on a fixed array (error E0344).
u8[4] and u8[8] are different types. Using one where the other is expected is error E0301.

Here is a full program that breaks the rule about push. It is meant to fail with E0344:

Aela

fn main() -> i32 {
    var block: i64[4] = [1, 2, 3, 4];
    block.push(5);
    return 0;
}

text

error[E0344]: i64[4] has a fixed length: push and pop need a growable array (T[])

Be careful with one thing. If the length is not a constant, for example a variable n, then T[n] is a growable array that simply starts with n zero elements. Only a literal number or a value parameter makes a fixed array.

Structs with value parameters

A struct can take value parameters too. You write them with their type, N: u64, so the compiler can tell them apart from type parameters. Then the fields can use them:

Aela

struct Buf(N: u64) {
    data: u8[N];
    used: i64;
}
fn capacity(N: u64; b: &Buf(N)) -> i64 {
    return N as i64;
}
fn sum(N: u64; xs: &i64[N]) -> i64 {
    var t: i64 = 0;
    for (let i: i64 in 0..(N as i64)) { t += xs[i]; }
    return t;
}
fn main() -> i32 {
    var small: Buf(16);
    var large: Buf(1024);
    println("\(capacity(&small)) \(capacity(&large))");    // 16 1024
    let xs: i64[5] = [1, 2, 3, 4, 5];
    println("\(sum(&xs))");                                // 15
    return 0;
}

Here is what this shows:

Buf(16) and Buf(1024) are different types. Each one has a data array of exactly that length.
A function lists its value parameters before the ;, just like type parameters: fn capacity(N: u64; b: &Buf(N)).
Calls do not write N. The compiler finds it from the argument. sum(&xs) with xs: i64[5] gives N = 5.
Inside the function, N is an ordinary value that cannot change. You can use it at run time, as in N as i64 or 0..(N as i64).

Since Buf(16) and Buf(1024) are different types, you cannot mix them. This example is meant to fail with E0301:

Aela

struct Buf(N: u64) {
    data: u8[N];
    used: i64;
}
fn main() -> i32 {
    var small: Buf(16);
    let large: Buf(1024) = small;
    return 0;
}

text

1error[E0301]: expected Buf(1024), found Buf(16)

Type parameters and value parameters can be mixed. Here is a ring buffer that holds N values of any type T:

Aela

struct Ring(T, N: u64) {
    slots: T[N];
    pos: i64;
}
fn put(T, N: u64; mut r: &Ring(T, N), x: T) -> void {
    r.slots[r.pos] = x;
    r.pos = (r.pos + 1) % (N as i64);
}
fn main() -> i32 {
    var r: Ring(string, 3);
    put(mut &r, "a");
    put(mut &r, "b");
    put(mut &r, "c");
    put(mut &r, "d");                   // wraps around and replaces "a"
    println("\(r.slots)");              // ["d", "b", "c"]
    return 0;
}

How other languages do this

C++ and Rust both have something similar:

C++

template <std::size_t N>
struct Buf {
    unsigned char data[N];
    long used;
};

Rust

struct Buf<const N: usize> {
    data: [u8; N],
    used: usize,
}

In Ada, an array type carries its bounds, and a record can take a discriminant that sets the size of an array inside it.

What Aela adds is the link to the verifier, which you will see in section 4. Because the length of data is N, the verifier can use facts about N to prove that every index is in bounds.

How value parameters are compiled

As with type parameters, a value parameter given a constant gets its own compiled copy. In Buf(16), N is simply the number 16. The array's length is then a constant, and the optimizer can remove bounds checks that it can prove are not needed. A local fixed array can also live in the function's stack frame instead of on the heap.

Limits

A fixed length must be a literal number or a value parameter. u8[N + 1] is a growable array, and Buf(2 * N) does not parse.
You cannot write value arguments at a call. They always come from the arguments' types.

Ada has a well-known feature called a subtype with a range:

Ada

subtype Percent is Integer range 0 .. 100;
function Half (P : Percent) return Percent is (P / 2);

A Percent is an Integer, but it may only hold values from 0 to 100. Aela has the same idea, called a refinement type:

Aela

type Percent = { p: i64 where 0 <= p && p <= 100 };
fn describe(p: Percent) -> string {
    if (p == 100) { return "full"; }
    if (p == 0) { return "empty"; }
    return "\(p)%";
}
fn main() -> i32 {
    let level: Percent = 75;
    println(describe(level));       // 75%
    println(describe(100));         // full
    return 0;
}

Read { p: i64 where 0 <= p && p <= 100 } as "an i64, call it p, where p is between 0 and 100".

The rules are simple:

The base type must be an integer type (error E0319).
The condition bounds the value by constants, using <, <=, >, >= or ==, joined with &&. Anything else, such as ||, is error E0321. The range cannot be empty (error E0320).
A Percent works as an i64 everywhere: in arithmetic, in comparisons, and as an argument.
A refinement type cannot be optional. Percent? is error E0316.

The range is checked whenever a value is stored as a Percent: as an argument, a return value, an assignment or a starting value. When the value is a constant, the check happens at compile time. This example is meant to fail with E0813:

Aela

type Percent = { p: i64 where 0 <= p && p <= 100 };
fn main() -> i32 {
    let level: Percent = 150;
    return 0;
}

text

1error[E0813]: the value is outside the range of its refinement type (0 to 100)

When the value is only known at run time, a normal build checks it at run time. This program compiles, but when it runs, it stops with trap: value outside its refinement type, because 200 is not a valid Percent:

Aela

type Percent = { p: i64 where 0 <= p && p <= 100 };
fn to_percent(x: i64) -> Percent {
    return x;
}
fn main() -> i32 {
    let n: i64 = 40 * 5;
    println("\(to_percent(n))");
    return 0;
}

The verifier can do better, as we will see next.

4. Specifications and the Verifier

A specification is a line that states a fact about your code. Aela has four kinds:

specification	where it goes	what it says
`#requires`	before a function	what must be true when the function is called
`#ensures`	before a function	what is true about the result when the function returns
`#invariant`	right before a loop	what is true at the start of every pass through the loop
`#variant`	before a loop, or before a recursive function	a number that gets smaller each time, so the loop or the recursion ends

A normal build does not check specifications. They are checked when you compile with --verify:

Shell

1aec --verify file.ae -o prog

For a package, use aec build --verify.

With --verify, the compiler also proves the basic safety of every line. Every array index must be proven in bounds (error E0809). Every plain +, -, * and / must be proven not to overflow (error E0810). Every value stored in a refinement type must be proven in its range (error E0813). If the verifier cannot prove something, the program does not compile.

SPARK, the verified form of Ada, works in a similar way. A contract there looks like this:

Ada

function Add_One (N : Integer) return Integer
  with Pre  => N >= 0 and N < 1000,
       Post => Add_One'Result = N + 1;

`#requires` and `#ensures`

Here is the same function in Aela:

Aela

#requires 0 <= n && n < 1000;
#ensures result == n + 1;
fn add_one(n: i64) -> i64 {
    return n + 1;
}
fn main() -> i32 {
    println("\(add_one(41))");      // 42
    return 0;
}

The verifier checks both sides of the promise:

Inside add_one, it may assume #requires. That is how it knows n + 1 cannot overflow.
At every return, it must prove #ensures. In #ensures, the word result means the value being returned.
At every call, it must prove #requires from what it knows at that place.

So this call is rejected under --verify with error E0804:

Aela

#requires 0 <= n && n < 1000;
#ensures result == n + 1;
fn add_one(n: i64) -> i64 {
    return n + 1;
}
fn main() -> i32 {
    println("\(add_one(5000))");
    return 0;
}

text

error[E0804]: the precondition (#requires) is not proven for this call to 'add_one'

Without --verify, the same program compiles and prints 5001. Specifications are only checked by the verifier.

If the function broke its own promise, for example with #ensures result == n + 2;, the verifier would report error E0805 at the return.

Value parameters in specifications

Specifications can talk about value parameters. This is where sections 2 and 4 come together:

Aela

struct Buf(N: u64) {
    data: u8[N];
    used: i64;
}
#requires N > 0;
fn first(N: u64; b: &Buf(N)) -> u8 {
    return b.data[0];
}
fn main() -> i32 {
    var b: Buf(4);
    b.data[0] = 42;
    println("\(first(&b))");        // 42
    return 0;
}

The verifier knows that b.data has exactly N elements. With #requires N > 0, it can prove that b.data[0] is in bounds. Without the #requires, it would reject b.data[0] with error E0809, because a Buf(0) has no element 0.

At the call first(&b), the compiler finds N = 4 and proves 4 > 0. A call with an empty buffer is rejected under --verify. This example is meant to fail with E0804:

Aela

struct Buf(N: u64) {
    data: u8[N];
    used: i64;
}
#requires N > 0;
fn first(N: u64; b: &Buf(N)) -> u8 {
    return b.data[0];
}
fn main() -> i32 {
    var empty: Buf(0);
    println("\(first(&empty))");
    return 0;
}

text

error[E0804]: the precondition (#requires) is not proven for this call to 'first'

Without --verify, this program compiles, and it stops with trap: index out of bounds when it runs. The verifier moves that failure from run time to compile time.

The verifier does not need to know N as a number. It can reason about it as a symbol. Here a function with a stronger #requires calls first, and the verifier proves that N >= 2 means N > 0:

Aela

struct Buf(N: u64) {
    data: u8[N];
    used: i64;
}
#requires N > 0;
fn first(N: u64; b: &Buf(N)) -> u8 {
    return b.data[0];
}
#requires N >= 2;
fn first_two(N: u64; b: &Buf(N)) -> i64 {
    let a: u8 = first(b);           // proved: N >= 2 means N > 0
    let c: u8 = b.data[1];          // proved: 1 < N
    return (a as i64) + (c as i64);
}
fn main() -> i32 {
    var b: Buf(8);
    b.data[0] = 40;
    b.data[1] = 2;
    println("\(first_two(&b))");    // 42
    return 0;
}

These proofs are made once for every possible N, not once per use.

A plain if also gives the verifier facts. Inside the branch after if (N == 0) { return 0; }, it knows N > 0:

Aela

fn last(N: u64; xs: &i64[N]) -> i64 {
    if (N == 0) { return 0; }
    return xs[(N as i64) - 1];      // proved: N > 0 here, so N - 1 is a valid index
}
fn main() -> i32 {
    let xs: i64[3] = [10, 20, 30];
    let empty: i64[0] = [];
    println("\(last(&xs)) \(last(&empty))");        // 30 0
    return 0;
}

Under --verify, a value stored as a refinement type must be proven to be in range. In return, the verifier may rely on the range wherever the value is read.

Here is the to_percent function from section 3, fixed so that the verifier accepts it. The if statements make sure the value is in range, so there is no trap left to happen:

Aela

type Percent = { p: i64 where 0 <= p && p <= 100 };
fn to_percent(x: i64) -> Percent {
    if (x < 0) { return 0; }
    if (x > 100) { return 100; }
    return x;                       // proved: 0 <= x <= 100 here
}
fn half(p: Percent) -> Percent {
    return p / 2;                   // proved: the verifier knows 0 <= p <= 100
}
fn main() -> i32 {
    let n: i64 = 40 * 5;
    let p: Percent = to_percent(n);
    println("\(p) \(half(p))");     // 100 50
    return 0;
}

The range also helps with overflow. Under --verify, s * 1000 on a plain i64 is rejected with error E0810, because s could be very large. With a refinement type, the verifier knows the result is small enough:

Aela

type Small = { s: i64 where -100 <= s && s <= 100 };
fn scale(s: Small) -> i64 {
    return s * 1000;                // proved: the result is between -100000 and 100000
}
fn main() -> i32 {
    println("\(scale(42))");        // 42000
    return 0;
}

Loops: `#invariant` and `#variant`

A loop can carry two specifications, written right before the while or for:

#invariant is a fact that is true every time the loop starts a new pass. The verifier proves it holds when the loop is first reached and after each pass. Then it may use the fact inside the loop and after it.
#variant is a number that never goes below zero and gets smaller on every pass. If such a number exists, the loop must end.

A recursive function can have a #variant too. It must get smaller at each recursive call. Under --verify, every recursive function needs one (error E0808).

Aela

#requires 0 <= n && n < 1000;
fn count_up(n: i64) -> i64 {
    var i: i64 = 0;
    #invariant 0 <= i && i <= n;
    #variant n - i;
    while (i < n) {
        i += 1;
    }
    return i;
}
#requires n >= 0;
#variant n;
fn countdown(n: i64) -> i64 {
    if (n == 0) { return 0; }
    return countdown(n - 1);
}
fn main() -> i32 {
    println("\(count_up(10)) \(countdown(10))");   // 10 0
    return 0;
}

In count_up, the number n - i starts at n, gets one smaller on each pass, and never goes below zero, because the invariant says i <= n. If you wrote #variant i; instead, the verifier would reject it with error E0807, because i gets bigger, not smaller.

What the verifier understands

The verifier uses one fixed method. It is fast and it does not guess, so whether your program compiles never depends on luck. The price is that it only understands simple facts. A specification must be made of comparisons joined by &&. The terms in a comparison may use variables, lengths such as xs.len, constants, + and -.

So products, function calls and || are not allowed. This example is meant to fail under --verify with error E0802:

Aela

#requires a * b < 100;
fn area(a: i64, b: i64) -> i64 {
    return a * b;
}
fn main() -> i32 { return 0; }

text

error[E0802]: this specification is beyond the built-in verifier (linear comparisons of variables, lengths and constants)

The usual fix is to give a bound for each variable on its own. That is often stronger than you need, but the verifier can check it:

Aela

#requires 0 <= a && a < 10 && 0 <= b && b < 10;
fn area(a: i64, b: i64) -> i64 {
    return a * b;
}
fn main() -> i32 {
    println("\(area(3, 4))");       // 12
    return 0;
}

5. What Aela Is Not

Aela takes a small, careful piece of dependent typing. It is enough to state the facts that matter in safety-critical code: sizes, ranges, and the conditions a function needs. But Aela is not:

a theorem prover,
an interactive proof assistant,
a language where you write mathematical proofs in your code,
a language where types can be computed by any expression.

Systems like Coq, Agda and Lean can prove much deeper things, but they are hard to use for embedded software, and their proofs can take a long and unpredictable time to check. Aela chooses a smaller set of facts that it can always check quickly.

6. What Aela Is

Aela puts several tools together:

type parameters,
value parameters,
refinement types,
specifications (#requires, #ensures, #invariant, #variant),
the ownership and borrowing rules from earlier chapters,
a built-in verifier.

With --verify, they let the compiler prove that a program has:

no index out of bounds,
no arithmetic overflow,
no value outside its refinement type,
no loop or recursion that runs forever, where a #variant is given,
and the behavior you described in #requires and #ensures.

Aela sits in the same family as SPARK/Ada, Dafny and Why3, but with a simpler and more modern way of writing programs.

Value-aware types are not there for elegance. They are there so that the compiler can prove that whole classes of faults cannot happen, faults that are common in embedded systems.

Chapter Summary

Type parameters, as in struct Pair(T, U) and fn swap(T, U; p: Pair(T, U)), let one piece of code work with many types. Calls never write the types. Each set of types gets its own compiled copy.
A T can only be moved, stored, passed, copied, printed, compared with equal and hashed. To call methods on it, constrain it with an interface: T: Shape.
Enums and type aliases cannot be generic.
Value parameters, as in struct Buf(N: u64) and T[N], let a type depend on a number known at compile time. Buf(16) and Buf(1024) are different types.
Refinement types, as in type Percent = { p: i64 where 0 <= p && p <= 100 }, limit an integer to a range. A constant out of range is a compile error, and other values are checked when they are stored.
#requires, #ensures, #invariant and #variant state facts about functions and loops. aec --verify proves them, together with bounds, overflow and refinement ranges.
The verifier understands comparisons of simple sums joined by &&. For the same program, it always gives the same answer.

Foreword

Chapter 1. Basics

Hello, World In Other Languages

Hello, Aela!

Building and Running

Putting Values Into Strings

Comments

Exit Status and Arguments

Chapter 2. Variables, Types, and Basic Expressions

C

C++

Rust

Ada

Aela

Zero Values

let and var

Writing the Type

One Name, One Meaning

Basic Types

No Hidden Conversions

Arithmetic

Overflow

Floats

Comparisons and Logic

Assignment

Strings in Expressions

Summary

Chapter 3. Conditions and Branching

C

C Gotchas

1. Any number can be a condition

2. Assignment inside a condition

C++

Rust

Ada

Aela

A condition must be a bool

An assignment is not a condition

Operators in conditions

Example: A Three-Way Branch

C and C++

Rust

Ada

if Is Not an Expression

match

Every case must be handled

if (let ...): Checking an Optional

Summary

Chapter 4. Loops

Part 1 — Ordinary Loops

C

C++

Rust

Ada

Aela

break and continue

No while (let ...)

Basic for Loops

C (a range through an index)

C++

Rust (iterator style)

Ada

Aela

Arrays

Strings

Summary of Ordinary Loops

Part 2 — Verified Loops (Aela and SPARK Ada)

Why invariants?

SPARK Ada example (for reference)

Aela example (the same idea, shorter)

What --verify checks for you

Summary (Verification Features)

Chapter 5. Functions

Part 1. Ordinary Functions

C

C++

Rust

Ada

Aela

Default values and variadic parameters

`let` and `var`

A condition must be a `bool`

`if` Is Not an Expression

`match`

`if (let ...)`: Checking an Optional

`break` and `continue`

No `while (let ...)`

Basic `for` Loops

What `--verify` checks for you

Part 2. Passing Data, References and `mut &`

2.1 `Vec(T)`

2.2 `Map(K, V)`

2.4 `OrderedMap(K, V)`

2.5 `Set(T)`

3.4 The `std/string` module

Arrays (`T[]`)

Library containers (`std/containers`)