Algebraic Handler Lookup in Koka, Eff, OCaml, and Unison

Algebraic Handler Lookup in Koka, Eff, OCaml, and Unison
âť“
This was a report from GPT3o-mini with Deep Research
đź’­
What are the different ways to do handler look up in programming languages that support algebraic effects? I know sometimes, they're also called "abilities" in some languages. A starting point of languages that I know support algebraic effects are, Koka, Eff, Multicore OCaml, and Unison. There might be other languages that support algebraic effects, and I'd like for you to add those languages to the list and look into them as well.

So for each languages that support algebraic effects that you gathered, detail
1. how the handler lookup mechanism works
2. how the types enforce that the correct effects are raised
3. how the types enforce that all raised effects are handled somewhere. 4. how the language enforces the algebra of the effects. Before you begin, are there any other details I should be asking you for?

You're already asking very insightful and detailed questions! To ensure I provide the most useful information for you, here are a few clarifications:

  1. Scope of Languages: Should I focus only on languages with first-class support for algebraic effects, or would you also like information on languages that approximate them with monads or delimited continuations?
  2. Practical Examples: Would you like code samples demonstrating how each language handles effect lookup, type enforcement, and algebra enforcement?
  3. Comparison and Trade-offs: Would you be interested in a comparison of different handler lookup mechanisms across languages, highlighting their trade-offs in terms of expressiveness, performance, and ease of reasoning?
  4. Runtime vs. Compile-Time Guarantees: Do you want an exploration of how much of effect handling is enforced statically by types vs. dynamically at runtime?
  5. Use Cases: Are you particularly interested in any real-world applications of these mechanisms, such as concurrency, error handling, or modular program composition?

Let me know if these additional angles would be helpful, and I’ll tailor my research accordingly!

đź’­
1. Only languages with first class support.
2. Show a practical example of usage, yes. So defining a method that raises an effect with types, a handler that handles said type. and any algebraic enforcement of the effects. Use the same example for all languages, so I can compare and contrast them.
3. Yes. that would be very helpful.
4. Yes, only in the sense of what can you do dynamically at runtime? I'm currently using Python to implement a single resumption algebric effects, so typing is limited to static typing. I want to know what I'm missing out on if a language could access types at runtime as well, like in Haskell or Unison.
5. No, I'm mainly interested in how handler lookups work, and what the pros and cons of different choices of how handler dispatching works, and how effect types fit into the picture. Thanks!

Great! I will investigate how handler lookup works in programming languages with first-class algebraic effects, including Koka, Eff, Multicore OCaml, and Unison, along with any other relevant languages. I will also explore how their type systems ensure correct effect raising and handling, and how they enforce the algebra of effects.

Additionally, I will:

  • Use the same example across all languages to illustrate effect raising, handling, and enforcement.
  • Compare the different handler lookup mechanisms and their trade-offs.
  • Highlight the runtime capabilities of these languages regarding effect handling, especially in contrast to a dynamically typed language like Python.

I'll get back to you with a detailed breakdown soon!


Algebraic Effects and Handler Lookup in Various Languages

Algebraic effects allow defining operations (effects) separately from their implementation. A handler gives meaning to these operations by intercepting them and possibly resuming the computation. We compare how several languages with first-class algebraic effects implement handler lookup and enforce effect discipline.

Koka

1. Handler Lookup Mechanism: Koka uses evidence passing for handlers, meaning the compiler transforms effectful code to explicitly carry handler “evidence” as hidden parameters​

college-de-france.fr. Rather than a runtime stack search, an effect operation is dispatched in O(1) by directly calling the corresponding handler via the evidence. In other words, the nearest handler is determined at compile-time by the lexical scope and passed in, avoiding a linear search on the call stack​college-de-france.fr.

2. Type System Enforcement (Correct Effects Raised): Koka’s type system tracks effects using row polymorphism​

college-de-france.fr. The type of a function includes a set of effects it may perform. For example, one can define an effect and a function as:

effect state<a> {
  fun get() : a
  fun set(x: a) : ()
}

fun addAndGet(n: int) : <state<int>> int {
  val x = get()
  set(x + n)
  x + n
}

Here addAndGet has type int -> <state<int>> int, indicating it may perform the state<int> effect​

