Introduction

borrow-core is a systems language for people who like Rust’s ownership model and want a simpler story for everything else. You own values and borrow them with & and &mut, as in Rust. There is no garbage collector and no hidden reference counting: you write the allocations, and the compiler inserts the frees. Programs compile to WebAssembly or, through LLVM, to native code.

include textio

fn greet(n: i32) -> 1 =
  print_lit("hello, ");
  print_dec(n);
  print_byte(b'\n')

main -> 1 = greet(42)
-- output: hello, 42

It’s meant for the programs you’d write in Rust or C, such as command-line tools, services and systems code, without fighting the borrow checker over errors and async.

• One mechanism for effects. Errors, I/O, generators and async tasks are all effects: operations called like functions, given their meaning by a handler further up. raise is an operation, a generator is a function that performs yield, and await is an operation. There is no Result threaded by hand, no ?, no separate exception system and no separate iterator protocol.
• No coloured functions. A function that raises, waits or writes is called like any other. Its effects are inferred, and the handler around the call serves them. A higher-order function such as map is written once and serves a pure callback, a failing one and an awaiting one alike.
• Handlers compile away. There is no handler stack and no run-time search. An operation that answers at once is a direct call, raise is a branch after each call that may raise, and a task or generator that suspends is a state machine, the way Rust compiles async fn.
• No garbage collector, and allocation where C or Rust would allocate. Owned values are freed when their owner is done with them, and nothing is reference counted. A borrowed local and a handler’s state live in the stack frame.
• Safety that’s proved, not just tested. If your program compiles, it doesn’t use freed memory, free anything twice or leak (Safety guarantees).

The chapters under The language teach it in the order you meet it: values and functions, ownership, data, errors, I/O, iteration, effects and async. Effects and handlers ends with a generic retry with exponential backoff, tested against a fake timer, which uses most of it at once. Recipes shows short programs for everyday tasks, and the Language reference and Standard library are for looking things up.

The language is young, and Status lists what isn’t built yet. Every example in this book is a program the test suite runs, and the output shown is its output.

Getting started

Installing

The compiler, bcc, is written in Lean 4 and built from source. You need:

• elan, the Lean toolchain manager. It installs the pinned toolchain on first use.
• wasmtime, to run compiled programs. Any version with tail-call support works.
• clang, only if you want native builds.

On macOS, brew bundle in the repository installs elan and wasmtime (and mdbook, for building this book). Then clone the repository and build the compiler:

git clone https://github.com/empath-nirvana/borrow-core
cd borrow-core
lake exe cache get      # downloads prebuilt Mathlib, which the proofs use, instead of compiling it
lake build bcc

The compiler is at .lake/build/bin/bcc.

A first program

Save this as hello.bc:

include textio

-- The sum of the squares below `n`.
fn squares(n: i32) -> i32 =
  let mut s = 0;
  for i in 0..n { s = s + i * i };
  s

main -> 1 =
  print_lit("squares below 4: ");
  print_dec(squares(4));
  print_byte(b'\n')
-- output: squares below 4: 14

and run it:

$ bcc run hello.bc
squares below 4: 14
()
live 0

fn declares a function, and main is where the program starts. include textio brings in the text and I/O library: print_lit writes a string literal, print_dec a number in decimal, and print_byte one byte. main -> 1 says that main returns nothing interesting: 1 is the unit type, whose one value is ().

The last two lines come from bcc, not from the program. () is the value main returned, and live 0 is the number of heap objects still allocated when it finished: live 0 means nothing leaked. Every program in this book ends that way; the examples show only the program’s own output.

If something is wrong, bcc run prints the error, with its line and column, instead of running the program.

The bcc commands

A program reads standard input and writes standard output as usual, and takes arguments after the file name: bcc run tool.bc a b < input.

bcc run and bcc compile use the compiler’s current backend by default. Until the old backend is retired, --backend old right after the command selects it: bcc run --backend old file.bc.

The next chapter starts the language from here. Recipes has short programs for everyday tasks, and the Language reference and Standard library are for looking things up. For larger programs, see the Advent of Code and LeetCode ports in corpus/aoc/ and corpus/leetcode/.

Values, functions and numbers

This chapter covers the parts of the language that look like most others: functions, let, if, numbers, records and variants, generics and closures. Ownership, the part that is different, is the next chapter. The Language reference has the whole syntax in one place.

A program

A program is a list of declarations ending with main, where it starts:

include textio

fn square(x: i32) -> i32 = x * x

main -> 1 =
  print_dec(square(6) + square(2));
  print_byte(b'\n')
-- output: 40

fn name(params) -> T = e declares a function. Every parameter has its type written, and so does the result. main -> 1 returns nothing interesting: 1 is the unit type, whose one value is (). A function calls the functions declared before it; functions that call themselves or each other are in Recursion.

A body is a sequence of statements separated by ;, and its value is the value of the last one:

include textio

fn hyp2(a: i32, b: i32) -> i32 =
  let aa = a * a;
  let bb = b * b;
  aa + bb

main -> 1 =
  let x = hyp2(3, 4);
  let x = x + 1;
  print_dec(x);
  print_byte(b'\n')
-- output: 26

let x = e; binds a name, and a later let of the same name shadows it. A type can be written, let x: i64 = 5;, and is needed where nothing else fixes it. A constant is declared at the top level with def: def max_depth : i32 = 64.

Mutable variables and loops

let mut x = e; declares a variable that can be assigned, x = e;. while c { … } repeats its body while c is true, and if c { … } else { … } chooses one branch; both branches have the same type. An if whose body is a statement needs no else: if x > max { max = x }.

include textio

-- The number of Collatz steps from `n` to 1.
fn collatz(n: i32) -> i32 =
  let mut x = n;
  let mut steps = 0;
  while x != 1 {
    if x % 2 == 0 { x = x / 2 } else { x = 3 * x + 1 };
    steps = steps + 1
  };
  steps

main -> 1 =
  print_dec(collatz(27));
  print_byte(b'\n')
-- output: 111

A while may run forever, and the compiler knows it: a function with one is div (it may diverge), which it infers. Loops over data, which always finish, are for loops (Iteration).

Numbers

An integer literal is an i32 unless another integer type is expected. The operators are + - * / %, the comparisons == != < <= > >=, and &&, || and not(b) on bool; each works at the type of its operands, so x * 2 at an i64 is a 64-bit multiplication. Comparisons are signed, and 0 - x negates.

/ and % truncate toward zero. A division with no answer (by zero, or MIN / -1) raises an error rather than trapping; Errors shows how to handle it.

include textio

fn mean(a: i64, b: i64, c: i64) -> i64 = (a + b + c) / 3

main -> 1 =
  let big: i64 = 4000000000;
  print_dec64(mean(big, big, 1));
  print_byte(b'\n');
  print_dec(17 % 5);
  print_byte(b'\n');
  print_dec((0 - 7) / 2);
  print_byte(b'\n')
-- output: 2666666667
-- output: 2
-- output: -3

print_dec prints an i32 and print_dec64 an i64.

A byte is a u8. Arithmetic on bytes is done at i32 and narrowed back, and to_i32(b) and to_u8(n) convert between the two:

include textio

main -> 1 =
  let c = b'a' + 2;
  print_byte(c);
  print_byte(b' ');
  print_dec(to_i32(c) - to_i32(b'a'));
  print_byte(b'\n')
-- output: c 2

The bitwise operations, shifts and integer conversions are written as calls of the machine instruction, with the width as a suffix: host[and32](x, 1), host[shl64](n, 3).

host[extend_s](x) widens an i32 to an i64 (extend_u for unsigned), and host[wrap](n) keeps an i64’s low 32 bits.

Floats

A literal with a fraction or an exponent is a float, an f64 unless an f32 is expected. + - * / and the comparisons work at floats as IEEE 754 defines them: a NaN compares unequal to everything, itself included. include float brings the rest: sqrt_f64, abs_f64, floor_f64, round_f64, conversions such as f64_of_i32 and i32_of_f64_sat, and print_f64, which prints the shortest decimal that reads back as the same float.

include float

fn hypot(x: f64, y: f64) -> f64 = sqrt_f64(x * x + y * y)

main -> 1 =
  let h = hypot(3.0, 4.0);
  print_f64(h / 3.0);
  print_byte(b'\n');
  print_dec(i32_of_f64_sat(h * 10.0));
  print_byte(b'\n')
-- output: 1.6666666666666667
-- output: 50

A float has no hash or total order of its own, so it can’t be a map key directly; include float has total_cmp_f64 and ord_f64 for when you need one.

Records and variants

data declares a type of your own. A record has named fields, read and written with .:

include textio

data Point = { x: i32, y: i32 }

fn manhattan(p: Point) -> i32 = p.x + p.y

main -> 1 =
  let mut p = Point { x: 3, y: 4 };
  p.x = p.x * 10;
  print_dec(manhattan(p));
  print_byte(b'\n')
-- output: 34

A record pattern, Point { x, y }, takes a record apart in a let or a match and binds each field to a variable of its name; Point { x: a, y: b } binds them to other names. Construction has the same shorthand: Point { x, y } builds a record from variables named like its fields.

include textio

data Point = { x: i32, y: i32 }

-- The point reflected in the diagonal.
fn flip(p: Point) -> Point =
  match p { Point { x, y } -> Point { x: y, y: x } }

-- The point moved right by `dx`.
fn shift(p: Point, dx: i32) -> Point =
  let Point { x, y } = p;
  let x = x + dx;
  Point { x, y }

main -> 1 =
  let p = shift(flip(Point { x: 1, y: 2 }), 10);
  print_dec(p.x);
  print_byte(b' ');
  print_dec(p.y);
  print_byte(b'\n')
-- output: 12 1

A variant is one of several cases, each with its own fields, and match takes it apart:

include textio

data Shape = Rect(w: i32, h: i32) | Circle(r: i32)

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

main -> 1 =
  print_dec(area(Rect(3, 4)) + area(Circle(2)));
  print_byte(b'\n')
-- output: 24

A match must cover every case, and it can match several values at once, match (state, byte) { (Locked, b'c') -> Open | … }. Declarations can be generic, data Pair[A, B] = { fst: A, snd: B }, and the prelude has Option[T], with Some(x) and None. Recursive types, such as lists and trees, are in Data and generics.

Tuples and sums

(a, b) is a pair, of type A * B, and (a, b, c) a triple, of type A * B * C. let (x, y) = p; takes one apart, and patterns nest.

A sum A + B holds either an A, written inl a, or a B, written inr b, and match takes it apart. Library functions use sums for answers that may be missing: A + 1 is an A or nothing (inr ()), and an error handler answers A + E, the value or the error.

include textio

type Size = (i32 * i32) + i32

fn cells(s: Size) -> i32 =
  match s {
    inl (w, h) -> w * h
  | inr n -> n
  }

main -> 1 =
  let a: Size = inl (3, 4);
  let b: Size = inr 2;
  print_dec(cells(a) + cells(b));
  print_byte(b'\n')
-- output: 14

type Size = … gives a type a name; the name and its definition are interchangeable. inl and inr need to know the whole sum, so they appear where a type is expected: an annotated let, an argument, a result.

Generic functions

A function may take type parameters in brackets. They are inferred at each call from the arguments, or written, pick[i32](…):

include textio

fn swap_pair[A, B](p: A * B) -> B * A = let (a, b) = p; (b, a)

fn pick[A](c: bool, x: A, y: A) -> A = if c { x } else { y }

main -> 1 =
  let (n, ok) = swap_pair((true, 7));
  let m = pick[i64](ok, 1, 2);
  print_dec(n);
  print_byte(b' ');
  print_dec64(m);
  print_byte(b'\n')
-- output: 7 1

A generic function is compiled once for each type it is used at, as in Rust: there is no boxing and no dictionary. What a generic function may do with a value of type A is checked at each use: a body that copies an A works only where A can be copied (next chapter).

Functions as values

A function can be passed to another. Its parameter’s type says how often it may be called:

• !(A => B) is a function that can be called any number of times. A named function is one, and so is a closure !{ x -> … }, which takes what it needs as arguments rather than capturing local variables.
• A => B is a function called at most once. A closure { x -> … } of this type may capture anything in scope, including local variables and owned values.

include textio

fn twice(f: !(i32 => i32), x: i32) -> i32 = f(f(x))

fn double(x: i32) -> i32 = x * 2

fn apply_once(f: i32 => i32, x: i32) -> i32 = f(x)

main -> 1 =
  let k = 5;
  print_dec(twice(double, 3));
  print_byte(b' ');
  print_dec(twice(!{ x -> x + 1 }, 0));
  print_byte(b' ');
  print_dec(apply_once({ x -> x + k }, 1));
  print_byte(b'\n')
-- output: 12 2 6

A closure’s parameter types come from the parameter it is passed to, so a closure bound with let needs its type written: let f: !(i32 => i32) = !{ x -> x + 1 };. A pattern can take the argument apart, !{ (a, b) -> a + b }.

A function whose body performs effects, raises an error or waits, is passed the same way, and the function it is passed to needs nothing extra to accept it: Effects and handlers explains how. A callback that keeps state from one call to the next is a handler with state (Effects and handlers).

Ownership and borrows

Every value is either unrestricted or linear. An unrestricted value holds no resource, and may be copied and used any number of times or not at all. A linear value is used exactly once: passed on, taken apart, or consumed by its consume. Most linear values own something (memory, a capability, a suspended computation), and a borrow is linear too. Most linear types have a consume that the compiler derives from their structure, and the checker inserts it where a value goes unused, so an owned cell behaves much as it does in Rust. The difference is that Rust lets any value go unused, while here a value goes unused only through its consume, and some types have none (Linear values). Borrowing lends a value for a while without giving it up. A program that type-checks has no use after free, no double free and no leak (Safety guarantees).

Unrestricted and linear values

These types are unrestricted: the numbers, bool, 1, ! functions, tuples and sums of unrestricted types, and recursive data of these (copied with clone). Everything else is linear:

alloc(v) puts v in a new heap cell, a ref A, and free(c) takes the value back out and frees the cell. Using an owned value moves it, and a value that has moved can’t be used again:

include textio

fn take_all(c: ref i32) -> i32 = free(c)

main -> 1 =
  let c = alloc(40);
  let d = c;
  print_dec(take_all(d) + 2);
  print_byte(b'\n')
-- output: 42

fn take_all(c: ref i32) -> i32 = free(c)

main -> i32 =
  let c = alloc(1);
  let n = take_all(c);
  n + free(c)
-- expect: 5:3: `c` is used twice here, and its type `ref i32` is linear

The second use is an error, so there is no use after free and no double free. A value that is never used is not an error: the checker inserts its consume where its scope ends, which frees it, much as Rust consumes it.

include textio

main -> 1 =
  let unused = alloc(1);
  let c = alloc(41);
  print_dec(free(c) + 1);
  print_byte(b'\n')
-- output: 42

The run ends with live 0: both cells were freed. A value whose type is not consumable (a capability, a one-shot closure that must be called, a declared type that must be closed) must be used, and leaving it unused is an error that names it (Linear values).

Borrowing for one call

&x lends x shared, and &mut x lends it exclusively, to one call. After the call, x is usable again, changed if it was lent &mut. The function receives a borrow, imm 'a A or mut 'a A, whose lifetime 'a is a parameter of the function:

include textio

fn get<'a>(r: imm 'a i32) -> i32 = *r

fn bump<'a>(r: mut 'a i32) -> 1 = modify r { v -> v + 1 }

-- Adds `k`, and answers the old value.
fn add<'a>(m: mut 'a i32, k: i32) -> i32 = modify m { v -> (v + k, v) }

main -> 1 =
  let c = alloc(5);
  bump(&mut c);
  let old = add(&mut c, 10);
  let now = get(&c);
  print_dec(old);
  print_byte(b' ');
  print_dec(now);
  print_byte(b'\n')
-- output: 6 16

• *r reads through a borrow. It copies the contents, so it needs a copyable content type.
• modify m { v -> e } replaces the contents v of a mut borrow by e. When e is a pair (new, result), the contents become new and modify answers result.

&x and &mut x work on a let mut variable too, with no heap cell: the compiler gives the variable a slot in the stack frame for the call. Through a mut borrow of a record, a field is assigned as on the record itself:

