Understanding Algebraic Effects

Separate what a computation requests from how that request is handled.

9.1 perform requests an operation

When a function needs to request an operation, Tauto can express it with algebraic effects. The caller uses perform to make the request; an enclosing handle gives it meaning.

effect ask(n: i64): i64 resume ω

let result := handle {
  perform ask(5) + 1
} with {
  ask(n), k => k(n) + k(n + 1)
  return v => v
}

perform show("result", result)

// Resume one continuation twice and add the two results.

result = 13

result = 13

ask(5) is not an ordinary function call. The handler receives the rest of the computation after the operation as k.

9.2 Follow the continuation k

In perform ask(5) + 1, the remaining computation adds 1 to the answer. Therefore k(5) returns 6, and k(6) returns 7. The handler adds them to produce 13.

resume ω permits the continuation to be resumed any number of times (the next chapter explains this in more detail). Ownership checking and resumption quantities work together to prevent duplication of a continuation from consuming a resource twice.

9.3 Express failure with a handler

effect fail(why: Text): i64

fn safe_div(a: i64, b: i64): i64 {
  if b == 0 {
    perform fail("division by zero")
  } else {
    div(a, b)
  }
}

let answer := handle { safe_div(84, 0) } with {
  fail(why), k => 0 - 1
  return value => value
}
perform show("answer", answer)

// Handle division failure by discarding the remaining computation.

・ safe_div

answer = -1

answer = -1

This handler does not call k. It returns -1 without returning to the remaining computation, producing an exception-like early exit.

The standard library also has a fail, declared as fail<E>: (e: E) -> Never resume 0. Its result is Never and its resumption quantity is 0: it does not resume. The fail declared in this example is a separate, local operation. For an effect that never resumes, do not write k at all.

9.4 Effect rows

An annotation such as ! {out_of_bounds} after a function's result type describes the effects that remain for its caller to handle. ! {} means that no effects remain. Effect rows are checked when functions are composed.

Exercise 9.1: What value would the program produce if the handler became ask(n), k => k(n) * k(n + 1)?