github.com. The compiler ensures you can only call get() or set() inside a function whose effect type includes state<int>; attempting to perform an effect not listed in the type is a type error.

3. Ensuring All Effects Are Handled: Koka provides effect safety, meaning any effect raised must be handled by some enclosing handler or be reflected in the function’s effect type​

v2.ocaml.org. If a function with an effect (e.g. <state<int>>) is called in a context that doesn’t allow that effect, the type checker rejects it. This ensures that by the time you reach a “pure” boundary (like the program’s main), all effects have been handled (eliminated from the type). In practice, you handle effects by running a computation under a handler. For example, Koka’s standard library provides combinators to run a state effect:

fun runStateExample(): int {
  // Run addAndGet with an initial state of 0 using a state handler
  handle (state<Int>) with { | get -> currentState 
                              | set(newState) -> () } in {
    // initial state
    var currentState: int = 0 
    addAndGet(5)            // performs state operations
  }
}

The above is illustrative; actual Koka syntax may differ, but the idea is that the handle block provides implementations for get and set and an initial state.)

The type of runStateExample is pure (int with no effects) because the state effect is handled within it. Unhandled effects cannot “leak” to the top level in Koka – they must appear in the type and ultimately be handled.

4. Enforcing the Algebra of Effects: In Koka, an effect is declared with a set of operations (an algebraic interface), and any handler for that effect must implement how each operation behaves. The effect algebra refers to the laws or behavior of those operations. Koka’s design doesn’t automatically enforce specific algebraic laws (e.g. commutativity of independent operations) – that’s up to the semantics of your handler – but it does enforce the structure: you cannot invoke an operation that wasn’t declared, and you must handle (or propagate) all operations in a pure context. Because effects are tracked in types, the compiler can reorder independent effects safely and even infer when an effect is effectively unused (e.g. a state handled and removed yields a pure result)​

arxiv.org​arxiv.org. This means the presence or absence of effects is rigorously checked, which aligns with treating effects as an algebraic theory in the type system.

5. Dynamic Capabilities vs. Python: Algebraic effects allow capturing and manipulating the continuation of a computation – for example, a handler can intercept an operation, perform some logic, and then resume the computation. This enables advanced control flow like resumable exceptions, backtracking, or coroutines within the language​

v2.ocaml.org​v2.ocaml.org. In Koka (and similar languages), you can dynamically install different handlers at runtime to change the behavior of effectful operations without changing the effectful code. For instance, the same addAndGet function could be run with one handler that logs state changes, or another that just provides a mutable cell, simply by choosing a different handler. This kind of dynamic dispatch of effects with guaranteed type safety is hard to achieve in a dynamically typed language like Python. Python lacks a built-in mechanism to capture a function’s continuation and resume it later – you’d have to simulate with generators, context managers, or by manually passing callbacks, which is far less general and safe. Moreover, Python’s dynamic typing can’t enforce that a given “effect” (like an expected exception or callback) is handled; any mistakes would surface as runtime errors. In contrast, Koka ensures at compile time that effectful operations are accounted for, and at runtime its handlers can even resume or replay computations (e.g. try an operation multiple times) – something not directly possible in Python without implementing a custom control flow.

Eff

1. Handler Lookup Mechanism: Eff (a research language by Bauer and Pretnar) treats effect handlers similarly to exception handlers, but generalized. You wrap a computation with a with ... handle ... block that installs a handler​

math.andrej.com. When an effect operation is performed inside that computation, control transfers to the nearest enclosing handler that has a clause for that operation. This lookup is dynamic, following the call stack: an unhandled effect bubbles outward until a matching handler is found (just like unwinding for exceptions)​v2.ocaml.org. Internally, Eff can be understood in terms of multi-prompt delimited continuations, where each effect type acts like a prompt/tag; performing an effect searches for the matching prompt in the stack. The first matching handler captures the continuation and handles the operation.

2. Type System Enforcement (Correct Effects Raised): Eff is statically typed and has a type and effect system​

math.andrej.com. Every function’s type can include an effect component (often a set of effect labels) indicating which effects it may perform. You can only perform an operation if the effect is declared in the current context’s effect type. For example, in Eff one might declare:

operation Get : int      (* declares an effect operation returning int *)
operation Put : int -> () 
let addAndGet x = 
  let curr = Get in       (* perform Get operation *)
  let ()  = Put (curr + x) in  (* perform Put operation *)
  curr + x 
(* The inferred type of addAndGet might be: int -> int !{State} *)

The notation !{State} (hypothetical syntax) indicates this function can perform the State effect. Eff’s compiler will infer or check these effect annotations​

arxiv.org​arxiv.org. If you attempt to perform an effect not in the type, the program is rejected.

3. Ensuring All Effects Are Handled: Eff provides effect safety much like Koka​

v2.ocaml.org. An unhandled effect in Eff is a compile-time error; you cannot simply run a computation that might perform effects without handling them. To eliminate an effect from the type, you wrap the computation in an appropriate handler. Eff’s effect typing is non-monotonic, meaning that when you handle an effect, it is removed from the effect set of that computation’s type​arxiv.org. For instance, if addAndGet has effect State, then an expression with stateHandler(initial=0) handle addAndGet(5) would be pure (the handler consumes the State effect). If any effect remains unhandled by the time you reach the top level, the program won’t typecheck. Thus, all raised effects must be accounted for by some handler. (Eff does not provide a default behavior for effects—“there is no need for a default behaviour to start with”, so unhandled effects are simply not allowed​eff-lang.org.)

4. Enforcing the Algebra of Effects: In Eff, an effect is essentially an interface consisting of operations, and a handler gives an implementation (an algebra) for those operations​

math.andrej.com​math.andrej.com. The language ensures that a handler covers the operations you care to handle, and any not handled explicitly will remain in the effect type, forcing an outer handler. This effectively means that to completely handle an effect, you must provide interpretations for all of its operations. Eff’s rigorous effect type system allows equational reasoning about effects – for example, one can prove that two sequences of operations commute if their effect sets don’t interfere​arxiv.org. However, the language itself doesn’t enforce algebraic laws like commutativity; it simply provides the framework (handlers and effect types) so that programmers or researchers can reason about and ensure such laws. In essence, Eff enforces the structure of the algebra (each operation is invoked and handled explicitly) and leaves the semantics (the laws) to the handler implementations and external reasoning.

5. Dynamic Capabilities vs. Python: Eff demonstrates many dynamic tricks impossible or unsafe in Python. A handler in Eff can capture the continuation of a computation at the point an effect is performed, allowing the handler to decide if, when, and how to resume that computation​

v2.ocaml.org​v2.ocaml.org. For example, one could implement backtracking search by capturing a continuation and invoking it multiple times with different choices – effectively cloning the computation for each choice. Python does not support capturing an arbitrary call stack segment and re-running it; at best, one can use generators or threads to achieve limited forms of backtracking or coroutines, but these are ad-hoc and not enforced by the language’s type system. Moreover, in Eff you can dynamically layer handlers – e.g., handle an output effect by appending to a log, or swap in a handler that completely silences the output​eff-lang.org​eff-lang.org. Achieving the same in Python would require monkey-patching global behavior or passing around callback hooks, with no compile-time guarantees. Eff’s approach allows, for instance, treating all state modifications as transactional by wrapping a state handler that can roll back on error, which would be extremely complex to do reliably in Python. All these dynamic control-flow manipulations in Eff are type-safe, meaning if your program compiles, you haven’t forgotten to handle a case – a guarantee Python lacks.

Example (Eff): To mirror the state example, in Eff you might write:

operation Get : int
operation Put : int -> ()

let addAndGet n : int !{State} =
  let curr = Get in           (* perform state read *)
  Put (curr + n);             (* perform state write *)
  curr + n

(* A handler for the State effect: *)
let stateHandler init = handler
  | val x       -> x                        (* result case *)
  | #Get k      -> k! init init             (* on Get, k is the continuation; pass the state as result and current state *)
  | #Put new k  -> k! () new                (* on Put, update state and resume *)
in

with stateHandler(0) handle addAndGet 5    (* runs addAndGet with initial state 0, yielding 5 and final state discarded or accessible if handler returns it *)