include textio

data Point = { x: i32, y: i32 }

fn nudge<'a>(p: mut 'a Point, dx: i32) -> 1 = p.x = p.x + dx

main -> 1 =
  let mut p = Point { x: 1, y: 2 };
  nudge(&mut p, 10);
  nudge(&mut p, 5);
  print_dec(p.x);
  print_byte(b'\n')
-- output: 16

Borrow blocks

borrow imm x { b -> … } and borrow mut x { m -> … } lend x for a block of code rather than one call. Inside the block, x itself is out of reach; after it, x is back. The block’s value is the block’s result:

include textio

main -> 1 =
  let c = alloc(5);
  let k = 7;
  let old = borrow mut c { m ->
    let old = modify m { v -> (v + k, v) };
    modify m { v -> (v * 2, old) } };
  print_dec(old);
  print_byte(b' ');
  print_dec(free(c));
  print_byte(b'\n')
-- output: 5 24

The block introduces a lifetime of its own. It is unnamed unless a type written inside the block mentions it, in which case it is written first: borrow imm a { 'x, v -> … }.

Inside the block, m is a value like any other: passing it to a function moves it. So a function that takes a mut borrow and is meant to be called more than once hands it back, fn f<'a>(m: mut 'a A) -> mut 'a A * B, and the caller binds it again, let (m, r) = f(m);. The view functions of the next chapter work this way.

An imm borrow is linear too, but it has a derived copy: a second use of it is a copy, which the compiler inserts, and which costs nothing at run time (the copy is the same pointer). So an imm borrow, or an array_imm view, can be read as often as you like:

fn twice<'a>(r: imm 'a i32) -> i32 = *r + *r

main -> i32 =
  let c = alloc(21);
  let n = twice(&c);
  free(c) * 0 + n
-- answer: i32[42]

A mut borrow has no derived copy, so a second use of one is refused, as for an owned value.

What the checker refuses

The owner can’t be used while it is lent:

main -> i32 =
  let c = alloc(5);
  let n = borrow mut c { m -> free(c) };
  n
-- expect: 3:11: `c` is used twice here, and its type `ref i32` is linear

and a borrow can’t outlive its lend: a call whose result mentions the lent place’s lifetime can’t hand the place back.

fn keep<'a>(r: imm 'a i32) -> imm 'a i32 = r

main -> i32 =
  let c = alloc(5);
  let r = keep(&c);
  free(c)
-- expect: 5:11: the call's result mentions the lifetime of the lent place, so the place cannot be handed back after it

Any number of imm borrows of a place may be live at once, and a mut borrow is exclusive, so two &mut of one place are never live together. Lifetimes are lexical, as Rust’s were before non-lexical lifetimes: a borrow lasts for its call or its block.

Recursive data is copied only when you say so

A list of integers holds no resource, so it can be copied, but copying it allocates every node, so it’s like a Rust type that is Clone but not Copy. Where a use would copy recursive data, the copy is written clone(x); without it, the second use is an error that says so:

include list

main -> i32 =
  let xs = cons(1, cons(2, nil()));
  let a = with on_exhausted(!{ u -> 0 }) { fold(xs, 0, !{ (s, x) -> s + x }) };
  let b = with on_exhausted(!{ u -> 0 }) { fold(xs, 0, !{ (s, x) -> s + x }) };
  a + b
-- expect: 5:49: `xs` is used again at 6:49, so this use copies it, and its type `mu X. 1 + i32 * X` holds recursive data: the copy allocates every node. Write `clone(xs)` to copy it here, or do not use `xs` after this

Writing fold(clone(xs), …) in the first call makes it run. An i32 or a pair of them is copied as a few words, and needs nothing written. (List, fold and on_exhausted are the next chapter’s.)

Lifetimes in signatures

A function that takes a borrow names its lifetime, fn f<'a>(r: imm 'a A), and a result that holds part of the borrow mentions it, as Rust’s do. A view of an array element, for example, lives as long as the view of the array it came from:

fn get[A]<'a>(v: array_imm 'a A, i: i32) -> imm 'a A + 1

Lifetimes are not elided in signatures. Inside a body they are inferred, except where a borrow block’s lifetime must be named (above).

A lifetime parameter can be declared shorter than another, fn f<'x, 'w < 'x>(…), for a result that must not outlive a borrow it was made from. main runs under a lifetime of its own, 'main, which lasts for its whole body; a call that needs a lifetime its arguments don’t give gets the innermost one in scope, and f['main](…) passes main’s by name. A generic function can require that a type argument outlive one of its lifetimes, as in Rust: fn hold[S]<'c>(s: S) -> … where S: 'c.

Data and generics

This chapter covers the data a program builds: recursive types such as lists and trees, the folds that walk them, arrays, vectors and strings, and the generic code over them: poly families, operators at your own types, and the hash map and set.

Recursive data

A data declaration may mention itself. A binary tree is a leaf, or a node with two subtrees and a value:

include textio

data Tree = Leaf | Node(left: Tree, val: i32, right: Tree)

fn branch(l: Tree, v: i32, r: Tree) -> Tree = box Node(l, v, r)

-- The sum of the values; consumes the tree.
fn sum(t: Tree) -> i32 = fold_own t { Leaf -> 0 | box Node(l, v, r) -> l + v + r }

main -> 1 =
  let t = branch(branch(Leaf, 1, Leaf), 2, branch(Leaf, 3, Leaf));
  print_dec(sum(t));
  print_byte(b'\n')
-- output: 6

A node holds a tree, so it has to live on the heap, and you say so: box Node(l, v, r) allocates it, where Rust would write Box::new. Nothing else allocates. Cases that hold no tree, like Leaf, need no box.

fold_own walks the tree bottom up. In the Node arm, l and r are not subtrees but the fold’s answers for them, here their sums, and the pattern box Node(…) frees each node as the fold passes it, so the run ends with nothing allocated.

Folds

A fold walks recursive data bottom-up: each arm sees a node with its subtrees already folded. There are three, one for each way of holding the data:

include textio

data Tree = Leaf | Node(left: Tree, val: i32, right: Tree)

fn branch(l: Tree, v: i32, r: Tree) -> Tree = box Node(l, v, r)

-- Reads the tree through a borrow: `v` is a view of the node's value.
fn sum<'a>(t: imm 'a Tree) -> i32 = fold_imm t { Leaf -> 0 | Node(l, v, r) -> l + *v + r }

-- The largest value; consumes the tree.
fn largest(t: Tree) -> i32 =
  fold_own t {
    Leaf -> 0
  | box Node(l, v, r) -> if l > v && l > r { l } else if r > v { r } else { v }
  }

main -> 1 =
  let t = branch(branch(Leaf, 1, Leaf), 7, branch(Leaf, 3, Leaf));
  let s = sum(&t);
  print_dec(s);
  print_byte(b' ');
  print_dec(largest(t));
  print_byte(b'\n')
-- output: 11 7

Folds work on generic data too:

include textio

data List[T] = Nil | Cons(head: T, tail: List[T])

fn cons[T](x: T, rest: List[T]) -> List[T] = box Cons(x, rest)

fn len[T]<'a>(l: imm 'a List[T]) -> i32 = fold_imm l { Nil -> 0 | Cons(_, rest) -> 1 + rest }

fn first[T](l: List[T]) -> Option[T] = match l { Nil -> None | box Cons(x, rest) -> Some(x) }

main -> 1 =
  let xs = cons(1, cons(2, cons(3, Nil)));
  let n = len(&xs);
  print_dec(n);
  print_byte(b' ');
  match first(xs) { Some(x) -> print_dec(x) | None -> print_lit("empty") };
  print_byte(b'\n')
-- output: 3 1

first keeps the head and consumes the rest of the list, which the compiler frees.

Collections of recursive data

Vec[T], the prelude’s growable vector (below), holds recursive data like any other value, and a type may hold a vector of itself with no box: the vector’s storage is already on the heap. A rose tree, Rust’s struct Tree { val: i32, kids: Vec<Tree> }, is

include textio
include rec

data Tree = Tree(val: i32, kids: Vec[Tree])

-- A node with no children: an empty vector, which allocates nothing.
fn tip(n: i32) -> Tree = Tree(n, box buf[Tree](0))

-- `t` added as the last child of `p`.
fn adopt(p: Tree, t: Tree) -> Tree =
  match p { Tree(n, kids) -> push(&mut kids, t); Tree(n, kids) }

-- The sum of the values, consuming the tree: each child taken out of its vector.
fn sum(t: Tree) -> i32 =
  match t {
    Tree(v, kids) ->
      let n = len_of(&kids);
      let mut s = v;
      for i in 0..n {
        let child = take(&mut kids, i);
        match child { Some(c) -> s = s + sum(c) | None -> () }
      };
      s
  }

main -> 1 =
  let t = adopt(adopt(tip(10), tip(1)), adopt(tip(2), tip(3)));
  print_dec(with on_exhausted(!{ u -> 0 - 1 }) { sum(t) });
  print_byte(b'\n')
-- output: 16

take(&mut kids, i) moves element i out, leaving an empty node in its place. sum calls itself, which is what on_exhausted is for (Recursion, next). A node with a fixed number of children can hold an array of itself in the same way, data Tree = Tip(i32) | Node(i32, array Tree), and a trie node is data Trie = Trie(bool, Vec[Option[Trie]]). A map can hold the type too, as a JSON value’s object does: data Json = Null | Num(i32) | Obj(Map[string, Json]) (Maps and sets).

Recursion

A function that calls itself runs with a budget of depth, 10000 levels, instead of an unbounded stack. When the budget runs out the recursion raises an error, Exhausted, which unwinds every level, freeing what each held, like any other error. The compiler checks that something handles it, and include rec has the two handlers:

• with on_exhausted(f) { … } answers f(()) if the budget runs out, so f is a closure that ignores its argument: !{ u -> 0 - 1 } answers −1;
• with deep { … } keeps the pending calls on the heap instead of the stack, so the recursion is limited only by memory.

include textio
include rec

fn down(n: i32) -> i32 = if n == 0 { 0 } else { 1 + down(n - 1) }

main -> 1 =
  print_dec(with on_exhausted(!{ u -> 0 - 1 }) { down(500) });
  print_byte(b' ');
  print_dec(with on_exhausted(!{ u -> 0 - 1 }) { down(20000) });
  print_byte(b'\n')
-- output: 500 -1

down(20000) is deeper than the budget, so its answer is −1. with deep { down(20000) } would run it to the end. A fold doesn’t count as recursion and needs no handler.

Functions declared one after the other may call each other, as even calling odd and odd calling even, and a recursion may be generic. Each use at new types is compiled as its own copy of the recursion:

include textio
include rec

data List[T] = Nil | Cons(head: T, tail: List[T])

fn cons[T](x: T, rest: List[T]) -> List[T] = box Cons(x, rest)

fn map[A, B](l: List[A], f: !(A => B)) -> List[B] =
  match l { Nil -> Nil | box Cons(x, rest) -> cons(f(x), map(rest, f)) }

fn sum(l: List[i32]) -> i32 = fold_own l { Nil -> 0 | box Cons(x, rest) -> x + rest }

main -> 1 =
  let xs = cons(1, cons(2, cons(3, Nil)));
  let ys = with on_exhausted(!{ u -> Nil }) { map(xs, !{ x -> x * x }) };
  print_dec(sum(ys));
  print_byte(b'\n')
-- output: 14

include list has a ready-made generic List[A] with nil(), cons(x, xs), map, filter and fold.

Layers

A layer wraps every call a recursion makes of itself, without touching the recursive function. It is a generic function of the call and its argument, and with L { … } applies it to the recursions in the block. Here a layer counts the calls of fib:

include textio
include rec

effect Count { fn tick() -> i32 }

handler count(mut n: i32): Count = { tick() = { n = n + 1; n } }

fn counted[A, B](call: !(A => B), a: A) -> B = tick(); call(a)

fn fib(n: i32) -> i32 = if n < 2 { n } else { fib(n - 1) + fib(n - 2) }

main -> 1 =
  let c = alloc(0);
  let f = with count(&mut c) { with counted { with on_exhausted(!{ u -> 0 - 1 }) { fib(10) } } };
  print_dec(f);
  print_lit(" after ");
  print_dec(free(c));
  print_lit(" calls\n")
-- output: 55 after 176 calls

fib(10) makes 176 calls of itself, each counted; the first call, from outside, is not. The same shape gives tracing or a step limit. Effects and handlers (effect, handler, with) are their own chapter.

Arrays

array A owns n cells, n known when the program runs. array_new[A](n, f) makes one, with f(i) at index i. An array is owned, so it is lent to be read:

• at(&a, i, d) copies element i, or answers d when i is out of range;
• borrow imm a { v -> … } lends the whole array as a view, array_imm 'a A, and borrow mut a { v -> … } as a mutable one, array_mut 'a A;
• a for over a view visits each element’s borrow, read with *p.

include slice has the view operations, as Rust’s slice methods: len, get, set, swap_at, split_at, reverse, fill, find, binary_search, sort, and their _mut forms.

include textio
include slice

fn sum<'a>(v: array_imm 'a i32) -> i32 =
  let mut s = 0;
  for p in v { s = s + *p };
  s

fn scramble(i: i32) -> i32 = (i * 7) % 5

main -> 1 =
  let a = array_new[i32](5, scramble);
  let s = borrow imm a { v -> sum(v) };
  borrow mut a { v -> let v = sort(v, cmp_i32, 0); discard_mut(v) };
  let lo = at(&a, 0, 0);
  let hi = at(&a, 4, 0);
  print_dec(s);
  print_lit(", from ");
  print_dec(lo);
  print_lit(" to ");
  print_dec(hi);
  print_byte(b'\n')
-- output: 10, from 0 to 4

A function that changes a view hands its array_mut back, so a block that sorts in place ends with discard_mut(v), which ends the view. A view can be split at a run-time index into two views of the same elements (split_at, split_at_mut), as Rust’s split_at_mut is, so a quicksort sorts each half in place with no allocation per element.

Buffers and strings

buf A is a growable array, include buf, and Vec[T] is the prelude’s name for one: data Vec[T] = Vec(buf T), and every buffer function works on a Vec. box buf[A](cap) allocates one with room for cap elements (box buf[A](0) allocates nothing until the first push), push(&mut v, x) appends, pop(&mut v) takes the last as an Option, take(&mut v, i) moves element i out, and len_of(&v) is the length. A buffer lends its elements as a view, as an array does, so get, set and the rest of include slice index it:

include textio
include slice

fn sum<'a>(v: array_imm 'a i32) -> i32 = let mut s = 0; for p in v { s = s + *p }; s

main -> 1 =
  let mut v: Vec[i32] = box buf[i32](2);
  for i in 0..5 { push(&mut v, i * i) };
  let n = len_of(&v);
  let s = borrow imm v { w -> sum(w) };
  borrow mut v { w -> let w = set(w, 0, 100); discard_mut(w) };
  let first = borrow imm v { w -> at(w, 0, 0) };
  print_dec(n);
  print_byte(b' ');
  print_dec(s);
  print_byte(b' ');
  print_dec(first);
  print_byte(b'\n')
-- output: 5 30 100

A buffer’s spare capacity holds placeholder elements, so its element type must have one: numbers, views, arrays, buffers, and data built from them do, but a heap cell ref A doesn’t, and buf[ref i32] is refused.

string is a buffer of UTF-8 bytes, and text 'a a view of some (include textio, which brings include text and the I/O helpers). box string(cap) makes one; push_lit(&mut s, "…"), push_dec(&mut s, n) and push_char(&mut s, 'c') append. A string literal "…" is data the program owns no copy of. Text views are cut without copying (split_once, trim, next_line, fold_lines), eq_lit(t, "…") compares one with a literal, and parse_i32 reads a number, raising on bad input (Errors).

include textio

fn point(x: i32, y: i32) -> string =
  let mut s = box string(16);
  push_lit(&mut s, "(");
  push_dec(&mut s, x);
  push_lit(&mut s, ", ");
  push_dec(&mut s, y);
  push_char(&mut s, ')');
  s

