wiki

Effect handler

Performing an effect is like raising an exception that carries a way back[1][4]. The nearest enclosing handler for that effect receives the effect's value and a continuation, the rest of the computation up to the handler, and decides whether and how to resume it. Because the continuation is available, a handler can implement control structures that exceptions cannot: generators that suspend a traversal, schedulers that interleave threads, state, and asynchronous I/O whose callers look synchronous[6]. The idea comes from Plotkin and Power's algebraic effects[3] and Plotkin and Pretnar's handlers of 2009[1], was explored in languages such as Eff and Koka[4][5], and entered a mainstream language with OCaml 5 in 2022, whose handlers use one-shot continuations implemented as separately allocated stacks[2][7]. A handler is a delimited form of CPS: the continuation it receives is what a CPS transform would have passed explicitly, but the code performing the effect is written in direct style.

§ 01

Example

OCaml 5: an effect that asks the handler for an int. The handler answers 42 by resuming the continuation.

open Effect
open Effect.Deep
(* An effect that asks the handler for an int. *)
type _ Effect.t += Ask : int Effect.t
let run f =
match_with f ()
{ retc = (fun x -> x);
exnc = raise;
effc = (fun (type a) (eff : a Effect.t) ->
match eff with
| Ask -> Some (fun (k : (a, _) continuation) -> continue k 42)
| _ -> None) }

Running it.

43
1764

The effect Ask is declared as a constructor of the extensible GADT Effect.t, whose index is the type of the value perform returns. The handler's effc function inspects each effect and returns a function of the continuation k for the effects it handles, or None to let an outer handler handle it.

§ 02

Semantics

Let be an evaluation context with no handler for the operation . A deep handler with return clause and operation clause reduces by[1][4]:

The continuation passed to the operation clause, , is the context up to and including the handler: deep handlers reinstall themselves around the resumed computation, so every later effect is handled the same way. Shallow handlers, also available in OCaml as Effect.Shallow, do not, and the resumed computation must be handled again explicitly. An exception handler is the special case that never uses .

In the algebraic view, effects are operations of an algebraic theory, a computation is a tree of operations with values at the leaves, and a handler is a homomorphism out of that tree, which interprets each operation[3][1]. The same trees are the free monad of the operations, and handlers are their interpreters.

§ 03

Implementation

1. perform Askmainmatch_with (handler)f ()g xperform Askone stack: main, thenthe handled computation2. the handler runsmaineffc: continue k 42f ()g xperform Askk: the suspended frames,not copied3. continue k 42maineffcf ()g xAsk returns 42k reattached; its resultbecomes the handler's
In OCaml 5, a handled computation runs on its own stack segment, a fiber. Perform detaches the frames between it and the handler, which become the continuation k; continue reattaches them. Nothing is copied, so a continuation can be resumed only once.

OCaml 5 runs each handled computation on a fiber, a separately allocated stack segment that starts small and grows on demand[2]. perform unlinks the fibers between the current point and the matching handler and passes them to the handler as the continuation, and continue links them back. Both take time independent of the depth of the stack. Because the continuation is the suspended stack itself rather than a copy, it can be resumed at most once; resuming it again raises an exception[7].

Trying to resume a continuation twice, which nondeterministic search would need.

open Effect
open Effect.Deep
type _ Effect.t += Choose : bool Effect.t
(* Trying both answers needs the continuation twice. *)
let both f =
match_with f ()
{ retc = (fun x -> [ x ]);
exnc = raise;
effc = (fun (type a) (eff : a Effect.t) ->
match eff with
| Choose -> Some (fun (k : (a, _) continuation) -> continue k true @ continue k false)
| _ -> None) }

Running it.

Continuation_already_resumed

Multi-shot continuations, which copy the stack, support backtracking and probabilistic programming but make every continuation expensive; Eff and Koka provide them, and OCaml omits them[2][5].

§ 04

Uses

Generators

Any internal iterator can be turned into an on-demand sequence. The iterator performs an effect for each element, and the handler suspends the traversal there and returns the element with a way to continue.

A sequence from a tree iterator.

open Effect
open Effect.Deep
type tree = Leaf | Node of tree * int * tree
(* An internal iterator: it calls f on each element, in order. *)
let rec iter f = function
| Leaf -> ()
| Node (l, x, r) -> iter f l; f x; iter f r
(* Turn any iterator into an on-demand sequence: each element is performed
as an effect, and the handler suspends the traversal there. *)
let to_seq (type a) (iter : (a -> unit) -> unit) : a Seq.t =
let module M = struct type _ Effect.t += Yield : a -> unit Effect.t end in
let rec start () =
match_with iter (fun x -> perform (M.Yield x))
{ retc = (fun () -> Seq.Nil);
exnc = raise;
effc = (fun (type b) (eff : b Effect.t) ->
match eff with
| M.Yield x -> Some (fun (k : (b, _) continuation) -> Seq.Cons (x, fun () -> continue k ()))
| _ -> None) }
in
start