This is pseudo-code illustrating an Eff handler. The handler treats the computation as a function from state to result (the continuation k is invoked with the appropriate state). After handling, the effect {State} is removed from the type. Trying to use addAndGet without a handler or outside a {State} context would be a compile error.

Multicore OCaml (OCaml 5+)

1. Handler Lookup Mechanism: OCaml 5 introduced effect handlers as an extension to the language​

news.ycombinator.com. In OCaml, performing an effect is done via perform EffectName(arguments) and handlers are installed with a syntax similar to exceptions using pattern matching. The lookup is dynamic and works like unwinding the call stack: when perform E is executed, the runtime jumps to the nearest surrounding handler that matches effect E​v2.ocaml.org. If none is found in the current function, it unwinds to the caller, and so on. This is analogous to exception lookup, except the handler pattern is marked with the effect keyword. For example:

effect Get : int        (* declare an effect *)
effect Put : int -> unit

let addAndGet n =
  let x = perform Get in        (* raise Get effect *)
  let () = perform (Put (x + n)) in  (* raise Put effect *)
  x + n

(* Using the effect with a handler *)
let result =
  try addAndGet 5 with
  | effect Get k ->       (* handle Get by providing a state *)
      (* here k is the continuation; resume it with the state value *)
      continue k state_value 
  | effect (Put new_val) k ->
      state_value := new_val;   (* update state *)
      continue k ()

This handler intercepts Get and Put. The special pattern effect E p, k binds k to the continuation. OCaml supports deep handlers (handle all effects in the block) and shallow handlers (handle one effect at a time)​

v2.ocaml.org, but in both cases, it’s the innermost dynamically enclosing handler that catches a performed effect.

2. Type System Enforcement (Correct Effects Raised): Unlike Koka or Eff, OCaml’s type system does not track effects in types. Effects are more like exceptions: any function can perform E without mentioning E in its type. The only static check is that the type of the performed effect’s payload matches its declaration. For instance, perform Get is only allowed if Get : int Effect.t (so it returns an int)​

v2.ocaml.org. But there’s no static annotation that addAndGet is effectful. In other words, OCaml functions do not have an effect signature – the type system won’t stop you from calling an effectful function in a context that isn’t handling the effect. The responsibility is on the programmer to know which effects might be raised. The effect declaration itself uses OCaml’s extensible variant type mechanism (extending the built-in Effect.t type), which ensures only valid effect constructors can be performed​v2.ocaml.org, but beyond that, “correct effects” are not enforced by the type system.

3. Ensuring All Effects Are Handled: OCaml does not provide compile-time effect safety​

v2.ocaml.org. If you perform an effect and no handler for it exists dynamically, the runtime will raise a special Effect.Unhandled exception at the point of the perform​v2.ocaml.org. This is a runtime error analogous to an uncaught exception. For example, if addAndGet 5 is called outside of any handler for Get/Put, the program will throw Effect.Unhandled Get. There is no static guarantee all effects are handled – it’s up to the developer to ensure handlers are in place. (This is a deliberate design trade-off in OCaml to keep the type system simple; “unlike languages such as Eff and Koka, effect handlers in OCaml do not provide effect safety”​v2.ocaml.org.)

4. Enforcing the Algebra of Effects: OCaml’s language runtime enforces one important aspect of effect algebra: linearity of continuations. Once an effect’s continuation (k) is captured in a handler, OCaml ensures you resume it at most once​

v2.ocaml.org​v2.ocaml.org. If you attempt to continue k twice (or not at all), OCaml raises a runtime error (Continuation_already_resumed for double resume)​v2.ocaml.org. This effectively treats continuations as one-shot – ensuring that effects like state or I/O aren’t accidentally performed more times than intended via multiple resumption (which could violate linear resource usage​v2.ocaml.org). Aside from this, OCaml doesn’t enforce algebraic laws of effects – you can implement any semantics in handlers. Because OCaml doesn’t require handlers to handle every operation of an effect (effects are declared individually), you could have an effect with multiple operations and only handle some of them, leaving others unhandled (leading to Unhandled exceptions if actually performed). The algebraic structure (which operations exist for an effect) is defined by how you extend the Effect.t type (each effect X : ... adds a constructor), but there’s no requirement that a handler provide cases for all of them. In practice, to fully define an effect’s meaning you’d handle all its operations, but the language won’t stop you from handling only a subset (unhandled ones just propagate outward).

