Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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.