main -> 1 =
  let s = point(3, 0 - 4);
  let n = len_of(&s);
  borrow imm s { t -> print_str(t) };
  print_lit(" is ");
  print_dec(n);
  print_lit(" bytes\n")
-- output: (3, -4) is 7 bytes

poly families

A generic function fn f[T](…) has one body for every T. A family has one body per type, chosen by the type, as a Rust trait with one method is. It is declared by its signature with no body, and each poly f at H = … gives its case at a type H:

include textio

poly weight[T](x: T) -> i32

poly weight at i32 = x
poly weight at bool = if x { 1 } else { 0 }
poly weight[A, B] at A * B = let (a, b) = x; weight(a) + weight(b)

main -> 1 =
  print_dec(weight((40, (true, true))));
  print_byte(b'\n')
-- output: 42

A call picks the case from its argument’s type, at compile time; a case may itself be generic, as the one at A * B is, and calls the family at the parts. The rules keep the choice a function of the type:

• One case per type. A second case at the same type is an error, never resolved by order.
• The most specific case wins, and two cases that overlap with neither more specific are an error.
• A type with no case is an error at the call that needs it.

A family’s cases are global to the program.

Operators at your own types

+, -, *, ==, !=, <, <=, > and >= are families too. At the integer and float types they are the machine instructions. At any other type, a program gives a case, poly (+) at H = …, whose parameters are a and b:

include textio

data Complex = C(re: i32, im: i32)

poly (+) at Complex =
  match (a, b) { (C(ar, ai), C(br, bi)) -> C(ar + br, ai + bi) }

poly (*) at Complex =
  match (a, b) { (C(ar, ai), C(br, bi)) -> C(ar * br - ai * bi, ar * bi + ai * br) }

-- `x₁·y₁ + x₂·y₂`, at any type with `+` and `*`.
fn dot[T](x: T * T, y: T * T) -> T =
  let (x1, x2) = x;
  let (y1, y2) = y;
  x1 * y1 + x2 * y2

main -> 1 =
  print_dec(dot((1, 2), (3, 4)));
  print_byte(b'\n');
  match dot((C(1, 2), C(1, 1)), (C(3, 4), C(0 - 1, 3))) {
    C(re, im) -> print_dec(re); print_lit(" + "); print_dec(im); print_lit("i\n")
  }
-- output: 11
-- output: -9 + 12i

dot at i32 is compiled with the machine’s mul and add; at Complex with the cases above. A different arithmetic is a different type, never a different scope. Give the type a data declaration, as here: a type name is only an alias, so a case at type Complex = i32 * i32 would be a case at every pair of i32s.

Equality, hashing and order

include key declares the families a map uses: equal, hash and order, each taking its operands as views so that a key is read where it is stored. They have cases at the integers, 1, tuples, sums, arrays and buffers (so bool, string and text are covered), compared structurally. == and equal are separate families: a float has ==, IEEE 754’s, and no equal, so a float is not a map key.

Maps and sets

include map is a hash map, Map[K, V], and a set, Set[K]. A map is a value: it is lent to each operation, and an operation that changes it takes it &mut. map in the standard library lists every operation.

Counting the letters of a word:

include textio
include map

-- How often each byte of `t` occurs.
fn tally<'t>(t: text 't) -> Map[u8, i32] =
  let mut counts = map_new[u8, i32](16);
  for p in t {
    let c = *p;
    let old = map_lookup(&counts, c);
    let n = match old { Some(n) -> n + 1 | None -> 1 };
    map_insert(&mut counts, c, n)
  };
  counts

main -> 1 =
  let counts = borrow imm "mississippi" { t -> tally(t) };
  let kinds = map_len(&counts);
  print_dec(kinds);
  print_lit(" letters:");
  borrow imm counts { 'x, r ->
    for e in map_iter(r) { let (k, v) = e; print_byte(b' '); print_byte(k); print_dec(*v) } };
  print_byte(b'\n')
-- output: 4 letters: s4 p2 m1 i4

borrow imm m { 'x, r -> … } lends the map’s entries: map_iter(r) visits every entry, each value as a view, and map_get(r, k) answers a view of one value in place, so values that aren’t copyable, such as vectors, are read without copying. While the map is lent it can’t change. The hash is deterministic, so the order of iteration is the same on every run. map_iter copies each key out, so its keys are integers or views; map_entries(r) lends each key as well, imm 'k K, for keys such as strings, and map_drain(m) consumes the map, each entry taken out as an owned pair.

Errors

An error is raised with raise(e) and handled with with h { … } around the code that may raise it. There is one model: no Result type threaded by hand, no ?, no exceptions separate from the rest of the language. raise is an operation of an ordinary effect, Fail[E], and its handlers are ordinary handlers (Effects and handlers has the general mechanism).

Raising and handling

include fail declares the effect and three handlers:

A function that raises says so after its result type, with Fail[E], and a function that calls one that raises raises too, with nothing written: its row, the effects it may perform, is inferred. A call of a function that raises needs no ?: the error goes on by itself to the nearest handler.

include textio
include fail

-- The sum of the elements; a negative one raises its index.
fn checked<'a>(v: array_imm 'a i32) -> i32 with Fail[i32] =
  let mut s = 0;
  let mut i = 0;
  for p in v { let x = *p; if x < 0 { raise(i) }; s = s + x; i = i + 1 };
  s

-- A function that calls one that raises raises too: its row is inferred.
fn twice<'a>(v: array_imm 'a i32) -> i32 = checked(v) * 2

fn report(r: i32 + i32) -> 1 =
  match r {
    inl n -> print_lit("sum "); print_dec(n)
  | inr i -> print_lit("negative at "); print_dec(i)
  };
  print_byte(b'\n')

fn good(i: i32) -> i32 = i * 10
fn bad(i: i32) -> i32 = if i == 2 { 0 - 1 } else { i }

main -> 1 =
  let a = array_new[i32](3, good);
  let b = array_new[i32](3, bad);
  let x = borrow imm a { v -> with to_result { twice(v) } };
  let y = borrow imm b { v -> with to_result { twice(v) } };
  let z = borrow imm b { v -> with default(0) { twice(v) } };
  report(x);
  report(y);
  print_dec(z);
  print_byte(b'\n')
-- output: sum 60
-- output: negative at 2
-- output: 0

A raise that no handler can reach is a compile-time error naming the function that performs it (`f` performs `Fail`, but no handler of `Fail` is in scope here): an error never escapes main unnoticed. The one exception is division, below.

If you do write the row, the compiler holds you to it: performing an effect the row leaves out is an error. A row may also give the error’s type where nothing else does.

What happens to values when an error leaves

An error unwinds: what the code it leaves owned is freed by its derived consumes, and every borrow it was inside ends, the place going back to its owner. Here the cell that checked holds when it raises is freed on the way out, and the run ends with nothing live:

include textio
include fail

-- Holds a cell while it checks `x`; an error frees the cell by its consume.
fn checked(x: i32) -> i32 with Fail[i32] =
  let c = alloc(x * 10);
  if x < 0 { raise(x) };
  free(c)

main -> 1 =
  print_dec(with default(0) { checked(4) });
  print_byte(b' ');
  print_dec(with default(0) { checked(0 - 3) });
  print_byte(b'\n')
-- output: 40 0

A value that is not consumable (a capability, a one-shot closure that must be called, a must_close value) can’t be live where an error may leave, and the checker names it (What an abort does). An error’s payload is plain data, borrows or ! values.

The handler of Fail is a handler like any other, so it can be written for a purpose. to_result itself is

effect Fail[E] { ctl raise(e: E) -> never }

handler to_result[E, A]: Fail[E], A -> A + E = {
  return(a) = inl a;
  raise(e) = inr e
}

ctl raise(e: E) -> never declares an operation that never returns to its caller (it answers the empty type never), so the handler’s clause receives only the error.

Errors of several types

A function may raise errors of several types: Fail[i32] and Fail[ParseError] are two instances of Fail, each handled by the innermost handler of its own instance, whatever the order of the handlers. The library’s parsers raise their own error types: parse_i32 raises a ParseError (include text), which says why the text isn’t a number: inl () when it has no digits, inr (inl b) for a byte b that isn’t a digit, and inr (inr ()) for a number too large for an i32.

include textio

-- The two numbers of `"a b"`, added.
fn parse_sum<'t>(t: text 't) -> i32 with Fail[ParseError] =
  match split_once(t, b' ') {
    inl (a, b) -> parse_i32(a) + parse_i32(b)
  | inr t -> parse_i32(t)
  }

fn show(s: string) -> 1 =
  let r = borrow imm s { t -> with to_result { parse_sum(t) } };
  match r {
    inl n -> print_dec(n)
  | inr (inl u) -> print_lit("no digits")
  | inr (inr (inl b)) -> print_lit("not a digit: "); print_byte(b)
  | inr (inr (inr u)) -> print_lit("too large")
  };
  print_byte(b'\n')

main -> 1 =
  show(string_of_lit("12 30"));
  show(string_of_lit("12 x7"))
-- output: 42
-- output: not a digit: x

Several instances, and names shows two instances in one row, and two handlers of one instance told apart by name.

Division

a / b and a % b at i32, i64 and u8 truncate toward zero, the remainder taking the dividend’s sign.

Dividing by zero, or MIN / -1 at a signed width, raises Fail[DivError]. Its two values are div_by_zero and div_overflow. It’s an ordinary Fail, so to_result, default and map_err handle it, and a function can raise its own Fail[E] and divide too. Dividing by a nonzero literal can’t fail and needs no handler. checked_div and checked_rem return an Option-like sum instead. The Euclidean forms, div_euclid and rem_euclid, come with include arith (arith).

include textio

fn mean(sum: i32, n: i32) -> i32 = sum / n

main -> 1 =
  print_dec(with default(0) { mean(7, 0) });
  print_byte(b' ');
  match with to_result { mean(9, 3) } {
    inl m -> print_dec(m)
  | inr e -> print_lit("no mean")
  };
  print_byte(b' ');
  print_dec((0 - 7) / 2);
  print_byte(b'\n')
-- output: 0 3 -3

A division error that reaches main unhandled is not a compile-time error, so that arithmetic reads as it does elsewhere: the program unwinds, writes error: division by zero on standard error, and exits with status 1, after freeing what it held.

main -> i32 = let n = 0; 10 / n

Input and output

Standard input, standard output, standard error, the clock and the command-line arguments are each an effect, and their operations are called like ordinary functions. main gets them for free. Any other function gets them from its caller, and its row (the list of effects it performs) says which ones it uses. You usually don’t write the row, since it’s inferred, but you can (with Stdout).

That gives you two things. A function’s signature tells you what it can touch. And a test can serve the same effect with a handler of its own, say a fake stdout that collects into a string.

The effects

The operations work on bytes and byte views. Text and numbers are library code on top:

• include io adds print_dec, print_dec64, eprint_dec and ns_of_ms;
• include textio adds print_lit("…"), print_str(t) for a text view, eprint_lit, read_input() (the whole input as a string), next_arg(s) (the next argument appended to a string, and whether there was one) and print_string(s), which prints an owned string and hands it back so you can keep using it.

Standard library lists all of them.

include textio

main -> 1 = print_lit("Hello, world!\n")
-- output: Hello, world!

Functions that do I/O

In main, an operation that no with handles goes to the platform: the operating system’s streams, clock and arguments, under WebAssembly and natively alike. Every other function just performs its effects, and whoever calls it provides them. This one can write to standard output and nothing else:

include textio

-- A report, written to whatever serves `Stdout`.
fn report(lines: i32, bytes: i32) -> 1 with Stdout =
  print_lit("lines ");
  print_dec(lines);
  print_lit(", bytes ");
  print_dec(bytes);
  print_byte(b'\n')

main -> 1 =
  let s = read_input();
  let bytes = len_of(&s);
  let lines = borrow imm s { t -> fold_lines(t, !{ (l, n) -> n + 1 }, 0) };
  report(lines, bytes)
-- stdin: one
-- stdin: two
-- stdin: three
-- output: lines 3, bytes 14

with Stdout is optional here: the row is inferred from print_lit. If you write it, the checker holds you to it, and a function that performs an effect its row leaves out is rejected. A function with no effects does no I/O. That’s guaranteed, not a convention (Safety guarantees).

Serving an effect yourself

A handler of Stdout is an ordinary declaration. A test, or a program that wants the output in a string, can run report under a handler of its own. report itself doesn’t change:

include textio

fn report(lines: i32, bytes: i32) -> 1 with Stdout =
  print_lit("lines ");
  print_dec(lines);
  print_lit(", bytes ");
  print_dec(bytes);
  print_byte(b'\n')

-- A fake standard output: the bytes written, kept in a string.
handler collect(mut out: string): Stdout = {
  print_byte(b) = { push_byte(&mut out, b) };
  print_bytes(v) = { push_str(&mut out, v) }
}

main -> 1 =
  let c = alloc(box string(16));
  with collect(&mut c) { report(3, 14) };
  let s = free(c);
  print_lit("report wrote ");
  print_dec(len_of(&s));
  print_lit(" bytes\n")
-- output: report wrote 18 bytes

with collect(&mut c) { … } runs the block with collect serving Stdout. Its state is lent from the cell c, so afterwards c holds everything that was written. A fake clock or scripted input works the same way.

Reading input

input_byte() returns the next byte, or inr () at the end. A loop over it runs as long as the input does, so it’s a while:

include textio

-- Upper-cases its input until the input ends; the number of bytes.
fn shout() -> i32 =
  let mut n = 0;
  let mut more = true;
  while more {
    match input_byte() {
      inl b -> if b >= b'a' && b <= b'z' { print_byte(b - 32) } else { print_byte(b) }; n = n + 1
    | inr u -> more = false
    }
  };
  n

main -> 1 =
  let n = shout();
  print_dec(n);
  print_lit(" bytes\n")
-- stdin: Hi there
-- output: HI THERE
-- output: 9 bytes

For text, read_input() reads the whole input into a string, and the text functions cut it into lines and fields without copying: fold_lines, next_line, split_once, trim. Here each line is a number, and a line that isn’t one is skipped and counted:

include textio

-- One line added to the running sum, or counted as skipped if it isn't a number.
fn add_line<'a>(line: text 'a, acc: i32 * i32) -> i32 * i32 =
  let (sum, skipped) = acc;
  match with to_result { parse_i32(line) } {
    inl n -> (sum + n, skipped)
  | inr e -> (sum, skipped + 1)
  }

main -> 1 =
  let s = read_input();
  let r = borrow imm s { t -> fold_lines(t, !{ (l, acc) -> add_line(l, acc) }, (0, 0)) };
  let (sum, skipped) = r;
  print_dec(sum);
  print_lit(" (");
  print_dec(skipped);
  print_lit(" skipped)\n")
-- stdin: 10
-- stdin: 20
-- stdin: abc
-- stdin: 12
-- output: 42 (1 skipped)

eprint_lit and eprint_dec write to standard error the same way.

The clock and the arguments

now() is the monotonic clock in nanoseconds, as an i64. sleep(ns) waits at least that long. Times saturate rather than wrap.

include textio

main -> 1 =
  let t0 = now();
  sleep(ns_of_ms(2));
  let t1 = now();
  if t1 - t0 >= ns_of_ms(2) { print_lit("slept\n") } else { print_lit("woke early\n") }
-- output: slept

The arguments come as one stream of bytes. next_arg reads the next one into a string:

include textio

-- Writes each argument on a line of its own, numbered; the number of arguments.
fn echo() -> i32 =
  let mut n = 0;
  let mut more = true;
  while more {
    let (s, got) = next_arg(box string(16));
    if got {
      n = n + 1;
      print_dec(n);
      print_byte(b' ');
      let s = print_string(s);
      print_byte(b'\n')
    } else { more = false }
  };
  n

main -> 1 = let n = echo(); ()

bcc run prog.bc alpha beta passes alpha and beta; bcc interp prog.bc -- alpha beta does the same in the interpreter.

Iteration

There are three kinds of loop. A for over data (a range of integers, an array, a view) runs once per element and always finishes. A while or loop may run forever. A for over a generator runs its body once for each value the generator yields. The compiler tells the first kind apart from the other two, and that’s how it knows which functions terminate.