5. Dynamic Capabilities vs. Python: OCaml’s effect handlers bring powerful dynamic control to an otherwise statically typed language. At runtime, you can capture the execution state at an effect and decide what to do – e.g., pause the computation or schedule it elsewhere. Indeed, a primary use-case in OCaml is to implement lightweight concurrency (threads, generators) using effect handlers​

v2.ocaml.org​v2.ocaml.org. For example, one can create a scheduler where an effect Yield captures a continuation representing a “paused thread” and the handler stores it, later resuming those continuations to round-robin schedule tasks​v2.ocaml.org​v2.ocaml.org. This kind of inversion of control – where a function deep in the call stack yields control and is resumed later – cannot be done transparently in Python. Python’s generators and async/await provide some similar abilities, but those require the functions to be written in a specific style (using yield or await), whereas effect handlers can turn any regular function into a coroutine by handling an effect. Moreover, effect handlers can be composed: you can have multiple different handlers for different effects co-existing, intercepting different operations. In Python, composing different cross-cutting concerns (logging, exception handling, state threading) often requires messy combinations of context managers, decorators, or frameworks. OCaml’s approach lets you do this dynamically with clear separation of concerns. While Python can simulate some of these patterns, it cannot ensure at compile time that a given “effect” is handled, nor can it capture and resume arbitrary call stack segments as first-class values – which is exactly what algebraic effects provide.

Example (OCaml): Using the earlier Get/Put example, in OCaml:

(* Define effects *)
effect Get : int
effect Put : int -> unit

let addAndGet n =
  let x = perform Get in        (* might raise Get effect *)
  perform (Put (x + n));        (* might raise Put effect *)
  x + n

(* Running addAndGet with a handler *)
let (result, final_state) =
  let state = ref 0 in
  try 
    (addAndGet 5, !state) 
  with
  | effect Get k -> 
      let curr = !state in
      continue k curr            (* resume addAndGet, substituting the result of perform Get with curr *)
  | effect (Put new_val) k ->
      state := new_val; 
      continue k ()              (* resume, substituting perform Put with () *)

In this pseudo-code, state is a reference (since OCaml has mutable refs) capturing the state. After the try...with, result would be 5 and final_state would be 5 (the updated state). If we call addAndGet outside of the try handler, it would raise Effect.Unhandled Get at runtime​

v2.ocaml.org.

Unison

1. Handler Lookup Mechanism: Unison implements algebraic effects via its abilities system. The lookup of a handler in Unison is more structured: you use a handle ... with ... block to run a computation with a given ability handler​

unison-lang.org. This is lexically scoped, but at runtime it acts similarly to dynamic scope – when a computation requires an ability (performs an effect), it is handled by the nearest enclosing handle that provides that ability. Internally, Unison transforms the code so that calls to ability operations are routed to the handler. The handler is typically a function that pattern-matches on requests. For example:

ability State a where
  get : a           -- operation to get the state
  put : a -> ()     -- operation to set the state

-- A function using the State ability:
addAndGet n : '{State Nat} Nat =    -- `{State Nat}` denotes an ability requirement
  x = State.get
  State.put (x + n)
  x + n

-- A handler for State that uses a mutable reference
handleState : Nat -> Request (State Nat) r -> r
handleState initial req =
  case req of
    {State.get -> k}    ->       -- handle `get` requests
      handleState initial (continue k initial)
    {State.put new -> k} ->      -- handle `put` requests
      handleState new (continue k ())
    {r -> _} ->                 -- final result `r` (when computation is done)
      (r, initial)

handle addAndGet 5 with handleState 0 will run addAndGet 5 with initial state 0. The mechanism ensures that any call to State.get or State.put inside addAndGet is intercepted by handleState. In Unison, this lookup is guaranteed by the compiler transformation – you cannot call an ability operation without a corresponding handler in scope (the code won’t compile)​

unison-lang.org.

2. Type System Enforcement (Correct Effects Raised): Unison’s type system makes abilities explicit in function types. A function type is written Input ->{Ability} Output​

