# 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.
```

Updated