Tutorial 3: Effect instances

Modularity of effects

One amazing feature of effect handlers is modularity. For example, we define the Choice effect that consists of one operation, choose, which takes a list of elements as its argument and returns a single element. We define a standard handler that interprets this signature as a nondeterministic choice and collects all possible results on a list:

signature Choice =
| choose : forall {T : Type}, List T => T

let rec concatMap f xs =
  match xs with
  | []       => []
  | x :: xs' => f x @ concatMap f xs'
  end

let hChoice =
  handler
  | choose xs => concatMap resume xs
  | return x  => [x]
  end

Another effect is Error, already described in the previous section:

signature Error =
| fail : forall {T : Type}, Unit => T

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

let div x y =
  if y = 0
    then fail ()
    else x / y

Now, we come up with a computation e that uses both Choice and Error. There are two natural ways to combine these two effects: one is when a single failure applies to the entire computation, killing off all nondeterministic branches, while in the other the failure is local, affecting only the current branch. We can achieve both scenarios simply by reordering handlers:

[IO,RE]> let e () = div 100 (choose [0,1] + choose [5,0]);;
[IO,RE]> handle handle e () with hChoice with hErrorOpt;;
None
: Option (List Int)
[IO,RE]> handle handle e () with hErrorOpt with hChoice;;
[Some 20, None, Some 16, Some 100]
: List (Option Int)

Effect instances

Modularity as in the example above is achieved easily, because each handler knows which effect it handles. But how one can use the same effect combined with itself? For example, we can define the "mutable memory cell" effect as follows:

signature State (S : Type) =
| put : S    => Unit
| get : Unit => S

let hState init =
  handler
  | put s     => fn _ => resume () s
  | get _     => fn s => resume s s
  | return x  => fn _ => x
  | finally f => f init
  end

What if we wanted to use two such cells? Helium now offers a mechanism to distinguish between instances, as in the following example, in which we use two memory cells, called respectively `a and `b:

let fib n =
  handle `a in handle `b in
    let rec aux n =
      if n = 0
        then get `a ()
        else (put `b (get `a () + get `b ());
              put `a (get `b () - get `a ());
              aux (n - 1))
    in aux n
  with hState 1 with hState 0

The syntax handle `a in e with h means that in the expression e we can decorate the operations of the effect with instance annotation `a. Think of `a as a variable bound in e by the handler. Since instance variables cannot mix with other values, there is a separate syntax for them: they are identifiers preceded by a backtick `.

Instance abstraction

Since instance variables are bound by handlers, how can we write a function that invokes some effects, but does not handle them? The answer is: take the instances as arguments. Since we have a separate syntax for them, they won't be confused with the usual arguments.

let swap `a `b () =
  let c = get `a ()
  in (put `a (get `b ());
      put `b c)

Now, we can take a look at the type of swap:

[IO,RE]> swap;;
<func> : forall (`a : State 't) (`b : State 't), Unit ->[`a,`b] Unit

It means that swap takes two instances, both of the effect State 't for a type 't. The annotation [`a,`b] in the type Unit ->[`a,`b] Unit means that the type-and-effect system of Helium discovered that when applied to an argument, the function swap may invoke effects on the instances `a and `b. We can use swap simply giving it instances as arguments:

let foo () =
 handle `a in handle `b in handle `c in
   swap `a `b ();
   (get `a (), get `b (), get `c ())
 with hState 1 with hState 2 with hState 3

Automatic instance abstraction and application

It is often the case that we do not want to bother with instances. Consider, for example, the following function that manipulates state:

let update f = put (f (get ()))

Quite obviously, update is concerned only with one instance of state. In such situations, Helium will automatically add appropriate instance abstractions and applications, so that the function above is equivalent to

let update_explicit `a f = put `a (f (get `a ()))

To see that it is the case, let's look at the type of update:

[IO,RE]> update;;
<func> : forall (`a : State 't), ('t ->[`a,'e] 't) ->[`a,'e] Unit

We can see that the system added the forall quantification over instances.

The same applies to handlers. If there is only one handler for a particular effect in the scope, it is Ok not to mention the instances at all. For example, the code

handle
  put 2;
  update (fn x => x*x);
  printInt (get ())
with hState 0

is equivalent to

handle `a in
  put `a 2;
  update `a (fn x => x*x);
  printInt (get `a ())
with hState 0

The system was simply clever enough to notice that there is only one instance of state in the context in which put, get, and update are called. In particular, the following does not type-check:

handle `a in handle `b in
  put 2
with hState 0 with hState 0

Obviously, the system cannot know if put refers to the instance `a or `b. The error message says so:

[IO,RE]>
handle `a in handle `b in
  put 2
with hState 0 with hState 0;;
repl:3:3-5: error: Ambiguous instance of signature State 't. Try applying it explicitly.

Wiki

helium / popl20 / Tutorial_Instances

Tutorial 3: Effect instances

Modularity of effects

Effect instances

Instance abstraction

Automatic instance abstraction and application