I'm publishing this series ahead of Code BEAM Europe this October, where I'll reveal Bondy, a new declarative language for the BEAM: statically typed, functional, relational and rule-based.

Here is an Erlang spec:

-spec price(Order :: order()) -> integer().

It tells you what goes in and what comes out. It does not tell you whether price/1 reads a config file or calls a pricing service over the network. Nor does it say whether it writes to an ETS cache, sends a message to a logger, or asks the clock what day it is. All of those are invisible in the signature. All of them change what you can safely do with it: call it twice, cache its result, run it on another node, or call it from inside a rule.

Erlang handles this for guards by limiting them to a fixed list of built-in functions, since the runtime can't know whether anything else has side effects. You can write when is_integer(X), X > 0 but not when valid_price(X). It's safe, and it means any non-trivial condition moves out of the guard and into the body.

Bondy keeps the safety and drops the restriction. The compiler works out what every function may do, and a guard can call any function it can show is harmless.

Capabilities

A capability is something a function may do beyond computing its result. The kinds include the file system, the network, ETS tables, the process dictionary, processes and their messages, the clock and random numbers. The compiler infers, for every function, the set of capabilities its body uses, including everything it calls. You write no annotations for this.

That set is part of the function's type. A function type in Bondy is not only "takes Int, returns Int" but "takes Int, returns Int, and may do these things". Keeping it on the type, rather than in a side table, is what makes the next section work.

A function whose set is empty does nothing but compute. The compiler describes functions with a small vocabulary of laws:

• pure: it changes nothing outside itself, and the only outside things it reads are the clock and random numbers. Writing, sending, spawning and reading an ETS table all make a function impure.
• deterministic: the same input always gives the same output. No clock, no randomness, no outside state.
• total: it always returns.
• idempotent: applying it twice gives the same result as applying it once, f(f(x)) == f(x). Normalising data is the typical case, and so is unifying a value with a fixed shape: doing it again adds nothing.
• monotone: giving it more information never gives you less back. This is what lets the engine run a function over data that is still arriving.

Each law includes the ones below it: a monotone or idempotent function is also deterministic, and a deterministic function is also pure. total is separate.

idempotent and monotone both include deterministic, which includes pure. The compiler checks these two only for functions whose body it can analyse, such as a one-argument function that unifies its argument with a fixed shape. For anything else, you state them as a hint (below).

Stating a law, and having it checked

You can write a law down with @law, and the compiler checks it:

@law(:pure, :deterministic)
public function double(x: Int) :: Int -> 
    x * 2

@law(:pure)
public function shout(msg: String) :: String ->
    IO.println(msg)
    msg

double compiles. shout does not:

Function shout/1 declares @law(:pure) 
but the analysis cannot prove it: its inferred capability set 
is not empty. This is not a proof that the law is false: the 
analysis is sufficient, not complete. Restructure the function into 
the fragment the compiler recognises, or carry the law as 
@law(pure: :hint) to assert it untested

The message is careful about what it knows. The analysis never calls something pure that is not, but it may fail to prove that something is pure when it is. When that happens and you know better, @law(pure: :hint) records the claim without the check, and the difference between checked and trusted stays visible in the code.

Reading the clock shows the difference between the first two laws. This function is pure, because it only reads the clock, but it is not deterministic:

@law(:pure)
public function now_ms() :: Int -> 
    Time.system_time()

That compiles. Declare it @law(:deterministic) instead and the compiler refuses: "its inferred capability set admits nondeterminism".

Guards

Back to the rules post. A rule's when guard runs while the engine decides which rule fires. If a guard wrote to a log, the log would depend on the order the engine tried rules in. If it read the clock, the same facts could fire different rules on different runs. So a guard can call your own functions, and the compiler requires them to be deterministic and to always return:

constraint Reading = {sensor: String, value: Int}
event Alarm        = {sensor: String}

function too_hot(v: Int) :: Bool -> 
    v > 100

rule alarm =
    on
        Reading(sensor: s, value: v) as r
    remove
        r
    when
        too_hot(v)
    tell
        Alarm(sensor: s)
    end