for over data

for x in a..b counts from a up to b - 1. A for over an array or a view visits its elements, and the source’s type decides how, much like Rust’s IntoIterator:

• over an owned array, the elements are copied out and the array is consumed after the loop;
• over &a, each element is lent imm and you keep the array;
• over &mut a, each element is lent mut, so the loop can change it in place;
• over a view, each of its elements is lent.

include textio

fn tab(i: i32) -> i32 = (i + 1) * 10

main -> 1 =
  let mut a = array_new[i32](5, tab);
  let first = for x in &a { let v = *x; if v > 25 { break v } } else { 0 };
  let mut odd = 0;
  for i in 0..10 { if i % 2 == 0 { continue }; odd = odd + i };
  for p in &mut a { modify p { v -> v + 1 } };
  let mut sum = 0;
  for x in a { sum = sum + x };
  print_dec(first);
  print_byte(b' ');
  print_dec(odd);
  print_byte(b' ');
  print_dec(sum);
  print_byte(b'\n')
-- output: 30 25 155

• break leaves the loop, and break v leaves it with the loop’s value v; else { e } after the loop gives the value when the source ends without a break.
• continue goes on to the next element.
• return e returns from the enclosing function.
• A let mut variable assigned in the body is carried from one turn to the next and is there after the loop.

Over an array of records lent &mut, a field is assigned directly: for p in &mut particles { p.x = p.x + p.v }.

Loops that may not end

while c { … } and loop { … } may run forever, so a function containing one is div: it may diverge. You never write this; it’s inferred, and it spreads like any other effect, so a function that calls a div function is div too. If you want a guarantee that a function terminates, mark it total and the compiler checks it:

include textio

total fn sum_to(n: i32) -> i32 =
  let mut s = 0;
  for i in 0..n { s = s + i };
  s

main -> 1 =
  print_dec(sum_to(10));
  print_byte(b'\n')
-- output: 45

A total fn with a while is rejected:

total fn spin(n: i32) -> i32 =
  let mut i = 0;
  while i < n { i = i + 1 };
  i

main -> i32 = spin(3)
-- expect: 3:3: `spin` is declared `total`, but it has a `while` (SPEC §14)

div_fuel(e, n) runs a div computation for at most n steps: it answers inl the value if e finished in time, and inr () if not. Code that runs a loop this way is total again. Nobody knows whether the Collatz loop always reaches 1, so collatz is div, but a bounded run of it is total:

include textio

fn collatz(n: i32) -> i32 =
  let mut x = n;
  let mut steps = 0;
  while x != 1 {
    if x % 2 == 0 { x = x / 2 } else { x = 3 * x + 1 };
    steps = steps + 1
  };
  steps

total fn collatz_within(n: i32, fuel: i32) -> Option[i32] =
  match div_fuel(collatz(n), fuel) { inl s -> Some(s) | inr u -> None }

fn show(r: Option[i32]) -> 1 =
  match r { Some(s) -> print_dec(s) | None -> print_lit("gave up") };
  print_byte(b'\n')

main -> 1 =
  show(collatz_within(27, 200));
  show(collatz_within(27, 50))
-- output: 111
-- output: gave up

A higher-order function written with a total callback in mind works with a div one too: the compiler makes a copy of it for the div callback, and that copy is div. Functions don’t come in two colours.

Generators

A generator is a function that yields a sequence of values and then returns. Yielding is an ordinary effect, Yield[T], from the library (include yield), with one operation, yield(x: T). A for over a call of such a function handles the effect: its body runs at each yield, with the yielded value. for x in lo..hi is a counted loop rather than a generator, so the examples below write a small range generator where they need one.

include textio
include yield

fn range(lo: i32, hi: i32) -> 1 with Yield[i32] =
  let mut i = lo;
  while i < hi { yield(i); i = i + 1 };
  ()

fn squares(lo: i32, hi: i32) -> 1 with Yield[i32] =
  for x in range(lo, hi) { yield(x * x) };
  ()

main -> 1 =
  for x in squares(1, 5) { print_dec(x); print_byte(b'\n') }
-- output: 1
-- output: 4
-- output: 9
-- output: 16

The for is a handler of Yield (see Effects), and its body is the handler’s clause: each yield is a direct call of the body, so the program allocates nothing.

A for over a generator that loops is div; over one that doesn’t, it’s total. A for over data whose body yields counts as a looping generator, so squares is div.

Leaving early: break and return

break in a for’s body stops the generator, and anything the generator owns is consumed. return e returns from the function around the loop. Inside a generator, break leaves the innermost loop, and return ends the generator from any depth.

include textio
include yield

fn range(lo: i32, hi: i32) -> 1 with Yield[i32] =
  let mut i = lo;
  while i < hi { yield(i); i = i + 1 };
  ()

-- The first square above `k`.
fn first_square_above(k: i32) -> i32 =
  for x in range(1, 100) { if x * x > k { return x * x } };
  0

main -> 1 =
  let mut acc = 0;
  for x in range(1, 100) { if x > 4 { break }; acc = acc + x };
  print_dec(acc);
  print_byte(b' ');
  print_dec(first_square_above(50));
  print_byte(b'\n')
-- output: 10 64

The value of a loop

A generator returns a value, and let r = for x in g(…) { … }; keeps it, or keeps e after a break e:

include textio
include yield

-- Yields the decimal digits of `n`, last first, and returns how many there were.
fn digits(n: i32) -> i32 with Yield[i32] =
  let mut x = n;
  let mut k = 0;
  while x > 0 { yield(x % 10); x = x / 10; k = k + 1 };
  k

main -> 1 =
  let k = for d in digits(4096) { print_dec(d) };
  print_lit(" has ");
  print_dec(k);
  print_lit(" digits\n")
-- output: 6904 has 4 digits

A generator that calls another passes on whatever the callee yields, then carries on with what it returns: let n = digits(x); yield(n) inside a generator yields the digits and then their count.

Stored generators

Pass a generator call where a stored generator is expected, as in take(10, fib()) below or let g: U (pull i32 0 1) = fib();, and you get the generator as a value instead of running it. In U (pull A B R), A is what it yields, B what it returns when it finishes (0 for one that never does), and R what closing it early gives back, usually 1. Nothing runs until you ask for the next item; each request runs it to its next yield, and closing it cancels the rest. A for over a stored generator pulls from it until it returns. This is how you write adapters like take:

include textio
include yield

fn fib() -> 0 with Yield[i32] =
  let mut a = 0;
  let mut b = 1;
  loop {
    yield(a);
    let c = a + b;
    a = b;
    b = c
  }

fn take(n: i32, it: U (pull i32 0 1)) -> 1 with Yield[i32] =
  let mut i = 0;
  for x in it {
    if i < n { yield(x); i = i + 1 } else { break }
  };
  ()

main -> 1 =
  for x in take(6, fib()) { print_dec(x); print_byte(b'\n') }
-- output: 0
-- output: 1
-- output: 1
-- output: 2
-- output: 3
-- output: 5

include adapters gives you the usual ones (map, filter, take, skip, enumerate, chain, flat_map, take_until, scan, zip, chunks, lines, batch), all generic generators over stored generators, so a pipeline is just calls:

include textio
include adapters

fn range(lo: i32, hi: i32) -> 1 with Yield[i32] =
  let mut i = lo;
  while i < hi { yield(i); i = i + 1 };
  ()

fn times(p: i32 * i32) -> i32 = let (i, x) = p; i * x
fn even(x: i32) -> bool = x % 2 == 0

main -> 1 =
  let mut acc = 0;
  for y in take(filter(map(enumerate(range(10, 1000)), times), even), 5) { acc = acc + y };
  print_dec(acc);
  print_byte(b'\n')
-- output: 320

Pipelines

e |> f(a, …) is f(e, a, …): the value on the left becomes the first argument of the call on the right, so a chain of adapters reads left to right. The adapters are listed in adapters.

include textio
include adapters

fn range(lo: i32, hi: i32) -> 1 with Yield[i32] =
  let mut i = lo;
  while i < hi { yield(i); i = i + 1 };
  ()

main -> 1 =
  let mut b = 0;
  for y in range(0, 10) |> map(!{ x -> x * x }) |> filter(!{ x -> x > 5 }) |> take(3) {
    b = b + y
  };
  print_dec(b);
  print_byte(b'\n')
-- output: 50

|> into a handler is with: e |> to_result is with to_result { e } (Effects and handlers).

Borrows and loops

A borrow block around a loop is free: the loop body can use the borrow at every step. What the loop carries from one step to the next can’t hold the borrow, though, so a generator that takes the borrow as an argument can’t run in a for inside the block; the checker says which iterator holds it. A borrow held across a yield is not implemented yet (Status). Until it is, give the generator the data it owns (a literal is persistent, so it can simply be passed), have it hand the data back when it finishes, or iterate by index with a counted for.

Effects and handlers

An effect is a set of operations. A handler gives each operation a meaning, and with h { … } runs a block with h handling the effect. You call an operation like a function. Errors (Errors), I/O (Input and output), generators (Iteration) and tasks (Async tasks) are all effects of this one kind, declared in the library. This chapter covers the mechanism they share.

There are no coloured functions. A function that performs an effect is called like any other. Its row (the effects it performs) is inferred, and the handler around the call serves them.

Answering operations

An operation declared fn answers its caller straight away. Its handler can keep state in a mut parameter, which each clause can read and assign:

include textio

effect Counter { fn tick() -> i32 }

handler count(mut n: i32): Counter = { tick() = { n = n + 1; n } }

main -> 1 =
  let r = with count(0) { let a = tick(); let b = tick(); a * 10 + b };
  print_dec(r);
  print_byte(b'\n')
-- output: 12

Inside a clause, the state (n here) behaves like a let mut variable, and the clause’s value is the operation’s answer. An operation that answers straight away compiles to a direct call of its clause.

Functions that perform effects

A function that calls an operation, or calls a function that does, has the effect in its row, which is inferred. It runs under whichever handler is in scope where it’s called. The compiler makes one copy of it per handler, the way a generic function gets one copy per type.

include textio
include slice

effect Log { fn note(x: i32) }

handler summed(mut s: i32): Log = { note(x) = { s = s + x; () } }
handler count(mut n: i32): Log = { note(x) = { n = n + 1; () } }

fn walk<'a>(v: array_imm 'a i32) -> 1 =
  for p in v { note(*p) };
  ()

main -> 1 =
  let a = array_new[i32](3, !{ i -> (i + 1) * 5 });
  let c = alloc(0);
  let t = alloc(0);
  borrow imm a { v -> with count(&mut c) { walk(v) } };
  borrow imm a { v -> with summed(&mut t) { walk(v) } };
  print_dec(free(c));
  print_lit(" notes, adding up to ");
  print_dec(free(t));
  print_byte(b'\n')
-- output: 3 notes, adding up to 30

with h(&mut c) { … } lends the state from a cell, and the cell holds the final state after the block. walk is compiled twice, once per handler, and each copy calls its handler’s clause directly.

You can write a row after the result type, fn f(…) -> T with Log, Fail[i32], and the checker holds the function to it.

Control operations and their continuation

An operation declared ctl is a control operation. Its clause receives the rest of the computation as a continuation k and decides whether and how to go on. k(v) resumes the body with v as the operation’s answer, and returns what the handler returns for the rest of the body. The declaration says how often k may be resumed:

A control handler names the type of the body it handles and what it returns (Watch, i32 -> i32 below), and its return(a) clause receives the body’s value. This handler resumes while the values are small and abandons the body at the first large one:

include textio

effect Watch { ctl watch(x: i32) -> bool }

-- Resumes with `true` while the value is small; at the first large one, stops the body there.
handler until_large: Watch, i32 -> i32 = {
  return(a) = a;
  watch(x, k) = if x < 100 { k(true) } else { 0 - x }
}

fn walk(n: i32) -> i32 =
  let c = alloc(0);
  let mut s = 0;
  for i in 0..n { if watch(i * i) { s = s + 1 } };
  s + free(c)

main -> 1 =
  print_dec(with until_large { walk(5) });
  print_byte(b' ');
  print_dec(with until_large { walk(20) });
  print_byte(b'\n')
-- output: 5 -100

When the clause doesn’t resume, the rest of walk is cancelled. The cell c it owns is freed, and the run ends with nothing allocated.

A clause runs once per operation, so anything it needs across calls lives in the handler’s state: its parameters (mut ones can be assigned) and any capabilities its clauses use.

include textio

effect Ask { ctl ask() -> i32 }

-- Answers each `ask` with the cell's content, which it then increments.
handler asking(mut c: ref i32): Ask, i32 -> i32 = {
  return(a) = a + free(c);
  ask(k) = { let v = free(c); c = alloc(v + 1); k(v) }
}

main -> 1 =
  print_dec(with asking(alloc(5)) { let x = ask(); let y = ask(); x * 10 + y });
  print_byte(b'\n')
-- output: 63

The two asks read 5 and 6, and the return clause adds the cell’s last content, 7.

An abort unwinds: whatever the code it leaves owned is freed by its derived consumes, and any borrow it was inside ends, so the place goes back to its owner. A value that is not consumable (a closure that must be called, a capability, a must_close value) can’t be live where an abort may leave, and the checker tells you which one it is (What an abort does).

Each operation goes to the innermost handler around it, decided at compile time.

Several instances, and names

Fail[i32] and Fail[u8] are two instances of Fail, and a row can hold both. An operation goes to the innermost handler of its instance, worked out from its argument’s type, so the order you nest the two handlers in doesn’t matter. If an operation’s instance is ambiguous (raise(1) with two integer instances in scope), the checker asks you for an ascription, raise((1 : u8)), or a name.

include textio
include fail

-- Raises a `u8` error for a large `n`.
fn small(n: i32) -> i32 with Fail[u8] = if n > 9 { raise(u8[2]) } else { n }

-- Raises its own `i32` error for a negative `n`, and passes on `small`'s.
fn check(n: i32) -> i32 with Fail[i32], Fail[u8] = if n < 0 { raise(n) } else { small(n) }

fn show(n: i32) -> 1 =
  let r = with to_result[i32, i32 + u8] { with to_result[u8, i32] { check(n) } };
  match r {
    inl (inl v) -> print_dec(v)
  | inl (inr b) -> print_lit("too large, code "); print_dec(to_i32(b))
  | inr e -> print_lit("negative: "); print_dec(e)
  };
  print_byte(b'\n')

main -> 1 = show(5); show(10); show(0 - 1)
-- output: 5
-- output: too large, code 2
-- output: negative: -1

Two handlers of the same instance are told apart by name: with n = h(…) { … } names a handler, n.op(v) performs at it, and a row can name its entries, with a: Log, b: Log:

include textio

effect Log { fn note(x: i32) }

handler summed(mut s: i32): Log = { note(x) = { s = s + x; () } }

fn both(n: i32) -> 1 with a: Log, b: Log = a.note(n); b.note(n * 10)

main -> 1 =
  let c = alloc(0);
  let d = alloc(0);
  with a = summed(&mut c) { with b = summed(&mut d) { both(3) } };
  print_dec(free(c));
  print_byte(b' ');
  print_dec(free(d));
  print_byte(b'\n')
-- output: 3 30

A generic function means the same thing at every type. In f[E] with the row Fail[E], Fail[ParseError], each operation goes to the entry it names in f’s own types, even when f is used at E := ParseError. A handler of Fail[E] inside f never accidentally catches the caller’s Fail[ParseError].

Blocks that perform effects

A closure passed as an argument is a block. Its type names no effects, and its operations go to the handlers around the place it’s written, never to a handler inside the function it’s passed to. The function is compiled once per block row, so one function serves pure blocks and effectful ones without any annotation.

include textio
include fail

fn twice(f: !(i32 => i32), x: i32) -> i32 = f(f(x))

fn guarded(f: !(i32 => i32)) -> i32 = with default[1, i32](0) { f(1) }

main -> 1 =
  print_dec(twice(!{ x -> x + 5 }, 1));
  print_byte(b'\n');
  match with to_result[1, i32] { guarded(!{ x -> raise(()) }) } {
    inl v -> print_lit("guarded caught it\n")
  | inr u -> print_lit("the error went past guarded\n")
  }
