Adding an Effect System to OCaml

I am going to show work in progress on algebraic effects and an effect system for OCaml. I will first explain effect handlers and then demonstrate a prototype that tracks effects in types, including a way to reason about locally mutable state.

A side effect is an observable consequence of a computation other than its return value. Algebraic effects provide a way to describe effectful operations separately from the context that implements them. This is an intuition for the idea rather than a complete mathematical definition.

Suppose a computation gets an integer state, increments it, and sets it again. At the get operation, we can pause the computation, ask the surrounding context to supply the result, then resume the remainder with that value. The computation can be described without deciding how get and set are implemented.

This becomes useful when we want operations that a language does not natively provide. Even in OCaml, which already has state, operating-system interactions and exceptions, we may want a different kind of effect. The motivating example here is concurrency.

Consider a recursive function that performs fork to start concurrent work and yield to give another computation a turn. Its code describes the desired operations; an effect handler supplies their meaning. A small scheduler can maintain a queue of work and decide which continuation to run next.

When a computation yields, the handler receives a continuation representing the suspended remainder, puts it on the queue and resumes another item. When it forks, the scheduler queues the current continuation and runs the new function under the handler. Running the example produces interleaved output.

The perform-and-handle structure resembles exceptions. As an intuition for runtime behavior, an algebraic effect is like an exception that can be resumed. Ordinary exceptions illustrate the non-resumable case: a search function can raise Not_found when it cannot locate an element.

A handler can turn Not_found into None and a successful value into Some. OCaml’s match-with-exception form can delimit the handled computation more precisely than a broad try block: an unrelated exception raised outside the match’s scrutinee is not accidentally caught.

Generators provide another example. An even-number generator repeatedly increments a counter and performs a Return effect whenever it finds an even value. Rather than adding a special generator feature to the language, we can describe the operation and write a handler for it.

A handler that totals the first N results adds each returned value to an accumulator, counts it, and resumes the continuation until it has enough values. If the generator terminates normally, the handler can return the accumulated total. For an infinite even-number generator, that normal-return branch does not occur.

We can also implement a simple state effect. A factorial computation requests get and set operations; a handler turns it into a function that takes an initial state and threads the updated state through the remaining computation. This resembles the standard construction used for a state monad.

At runtime, entering a handler creates a fresh dynamically resizable, heap-allocated stack. Performing an effect packages that stack as a continuation and returns to the handler on the previous stack. Continuing reinstates the captured stack so execution resumes where it stopped.

There is a problem: a computation may perform an effect in a context that has no handler for it. An unhandled Not_found exception is the familiar example; an unhandled generator Return operation fails for the same underlying reason. We would like to catch this mismatch before running the program.

Monads are one way to represent effects in types. An exception-style result makes the possibility of Not_found visible in the type of both the search and its result, rather than leaving the exception implicit. That helps prevent an unhandled case.

But monadic code can require separate higher-order operations for pure and effectful functions, such as map and a monadic map. Combining multiple effects may require transformers or a new combined monad. Intermediate data structures and closures may also put more pressure on compiler optimization and inlining.

An effect system offers another approach: give each expression both a value type and an effect description, and include effects in function types. A function that performs get can say in its type that a suitable get handler is required in the surrounding context.

The effect description can be understood as the handlers needed to run the function safely. Operations with different labels can be reordered in the description; repeated operations with the same label can require meaningful ordering. A context that supports more effects can safely run a function that needs fewer.

For a head function that throws Empty on an empty list, the prototype shows Empty in the function’s type. Calling it without an appropriate handler is rejected. Likewise, the generator’s type records Return instead of misleadingly looking like a plain unit-to-unit function.

Higher-order functions need effect variables. If a function passed to list map performs an effect, calling map performs that effect too. An effect variable records this relationship without making a separate map for every possible effect.

Most higher-order functions pass through their argument functions’ effects in a regular way. The prototype uses shorthand arrow syntax for common effect variables, keeping types concise. Map is polymorphic in its effects: it can work with a pure function or propagate the effects of an impure one.

To test a larger example, I converted a concurrency library written by my colleague in London. The original library represents concurrent computations with a fiber type and uses return and bind. Its interface includes fork, futures, wait, yield and run.

In the effect-based interface, fork takes an ordinary function that performs asynchronous effects and returns a future; wait and yield also record the async effect. Run takes a computation with that effect and supplies a handler, yielding a function without it. The types make the handler’s role visible.

