Intrinsic Effects

At first glance Hemlock’s effects system looks pretty typical, but as soon as you notice that there is no support for effect handlers, you may wonder if Hemlock even has an effects system. And what is parametric mutability all about?

Hemlock’s effects/mutability system started out solely focused on how to specify interactions between mutable values and the language runtime. We wanted function signatures to comprehensively divulge their effects on mutable values, and thus the (hopefully) common case of pure function calls could be aggressively optimized without worrying about hidden effects. We had a relatively simple taxonomy of load/store effects both for the “internal” runtime environment and for the “external” operating system (OS). That seemed sufficient until we realized that halting is an effect we can’t always safely ignore.

Let’s look at an example where ignoring the hlt (may-halt) effect is okay. Consider division, where division by 0 halts execution.

# val assert 'a: bool >hlt-> a

# val validate_divisor: uns -> unit
let validate_divisor y =
    assert (y <> 0)

# val div: uns -> uns -> uns
let div x y =
    validate_divisor y
    x / y

The div function signature conceals the transitive hlt effect in assert, but that’s totally okay, because we don’t need to validate the inputs unless the result is actually needed by the program. But it’s not okay that validate_divisor conceals the hlt effect. The result of validate_divisor isn’t used, so the compiler can optimize out the call to validate_divisor! This is why we introduced the hlt effect, but as you can see, it’s not good enough to just give assert a hlt effect. validate_divisor also needs to have a hlt effect, because no data dependencies mandate its execution. This is why we added expose/conceal machinery to Hemlock (a story with its own twists and turns).

# val validate_divisor: uns >hlt-> unit
let validate_divisor y = expose hlt
    assert (y <> 0)

More recently we realized that a concealed-by-default alloc (automatic runtime allocation) effect can be used to prohibit allocation in low-level code. This means the garbage collector can safely be written in Hemlock!

Semi-convergent

I was unaware of the literature on algebraic effects systems until relatively recently, so it was a shock to see how similar Hemlock’s effects algebra looks relative to the one proposed for OCaml, as described in this presentation by Leo White. This recent Koka workshop got me thinking about how Hemlock’s effects system looks similar in many ways, but it’s a very different beast.

As mentioned, Hemlock does not have effect handlers; instead its effects are intrinsic to computations. In other words, there are fundamental computations at the foundation of Hemlock’s runtime which are labeled as having e.g. st (store) effects, but there’s no “handling” of those effects; they simply occur as a transitive side effect of computation. The effects system is an inviolable contract between the programmer and the compiler that informs program behavior and valid optimizations.

One could rightly argue that the lack of effect handlers reduces available functionality. Indeed Hemlock eschews non-local control flow (continuations, effect handlers, exceptions, coroutines, generators, async/await, etc.) in favor of shared-nothing asynchronous actor-based parallelism. On the flip side, Hemlock’s approach to effects appears to have some advantages:

• There is no run-time overhead.
• Concealable effects protect against brittle API problems, as exemplified by Java’s checked exceptions.
• Effect prohibition (e.g. of alloc) may enable highly constrained low-level programming.

We try really hard to base Hemlock on designs which have proven effective in other languages. But Hemlock’s effects/mutability system addresses a niche that to our knowledge has barely been explored by other languages. We’ve had the luxury of several years(!) to iterate on a design that is barely recognizable from where we started, and the resulting approach looks very promising. May the implementation bear that out.