-- output: 11
-- output: the error went past guarded

The block’s raise skips past guarded’s own default and reaches the to_result where the block was written. A block can be called or passed on to another function, but not stored or returned.

A block can also use a handler’s capability, or yield to a for it’s written inside.

Computation parameters and |>

Sometimes the function should handle what its argument does: retry catches the errors of the attempt it’s given, and a timeout stops it. A parameter whose type carries a row, f: !(i32 => A with Fail[i32]), is a computation parameter. The callee handles the listed effects of each call f(…) itself. Any other effect of the argument still goes to where the argument was written.

Here is a generic retry with exponential backoff, tested against a fake timer:

include fail
include textio

effect Timer { fn pause_for(ms: i32) }

-- A flaky service: down for its first two attempts.
fn call(attempt: i32) -> i32 with Fail[i32] =
  if attempt < 2 { raise(503) } else { 200 }

-- Try `f` up to `times` times, doubling the pause after each failure.
fn retry[A](times: i32, base: i32, f: !(i32 => A with Fail[i32])) -> A with Fail[i32], Timer =
  let mut pause = base;
  let mut last = 0;
  let r : Option[A] = for attempt in 0..times {
    match with to_result { f(attempt) } {
      inl a -> break Some(a)
    | inr e -> last = e; if attempt + 1 < times { pause_for(pause); pause = pause * 2 }
    }
  } else { None };
  match r { Some(a) -> a | None -> raise(last) }

-- A fake timer for testing: it adds up the time it was asked to wait.
handler fake_timer(mut waited: i32): Timer = { pause_for(ms) = { waited = waited + ms; () } }

fn attempt(times: i32) -> 1 =
  let c = alloc(0);
  let r = with fake_timer(&mut c) {
    with to_result { retry(times, 10, !{ n -> call(n) }) }
  };
  match r {
    inl ok -> print_lit("ok "); print_dec(ok)
  | inr e -> print_lit("gave up: "); print_dec(e)
  };
  print_lit(" after waiting "); print_dec(free(c)); print_lit("ms\n")

main -> 1 = attempt(5); attempt(2)
-- output: ok 200 after waiting 30ms
-- output: gave up: 503 after waiting 10ms

With five attempts, the third succeeds with 200 after waits of 10 and 20. With two, both fail and the last error reaches the caller. retry never says which timer it uses: its caller picks one, here a fake that just adds up the waits. Had f been a plain block parameter, f: !(i32 => A), the block’s raise would go straight to the to_result in attempt and nothing would be retried. Passing a named function works too: retry(3, 10, call) means retry(3, 10, !{ a -> call(a) }).

|> stacks these stages. When h is a handler, e |> h(…) is with h(…) { e }, and when h is a function whose first parameter is a computation parameter, it’s h(!{ () -> e }, …). A chain reads in the order it wraps, innermost first: step() |> timeout |> retry(3, 10) |> logged. For any other function, e |> f(a) is f(e, a) (Iteration).

Async tasks

Async is just another effect. await() is an ordinary operation, a task is a computation paused at one, and a scheduler is a handler. The one in include async is written in the language itself, with no runtime support. A function that awaits is an ordinary function with Async in its row. There’s no async keyword, and the same function runs inside a task or outside one. Tasks compile to state machines, as Rust’s async fns do, with no garbage collector and no reference counting.

The library’s scheduler is cooperative and single-threaded.

Spawning and running tasks

include async gives you:

The values come back as a List, so the examples below print one with a small helper.

include async
include textio

fn print_all(xs: List[i32]) -> 1 =
  with on_exhausted(!{ u -> false }) {
    fold(xs, true, !{ (first, x) -> if not(first) { print_lit(", ") }; print_dec(x); false })
  };
  print_byte(b'\n')

fn ticker(tag: i32, n: i32) -> i32 with Async =
  let mut acc = 0;
  for _ in 0..n { acc = acc * 10 + tag; await() };
  acc * 10 + tag

main -> 1 =
  let q = queue[i32]();
  let q = push(q, with spawn { ticker(1, 2) });
  let q = push(q, with spawn { ticker(2, 1) });
  print_all(run_until_empty(q))
-- output: 111, 22

ticker doesn’t name a scheduler; it runs under whoever spawns it. A task is a value, so a program can also drive tasks itself with resume and cancel, or write its own scheduler as a handler of await.

A logged task records entries with log(x) as it runs, and run_logged answers them in the order they were logged, interleaved across tasks:

include async
include textio

fn print_all(xs: List[i32]) -> 1 =
  with on_exhausted(!{ u -> false }) {
    fold(xs, true, !{ (first, x) -> if not(first) { print_lit(", ") }; print_dec(x); false })
  };
  print_byte(b'\n')

-- Logs each step it takes, and answers its tag.
fn worker(tag: i32, steps: i32) -> i32 with Async =
  for i in 0..steps { log(tag * 10 + i); await() };
  tag

main -> 1 =
  let q = lqueue[i32]();
  let q = lpush(q, with spawn_logged { worker(1, 2) });
  let q = lpush(q, with spawn_logged { worker(2, 3) });
  let (values, log) = run_logged(q);
  print_all(values);
  print_all(log)
-- output: 1, 2
-- output: 10, 20, 11, 21, 22

Cancellation

A task is linear, with a cancel branch: it has to be either run to the end or cancelled. Cancelling frees everything the task owns, so nothing leaks. Here the first of two lookups to finish wins, and the other is cancelled along with the cell it holds:

include async
include textio

-- A lookup that takes `steps` turns, holding a cell it owns.
fn lookup(key: i32, steps: i32) -> i32 with Async =
  let buf = alloc(key);
  for _ in 0..steps { await() };
  free(buf) * 10

-- The value of the first task to finish (`inl` for `a`, `inr` for `b`); the other is cancelled.
fn race[A](a: Task[A], b: Task[A], turns: i32) -> A + (A + 1) =
  if turns == 0 { cancel(a); cancel(b); inr (inr ()) } else {
    match resume(a) {
      inl v -> cancel(b); inl v
    | inr ra ->
        match resume(b) {
          inl w -> cancel(ra); inr (inl w)
        | inr rb -> race(ra, rb, turns - 1)
        }
    }
  }

main -> 1 =
  let a = with spawn { lookup(3, 3) };
  let b = with spawn { lookup(4, 6) };
  match with on_exhausted(!{ u -> inr (inr ()) }) { race(a, b, 10) } {
    inl v -> print_lit("first: "); print_dec(v)
  | inr (inl w) -> print_lit("second: "); print_dec(w)
  | inr (inr u) -> print_lit("neither")
  };
  print_byte(b'\n')
-- output: first: 30

The run ends with nothing allocated: cancelling the slow task freed its cell. race calls itself, so its call goes under on_exhausted (Recursion).

Borrows across await

A task may borrow its own data across an await, with no Pin and nothing written:

include async
include textio

fn print_all(xs: List[i32]) -> 1 =
  with on_exhausted(!{ u -> false }) {
    fold(xs, true, !{ (first, x) -> if not(first) { print_lit(", ") }; print_dec(x); false })
  };
  print_byte(b'\n')

fn task(n: i32) -> i32 with Async =
  let c = alloc(n);
  let v = borrow mut c { m ->
    let old = modify m { x -> (x + 1, x) };
    await();
    let now = modify m { x -> (x * 10, x) };
    old + now };
  v + free(c)

main -> 1 =
  let q = queue[i32]();
  let q = push(q, with spawn { task(1) });
  let q = push(q, with spawn { task(2) });
  print_all(run_until_empty(q))
-- output: 23, 35

Each task holds a mut borrow of its own cell while it’s suspended, and the compiler checks it like any other borrow. That one form, a mut borrow block of the task’s own cell whose body uses only the borrow, is the only borrow a task keeps across an await from inside; other borrows held across an await are not implemented yet (Status). Until then, end the borrow before the await (put the borrow block around the work between two awaits), or move the value into the task and have the task hand it back. A task spawned with spawn_in inside a borrow block can also hold that outer borrow across its awaits, and use effects such as standard output that the surrounding block gives it.

Linear values

Every value has one of two kinds of type. An unrestricted type (a number, bool, 1, a ! function, tuples and sums of these, and recursive data of these, whose copy is written clone) can be copied and discarded freely. Every other type is linear: a value of it is used exactly once. There is no third kind. Ownership and borrows introduced the two; this chapter says what linearity means for the data, handlers, errors and tasks of the chapters since.

Most linear values don’t feel that way, because most linear types have a consume: a way to consume a value that the compiler works out from the type’s structure. A cell’s consume frees it and then consumes what it held; a tuple’s or a record’s consumes each field; a task’s cancels it. Where a value goes unused, the checker inserts its consume at the end of its scope, and that consume is the value’s one use. Every consume in a program is derived from a type; there are no written consumes.

include textio

data Note = { tag: i32, body: ref i32 }

main -> 1 =
  let n = Note { tag: 1, body: alloc(40) };
  let m = Note { tag: 2, body: alloc(2) };
  let Note { tag, body } = m;
  print_dec(free(body) + 40);
  print_byte(b'\n')
-- output: 42

n is never used, so the checker inserts Note’s consume where main ends: it frees the cell in body, and the run ends with nothing allocated.

A shared borrow imm 'a A is linear too. Its consume ends the loan, and it also has a derived copy: one shared borrow can be split into two. A use of a borrow after its first is its derived copy, which the checker inserts the way it inserts a consume. Ownership’s twice reads one borrow twice; a borrow can be passed on as often, too:

include textio

fn get<'a>(r: imm 'a i32) -> i32 = *r

-- Passes one borrow on to two calls, and reads it a third time.
fn thrice<'a>(r: imm 'a i32) -> i32 = get(r) + get(r) + *r

main -> 1 =
  let c = alloc(5);
  let n = thrice(&c);
  print_dec(n + free(c));
  print_byte(b'\n')
-- output: 20

r has three uses in thrice, so the checker inserts two copies of it. bcc copies <file> lists every copy the checker inserted, a function’s once for each call of it that the program reaches. The copy is the borrow’s alone: a second use of a mut borrow, an owned value or a declared value is still an error, “x is used twice here, and its type … is linear”.

Linear types that are not consumable

Some linear types are not consumable. Consuming a value of one means doing something the program has to say: calling it, resuming it, closing it. They are:

• Capabilities: standard input, standard output and the other host capabilities (the clock, the arguments). Your program never holds one: the platform’s handlers keep them as their state (Input and output).
• Continuations of must_resume ctl operations, which a handler must resume.
• One-shot functions A => B, which can be disposed of only by calling them.
• Declared types: a data declaration whose field is marked must_close.

A value of one of these types has to be consumed on every path, and leaving one unused is an error that names it:

effect Ask { must_resume ctl ask() -> i32 }

handler skip: Ask, i32 -> i32 = {
  return(a) = a;
  ask(k) = 0
}

main -> i32 = with skip { ask() + 1 }
-- expect: 5:7: `k` is not consumed in its scope, and its type `U ((i32 -o F i32) & top)` is linear and is not consumable

Messages print types as the core sees them: U ((i32 -o F i32) & top) is the continuation, a suspended function from the operation’s answer with no cancel branch (top). The clause has to call k. A one-shot function has to be called:

fn adder(k: i32) -> i32 => i32 = { x -> x + k }

main -> i32 =
  let f = adder(5);
  5
-- expect: 4:7: `f` is not consumed in its scope, and its type `i32 => i32` is linear and is not consumable

Declared types

Marking a field must_close puts the whole type among the linear types that are not consumable. Use it for a value whose silent disappearance would be a bug: a transaction that has to be committed, a guard that has to be released. must_close(commit) also names the function that consumes it, which the error messages point at. In a message, a marked field carries a tok, the token that makes the type linear and not consumable:

data Txn = { id: i32, must_close(commit) log: i32 }

fn begin(id: i32) -> Txn = Txn { id: id, log: 0 }

fn commit(t: Txn) -> i32 = match t { Txn { id, log } -> id * 100 + log }

main -> i32 =
  let t = begin(7);
  5
-- expect: 8:7: `t` is not consumed in its scope, and its type `i32 * i32 * tok` is linear and is not consumable: `Txn` holds the field `log`, marked `must_close`; pass it to `commit` before its scope ends

Naming commit doesn’t make anything call it: the program does, by writing the call. A match on a declared value consumes it, so commit is an ordinary function, and so is anything else that takes a Txn apart:

data Txn = { id: i32, must_close(commit) log: i32 }

fn begin(id: i32) -> Txn = Txn { id: id, log: 0 }

fn write(t: Txn, x: i32) -> Txn = match t { Txn { id, log } -> Txn { id: id, log: log + x } }

fn commit(t: Txn) -> i32 = match t { Txn { id, log } -> id * 100 + log }

main -> i32 =
  let t = begin(7);
  let t = write(t, 5);
  let t = write(t, 7);
  commit(t)
-- answer: i32[712]

A type that holds a declared value is not consumable either, so a record that stores a guard beside its data has to be consumed as well. A borrow of a declared value does have one: the loan ends and the value is still there, so &t can be passed to functions that read its fields before t is committed.

Resources are handlers

A resource that has to be closed doesn’t have to be a value you carry around. Hold it in a handler’s state, give the handler operations that use it, and let the handler close it when the block ends. The platform serves standard output this way: the capability is the state of a handler written once in the library, and your program performs print_byte and never sees it.

A program’s own resource works the same. This handler holds a transaction, logs into it, and commits it in its return clause:

include textio

data Txn = { id: i32, must_close(commit) log: i32 }

fn write(t: Txn, x: i32) -> Txn = match t { Txn { id, log } -> Txn { id: id, log: log + x } }

fn commit(t: Txn) -> i32 = match t { Txn { id, log } -> id * 100 + log }

effect Log { must_resume ctl log(x: i32) -> 1 }

-- Runs a block inside the transaction `t`, and commits it when the block answers.
handler in_txn(mut t: Txn): Log, i32 -> i32 = {
  return(a) = a + commit(t);
  log(x, k) = { t = write(t, x); k(()) }
}

main -> 1 =
  print_dec(with in_txn(Txn { id: 7, log: 0 }) { log(5); log(7); 0 });
  print_byte(b'\n')
-- output: 712

The block holds no transaction and owes no commit. commit runs once, in the handler, where the program wrote it.

finally

For cleanup of your own, put finally { … } after a with. The block runs when the with is left, whether it answered or an error passed through it. It is written once and placed on both exits; each placement is a call you wrote, checked like any other code, so it is not a consume.

include textio
include fail

data Guard = { must_close(release) lock: i32 }

fn release(g: Guard) -> 1 = match g { Guard { lock } -> () }

effect Step { fn step(x: i32) }

handler counted(mut n: i32): Step = { step(x) = { n = n + 1 } }

fn work(x: i32) -> i32 with Step, Fail[i32] =
  step(x);
  if x > 100 { raise(x) } else { x * 6 }

-- Runs `work` holding a guard, and releases it however `work` ends.
fn guarded(x: i32) -> i32 + i32 =
  let g = Guard { lock: x };
  with to_result[i32, i32] {
    with counted(0) { work(x) } finally { release(g) }
  }

fn show(r: i32 + i32) -> 1 with Stdout =
  match r { inl v -> print_dec(v) | inr e -> print_lit("raised "); print_dec(e) };
  print_byte(b'\n')

main -> 1 =
  show(guarded(7));
  show(guarded(500))
-- output: 42
-- output: raised 500

The second call raises inside counted, the error passes through it to to_result, and the finally releases the guard on the way. Both runs end with nothing allocated. A finally block can’t do I/O yet.

Values a program wants to discard

When you want a value to be consumable, there are three ways to get there, and each is something the compiler derives or something you write.

Keep the type’s fields consumable. A record or variant whose fields all have derived consumes has one too, built from theirs, and the checker inserts it (Note above).

Use a task, or declare the operation plain ctl. A task can be run to the end or cancelled, and cancelling it is its consume: it frees what the task owns. An unused task is cancelled where its scope ends:

include async
include textio

-- A lookup that takes `steps` turns, holding a cell it owns.
fn lookup(key: i32, steps: i32) -> i32 with Async =
  let buf = alloc(key);
  for _ in 0..steps { await() };
  free(buf) * 10

