Tutorial 2: Effects and Handlers

The key feature of Helium is an approach to control operators that is based on algebraic effects and their handlers. In the following, we briefly introduce these features from a programmer's perspective.

Effect signatures and operations

In Helium, effects are a special brand of types that track what computational effects can be performed by a given computation. They are declared locally and available only within their scope, and the type system makes sure that an effect cannot escape its scope. New effects can be introduced by declaring their signature. For example, we can declare a simple effect, Error, as follows:

signature Error (A : Type) =
| fail : forall {T : Type}, A => T

This definition specifies that the Error effect has one operation called fail, which we can use as any other identifier. This operation has the following polymorphic type:

fail : forall (`a : Error 't) {'s : Type}, 't ->[`a] 's

This means we can apply fail to any argument and use the resulting expression in any context, but the resulting computation will have an effect Error a associated with it (possibly, among other effects). The first universally quantified varible `a says that this operation works for any instance of the effect Error. Instances are discussed in the next section, we can safely ignore them for now. The type of fail means that we cannot simply use fail in the REPL, as the only effects the REPL expects is IO and RE (runtime error):

[IO,RE]> fail 5;;
repl:1:1-4: error: There is no implicit scope which can bind instance of signature Error 'a.

Effect handlers

How, then, can we call a computation that performs an effect (other than IO or RE) from the REPL? We have to provide a handler. Note that we didn't give a definition of what the fail operation does — it is simply a "constructor" of the Error effect. The interpretation of this constructor is a job for a handler. For example, given a computation that may use the fail operation, we could wrap its result in the usual Option datatype, returning Some if the result was computed successfully, and None if we encounter an error. The definition of such a handler in Helium looks as follows:

let hErrorOpt =
  handler
  | fail _   => None
  | return n => Some n
  end

We can then use this newly defined handler with a computation that may perform an effect:

[IO,RE]> handle 2 + 2 with hErrorOpt;;
Some 4 : Option Int
[IO,RE]> handle 2 + fail () with hErrorOpt;;
None : Option Int

Resuming the computation

The particularly appealing aspect of effect handlers is the they can resume the computation after encountering an operation. For example, let us look at another simple effect, Reader:

signature Reader (A : Type) =
| ask : Unit => A

We can define a simple computation using the Reader effect:

let c () = ask () * ask () + 17

and handle it to provide the ask operations with an answer — say, 5:

[IO, RE]>
handle c () with
| ask () => resume 5
end;;
42
: Int

Note that when there is no explicit return clause, identity is taken as a default. For convenience, we also provide a way of naming the resumption: the above handler can be declared as follows:

let with5 c =
  handle c with
  | ask () / r => r 5
  end

Wiki

helium / popl20 / Tutorial_EffectsAndHandlers

Tutorial 2: Effects and Handlers

Effect signatures and operations

Effect handlers

Resuming the computation