unison-lang.org. For example, addAndGet might have type Nat ->{State Nat} Nat, meaning it requires the State Nat ability. The compiler checks that any call to a function is in a context that provides the required abilities​unison-lang.org. If you attempt to perform an ability operation without that ability in your context, you get a compile-time ability check failure​unison-lang.org​unison-lang.org. In practice, this means you either call addAndGet inside a handle ... with ... for State Nat, or your calling function itself must be annotated to require State Nat (propagating the requirement). Thus, Unison ensures you only raise effects (make ability requests) that are declared. The ability set in the type acts like a contract – you can’t do a sneaky effect that’s not in the type.

3. Ensuring All Effects Are Handled: In Unison, any ability requirements must be satisfied by the environment. At the top level (in a program or a pure function), the ability set must be empty (top-level definitions are required to be pure)​

unison-lang.org. This forces all effects to be handled by the time you leave a handle block or exit a function. If an ability is not handled, the program simply won’t typecheck (“a type error will result if an ability is required in a scope where it is not provided by an enclosing handle”​unison-lang.org). This is strict effect safety. For example, if main : '{IO} () (meaning main does IO), the runtime will likely handle the IO ability by actually performing the IO (Unison has some built-in abilities like IO that are ultimately handled by the runtime), but you cannot have an ability like State unhandled at the top – you’d need to wrap it in a handler that, say, uses a pure state or converts it to an output value. Unison thus statically guarantees all ability requests are accounted for by some handler.

4. Enforcing the Algebra of Effects: Unison’s abilities are declared much like interfaces with a set of operations (see the ability State a where ... syntax above). The language requires that any handler for an ability provides a function that accepts a Request of that ability​

unison-lang.org. This Request object encapsulates either a request (with a constructor corresponding to one of the ability’s operations and a continuation) or the final result. A handler function must pattern match on all possible request constructors it wants to handle. If it omits some (say a handler only matches State.get but not State.put), then any State.put will not be handled by that handler and will bubble to an outer handler (or cause a compile error if none). In practice, to fully handle an ability, you implement all its operations. The compiler doesn’t force you to cover every constructor in one handler (you could have a chain of handlers each handling different operations of the same ability), but it ensures that if something isn’t handled, it remains as a requirement in the type. Unison’s design (inspired by Frank​unison-lang.org) maintains the algebraic structure by making the ability an explicit parameter of the computation. Notably, a Unison handler can choose to ignore the continuation (k) or call it multiple times​unison-lang.org, enabling algebraic manipulations like aborting a computation or duplicating it (for nondeterminism). These are not arbitrary gotos; they must respect the ability’s interface. While Unison doesn’t check algebraic laws (e.g. you could implement handlers that don’t obey state laws, if you wanted), its pure functional nature means you can reason about handler behavior. The ability system does enforce that abilities compose and distribute correctly – for instance, ability polymorphism is handled by type polymorphism, and an empty ability set means a computation is pure (no effects)​unison-lang.org​unison-lang.org.

5. Dynamic Capabilities vs. Python: Unison’s abilities allow for very dynamic behaviors while still being statically checked. At runtime, you can provide different handlers to the same computation to change its outcome. For example, you might run a parser with an ability Choice using one handler that finds the first successful parse or another that collects all possible parses. The parser code doesn’t change; just the handler does. In a dynamically-typed language like Python, achieving this would require designing the parser to call into user-provided callbacks or using exceptions for backtracking – techniques that are error-prone and not enforced by the language. Unison can also perform multi-shot continuations easily – a handler can call the continuation multiple times to, say, explore different branches (for nondeterministic effects)​

unison-lang.org. Python doesn’t support copying a call stack to implement such logic; you’d have to manually manage recursion or threads. Furthermore, Unison’s type system ensures that if a function is pure (no abilities), it really can’t do I/O or mutate state – something you can never be sure of in Python without reading all the code. At runtime, Unison’s effect handling allows features like distributed computation (abilities for distributed nodes), where a handler might send requests over the network – all while the core logic is written as a pure sequence of calls. This separation of concerns (pure logic vs. effect interpretation) is much harder to achieve in Python, where concerns tend to tangle (for instance, printing or logging can happen anywhere with no guarantee it’s caught or redirectable). In short, Unison offers the dynamic flexibility of hooking into a program’s operations (like one could with monkey-patching in Python) but in a disciplined, type-safe manner.