too_hot has no annotations, and the rule compiles, because the compiler infers that too_hot does nothing but compare. Use a version with a debug print instead:

function too_hot_logged(v: Int) :: Bool ->
    IO.println("checking")
    v > 100

and the rule is rejected:

Function too_hot_logged/1 is called 
from a CHR rule guard but is not verified as pure and deterministic. 
A guard is evaluated during rule matching, where an effect or a 
nondeterministic result changes which rules fire; CHR rule guards 
require @law(:deterministic) and @law(:total).

The rule's body, its tell section, has no such restriction. It runs once the engine has decided, so it is the right place for effects.

Pure if its argument is pure

Plenty of functions take other functions:

public function twice(f: ((Int) :: Int), x: Int) :: Int -> 
    f.(f.(x))

Is twice pure? It depends entirely on f. A system that summarised each function with a single yes or no would have to answer "no", to be safe, and every caller of twice would inherit the "no". Because Bondy keeps capabilities on the function type, twice's type says instead that it does whatever f does. The answer is settled at each call:

@law(:pure, :deterministic)
public function quad(x: Int) :: Int -> 
    twice(fun(y) -> y * 2 end, x)

That compiles, and quad(3) is 12. Pass twice a function that prints, and the same @law line on the caller fails with law_not_verified. This is what lets functions that take functions be used inside guards and pure code without giving up the checks.

Limiting what a function may do

@law says what a function does not do. @capability says the most a function may do, as an upper limit the compiler holds the body to:

@capability(kind: :ets, mode: :read_write)
public function remember(table, key, value) ->
    Table.insert(table, (key, value))

That compiles. Declare the same body as read-only:

@capability(kind: :ets, mode: :read)
public function sneaky(table, key, value) ->
    Table.insert(table, (key, value))

and the body is caught writing:

Function sneaky/3 declares @capability (ets, Atom, read), but its 
body captures (ets, Atom, write), which the declaration does not 
cover. Widen the declaration to cover it, or compile with 
--laws=trust to assert the narrower declaration.

The same attribute goes on an @external, a Bondy binding to an Erlang function, to say what the foreign code does. For Erlang functions the compiler already knows about, such as file:read_file/1, it checks your declaration against what it knows. For the rest, your declaration is what it trusts.

Where it is checked

The compiler does not check capabilities at every call. Ordinary code calls whatever it likes, as it does in Erlang. The checks sit at the places where an effect would break a promise:

• a function that declares a @law or a @capability
• a rule guard
• the body of a derivation rule, which must be deterministic for a query to have one answer
• a default or computed field in a shape, which may be evaluated more than once or in any order
• code compiled as untrusted (below)

Each of these asks the same question: are the capabilities of this function within what is allowed here? For guards and deterministic functions, the allowance is empty. A pure function is also allowed the clock and random numbers.

Untrusted code is the case this was built for. A compilation unit can be compiled in safe mode, with an explicit allowance: the capabilities the host grants it, for example "read and write ETS, nothing else". The compiler rejects a function that needs more. The unit also cannot declare its own laws, because code that is not trusted cannot vouch for itself. It is aimed at plugins, user-supplied logic, and code generated by tools rather than people. Today safe mode is an option of the compiler API, but there is no command-line switch for it yet.

What is not built yet

The capability kinds today are fairly coarse. A finer-grained ordering, where a grant for "this ETS table, read only" can stand in for a narrower request, is designed but not built. So are capabilities that can be handed from one process to another as values, scoped to a single interaction. I will write about both when they compile.

Why this design

Two choices shaped it.

Inferred, not declared. You can write @law and @capability, but you never have to. Ordinary code carries no annotations, and the compiler still knows what every function may do. Annotations appear only where you want a promise enforced.

Tracked, not handled. Languages such as Koka treat effects as operations that handlers can intercept and redefine. Bondy does not. It tracks what a function may do and checks it where it matters. That is all the BEAM needs: processes, messages and supervisors already cover what effect handlers are usually used for.

What you get is a spec that finally includes the part the Erlang spec left out. The rest of the series leans on it. Rules can call your functions, queries always have one answer, and code you did not write can run with only the capabilities you granted it.