main -> 1 =
  let a = with spawn { lookup(3, 3) };
  let b = with spawn { lookup(4, 6) };
  match resume(a) {
    inl v -> print_dec(v)
  | inr ra -> cancel(ra); print_lit("pending")
  };
  print_byte(b'\n')
-- output: pending

with spawn runs each lookup to its first await, so both have allocated their cell. b is never resumed, and where main ends its consume cancels it, which frees that cell. The continuation of an operation declared plain ctl has a cancel branch in the same way: a clause that doesn’t call k cancels the rest of the block, and when that cancel performs no operation it is k’s consume (Control operations).

Consume it with a function you write. A declared value is consumed by any match on it, so a function that takes it apart and answers nothing is a written way to let it go:

data Txn = { id: i32, must_close(commit) log: i32 }

fn commit(t: Txn) -> i32 = match t { Txn { id, log } -> id * 100 + log }

fn roll_back(t: Txn) -> 1 = match t { Txn { id, log } -> () }

main -> i32 =
  let a = Txn { id: 1, log: 5 };
  let b = Txn { id: 2, log: 9 };
  roll_back(a);
  commit(b)
-- answer: i32[209]

The call is in the program, where a reader can see it.

What an abort does

When a raise leaves a computation, or a block is cancelled, the rest of it doesn’t run. The abort itself consumes nothing. A value in scope that holds no owned cell (a number, a borrow, a ! function, data made of these) is abandoned: nothing runs for it, and that is safe because there is nothing to free. A value that owns a cell is consumed by its consume, in a finaliser the compiler places around the computation that may abort, so it is freed on the way out (Errors).

A value that is not consumable has neither, so it can’t be live across a computation that may abort. Consume it before, or close it in a finally:

include fail

data Guard = { must_close(release) lock: i32 }

fn release(g: Guard) -> 1 = match g { Guard { lock } -> () }

fn work(x: i32) -> i32 with Fail[i32] = if x > 100 { raise(x) } else { x * 6 }

fn guarded(x: i32) -> i32 + i32 =
  let g = Guard { lock: x };
  with to_result[i32, i32] {
    let y = work(x);
    release(g);
    y
  }

main -> i32 = match guarded(7) { inl v -> v | inr e -> 0 }
-- expect: 12:13: `g`, of type `i32 * tok`, is live across a computation that may abort, and its type is linear and not consumable, and an abort abandons only a value that holds no owned cell: `Guard` holds the field `lock`, marked `must_close`; pass it to `release` before the computation that may abort, or close it in a `finally`

The finally version is the one in Resources are handlers.

A handler’s state can carry a declared value across an abort only when the handler handles the abort itself and consumes the state in that clause. Here abort_txn is the handler’s own operation, and its clause rolls the transaction back:

include textio

data Txn = { id: i32, must_close(commit) log: i32 }

fn commit(t: Txn) -> i32 = match t { Txn { id, log } -> id * 100 + log }

fn roll_back(t: Txn) -> 1 = match t { Txn { id, log } -> () }

effect Abort { ctl abort_txn(e: i32) -> never }

-- Commits the transaction when the block answers, and rolls it back when it aborts.
handler in_txn(t: Txn): Abort, i32 -> i32 = {
  return(a) = a + commit(t);
  abort_txn(e) = { roll_back(t); e }
}

fn work(x: i32) -> i32 with Abort = if x > 100 { abort_txn(x) } else { x * 6 }

main -> 1 =
  print_dec(with in_txn(Txn { id: 7, log: 5 }) { work(5) });
  print_byte(b' ');
  print_dec(with in_txn(Txn { id: 8, log: 0 }) { work(500) });
  print_byte(b'\n')
-- output: 735 500

An abort that passes through the handler to one further out would leave the state behind, so the checker refuses it. Here the in_txn of Resources are handlers holds the transaction, and work raises a Fail[i32] that only the outer to_result handles:

include fail

data Txn = { id: i32, must_close(commit) log: i32 }

fn write(t: Txn, x: i32) -> Txn = match t { Txn { id, log } -> Txn { id: id, log: log + x } }

fn commit(t: Txn) -> i32 = match t { Txn { id, log } -> id * 100 + log }

effect Log { must_resume ctl log(x: i32) -> 1 }

handler in_txn(mut t: Txn): Log, i32 -> i32 = {
  return(a) = a + commit(t);
  log(x, k) = { t = write(t, x); k(()) }
}

fn work(x: i32) -> i32 with Log, Fail[i32] =
  log(x);
  if x > 100 { raise(x) } else { x * 6 }

fn run_it(x: i32) -> i32 + i32 =
  with to_result[i32, i32] {
    with in_txn(Txn { id: 7, log: 0 }) { work(x) }
  }

main -> i32 = match run_it(5) { inl v -> v | inr e -> 0 - e }
-- expect: 13:34: `t`, of type `i32 * i32 * tok`, is live across a computation that may abort, and its type is linear and not consumable, and an abort abandons only a value that holds no owned cell: `Txn` holds the field `log`, marked `must_close`; pass it to `commit` before the computation that may abort, or close it in a `finally`

Compared with Rust

In Rust, a value of a non-Copy type may be used at most once, and any value may go unused. A type can attach cleanup code that runs when a value goes out of scope, written by hand and free to do anything, and leaking a value (mem::forget) is safe. There is no way for a type to insist on being consumed; #[must_use] is a warning.

Here every type that isn’t unrestricted is linear, and the difference shows in three places:

• Consumes are derived, never written. A consume frees memory and closes codata by the type’s structure, and does nothing else. Cleanup that does something more is a call the program writes, in a finally, a handler or a consuming function.
• A type can have no consume. must_close, must_resume ctl and one-shot functions are linear and not consumable, and leaving one unused is a type error, not a lint.
• An abort runs only derived consumes. What an abort passes over either holds no owned cell and is abandoned, or is consumed implicitly in a finaliser the compiler places, or is refused. No code a type wrote runs on the way out, where Rust unwinds by running each value’s cleanup code.

Most programs see little of this: a cell, a string or a record of them is consumed where its scope ends, as in Rust.

Recipes

Short, complete programs for the things you usually try first in a new language. Each one runs as it is: save it as a .bc file and run it with bcc run. The -- stdin: lines under a program are the input it was run with, and the -- output: lines are what it printed.

Sum the numbers on standard input

include textio

main -> 1 =
  let s = read_input();
  let sum = borrow imm s { t -> fold_i32s(t, !{ (x, acc) -> acc + x }, 0) };
  print_dec(sum);
  print_byte(b'\n')
-- stdin: 1 2
-- stdin: 3
-- stdin: -4 10
-- output: 12

read_input() reads all of standard input into a string, and borrow imm s { t -> … } lends it as a text view t. fold_i32s walks every integer written in the text, in order, and folds it into a running value: a run of digits is a number, a - just before it makes it negative, and every other byte separates numbers, so spaces, newlines and commas all work. The closure !{ (x, acc) -> acc + x } gets each number and the sum so far.

Parse numbers and report bad input

include textio

data Tally = { line: i32, sum: i32, bad: Vec[i32] }

-- One more line: added to the sum if it is a number, its line number kept if not.
fn add_line<'a>(l: text 'a, t: Tally) -> Tally =
  match t {
    Tally { line, sum, bad } ->
      let line = line + 1;
      match with to_result { parse_i32(trim(l)) } {
        inl x -> Tally { line, sum: sum + x, bad }
      | inr e -> push(&mut bad, line); Tally { line, sum, bad }
      }
  }

fn report<'a>(bad: array_imm 'a i32) -> 1 =
  for n in bad { print_lit("line "); print_dec(*n); print_lit(" is not a number\n") }

main -> 1 =
  let s = read_input();
  let start = Tally { line: 0, sum: 0, bad: box buf[i32](0) };
  let t = borrow imm s { v -> fold_lines(v, !{ (l, t) -> add_line(l, t) }, start) };
  match t {
    Tally { line, sum, bad } ->
      borrow imm bad { v -> report(v) };
      print_lit("sum ");
      print_dec(sum);
      print_byte(b'\n')
  }
-- stdin:  12
-- stdin: four
-- stdin: 30
-- stdin: 3x
-- output: line 2 is not a number
-- output: line 4 is not a number
-- output: sum 42

parse_i32 raises a ParseError when the text isn’t a number, and with to_result { … } turns that into a value: inl the number, or inr the error (Errors). fold_lines hands each line to add_line with the state so far, a Tally record that counts lines, keeps the sum and collects the numbers of the bad lines in a Vec. match t { Tally { line, sum, bad } -> … } takes a record apart into variables named after its fields, and Tally { line, sum, bad } builds one back from variables of the same names. The report is printed once the fold has finished.

Count things with a map

include textio
include map

-- One more sighting of `x`.
fn seen(x: i32, counts: Map[i32, i32]) -> Map[i32, i32] =
  let mut counts = counts;
  let old = map_lookup(&counts, x);
  let n = match old { Some(n) -> n + 1 | None -> 1 };
  map_insert(&mut counts, x, n);
  counts

main -> 1 =
  let s = read_input();
  let counts = borrow imm s { t -> fold_i32s(t, !{ (x, m) -> seen(x, m) }, map_new[i32, i32](16)) };
  let mut best = 0;
  let mut most = 0;
  borrow imm counts { 'x, r ->
    for e in map_iter(r) { let (x, v) = e; let n = *v; if n > most { best = x; most = n } } };
  let distinct = map_len(&counts);
  print_dec(distinct);
  print_lit(" different numbers; ");
  print_dec(best);
  print_lit(" appears most, ");
  print_dec(most);
  print_lit(" times\n")
-- stdin: 3 1 4 1 5 9 2 6 5 3 5
-- output: 7 different numbers; 5 appears most, 3 times

map_lookup answers a copy of the count stored for a key, as an Option, and map_insert stores the new one; both take the map lent, &counts to read it and &mut counts to change it. To visit every entry, borrow imm counts { 'x, r -> … } lends the map and map_iter(r) yields each key with a view of its value, read with *v. The iteration order comes from the hash, and it’s the same on every run. Maps and sets lists the rest of the map’s operations.

Build a string

include textio

-- `[a, b, c]`, written into a new string.
fn show_list<'a>(v: array_imm 'a i32) -> string =
  let mut s = box string(32);
  push_char(&mut s, '[');
  let mut first = true;
  for p in v {
    if not(first) { push_lit(&mut s, ", ") };
    push_dec(&mut s, *p);
    first = false
  };
  push_char(&mut s, ']');
  s

fn square(i: i32) -> i32 = (i + 1) * (i + 1)

main -> 1 =
  let a = array_new[i32](5, square);
  let s = borrow imm a { v -> show_list(v) };
  let n = len_of(&s);
  let s = print_string(s);
  print_lit(" (");
  print_dec(n);
  print_lit(" bytes)\n")
-- output: [1, 4, 9, 16, 25] (17 bytes)

box string(32) allocates an empty string with room for 32 bytes; it grows when it needs to. push_char, push_lit and push_dec append a character, a literal and a number. The function hands the finished string back to its caller, which owns it from then on. print_string(s) prints it and hands it back, and the string is freed when main ends.

Read the command-line arguments

include textio

-- Greets each name given on the command line, or the world if none is.
main -> 1 =
  let mut n = 0;
  let mut more = true;
  while more {
    let (name, got) = next_arg(box string(16));
    if got {
      n = n + 1;
      print_lit("Hello, ");
      let name = print_string(name);
      print_lit("!\n")
    } else { more = false }
  };
  if n == 0 { print_lit("Hello, world!\n") }
-- output: Hello, world!

next_arg appends the next argument to the string it’s given, and answers it with whether there was one. The arguments come after the file name:

$ bcc run hello.bc Ada Grace
Hello, Ada!
Hello, Grace!
()
live 0

In the interpreter they come after --: bcc interp hello.bc -- Ada Grace.

Update a record’s Vec through &mut

include textio

data Scores = { best: i32, history: Vec[i32] }

-- Records one score: appended to `history`, and kept as `best` if it is the highest yet.
fn record<'a>(s: mut 'a Scores, x: i32) -> 1 =
  modify s { sc ->
    match sc {
      Scores { best, history } ->
        push(&mut history, x);
        let best = if x > best { x } else { best };
        Scores { best, history }
    } }

fn print_all<'a>(v: array_imm 'a i32) -> 1 =
  for p in v { print_byte(b' '); print_dec(*p) }

main -> 1 =
  let mut s = Scores { best: 0, history: box buf[i32](4) };
  record(&mut s, 12);
  record(&mut s, 40);
  record(&mut s, 27);
  let best = s.best;
  print_lit("best ");
  print_dec(best);
  print_lit(", history:");
  match s { Scores { best, history } -> borrow imm history { v -> print_all(v) } };
  print_byte(b'\n')
-- output: best 40, history: 12 40 27

record gets the scores lent mut and changes them in place. modify s { sc -> … } takes the record out of the borrow, and the record the block ends with is put back: here the same Vec with one more element pushed, and the new best. A copyable field is read directly, as in let best = s.best;. To read the Vec, main takes the record apart and lends the vector to print_all as a view.

A recursive function over a tree

include textio
include rec

fn max(a: i32, b: i32) -> i32 = if a > b { a } else { b }

data Tree = Leaf | Node(left: Tree, val: i32, right: Tree)

-- `t` with `x` added, smaller values to the left.
fn insert(t: Tree, x: i32) -> Tree =
  match t {
    Leaf -> box Node(Leaf, x, Leaf)
  | box Node(l, v, r) ->
      if x < v { box Node(insert(l, x), v, r) } else { box Node(l, v, insert(r, x)) }
  }

-- The height, read through a borrow.
fn height<'a>(t: imm 'a Tree) -> i32 =
  fold_imm t { Leaf -> 0 | Node(l, v, r) -> 1 + max(l, r) }

-- Prints the values in order, consuming the tree.
fn print_sorted(t: Tree) -> 1 =
  match t {
    Leaf -> ()
  | box Node(l, v, r) -> print_sorted(l); print_byte(b' '); print_dec(v); print_sorted(r)
  }

fn build(xs: array i32) -> Tree =
  let mut t = Leaf;
  for x in xs { t = insert(t, x) };
  t

main -> 1 =
  let t = with on_exhausted(!{ u -> Leaf }) { build(array_new[i32](7, !{ i -> (i * 5) % 7 })) };
  let h = height(&t);
  print_lit("height ");
  print_dec(h);
  print_lit(", sorted:");
  with on_exhausted(!{ u -> () }) { print_sorted(t) };
  print_byte(b'\n')
-- output: height 5, sorted: 0 1 2 3 4 5 6

A binary search tree, built by inserting the values one at a time. insert takes the tree and gives back a new one: the pattern box Node(l, v, r) frees the old node, and box Node(…) allocates its replacement. height only reads the tree, so it takes a borrow and uses fold_imm, which hands each node its subtrees’ heights. print_sorted consumes the tree as it prints it, so nothing is left to free. A function that calls itself needs a handler for running out of depth; on_exhausted gives the value to use if it does (Recursion).

A tree whose children are a Vec

include textio
include rec

-- A directory: the bytes of its own files, and its subdirectories.
data Dir = Dir(size: i32, subdirs: Vec[Dir])

fn files(n: i32) -> Dir = Dir(n, box buf[Dir](0))

fn with_sub(d: Dir, sub: Dir) -> Dir =
  match d { Dir(n, subs) -> push(&mut subs, sub); Dir(n, subs) }

-- The size of `d` and everything under it, and the number of directories; consumes `d`.
fn du(d: Dir) -> i32 * i32 =
  match d {
    Dir(size, subs) ->
      let mut bytes = size;
      let mut dirs = 1;
      let n = len_of(&subs);
      for i in 0..n {
        match pop(&mut subs) {
          Some(sub) -> let (b, k) = du(sub); bytes = bytes + b; dirs = dirs + k
        | None -> ()
        }
      };
      (bytes, dirs)
  }