Example (Unison): Using the same state example:

ability State a where
  get : a
  put : a -> ()

addAndGet : Nat ->{State Nat} Nat
addAndGet n =
  x = State.get       -- perform get
  State.put (x + n)   -- perform put
  x + n

-- A simple state handler that threads an integer state
handleState : Nat -> Request (State Nat) Nat -> Nat
handleState curr req =
  case req of
    {State.get -> k}      -> continue k curr |> handleState curr
    {State.put new -> k}  -> continue k ()   |> handleState new
    {result -> _}         -> result

-- Running the computation with a handler:
(handle addAndGet 5 with handleState 0)  -- returns 5, with state internally updated to 5

In this pseudo-Unison code, handleState is a recursive function that processes a Request (State Nat) Nat. It uses pattern matching to handle get and put requests, updating the state accordingly, and when the computation finishes ({result -> _} case), it returns the final result. The use of continue k ... resumes the captured continuation k with a value. If we didn’t provide a handleState handler and tried to use addAndGet 5 in a pure context, the Unison compiler would complain that the ability State Nat is not available (i.e., unhandled).

Other Languages with Native Algebraic Effects

  • Idris 2: Idris 2 is a dependently-typed language that includes algebraic effects in its core library. Its approach is similar to Unison’s abilities – effects are described as interfaces (with operations), and programs requiring effects get those in their type. Handlers in Idris 2 can be written to interpret those effects. One unique aspect is that Idris 2 can use linear types to ensure certain effects (like IO) are handled linearly (each request used exactly once), combining effect safety with resource safety. The handler lookup in Idris 2 is lexical (you call effectful code within a do-block that provides a handler), and the type system, being very powerful, can even express dependencies between effect usage and program state.

Frank: Frank is a research language that heavily influenced Unison​unison-lang.org. It explores a type-directed style of effect handling, where instead of an explicit handle syntax, functions can take handlers as arguments in a more seamless way. In Frank, an effectful function’s type specifies what handler it expects, and providing that handler is like passing an argument. This means handler lookup is almost entirely determined at compile time by function application. The algebra of effects in Frank is enforced by its type system in a very strict way: the empty ability in Frank means “ability polymorphic” (contrasting with Unison)​unison-lang.org, so to handle an effect you actually instantiate that polymorphism with a concrete ability. Frank’s design makes effect handling feel more like ordinary function calls, improving reasoning at the cost of a steeper learning curve.

  • Links (Effekt, etc.): Some other languages and research projects, like Links (a web programming language) and Effekt (research project in Scala), also support algebraic effects natively. They typically use row-polymorphic effect types (like Koka/Eff) to track effects and ensure handlers are provided. The handler lookup in these systems is dynamic (searching for the nearest handler), but the type systems guarantee that search will succeed (or else the program is rejected). These languages often enforce that effect operations cannot be invoked except under a matching handler context, effectively providing the same safety and flexibility we see in Eff and Koka.

Comparison of Handler Lookup Mechanisms

Lookup Strategies: Broadly, we see two strategies: dynamic search versus static routing. Languages like Eff, Unison, and OCaml perform a dynamic lookup for the nearest handler at runtime (though guided by lexical scope). This is analogous to exception handling – flexible, but potentially with a small runtime cost (scanning stack frames or jumping to handler addresses). Koka, by contrast, uses static routing via evidence passing​

college-de-france.fr, essentially turning effect handling into direct function calls. This yields constant-time dispatch for effects and can be inlined or optimized by the compiler. The trade-off is complexity in the compiler (Koka’s compiler carries around evidence and does a monadic transformation​college-de-france.fr), whereas dynamic systems are often easier to implement (just like implementing exceptions).

Expressiveness: All these languages achieve similar expressiveness in terms of what you can do with effects (since they all implement the theoretical concept of algebraic effects). However, certain choices impact multi-shot vs one-shot continuations. Eff (the research language) and Unison allow multi-shot continuations (a handler can invoke a continuation multiple times or not at all)​