The prototype groups asynchronous operations behind an abstract async effect. Exposing each operation could make the computation extensible to other schedulers, while hiding the details gives the library freedom to change them. Here I chose abstraction because there were many operations and the design was still changing.

A small example prints two strings repeatedly, yields between them, forks another computation and waits for its future. The effect version removes the explicit bind and return calls, so the code can be written in direct style. Running it still produces the expected interleaving.

This design also works naturally with higher-order functions. I can map fork over a list and iterate over the futures to wait for them using ordinary list functions. The effect variable propagates the asynchronous operation instead of requiring a separate monadic list API.

Another example searches an association list whose values are futures, waiting only as needed. It can both perform asynchronous operations and throw a tracked Not_found effect. Both effects appear in the type; there is no need to define a special combined fiber-and-error monad for the example.

The tracked throw operation is distinct from a resumable perform: it cannot be resumed, so it need not carry a continuation in the same way. That distinction also gives the implementation room for a faster exception path.

So far the type system tracks algebraic effects. I also want to track OCaml’s existing effects, such as mutable state and I/O, to distinguish pure from impure functions. Pure functions have constrained behavior and are generally easier to reason about.

Imagine replacing reference allocation, reading and writing with new, get and set effects. A handler could maintain a store mapping references to values, allocate locations, read them and update them. The factorial example then works with this handler, provided references belong to the correct store.

Such an implementation would be much slower than directly accessing memory. The point is not to replace OCaml’s efficient runtime implementation: we can reason about built-in operations as if an enclosing handler implemented them, while retaining the fast implementation.

The same idea applies to file I/O. Conceptually the runtime handles operations such as opening and reading a file. For this prototype, I group the built-in operations into an io effect instead of exposing every operation separately in ordinary types.

Backward compatibility matters. The existing OCaml function arrow continues to allow built-in effects, while a new double-headed arrow denotes a function without those effects. Together with effect-variable shorthand, a small family of arrows can describe the standard library without rewriting all existing types.

The prototype follows a Haskell-like notion of purity: a pure function may diverge or raise an ordinary exception, but catching an exception is effectful. I propose using tracked throw for recoverable errors and ordinary raise for exceptional situations indicating a broken program.

To test usability, I converted an earlier version of the OCaml standard library: about 101 files and 22,000 lines, with roughly 4,000 changed lines. About half of the changes were the annotations I wanted; much of the rest concerned technicalities around printf that better inference could reduce.

The exercise also exposed polymorphic comparisons, which must be treated as potentially effectful because they can inspect mutable state. Replacing them with specific comparisons makes that hidden behavior visible. The resulting list signatures show pure functions and propagate effects of supplied functions where appropriate.

Arrays provide a contrasting example: creating or updating mutable storage has an effect, and an initializer function may have effects of its own. An audience question about arrow notation reveals a subtlety about whether an effect variable already contains I/O; the concise notation must preserve the intended combination.

A difficulty remains. A factorial function that creates a reference, mutates it locally and returns only the result is observationally pure from the outside, yet a simple state effect marks it impure. We want to handle its local state without allowing references from unrelated stores to become confused.

The proposed solution adds a region parameter to reference types and to their state effects. A region identifies the part of the program in which a reference is used. This resembles Rust lifetime tracking, though the speaker notes a distinction: an escaped reference may remain as a value while its required effect cannot be run.

The ordinary reference type can be represented using a global region. A new private construct introduces a local region and handles its state, allowing the factorial function to be typed as pure. Trying to use a reference from outside the region produces an effect mismatch instead of silently crossing stores.

The same mechanism can apply to mutable record fields, associating access with the relevant region. These features were prototype work, and regions plus region-annotated effects also suggest further ways to track locality.

For example, a with-file function could give a file a region and allow reads and writes only inside the scope that handles that region. In response to a question, I note that nested file regions may be unified, so the system preserves enough locality for safety but may not retain every distinction between files.

Another possible extension is to separate state reads and writes. An immutable region could allow reads without writes, and a freezing operation could permit local mutation before returning an immutable value. The example uses higher-rank polymorphism and may be too heavy for routine use.

Multi-handlers are another possible direction: a handler could run two computations side by side and respond to effects from both. A pipe, for example, could match a send from one computation with a receive from the other, while defining what happens if either side finishes first.

An audience member asks whether a different type representation for multi-handlers could avoid subtyping, perhaps using sigma types. I explain that the current approach mostly uses polymorphism and retains strong inference; I am reluctant to sacrifice OCaml’s inference strength without a compelling reason. The specific proposal deserves a longer discussion after the talk.