main -> 1 =
  let src = with_sub(with_sub(files(120), files(300)), files(45));
  let root = with_sub(with_sub(files(10), src), files(2048));
  let (bytes, dirs) = with on_exhausted(!{ u -> (0, 0) }) { du(root) };
  print_dec(bytes);
  print_lit(" bytes in ");
  print_dec(dirs);
  print_lit(" directories\n")
-- output: 2523 bytes in 5 directories

Each directory holds its subdirectories in a Vec[Dir]; the vector’s storage is on the heap already, so no box is needed. du takes a directory apart, pops each subdirectory off its vector, adds up what the recursive call returns, and answers a pair: the bytes and the number of directories. Each directory is freed once it has been counted.

Test I/O with a fake handler

include textio

-- The code under test: it writes to whatever serves `Stdout`.
fn fizzbuzz(n: i32) -> 1 with Stdout =
  for i in 1..n + 1 {
    if i % 15 == 0 { print_lit("FizzBuzz") }
    else if i % 3 == 0 { print_lit("Fizz") }
    else if i % 5 == 0 { print_lit("Buzz") }
    else { print_dec(i) };
    print_byte(b' ')
  }

-- A fake standard output that keeps what is written.
handler collect(mut out: string): Stdout = {
  print_byte(b) = { push_byte(&mut out, b) };
  print_bytes(v) = { push_str(&mut out, v) }
}

-- Runs `fizzbuzz(n)` with its output captured, and compares it with `want`.
fn check(name: lit, n: i32, want: lit) -> 1 =
  let c = alloc(box string(64));
  with collect(&mut c) { fizzbuzz(n) };
  let got = free(c);
  let ok = borrow imm got { t -> eq_lit(t, want) };
  if ok { print_lit("ok   ") } else { print_lit("FAIL ") };
  print_lit(name);
  print_byte(b'\n')

main -> 1 =
  check("first five", 5, "1 2 Fizz 4 Buzz ");
  check("fifteen", 15, "1 2 Fizz 4 Buzz Fizz 7 8 Fizz Buzz 11 Fizz 13 14 FizzBuzz ")
-- output: ok   first five
-- output: ok   fifteen

fizzbuzz writes to Stdout, and its signature says so. In a test, with collect(&mut c) { … } serves Stdout with a handler that appends each byte to a string, instead of the real standard output; fizzbuzz itself doesn’t change. Afterwards the cell c holds everything that was written, and eq_lit compares it with the expected text. A string literal’s type is lit, which is how check takes the name and the expected output. A fake clock or scripted input is written the same way (Serving an effect yourself).

Time something

include textio

fn collatz(n: i32) -> i32 =
  let mut x = n;
  let mut steps = 0;
  while x != 1 {
    if x % 2 == 0 { x = x / 2 } else { x = 3 * x + 1 };
    steps = steps + 1
  };
  steps

-- The number below `n` with the longest Collatz run.
fn longest(n: i32) -> i32 =
  let mut best = 1;
  let mut most = 0;
  let mut i = 1;
  while i < n {
    let s = collatz(i);
    if s > most { best = i; most = s };
    i = i + 1
  };
  best

main -> 1 =
  let t0 = now();
  let x = longest(100000);
  let t1 = now();
  print_dec(x);
  print_lit(" has the longest run; that took ");
  print_dec64((t1 - t0) / 1000000);
  print_lit(" ms\n")

$ bcc run --native collatz.bc
77031 has the longest run; that took 16 ms
()
live 0

now() is a monotonic clock in nanoseconds, as an i64, so the difference of two readings is the time between them, and dividing by 1000000 gives milliseconds. print_dec64 prints an i64. The time you see will differ from run to run.

A generator pipeline

include textio
include adapters

fn range(lo: i32, hi: i32) -> 1 with Yield[i32] =
  let mut i = lo;
  while i < hi { yield(i); i = i + 1 };
  ()

-- Whether `n` is prime, trying the divisors up to its square root.
fn is_prime(n: i32) -> bool =
  let mut ok = true;
  for d in 2..n {
    if d * d > n { break };
    match checked_rem(n, d) { inl r -> if r == 0 { ok = false; break } | inr e -> () }
  };
  ok

fn print_all<'a>(v: array_imm 'a i32) -> 1 =
  for p in v { print_byte(b' '); print_dec(*p) }

main -> 1 =
  let mut found: Vec[i32] = box buf[i32](8);
  for x in range(2, 1000) |> filter(is_prime) |> map(!{ p -> p * p }) |> take(6) {
    push(&mut found, x)
  };
  print_lit("squares of the first six primes:");
  borrow imm found { v -> print_all(v) };
  print_byte(b'\n')
-- output: squares of the first six primes: 4 9 25 49 121 169

range is a generator: it yields each number in turn (Generators). |> passes the value on its left as the first argument of the call on its right, so the pipeline reads in order: the numbers from 2, the primes among them, their squares, the first six. Nothing is computed ahead: take(6) stops the pipeline after the sixth value, so range never gets near 1000. The loop collects the values in a Vec, and they’re printed after it. is_prime uses checked_rem, which answers the remainder as a sum instead of raising on a zero divisor, so it’s a plain function that filter can take.

Language reference

This page states the language’s syntax and rules in one place, briefly. The guide chapters teach the same material with longer examples; each section below links to the one it summarises. The library’s types and functions are in the Standard library, and what isn’t built yet is in Status.

Lexical structure

Comments run from -- to the end of the line. There are no block comments.

Names. There are three kinds:

Literals.

A byte literal holds a printable ASCII character or one of the escapes \n, \t, \r, \0, \\, \'; a character literal takes the same escapes. A string literal is written on one line, is UTF-8, and takes the escapes \n, \t, \r, \0, \\, \" and \xNN (the byte with hexadecimal value NN). There are no negative literals: write 0 - 5.

include textio

main -> 1 =
  let n = 0x2A;                -- 42
  let big = i64[5000000000];
  let c = 'é';                 -- 233
  print_dec(n);
  print_byte(b' ');
  print_dec64(big);
  print_byte(b' ');
  print_dec(c);
  print_lit(" \x41\"\n")
-- output: 42 5000000000 233 A"

Reserved words. These can’t be used as names:

• the keywords of programs: borrow, box, break, clone, continue, def, div, effect, else, fn, fold_imm, fold_own, fold_reuse, for, handler, if, imm, in, include, inl, inr, let, loop, main, match, modify, mut, poly, return, total, type, while, with;
• the built-in types and operations: alloc, array, array_imm, array_mut, array_new, f32, f64, free, host, i32, i64, ref, swap, u8;
• words reserved for the compiler’s internal forms: abort, absurd, all, alloc_s, array_copy, array_empty, array_release, array_free, array_get, array_len, array_replace, array_size, block, bounded_fix, boxed, case, copy, copy_bang, count_fold, count_try, delay, delay_in, delay_out, dom, extern, fam, fixd, forall, force, release_bang, release_imm, release_mut, release_unk, free_s, fun, handle_with, input, iter, leaf, mu, node, nu, nu_in, nu_out, output, perform, roll, run, shape, shorten_imm, shorten_mut, sized, stream, stream_in, stream_out, str, thunk, thunkv, top, unbang, unbox, unfold, unfold_s, unk, unroll, unwind, val, view, every word beginning slice_, withbor or withload, withswap, and writes; and the upper-case U, F and Fun.

A few ordinary names mean something where a type or a declaration is expected, and are names anywhere else: data, at, where, ctl, bool, string, buf, text, text_mut, lit, never and pull.

Declarations

A program is a sequence of declarations, with at most one main. A name is in scope from its declaration on: a function or type is used after it is declared. Functions declared one after the other may call each other (Recursion).

In a function, the type parameters [T, …] and the lifetime parameters <'a, …> are each optional, as are the row with … and the bounds where …. A lifetime parameter may be bounded by another, <'x, 'w < 'x>. With no parameters, a function is fn f() -> B. Every parameter’s type and the result type are written.

include textio

data Pair[A] = { fst: A, snd: A }
type Grid = i32 * i32

def origin : i32 = 0

fn swapped[A](p: Pair[A]) -> Pair[A] = match p { Pair { fst, snd } -> Pair { fst: snd, snd: fst } }

fn first<'a>(r: imm 'a Grid) -> i32 = let (x, y) = *r; x

total fn area(g: Grid) -> i32 = let (w, h) = g; w * h

main -> 1 =
  let p = swapped(Pair { fst: 1, snd: 2 });
  let c = alloc((3, 4));
  let x = first(&c);
  print_dec(p.fst + origin);
  print_byte(b' ');
  print_dec(x * 10 + area(free(c)));
  print_byte(b'\n')
-- output: 2 42

• data cases with fields hold them positionally, C(A, B), or by name, C(f: A, g: B); a record has one case, named after the type. A case that holds the type itself is built with box (Data and generics).
• type names a type; the name and the type are interchangeable (Tuples and sums).
• effect: an operation declared fn answers its caller; ctl receives the continuation and resumes it at most once, must_resume ctl exactly once, and ctl op(…) -> never never. -> B left out is -> 1. A handler of fn operations keeps its state in its mut parameter; a control handler names the body’s type A and its answer R, and has a return(x) clause (Effects and handlers).
• poly: a family has one type parameter, the type that chooses the case; the operators +, -, *, /, %, ==, !=, <, <=, >, >= are families (poly families).
• include brings a library module’s declarations into scope (Standard library). The prelude (bool, true, false, not, Option, Vec, to_i32, to_u8) is always in scope.

Types

A function of several parameters has a tuple as its argument type: fn f(x: i32, y: bool) is a !(i32 * bool => B). * binds tighter than +, which binds tighter than =>, and all three associate to the right: A * B + C => D is ((A * B) + C) => D.

Copyable types are the numbers, bool, 1, ! functions, and tuples and sums of copyable types; recursive data built from them is copied only by clone(x). Every other type is owned and used exactly once (Ownership and borrows).

Rows. A function’s row, the effects it performs, is inferred, and may be written after the result type: -> B with Fail[i32], Stdout. An entry may be named, with a: Log, b: Log, and a written row is checked (Effects and handlers).

Lifetimes. A lifetime is a parameter 'a of a function, a data or a type, the lifetime 'b a borrow block names, { 'b, x -> … }, or 'main, which lasts for main’s body. They are lexical, and never elided in signatures (Lifetimes in signatures).

Expressions and statements

A body is a sequence of statements separated by ;, and its value is the last one’s. A statement is one of:

The expressions are:

include textio

data Shape = Rect(w: i32, h: i32) | Circle(r: i32)
data Point = { x: i32, y: i32 }

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

fn kind(n: i32, b: u8) -> i32 =
  match (n, b) {
    (0, _) -> 0
  | (_, b'x') -> 1
  | _ -> 2
  }

main -> 1 =
  let mut p = Point { x: 1, y: 2 };
  p.x = p.x + 10;
  let Point { x, y } = p;
  let (a, b) = (area(Rect(2, 3)), area(Circle(1)));
  let mut best = a;
  if b > best { best = b };
  let sign = if x > y { 1 } else if x == y { 0 } else { 0 - 1 };
  print_dec(best);
  print_byte(b' ');
  print_dec(sign);
  print_byte(b' ');
  print_dec(kind(0, b'x') + kind(5, b'x') * 10 + kind(5, b'y') * 100);
  print_byte(b'\n')
-- output: 6 1 210

Patterns

let, match, closures and borrow blocks take patterns:

let takes a pattern that can’t fail: names, _, (), tuples, and constructors of a type with one case. A match may match several values at once, match (a, b) { (p, q) -> … }. There are no guards and no or-patterns.

Loops

In a loop’s body, break leaves the loop, break e leaves it with the value e, continue goes on to the next turn, and return e returns e from the enclosing function. for … { … } else { e } gives the loop’s value when its source ends without a break, and let r = for … { … }; binds the loop’s value (or, over a generator, what the generator returns). A let mut variable assigned in the body is carried from turn to turn and is there after the loop.

A for over data always finishes. A function with a while or a loop, or that calls one, may diverge, which is inferred; total fn asks the compiler to check that it can’t, and div_fuel(e, n) runs a diverging e for at most n steps (Loops that may not end).

include textio

main -> 1 =
  let a = array_new[i32](5, !{ i -> i * i });
  let first = for p in &a { let v = *p; if v > 5 { break v } } else { 0 };
  let mut odd = 0;
  for i in 0..10 { if i % 2 == 0 { continue }; odd = odd + i };
  let mut n = 1;
  while n < 100 { n = n * 3 };
  let mut k = 0;
  loop { k = k + 1; if k == 4 { break } };
  print_dec(first);
  print_byte(b' ');
  print_dec(odd);
  print_byte(b' ');
  print_dec(n);
  print_byte(b' ');
  print_dec(k);
  print_byte(b'\n')
-- output: 9 25 243 4

Operators and precedence

From the tightest binding to the loosest:

Arithmetic and comparisons work at the type of their operands: the machine instructions at the integer and float types, and a program’s poly cases at its own types (Operators at your own types). Integer arithmetic wraps, comparisons are signed, and / and % truncate toward zero; dividing by zero raises an error (Division). not(b) negates a bool. There are no unary minus, compound assignment or bitwise operators; bitwise operations and shifts are host[and32](a, b) and the like (Numbers).

include textio

fn twice(x: i32) -> i32 = x * 2

main -> 1 =
  let a = 1 + 2 * 3 - 8 / 2 % 3;
  let ok = a > 4 && not(a == 5) || false;
  let b = a |> twice;
  let o = if ok { 1 } else { 0 };
  print_dec(a);
  print_byte(b' ');
  print_dec(b);
  print_byte(b' ');
  print_dec(o);
  print_byte(b'\n')
-- output: 6 12 1

main

main -> T = body is where the program starts. main performs standard input and output, the clock and the arguments with nothing written; an operation no handler in the program serves goes to the platform (Input and output). An error that no handler catches is a compile error, except division, which ends the program with status 1 (Division).

When main finishes, bcc prints its result after the program’s own output, and then live N, the number of heap objects still allocated: 0, unless the result itself holds some. The result is printed in a raw form: an integer as its width and its bits read unsigned (i32[42], and i32[4294967295] for −1), bool as inl () (false) or inr () (true), records and tuples as tuples of their fields, cases of a sum as inl … and inr …, a heap object as <loc> and a function as <fun>. Most programs print what they mean to and return (), with main -> 1.

main -> i32 * bool = (6 * 7, 1 < 2)
-- answer: (i32[42], inr ())

Standard library

The library is ordinary borrow-core code in lib/, checked with your program. include name brings one module into scope, together with the modules it includes itself; only what a program calls is compiled. This page lists each module’s user-facing names, and the guide chapter linked from each section teaches them.

Reading the signatures

Signatures are written as they are declared. Two conventions recur.

Hand-back functions. A function that changes or reads a value without consuming it takes the value first and returns it first: push(b: buf A, x: A) -> buf A * 1. You call it with a lend, push(&mut b, x), which moves b in, rebinds it to what comes back, and answers the rest, here (). len_of(&b) reads one the same way and answers the i32. A lend must be the whole of a let or a statement: let n = len_of(&b);.

A function that returns the value alone, with nothing after it (truncate, clear, reserve, grow, heap_push, clear_str, and the view functions that hand back an array_mut), is rebound with let: let b = truncate(b, 1);, let v = set(v, 0, x);.

Sums. T + 1 is an optional T: inl x when there is one, inr () when not. bool is 1 + 1. An Option[T] matches as Some(x) or None.

The prelude

In scope in every program, with no include.

The built-in forms (alloc, free, array_new, checked_div, div_fuel, …) are in the Language reference.

fail

The Fail effect and its handlers. Errors teaches them.

arith

Euclidean division, and the names of division’s error. / and % raise Fail[DivError] with no include; include arith adds the rest. Division teaches them.

include textio
include arith

-- The minute within its hour of `m` minutes after midnight, which may be negative.
fn minute(m: i32) -> i32 = rem_euclid(m, 60)

main -> 1 =
  print_dec(minute(0 - 75));
  print_byte(b' ');
  print_dec((0 - 75) % 60);
  print_byte(b' ');
  match checked_div(minute(0), 0) {
    inl q -> print_dec(q)
  | inr e -> match e { inl u -> print_lit("division by zero") | inr u -> print_lit("overflow") }
  };
  print_byte(b'\n')
-- output: 45 -15 division by zero

rec

The handlers a recursive function needs. A function that calls itself has a budget of 10000 levels and performs Exhausted when it runs out. Recursion teaches them.

include textio
include rec

fn depth(n: i32) -> i32 = if n == 0 { 0 } else { 1 + depth(n - 1) }

main -> 1 =
  match with exhausted_to_option { depth(100) } {
    inl d -> print_dec(d)
  | inr u -> print_lit("too deep")
  };
  print_byte(b' ');
  print_dec(with deep { depth(100) });
  print_byte(b'\n')
-- output: 100 100

io

The system’s effects, and decimal output. main is given each effect by the platform; any other function performs them and its caller serves them. Input and output teaches them.

textio

Text over the standard streams. Input and output teaches them.

include textio

main -> 1 =
  let s = read_input();
  let n = borrow imm s { t -> fold_lines(t, !{ (l, k) -> k + 1 }, 0) };
  let s = print_string(s);
  print_dec(n);
  print_lit(" lines\n")
-- stdin: alpha
-- stdin: beta
-- output: alpha
-- output: beta
-- output: 2 lines

text

string, a growable buffer of UTF-8 bytes, and text 'a, a view of some (text_mut 'a when it is exclusive). A view is lent from a string with borrow imm s { t -> … }, or from a literal with borrow imm "…" { t -> … }, and the functions that cut it answer sub-views without copying. A string is a buf of u8, so len_of, pop and the rest work on it. Buffers and strings teaches them.

