An alternative effect API - #12736

Introduction

This PR proposes an alternative API for effects. Currently, the effect API is based around a single type of operations 'a Effect.t indexed by their return types (or arity in the literature). The core of this proposal is to replace this type by one that represents effects and is indexed by their effect type, which describes the operations of that effect.

The difference is best illustrated by an example. Currently, defining a shallow effect handler for integer state is done as follows:

type 'a Effect.t +=
  | Get : int Effect.t
  | Set : int -> unit Effect.t

let handle_counter init f x =
  let rec loop :
      type a r. int -> (a, r) continuation -> a -> r * int =
    fun state k x ->
      continue_with k x
        { retc = (fun v -> v, state);
          exnc = (fun e -> raise e);
          effc = (fun (type b) (eff : b t) ->
            match eff with
            | Get -> Some (fun (k : (b,r) continuation) ->
                loop state k state)
            | Set new_state -> Some (fun (k : (b,r) continuation) ->
                loop new_state k ())
            | e -> None) }
  in
  loop init (fiber f) x

The operations of state -- Get and Set -- are added to the type of operations. Then a handler is defined which handles those two operations. The call to continue_with (or indeed fiber) does not indicate which operations will be handled. The set of operations handled is represented by whether the effc function returns Some or None.

With the proposed API, the same handler is implemented by:

type int_state = effect
  | Get : int
  | Set : int -> unit

let counter : int_state Effect.t = Effect.create ()

let handle_counter init f x =
  let rec handle (state : int) = function
    | Result v -> v, state
    | Exn e -> raise e
    | Operation(Get, k) -> handle state (continue k state)
    | Operation(Set new_state, k) -> handle new_state (continue k ())
  in
  handle init (run counter f x)

Here we start by defining a new int_state effect type, describing the operations that make up the concept of integer state. Then we define a new effect counter that has that effect type. Then we define a handler for the counter effect. The call to run is explicitly passed counter as the effect to be handled.

You can see the API itself in the effect.mli file.

This PR doesn't include syntax for deep handlers as proposed in #12309. I have a half-finished branch for that on top of this API, but it needs a few more days work to finish.

Advantages

I think there are numerous advantages to the proposed API. I'm not necessarily claiming that it is impossible to achieve these things with the current API, but it is much more natural in the proposed one.

Aligns better with the theory

The proposed API is much closer to the theory of algebraic effects, where each algebraic effect is defined by a set of operations and equations on those operations.

Whilst not the most important advantage in itself, I think that in some sense the other advantages mostly stem from this one. If we only have a single type of operations we lose the ability to talk about actual algebraic effects and their operations. We cannot easily express the idea of a morphism between effects, and we cannot easily map between different representations of the same effect.

In addition to conflating effects and operations, the current API also conflates the mechanism for referring to an effect handler -- in the case of both these APIs that is a dynamically created value of type 'a Effect.t -- with the type of the effect handler -- i.e. it's operations. Computations using algebraic effects are a form of open term -- i.e. a term with free variables -- and conflating these two concepts is equivalent to conflating the name of a free variable with the type of that variable. This is discussed further in a recent talk I gave.

Exhaustivity checking

Associating operations with their effect allows us to talk about a handler for that whole effect, and gives exhaustivity warnings if a case is forgotten.

Currently, code like this give no error:

continue_with k x
  { retc = (fun v -> v, state);
    exnc = (fun e -> raise e);
    effc = (fun (type b) (eff : b t) ->
      match eff with
      | Get -> Some (fun (k : (b,r) continuation) ->
          loop state k state)
      | Set 0 -> Some (fun (k : (b,r) continuation) ->
          loop new_state k ())
      | e -> None) }

even though the handler does not handle Set for values other than 0.

Similarly, if we wish to add a new operation to an effect we must manually attempt to find all handlers for that effect and update them.

Supports different representations of effectful computation

By separating out the notion of effect type we can relate different representations of effectful computation.

For example, here is an implementation of "freer" monads:

type ('a, 'e) freer =
    | Pure : 'a -> ('a, 'e) freer
    | Impure : ('b, 'e) operation * ('b -> ('a, 'e) freer) -> ('a, 'e) freer

let return x = Pure x

let rec (>>=) m k =
  match m with
  | Pure x -> Pure (k x)
  | Impure(op, k') -> Impure(op, fun x -> k' x >>= k)

let perform_freer op = Impure(op, fun x -> Pure x)

And here is a function to translate that representation into the proposed effect API:

let rec run eff = function
  | Pure x -> x
  | Impure(op, k) -> run eff (k (perform eff op))

As another example, here is a simple API for named effect handlers:

type 'e handler

val perform_named : 'e handler -> ('o, 'e) operation -> 'o

val reperform_named :
  'e handler -> ('o, 'e) operation -> ('o, 'a) continuation -> 'a

type ('a, 'e) step =
  | Result of 'a
  | Exn of exn
  | Operation :
      ('o, 'e) operation * ('o, ('a, 'e) step) continuation -> ('a, 'e) step

val run_named : ('e handler -> 'a -> 'b) -> 'a -> ('b, 'e) step

Named handlers work by giving you a fresh name to refer to each handler directly -- the handler type above -- and then the user threads that value down to each corresponding use of perform. It's similar to systems based on capabilities.

And here are translations between named effect handlers and this proposed API:

let named_of_effect : 'e handler -> 'e Effect.t -> ('a -> 'b) -> 'a -> 'b
  fun handler eff f x ->
    let rec handle = function
      | Result x -> x
      | Exn e -> raise e
      | Operation(op, k) -> handle (reperform_named handled op k)
    in
    handle (run eff f x)

let effect_of_name : 'e Effect.t -> ('e handler -> 'a -> 'b) -> 'a -> 'b
  fun eff f ->
    let rec handle = function
      | Result x -> x
      | Exn e -> raise e
      | Operation(op, k) -> handle (reperform eff op k)
    in
    handle (run_named f x)

Note that all these transformations are completely generic in the type of the effect, which relies on having something in the type system that represents that type.

I'm particularly interested in supporting named effect handlers: using the local mode described in this blog post and this talk you can prevent unhandled effect errors, essentially giving a system of typed effects on the cheap.

Allows a simple shallow handler API

Separating out effect types from effects allows us to provide the a simple shallow handler API based on the step type:

type ('a, 'e) step =
  | Result of 'a
  | Exn of exn
  | Operation :
      ('o, 'e) operation * ('o, ('a, 'e) step) continuation -> ('a, 'e) step
(** [('a, 'e) step] is the result of running an effect handler until it
    returns a result, raises an exception or performs an operation. *)

val run : 'e t -> ('a -> 'b) -> 'a -> ('b, 'e) step
(** [run e f v] runs the computation [f v] handling effect [e]. *)

as opposed to the more complicated continue_with of the current API:

  type ('a,'b) handler =
    { retc: 'a -> 'b;
      exnc: exn -> 'b;
      effc: 'c.'c t -> (('c,'a) continuation -> 'b) option }
  (** [('a,'b) handler] is a handler record with three fields -- [retc]
      is the value handler, [exnc] handles exceptions, and [effc] handles the
      effects performed by the computation enclosed by the handler. *)

  val continue_with : ('c,'a) continuation -> 'c -> ('a,'b) handler -> 'b
  (** [continue_with k v h] resumes the continuation [k] with value [v] with
      the handler [h].

      @raise Continuation_already_resumed if the continuation has already been
      resumed.
   *)

This allows for much cleaner implementations of handlers, like the one for integer state in the introduction.

The simpler API relies on being able to specify the effect being handled explicitly in advance rather than every handler potentially handling all effects.

Easily supports multiple instances of the same effect

It is often useful to have multiple instances of the same effect. For example, using two pieces of state simultaneously. Such instances also often have parameterised effect types. This is awkward to represent currently, requiring functors (or first-class modules) over effect constructor definitions.

For example, here is the definition and a use of a generic handler for state in the current API:

module type State = sig
  type a
  type _ Effect.t += Get : a Effect.t
  type _ Effect.t += Set : a -> unit Effect.t
end

module Make (S : State) = struct

  let rec loop : type x y . S.a -> (x, y) continuation -> x -> y =
    fun s k ->
      continue_with k x {
        retc = (fun y -> y);
        exnc = raise;
        effc = fun (type b) (e : b Effect.t) ->
          match e with
          | S.Get () ->
              Some (fun (k : (b, _) continuation) -> loop s k  s);
          | S.Set  s ->
              Some (fun (k : (b, _) continuation) -> loop s k ());
          | _ ->
              None
      }

  let handle (s : S.a) (f : unit -> 'a) : 'a =
    loop s (fiber f) ()

end

module Counter = struct
  type a = int
  type _ Effect.t += Get : int Effect.t
  type _ Effect.t += Set : int -> unit Effect.t
end

module Message = struct
  type a = string
  type _ Effect.t += Get : string Effect.t
  type _ Effect.t += Set : string -> unit Effect.t
end

module Handle_counter = Make(Counter)
module Handle_message = Make(Message)

let foo () =
  Handle_counter.handle 0
    (fun () ->
       Handle_message.handle "Hello"
         (fun () ->
            ...
            perform Counter.Get;
            ...
            perform (Message.Set ...);
            ...))

With the proposed API this can be implemented as:

type 'a state = effect
  | Get : 'a
  | Set : 'a -> unit

let handle_state (type s) eff init f x =
  let rec handle (state : s) : (_, s state) step -> _ = function
    | Result res -> res, state
    | Exn e -> raise e
    | Operation(Get, k) ->
        handle state (continue k state)
    | Operation(Set new_state, k) -> handle new_state (continue k ())
  in
  handle init (run eff f x)

let counter = Effect.create ()
let message = Effect.create ()

let foo () =
  handle_state counter 0
    (fun () ->
       handle_state message "Hello"
         (fun () ->
            ...
            perform counter Get;
            ...
            perform message (Set ...);
            ...))

Supports general functions for manipulating effects

Separating effect names from effect types allows you to have general functions for manipulating effect names. For example, you can have a function that handles any effect by renaming it to another one:

val rename : from:'e Effect.t -> to_:'e Effect.t -> (unit -> 'a) -> 'a

Supports effect type abstraction

Separating effect names from effect types allows you to make the effect type abstract without necessarily making the name abstract. Without an effect system this distinction doesn't matter too much, and indeed there isn't even a static notion of equality on effect names yet, but if we ever attempt to track effects in the type system this distinction is very important. This paper tries to allow effect abstraction without that distinction and you can see how complicated it gets.

Better for teaching algebraic effects

This is clearly more subjective, but I believe that this API is much better for teaching algebraic effects and handlers.

Having a language-level notion of an effect type allows you to discuss the meaning of a particular effect. You can show the effect type for e.g. state and discuss its operations and the equations between those operations. That in turn allows you to discuss the relation to algebras and algebraic data-types.

The ability to translate between different representations of effectful computation makes it easier to discuss those other representations. It should fit much more naturally into a course also covering e.g. free monads.

I also think that the simpler shallow API is a little easier to grasp than the existing APIs or syntax for deep handlers. You just run a computation until it returns, raises or performs.

Supports more efficient implementation

Since the handled effect name is known in advance the matching logic can all be moved into the runtime, which should be noticeably more efficient. I haven't actually implemented this yet as I wanted to keep the diff on the runtime as small as I could.

Details

This PR is on top of #12735, and the first two commits come from that PR. The next commit makes an error message more precise so that it will still make sense with effect types. The next three commits adds the operation type and effect type declarations.

The operation type has two type parameters, the first is the return type of the operation, the second is the effect type to which the operation belongs.

effect type declarations have the form:

type t = effect
  | Op1 : ret
  | Op2 : arg -> ret

As with variant types, they simultaneously declare a type and some constructors. Unlike a variant type, the constructors produce values of the operation type rather than the effect type directly. The types can have type parameters, which can be referred to in the types of the operations.

The operations can be polymorphic. For example:

type t = effect
  | Choose : 'a * 'a -> 'a

defines an effect whose Choose operation is polymorphic in 'a. The type-checking for these is essentially the same as for existentials in a variant type.

The last two commits add the new effects API. The old API is implemented using the new one and made available as Effect.Legacy. I've made three copies of the tests that were in tests/effects, one in tests/effects-legacy using the old API, one in tests/effects-deep using deep handlers in the new API and one in tests/effects-shallow using shallow handlers in the new API.

Note that the deep handlers API is much more usable in combination with #12732. For instance, this scheduler in the old API without that PR:

let run main =
  let run_q = Queue.create () in
  let enqueue k = Queue.push k run_q in
  let dequeue () =
    if Queue.is_empty run_q then () else continue (Queue.pop run_q) ()
  in
  let rec spawn f =
    match_with f ()
      { retc = (fun () -> dequeue ());
        exnc =
          (fun e ->
            print_string (Printexc.to_string e);
            dequeue ());
        effc =
          (fun (type a) (e : a Effect.t) ->
            match e with
            | Yield ->
                Some
                  (fun (k : (a, unit) continuation) ->
                    enqueue k;
                    dequeue ())
            | Fork f ->
                Some
                  (fun (k : (a, unit) continuation) ->
                    enqueue k;
                    spawn f)
            | _ -> None); }
  in
  spawn main

becomes:

let run main =
  let run_q = Queue.create () in
  let enqueue k = Queue.push k run_q in
  let rec dequeue () =
    if Queue.is_empty run_q then () else continue (Queue.pop run_q) ()
  in
  let rec spawn f =
    run_with sched f ()
      { result = (fun () -> dequeue ());
        exn =
          (fun e ->
            print_string (Printexc.to_string e);
            dequeue ());
        operation =
          (fun op k ->
            match op with
            | Yield ->
                enqueue k;
                dequeue ()
            | Fork f ->
                enqueue k;
                spawn f) }
  in
  spawn main