Running it: the traversal stops after the five elements that were requested.

first five: 1 2 3 4 5
elements visited: 5 of 1000000

State

A handler whose return type is a function of the current state can implement mutable state for code that is written as if the state were global[4].

Get and Put as effects.

open Effect
open Effect.Deep
type _ Effect.t += Get : int Effect.t | Put : int -> unit Effect.t
(* State as a handler: the handled computation becomes a function of the
current state, and each effect passes the state along. *)
let run_state (type r) (f : unit -> r) (init : int) : r * int =
let g =
match_with f ()
{ retc = (fun x s -> (x, s));
exnc = raise;
effc = (fun (type b) (eff : b Effect.t) ->
match eff with
| Get -> Some (fun (k : (b, int -> r * int) continuation) (s : int) -> continue k s s)
| Put s' -> Some (fun (k : (b, int -> r * int) continuation) _ -> continue k () s')
| _ -> None) }
in
g init
(* Code written in direct style, with no state in sight. *)
let count_to n =
for _ = 1 to n do perform (Put (perform Get + 1)) done;
"done"

Running it.

done, final state 15

Schedulers

Lightweight threads are computations whose suspended continuations wait in a queue. Yield enqueues the current continuation and resumes the next; Fork starts a new thread. The OCaml Eio library structures asynchronous I/O this way, with effects for operations that would block[2].

A round-robin scheduler in a dozen lines.

open Effect
open Effect.Deep
type _ Effect.t += Yield : unit Effect.t | Fork : (unit -> unit) -> unit Effect.t
(* A round-robin scheduler for cooperative threads. Suspended threads are
continuations waiting in a queue. *)
let run main =
let queue = Queue.create () in
let next () = if not (Queue.is_empty queue) then (Queue.pop queue) () in
let rec spawn f =
match_with f ()
{ retc = (fun () -> next ());
exnc = raise;
effc = (fun (type a) (eff : a Effect.t) ->
match eff with
| Yield -> Some (fun (k : (a, _) continuation) -> Queue.push (fun () -> continue k ()) queue; next ())
| Fork f -> Some (fun (k : (a, _) continuation) -> Queue.push (fun () -> continue k ()) queue; spawn f)
| _ -> None) }
in
spawn main
let worker name n () =
for i = 1 to n do
Printf.printf "%s%d " name i;
perform Yield
done

Running it.

a1 b1 a2 main1 b2 a3 main2
§ 05

Typing

OCaml 5 does not track effects in types: a function's type does not say which effects it may perform, and performing an effect with no handler raises Effect.Unhandled at run time[7]. Languages designed around effects, such as Koka, give functions row-typed effect annotations, so that the type checker ensures every effect is handled and the compiler can specialize handlers[5]. Tracking effects in types also makes explicit which code may be suspended, which matters when resources must be released.

§ 06

History

Delimited continuations, from Felleisen's prompts of 1988[8] and Danvy and Filinski's shift and reset, gave programs access to the rest of a computation up to a delimiter, and Filinski showed that they can represent any monadic effect[9]. Plotkin and Power developed algebraic effects from 2001[3], and Plotkin and Pretnar added handlers in 2009[1]. Bauer and Pretnar's language Eff[4], Kammar, Lindley and Oury's libraries for Haskell and other languages[6], and Leijen's Koka[5] explored programming with them. The Multicore OCaml project implemented one-shot handlers with fibers, and they were released in OCaml 5.0 in December 2022[2].

see also

referenced by

further reading

  1. [1]G. Plotkin, M. Pretnar, “Handlers of algebraic effects”, ESOP (2009).
  2. [2]K. C. Sivaramakrishnan, S. Dolan, L. White, T. Kelly, S. Jaffer, A. Madhavapeddy, “Retrofitting effect handlers onto OCaml”, PLDI (2021).
  3. [3]G. Plotkin, J. Power, “Algebraic operations and generic effects”, Applied Categorical Structures 11 (2003).
  4. [4]A. Bauer, M. Pretnar, “Programming with algebraic effects and handlers”, Journal of Logical and Algebraic Methods in Programming 84 (2015).
  5. [5]D. Leijen, “Type directed compilation of row-typed algebraic effects”, POPL (2017).
  6. [6]O. Kammar, S. Lindley, N. Oury, “Handlers in action”, ICFP (2013).
  7. [7]OCaml manual, “Effect handlers”.
  8. [8]M. Felleisen, “The theory and practice of first-class prompts”, POPL (1988).
  9. [9]A. Filinski, “Representing monads”, POPL (1994).

last updated