unison-lang.org, enabling powerful constructs like backtracking, probabilistic branching, or undoing and redoing computations. OCaml’s handlers are deliberately limited to one-shot continuations – once resumed, a continuation cannot be reused​v2.ocaml.org. This restricts expressiveness slightly (you can’t directly implement nondeterministic branching by resuming twice), but simplifies reasoning about resources and improves performance for concurrency use-cases​v2.ocaml.org. Koka’s approach, being based on pure functions, conceptually could allow multi-shot usage (since a continuation is just a function), but it might rely on the programmer to not misuse linear resources if they do so. In practice, each language’s decision here reflects its goals: OCaml targets efficiency and predictable semantics for systems programming, whereas Eff and Unison, being more high-level, explore the full generality of algebraic effects.

Performance: Dynamic handler lookup typically involves checking for a handler at the perform site. In OCaml, performing an effect is quite efficient – it doesn’t copy the whole stack (the continuation is a linked stack slice)​

v2.ocaml.org​v2.ocaml.org, and invoking the handler is similar to an exception throw plus a function call. Still, if effects are very frequent (e.g. millions of tiny operations), a dynamic search might incur overhead. Koka’s evidence-passing shines in that scenario: effect calls are basically direct calls (no search)​college-de-france.fr. This can make effectful code as fast as or faster than equivalent code using monads or other abstractions. On the other hand, evidence passing can make the generated code larger or more complex, as it threads extra parameters everywhere (though Koka’s compiler mitigates this with optimization). Another consideration is that static effect systems can enable compile-time optimizations: for example, if the compiler sees that an effect is handled by a handler that simply calls the default behavior, it could inline or remove the indirection. Dynamic systems have to handle it at runtime. That said, for most use-cases, the difference is minor unless you’re writing performance-critical code with lots of fine-grained effects.

Ease of Reasoning: Static effect typing (as in Koka, Eff, Unison) makes reasoning about code easier for the programmer and the compiler. You can tell from a function’s type what it might do (e.g., fn : A ->{IO, State} clearly might perform I/O and state). This is similar to how one reasons about checked exceptions in Java, but more flexible. It aids in understanding and refactoring – the type will complain if you forgot to handle something. It also enables local reasoning: you know a pure function can’t suddenly do I/O or mutation. By contrast, OCaml’s lack of effect annotations means you must rely on documentation or naming conventions to know if a function might perform an effect. This can make larger codebases harder to reason about (similar to unchecked exceptions or global state). On the flip side, dynamic/untyped effect handling is more ergonomic when writing quick code: you don’t have to change type signatures or introduce polymorphism every time you add a new effect. It’s a trade-off between safety and convenience.

Trade-offs and Conclusion: The handler lookup mechanisms reflect deeper design philosophies. Koka (and similar systems like Links/Effekt) chooses a compile-time, principled approach, yielding optimizable and statically verifiable code at the cost of a more complex type system. Eff and Unison aim to combine the best of both worlds: they have effect types for safety, but the runtime model is flexible and general (multi-shot continuations, etc.), which maximizes expressiveness. OCaml integrates effect handlers in a more conservative way – dynamic lookup, no effect types – making it easier to retrofit into an existing language and runtime, and easier for programmers who don’t want to deal with effect annotations, but giving up some static guarantees.

In terms of reasoning, languages with effect types allow equational reasoning and formal verification of effectful code (as seen in research, e.g., proving state effect laws​

arxiv.org​arxiv.org). They encourage thinking of effects as part of a function’s API. Dynamically-checked systems require you to reason in terms of possible runtime errors (uncaught effects) similarly to unchecked exceptions.

In summary, the choice of handler lookup and effect tracking affects how predictable and composable effectful code is. Static, lexically-resolved handlers (like in Koka) offer predictability and performance, while dynamic handler lookup (as in Eff/Unison/OCaml) offers flexibility – especially with first-class continuations that can be manipulated in novel ways. All these languages illustrate that algebraic effects bring a level of modularity to effectful programming (you can add, remove, or change effects by swapping handlers) that is hard to replicate in a language like Python. Python might simulate one or two of these patterns, but algebraic effects provide a uniform, language-supported way to implement complex control-flow abstractions with clear semantics and (in most of these languages) strong safety guarantees​ eff-lang.org​eff-lang.org.