Introducing Effectful

This document introduces Effectful, an effect system embedded in python, designed for building composable and extensible software systems.

The key notions behind all effect systems are those of syntax and semantics, where syntax is the text you write on the page, and the semantics is the rules which give meaning to the text. Effectful lets you write these parts seperately, building them up as the program grows.

import functools

from effectful.ops.semantics import coproduct, fwd, handler
from effectful.ops.syntax import defdata, defop
from effectful.ops.types import Operation, Term


def fails(fn, raising=BaseException):
    """
    Ensures that `fn` raises an expected exception.
    If `fn` raises an exception matching `raising`, returns `None`.
    If `fn` raises an exception not matching `raising`, raises a `RuntimeError`
    If `fn` doesn't raise an exceptions, raises a `RuntimeError`.
    """
    try:
        fn()
        raise RuntimeError(f"{fn} should have failed, but didn't")
    except BaseException as e:
        if not isinstance(e, raising):
            raise RuntimeError(f"{fn} failed, but raised {e} instead of a {raising}")

Part 1: Adding Two Numbers

We can start by defining some syntax. In Effectful, we define syntax in terms of Operations, which can be used like functions. The following defines an add operation of two arguments, as well as a small test which verifies that our new operator handles numbers as we would expect.

@defop
def add(left: int, right: int) -> int:
    raise NotImplementedError("Not implemented")


def test_adding_two_numbers():
    assert add(1, 3) == add(2, 2)


assert isinstance(add, Operation)
fails(test_adding_two_numbers)

Our test currently fails, as there is no semantics given to the add syntax. In Effectful, all operations have a “default” semantics, a snippet of code which is run if the operation is called without an installed semantics. This code generally either throws an error or returns a None value.

Now that we have our syntax, what should our semantics look like? In Effectful, the semantics of an operator is just a function with the same call signature as that operator. Here’s a first pass:

def add_using_plus(left, right):
    if isinstance(left, int) and isinstance(right, int):
        return left + right
    else:
        raise NotImplementedError(f"Can't add {left} and {right}")

That seems like a rather natural semantics for addition. How do we associate it with our syntax?

To do this, we use the handler keyword, as follows:

with handler({add: add_using_plus}):
    test_adding_two_numbers()

Now our test passes without issue - we’ve defined a piece of syntax (the Operation called add) and given it a semantics (the function add_using_plus). The semantics only applies within the scope of the with block it’s used in, as with other ContextManagers.

A small bit of jargon: the handler function, as used before, takes as its argumnet a Mapping from Operations to Callable objects with the same signature. This Mapping is called an Interpretation, and is a first class value (it’s just a dictionary)

Part 2: Partially Static Data

By defining the syntax and semantics of the add operation separately, we’ve already gained quite a bit of power. Let’s see how we can extend our function to new domains:

x = defop(int)()


def test_adding_a_variable():
    assert add(x, 2) == add(x, 2)


fails(test_adding_a_variable)

with handler({add: add_using_plus}):
    fails(test_adding_a_variable)

To represent free variables, we use the defop helper to define a new 0-ary Operation. We can substitute values into variables by handling this operation with handler.

We’ve defined a variable x, along with a new test, which calls add on that instance. How should we deal with this? What we would like is a free object, a symbolic reification of the operation we wish to perform. In Effectful, this is called a Term:

def free_add(left, right) -> Term[int]:
    result = defdata(add, left, right)
    assert isinstance(result, Term)
    return result

Here, free_add just returns a Term representing the call to add itself, constructed by the special method Operation.__free_rule__ of add. A Term is just a record type. It takes an operation, a tuple of variadic arguments and a tuple of name-value pairs of keyword arguments.

We can install this as a semantics for the add operation, which would allow our new test to pass:

with handler({add: free_add}):
    test_adding_a_variable()
    fails(test_adding_two_numbers)

As the above test shows, we know that free addition works for variables, but it doesn’t work when adding two numbers: Syntactically, "1 + 3" != "2 + 2".

What we’d like to do is combine them. We could try to do something like that by hand:

def hand_mixed_add(left, right):
    if isinstance(left, int) and isinstance(right, int):
        return add_using_plus(left, right)
    else:
        return free_add(left, right)

This works, but we wouldn’t like to have to define this combination by hand. We’d like to define an open handler, a semantics for a program which can perform some computation or optionally defer to another semantics.

To do this in Effectful, we can modify our semantics to use the fwd keyword:

def eager_add(left, right):
    match left, right:
        case int(_), int(_):
            return add_using_plus(left, right)
        case _:
            return fwd()

The fwd() call defers execution to an outer interpretation, carrying along the arguments recieved by the original call. We can combine this open handler with an outer handler using the coproduct keyword:

mixed = coproduct({add: free_add}, {add: eager_add})

with handler(mixed):
    test_adding_two_numbers()
    test_adding_a_variable()

This is how we build larger applications in Effectful: each interpretation composes with the last, adding information and computational ability, much like an object-oriented program.

Part 3: Commutative Semigroups

We’ve seen how to define syntax using Operations, define and install semantics using handler, and combine semantics together using coproduct and fwd.

However, these are not helpful for performing more complex traversals, such as rewriting a value into normal form. Consider the following example:

y = defop(int)()


def test_mixed_together():
    assert add(add(x, 2), add(2, y)) == add(x, add(add(3, y), 1))


fails(test_mixed_together)

with handler(mixed):
    fails(test_mixed_together)

Some back-of-the-napkin math tells us that these are equivalent expressions, but how do we convince Effectful of that fact? We’d like to introduce some algebraic laws to the mix.

Specifically, \(\forall x, y, z \in \mathbb{N}\):

• add is commutative: \(y + x \equiv x + y\)

• add is associative: \(x + (y + z) = (x + y) + z\)

These laws can translated into rewrite rules:

• lexicographically order variables: \(y + x \Rightarrow x + y\)

• left-shift parenthesis: \(x + (y + z) \Rightarrow (x + y) + z\)

• order variables over parenthesis: \((a + y) + x \Rightarrow (a + x) + y\)

def commutative_add(left, right):
    match left, right:
        case Term(_, _, _), int(_):
            return add(right, left)
        case Term(lv, (), {}), Term(rv, (), {}) if id(lv) < id(rv):
            return add(right, left)
        case _:
            return fwd()


def associative_add(left, right):
    match left, right:
        case _, Term(_, (a, b), {}):
            return add(add(left, a), b)
        case _:
            return fwd()


# Additional law, requirement for normalization
# We could generalize this if we had an identity law as well
def associative_commutative_add(left, right):
    match left, right:
        case Term(_, (left, Term(mv, (), ())), {}), Term(rv, (), {}) if id(mv) < id(rv):
            return add(add(left, right), mv())
        case _:
            return fwd()

These semantic functions take the algebraic laws we wrote earlier and turned them into rewrite rules. Namely, we move expressions into a normal form by:

• moving constants to the left

• rewriting variables in lexicographical order

• Grouping towards the left

We often call add recursively inside of our semantics functions. When we do this, we gain access not only to the current semantic function, but also those above us and below us in the coproduct stack. This lets us perform fixed-point computations, which iteratively work over an entire structure.

When we install these rules, our test passes as expected:

add_stack = functools.reduce(
    coproduct,  # type: ignore
    (
        {add: free_add},
        {add: eager_add},
        {add: associative_commutative_add},
        {add: commutative_add},
        {add: associative_add},
    ),
)

with handler(add_stack):
    test_adding_two_numbers()
    test_adding_a_variable()
    test_mixed_together()