Building a string. The push_ functions are called with &mut s.

Reading text.

UTF-8 and parsing.

In place, and buffers of views.

include textio

-- The number after the `=` of `key = value`, or 0 when there is no `=`.
fn value<'t>(line: text 't) -> i32 with Fail[ParseError] =
  match split_once(line, b'=') {
    inl (k, v) -> parse_i32(trim(v))
  | inr l -> 0
  }

main -> 1 =
  let mut s = box string(16);
  push_lit(&mut s, "caf");
  push_char(&mut s, 0xe9);
  push_lit(&mut s, " = ");
  push_dec(&mut s, 42);
  let bytes = len_of(&s);
  let chars = borrow imm s { t -> count_chars(t) };
  let v = borrow imm s { t -> with default(0 - 1) { value(t) } };
  let s = print_string(s);
  print_lit(": ");
  print_dec(bytes);
  print_lit(" bytes, ");
  print_dec(chars);
  print_lit(" characters, value ");
  print_dec(v);
  print_byte(b'\n')
-- output: café = 42: 10 bytes, 9 characters, value 42

buf

buf A, a growable array, and a priority queue on one. Vec[T] wraps a buf T, and every function here works on both. borrow imm b { v -> … } and borrow mut b { v -> … } lend the elements as a view for slice. Buffers and strings teaches them.

An element type needs a placeholder for the spare capacity: numbers, views, arrays, buffers and data built from them have one; a heap cell ref A doesn’t. A heap’s elements are copied where they lie, so its A is copyable (i32, bool, tuples of them).

include textio

main -> 1 =
  let h = box buf[i32 * i32](4);
  let h = heap_push(h, 5, 50);
  let h = heap_push(h, 2, 20);
  let mut h = heap_push(h, 9, 90);
  for i in 0..3 {
    let r = heap_pop(&mut h);
    match r { inl (k, x) -> print_dec(x); print_byte(b' ') | inr u -> () }
  };
  let mut b = box buf[i32](2);
  push(&mut b, 1); push(&mut b, 2); push(&mut b, 3);
  let mut b = truncate(b, 1);
  let c = cap_of(&b);
  let n = len_of(&b);
  print_dec(n); print_byte(b' '); print_dec(c);
  print_byte(b'\n')
-- output: 20 50 90 1 8

slice

Functions on views: array_imm 'a A (shared) and array_mut 'a A (exclusive), lent from an array or a buffer by a borrow block. A function that changes a view hands it back, and discard_mut ends it. An index out of range reads the default and writes nothing. Searches and sorts take the element comparison as an argument, and functions that copy an element need a copyable A. Arrays teaches them.

include textio
include slice

fn scramble(i: i32) -> i32 = (i * 7) % 10

main -> 1 =
  let mut a = array_new[i32](6, scramble);
  borrow mut a { v -> let v = sort(v, cmp_i32, 0); let v = reverse(v); discard_mut(v) };
  let at5 = borrow imm a { v -> find(v, 5, eq_i32) };
  let has3 = borrow imm a { v -> contains(v, 3, eq_i32) };
  for x in &a { print_dec(*x); print_byte(b' ') };
  match at5 { inl i -> print_lit("5 at "); print_dec(i) | inr u -> print_lit("no 5") };
  if has3 { print_lit(", has 3") } else { print_lit(", no 3") };
  print_byte(b'\n')
-- output: 8 7 5 4 1 0 5 at 2, no 3

key

The families a map uses: one equality, hash and order per type. They have cases at the integers, 1, tuples, sums (so bool), arrays, views and buffers (so string and text), compared structurally, and a program adds cases at its own types with poly. A float has none. Equality, hashing and order teaches them.

A view 'a T of an integer, a tuple of them or a view is the value itself, so equal(x, y) takes the values.

include textio
include key

main -> 1 =
  if equal((1, true), (1, true)) { print_lit("equal ") } else { print_lit("different ") };
  print_dec(order((1, 5), (2, 0)));
  print_byte(b' ');
  if hash(7) == hash(7) { print_lit("same hash") } else { print_lit("?") };
  print_byte(b'\n')
-- output: equal -1 same hash

map

A hash map and a set, keyed by key’s families. A map is a value: an operation takes it with &m or &mut m. borrow imm m { 'x, r -> … } lends it as r : MapRef[K, V]<'h, 'k, 'x>, to read keys and values in place. Maps and sets teaches them.

The keys and values need a placeholder, as a buffer’s elements do. Every iteration is in slot order: the same on every run for the same insertions and removals, but neither insertion order nor sorted.

include textio
include map

main -> 1 =
  let mut seen = set_new[i32](8);
  let mut dups = 0;
  for x in 0..20 {
    let fresh = set_insert(&mut seen, (x * x) % 7);
    if not(fresh) { dups = dups + 1 }
  };
  let mut m = map_new[i32, i32](8);
  let old = map_insert(&mut m, 1, 10);
  let old = map_insert(&mut m, 1, 11);
  let gone = map_remove(&mut m, 2);
  let n = set_len(&seen);
  print_dec(n);
  print_byte(b' ');
  print_dec(dups);
  print_byte(b' ');
  match old { Some(v) -> print_dec(v) | None -> print_lit("none") };
  print_byte(b' ');
  match gone { Some(v) -> print_dec(v) | None -> print_lit("none") };
  print_byte(b'\n')
-- output: 4 16 10 none

list

A generic owned list. Its functions are recursive, so a call needs a rec handler around it. Recursion introduces it.

include textio
include list

main -> 1 =
  let xs = cons(1, cons(2, cons(3, cons(4, nil()))));
  let sum = with on_exhausted(!{ u -> 0 - 1 }) {
    fold(filter(map(xs, !{ x -> x * x }), !{ x -> x % 2 == 0 }), 0, !{ (a, x) -> a + x })
  };
  print_dec(sum);
  print_byte(b'\n')
-- output: 20

list’s map and filter share their names with those of adapters and iters, so a program that calls them includes only one of these modules.

yield

The effect a generator performs. Generators teaches it.

adapters

Generic generators over stored generators. A source U (pull A K R) yields As, returns K when it finishes, and hands back R when closed early (Stored generators). An adapter that runs its source to the end returns the source’s K; those that may stop it early take a source with R = K. Chain them with |> (Pipelines).

include textio
include adapters

fn range(lo: i32, hi: i32) -> 1 with Yield[i32] =
  let mut i = lo;
  while i < hi { yield(i); i = i + 1 };
  ()

main -> 1 =
  let mut last = 0;
  for s in range(1, 100) |> skip(2) |> scan(0, !{ (acc, x) -> acc + x }) |> take_until(!{ s -> s > 40 }) {
    last = s
  };
  let mut pairs = 0;
  for p in zip(range(0, 10), range(100, 103)) { let (a, b) = p; pairs = pairs + a * b };
  print_dec(last);
  print_byte(b' ');
  print_dec(pairs);
  print_byte(b'\n')
-- output: 33 305

iters

Adapters over data, a view or a count a..b. A for over a chain of them runs at most once per element, so it stays total. for over data covers the loop they feed.

include textio
include iters

fn big(x: i32) -> bool = x > 2

total fn weighted<'a>(v: array_imm 'a i32) -> i32 =
  let mut s = 0;
  for p in zip(filter(copied(elems(v)), big), 100..200) { let (x, y) = p; s = s + x * y };
  s

main -> 1 =
  let a = array_new[i32](5, !{ i -> i });
  let w = borrow imm a { v -> weighted(v) };
  print_dec(w);
  print_byte(b'\n')
-- output: 704

async

Tasks and a round-robin scheduler, written in the language. Async tasks teaches them.

async’s push shares its name with buf’s, so a program that queues tasks doesn’t push to a buffer by that name.

float

The float operations by name, conversions, IEEE 754’s total order, and printing and parsing in the shortest decimal that reads back as the same float. Each name below exists at f64 and, with f32 in place of f64, at f32. Floats introduces them.

include float

main -> 1 =
  let x = borrow imm "2.5e-3" { t -> with default(0.0) { parse_f64(t) } };
  let mut s = box string(32);
  push_f64(&mut s, x * 4.0);
  push_lit(&mut s, " ");
  push_f32(&mut s, f32_of_f64(0.1));
  let s = print_string(s);
  print_byte(b' ');
  print_dec(total_cmp_f64(neg_f64(0.0), 0.0));
  print_byte(b' ');
  match i32_of_f64(1.0e12) { inl n -> print_dec(n) | inr u -> print_lit("out of range") };
  print_byte(b'\n')
-- output: 0.01 0.1 -1 out of range

Status

borrow-core is young and still changing, but you can write real programs in it today. This page says what works, what you are likely to trip over, and what is coming. It is the one place the book lists what isn’t built yet.

What works today

• Ownership and borrows: imm and mut borrows, &x and &mut x, borrow blocks, let mut (Ownership and borrows)
• Functions and closures, reusable and one-shot (Functions as values)
• Numbers: i32, i64, u8, f32, f64; integer division by zero raises an error you can handle (Numbers, Division)
• Records and variants with match (Records and variants)
• Recursive data: lists and trees, folds, and types that hold a Vec, an array or a map of themselves (Data and generics)
• Recursion, with deep recursion on the heap (Recursion)
• Arrays, views and slices: split, swap, sort (Arrays)
• Vectors, buffers and UTF-8 strings (Buffers and strings)
• Generics: generic functions and types (Generic functions)
• poly families: operators, equality, hashing and order at your own types (poly families)
• Hash maps and sets (Maps and sets)
• Loops: counted for with break, continue and else; while and loop; bounded runs with div_fuel (Iteration)
• Generators and |> pipelines (Generators)
• Effects and handlers, with effects inferred (Effects and handlers)
• Errors as raise and handlers, no ? needed (Errors)
• I/O: standard input, output and error, the clock and the command-line arguments (Input and output)
• Async tasks: spawn, resume, cancel, logged and scoped tasks, and a task that borrows its own data across await (Async tasks)
• Two targets: WebAssembly (bcc run) and native code through LLVM (bcc run --native), with the same I/O on both (Getting started)
• Safety proved in Lean: a program that compiles can’t use memory after freeing it, free it twice or leak it (Safety guarantees)

Things you’ll run into

Types and syntax

• The unit type is spelled 1, not () (#148).
• No unary minus, +=, or bitwise and shift operators: write 0 - x, x = x + 1, host[and32](a, b), host[shl64](n, 3) (#583).
• No indexing sugar such as v[i] (#143).
• total, leaf, node and swap are reserved, so they can’t be names of variables or functions.
• == doesn’t compare two bools; use if or match.
• An if or borrow block can’t be a call’s argument: bind it with let first.

Borrows

• &mut r.field doesn’t parse: take the record apart, borrow the field, and build it again.
• &x and &mut x must be the whole call of a let or statement: write let n = len(&v); f(n), not f(len(&v)) (#510).
• A heap cell can’t be lent with &c to a function that does I/O or performs an answering (fn) operation; lend it with a block instead, borrow imm c { r -> show(r) }. A function that may raise takes &c like any other.
• A borrow can’t be lent on with &mut m; pass it and hand it back instead (Borrow blocks).
• Two borrow blocks can’t be nested over two different owners; inside a block, lend the second owner to a call with &d instead.
• A for over a view of a buffer or string must be in a function that takes the view, not directly inside the borrow block (a view of an array works either way).

Data

• A text view can be used only once, so a word can’t be looked up in a map and then inserted as a key.
• Folds (fold_imm, fold_own, fold_reuse) don’t walk a type that holds a Vec of itself; write the recursion, as in Collections of recursive data.

Loops, generators and effects

• The body of a while or loop can’t perform an operation that a handler in the program serves: no raise, no division by a variable, and no operation of your own effects. The platform’s I/O works. Use a counted for, or do it after the loop (#522).
• A generator can’t use a capability, such as standard output, across a yield. The body of a for over a library adapter (map, filter, take, …), or over a generator that calls another generator directly, can’t do I/O: collect the values in the loop and print after it.
• A callback stored with its effects, rather than called, isn’t supported yet (#161).
• An effect can’t mix answering (fn) and control (ctl) operations, and an operation can’t answer with a borrow into its handler’s state.
• An error can’t carry an owned value yet (#215).
• A reusable closure that keeps state between calls (Rust’s FnMut) has no surface syntax yet; a handler with state does the same job (Effects and handlers).

I/O and async

• A program can’t set its exit status.
• Async is cooperative and single-threaded, with no event loop over real I/O, platform timers or wakers yet (#52).
• A task can hold a mut borrow of its own cell across await, and a task of spawn_in a borrow lent from outside its scheduler. Other borrows held across an await or a yield are not implemented yet (Async tasks). Two tasks can’t share one output stream.

Performance

• Some programs are still slower than their Rust versions (#213).

On the roadmap

• Modules and packages (#63)
• Traits, or bounds on type parameters, and derived cases (#489)
• Operator sugar: unary minus, compound assignment, bitwise and shifts (#583)
• Files, environment variables and randomness; networking (#597)
• Threads and parallelism (#212)
• Interior mutability (#119)
• Unsafe code and a C FFI (#79)
• Panics and backtraces (#192)
• Libraries: JSON (#65), regular expressions (#225)
• Sized types (#72)

Safety guarantees

borrow-core’s ownership and borrowing rules are proved sound in Lean, a proof assistant, not just tested. For you as a programmer, that means a program bcc accepts:

• never uses memory after freeing it, and never frees it twice;
• never leaks: when it finishes, everything it allocated has been freed (the live 0 at the end of every run);
• finishes, unless its type says it may loop: it has a while or a loop, or calls a function that does. Mark a function total and the compiler checks that it finishes;
• does only the I/O its signature allows: a function given no I/O effect can’t touch a stream.

This holds however the program uses effects: errors that unwind through borrows, handlers, generators and cancelled tasks are all covered. And it isn’t only a claim about the checker in general: each time bcc accepts a program, it builds a proof for that particular program, made of the proved rules.

Two things sit outside the proof. The compiler, from the checked program to WebAssembly or native code, is tested rather than proved: every example in this book and every program in the test suite gives the same output compiled as in the reference interpreter, and ends with live 0. And a task that holds a borrow of its own data across await (Async tasks) relies on one stated assumption, which is not proved; bcc check names the programs that rely on it.

Borrows held across any suspension, an await or a yield, are not implemented yet. The proof for them is done and rests on one named assumption about handlers, HandlerLawN: that a handler which keeps an operation’s continuation to resume later, and the step that turns a suspended loop back into a value, keep the safety rules. It is stated in Lean and checked against every case found so far, but not yet proved. For now it covers programs that do no I/O.

SPEC.md is the precise definition of the language, and docs/internals/proved.md lists the theorems and where they live in the Lean sources.