# State¶

Many programs, even pure programs, can benefit from locally mutable state. For example, consider a program which tags binary tree nodes with a counter, by an inorder traversal (i.e. counting depth first, left to right). This would perform something like the following:

We can describe binary trees with the following data type `BTree`

and `testTree`

to represent the example input above:

```
data BTree a = Leaf
| Node (BTree a) a (BTree a)
testTree : BTree String
testTree = Node (Node Leaf "Jim" Leaf)
"Fred"
(Node (Node Leaf "Alice" Leaf)
"Sheila"
(Node Leaf "Bob" Leaf))
```

Then our function to implement tagging, beginning to tag with a
specific value `i`

, has the following type:

```
treeTag : (i : Int) -> BTree a -> BTree (Int, a)
```

## First attempt¶

Naïvely, we can implement `treeTag`

by implementing a helper
function which propagates a counter, returning the result of the count
for each subtree:

```
treeTagAux : (i : Int) -> BTree a -> (Int, BTree (Int, a))
treeTagAux i Leaf = (i, Leaf)
treeTagAux i (Node l x r)
= let (i', l') = treeTagAux i l in
let x' = (i', x) in
let (i'', r') = treeTagAux (i' + 1) r in
(i'', Node l' x' r')
treeTag : (i : Int) -> BTree a -> BTree (Int, a)
treeTag i x = snd (treeTagAux i x)
```

This gives the expected result when run at the REPL prompt:

```
*TreeTag> treeTag 1 testTree
Node (Node Leaf (1, "Jim") Leaf)
(2, "Fred")
(Node (Node Leaf (3, "Alice") Leaf)
(4, "Sheila")
(Node Leaf (5, "Bob") Leaf)) : BTree (Int, String)
```

This works as required, but there are several problems when we try to
scale this to larger programs. It is error prone, because we need to
ensure that state is propagated correctly to the recursive calls (i.e.
passing the appropriate `i`

or `i’`

). It is hard to read, because
the functional details are obscured by the state propagation. Perhaps
most importantly, there is a common programming pattern here which
should be abstracted but instead has been implemented by hand. There
is local mutable state (the counter) which we have had to make
explicit.

## Introducing `Effects`

¶

Idris provides a library, `Effects`

[3], which captures this
pattern and many others involving effectful computation [1]. An
effectful program `f`

has a type of the following form:

```
f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs
```

That is, the return type gives the effects that `f`

supports
(`effs`

, of type `List EFFECT`

) and the type the computation
returns `t`

. So, our `treeTagAux`

helper could be written with the
following type:

```
treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]
```

That is, `treeTagAux`

has access to an integer state, because the
list of available effects includes `STATE Int`

. `STATE`

is
declared as follows in the module `Effect.State`

(that is, we must
`import Effect.State`

to be able to use it):

```
STATE : Type -> EFFECT
```

It is an effect parameterised by a type (by convention, we write
effects in all capitals). The `treeTagAux`

function is an effectful
program which builds a new tree tagged with `Ints`

, and is
implemented as follows:

```
treeTagAux Leaf = pure Leaf
treeTagAux (Node l x r)
= do l' <- treeTagAux l
i <- get
put (i + 1)
r' <- treeTagAux r
pure (Node l' (i, x) r')
```

There are several remarks to be made about this implementation.
Essentially, it hides the state, which can be accessed using `get`

and updated using `put`

, but it introduces several new features.
Specifically, it uses `do`

-notation, binding variables with `<-`

,
and a `pure`

function. There is much to be said about these
features, but for our purposes, it suffices to know the following:

`do`

blocks allow effectful operations to be sequenced.`x <- e`

binds the result of an effectful operation`e`

to avariable

`x`

. For example, in the above code,`treeTagAux l`

is an effectful operation returning`BTree (Int, a)`

, so`l’`

has type`BTree (Int, a)`

.

`pure e`

turns a pure value`e`

into the result of an effectfuloperation.

The `get`

and `put`

functions read and write a state `t`

,
assuming that the `STATE t`

effect is available. They have the
following types, polymorphic in the state `t`

they manage:

```
get : Eff t [STATE t]
put : t -> Eff () [STATE t]
```

A program in `Eff`

can call any other function in `Eff`

provided
that the calling function supports at least the effects required by
the called function. In this case, it is valid for `treeTagAux`

to
call both `get`

and `put`

because all three functions support the
`STATE Int`

effect.

Programs in `Eff`

are run in some underlying *computation context*,
using the `run`

or `runPure`

function. Using `runPure`

, which
runs an effectful program in the identity context, we can write the
`treeTag`

function as follows, using `put`

to initialise the
state:

```
treeTag : (i : Int) -> BTree a -> BTree (Int, a)
treeTag i x = runPure (do put i
treeTagAux x)
```

We could also run the program in an impure context such as `IO`

,
without changing the definition of `treeTagAux`

, by using `run`

instead of `runPure`

:

```
treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]
...
treeTag : (i : Int) -> BTree a -> IO (BTree (Int, a))
treeTag i x = run (do put i
treeTagAux x)
```

Note that the definition of `treeTagAux`

is exactly as before. For
reference, this complete program (including a `main`

to run it) is
shown in Listing [introprog].

```
module Main
import Effects
import Effect.State
data BTree a = Leaf
| Node (BTree a) a (BTree a)
instance Show a => Show (BTree a) where
show Leaf = "[]"
show (Node l x r) = "[" ++ show l ++ " "
++ show x ++ " "
++ show r ++ "]"
testTree : BTree String
testTree = Node (Node Leaf "Jim" Leaf)
"Fred"
(Node (Node Leaf "Alice" Leaf)
"Sheila"
(Node Leaf "Bob" Leaf))
treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]
treeTagAux Leaf = pure Leaf
treeTagAux (Node l x r) = do l' <- treeTagAux l
i <- get
put (i + 1)
r' <- treeTagAux r
pure (Node l' (i, x) r')
treeTag : (i : Int) -> BTree a -> BTree (Int, a)
treeTag i x = runPure (do put i; treeTagAux x)
main : IO ()
main = print (treeTag 1 testTree)
```

## Effects and Resources¶

Each effect is associated with a *resource*, which is initialised
before an effectful program can be run. For example, in the case of
`STATE Int`

the corresponding resource is the integer state itself.
The types of `runPure`

and `run`

show this (slightly simplified
here for illustrative purposes):

```
runPure : {env : Env id xs} -> Eff a xs -> a
run : Applicative m => {env : Env m xs} -> Eff a xs -> m a
```

The `env`

argument is implicit, and initialised automatically where
possible using default values given by instances of the following type
class:

```
class Default a where
default : a
```

Instances of `Default`

are defined for all primitive types, and many
library types such as `List`

, `Vect`

, `Maybe`

, pairs, etc.
However, where no default value exists for a resource type (for
example, you may want a `STATE`

type for which there is no
`Default`

instance) the resource environment can be given explicitly
using one of the following functions:

```
runPureInit : Env id xs -> Eff a xs -> a
runInit : Applicative m => Env m xs -> Eff a xs -> m a
```

To be well-typed, the environment must contain resources corresponding
exactly to the effects in `xs`

. For example, we could also have
implemented `treeTag`

by initialising the state as follows:

```
treeTag : (i : Int) -> BTree a -> BTree (Int, a)
treeTag i x = runPureInit [i] (treeTagAux x)
```

## Labelled Effects¶

What if we have more than one state, especially more than one state of
the same type? How would `get`

and `put`

know which state they
should be referring to? For example, how could we extend the tree
tagging example such that it additionally counts the number of leaves
in the tree? One possibility would be to change the state so that it
captured both of these values, e.g.:

```
treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE (Int, Int)]
```

Doing this, however, ties the two states together throughout (as well as not indicating which integer is which). It would be nice to be able to call effectful programs which guaranteed only to access one of the states, for example. In a larger application, this becomes particularly important.

The library therefore allows effects in general to be *labelled* so
that they can be referred to explicitly by a particular name. This
allows multiple effects of the same type to be included. We can count
leaves and update the tag separately, by labelling them as follows:

```
treeTagAux : BTree a -> Eff (BTree (Int, a))
['Tag ::: STATE Int,
'Leaves ::: STATE Int]
```

The `:::`

operator allows an arbitrary label to be given to an
effect. This label can be any type—it is simply used to identify an
effect uniquely. Here, we have used a symbol type. In general
`’name`

introduces a new symbol, the only purpose of which is to
disambiguate values [2].

When an effect is labelled, its operations are also labelled using the
`:-`

operator. In this way, we can say explicitly which state we
mean when using `get`

and `put`

. The tree tagging program which
also counts leaves can be written as follows:

```
treeTagAux Leaf = do
'Leaves :- update (+1)
pure Leaf
treeTagAux (Node l x r) = do
l' <- treeTagAux l
i <- 'Tag :- get
'Tag :- put (i + 1)
r' <- treeTagAux r
pure (Node l' (i, x) r')
```

The `update`

function here is a combination of `get`

and `put`

,
applying a function to the current state.

```
update : (x -> x) -> Eff () [STATE x]
```

Finally, our top level `treeTag`

function now returns a pair of the
number of leaves, and the new tree. Resources for labelled effects are
intialised using the `:=`

operator (reminisicent of assignment in an
imperative language):

```
treeTag : (i : Int) -> BTree a -> (Int, BTree (Int, a))
treeTag i x = runPureInit ['Tag := i, 'Leaves := 0]
(do x' <- treeTagAux x
leaves <- 'Leaves :- get
pure (leaves, x'))
```

To summarise, we have:

`:::`

to convert an effect to a labelled effect.`:-`

to convert an effectful operation to a labelled effectful operation.`:=`

to initialise a resource for a labelled effect.

Or, more formally with their types (slightly simplified to account only for the situation where available effects are not updated):

```
(:::) : lbl -> EFFECT -> EFFECT
(:-) : (l : lbl) -> Eff a [x] -> Eff a [l ::: x]
(:=) : (l : lbl) -> res -> LRes l res
```

Here, `LRes`

is simply the resource type associated with a labelled
effect. Note that labels are polymorphic in the label type `lbl`

.
Hence, a label can be anything—a string, an integer, a type, etc.

`!`

-notation¶

In many cases, using `do`

-notation can make programs unnecessarily
verbose, particularly in cases where the value bound is used once,
immediately. The following program returns the length of the
`String`

stored in the state, for example:

```
stateLength : Eff Nat [STATE String]
stateLength = do x <- get
pure (length x)
```

This seems unnecessarily verbose, and it would be nice to program in a
more direct style in these cases. provides `!`

-notation to help with
this. The above program can be written instead as:

```
stateLength : Eff Nat [STATE String]
stateLength = pure (length !get)
```

The notation `!expr`

means that the expression `expr`

should be
evaluated and then implicitly bound. Conceptually, we can think of
`!`

as being a prefix function with the following type:

```
(!) : Eff a xs -> a
```

Note, however, that it is not really a function, merely syntax! In
practice, a subexpression `!expr`

will lift `expr`

as high as
possible within its current scope, bind it to a fresh name `x`

, and
replace `!expr`

with `x`

. Expressions are lifted depth first, left
to right. In practice, `!`

-notation allows us to program in a more
direct style, while still giving a notational clue as to which
expressions are effectful.

For example, the expression:

```
let y = 42 in f !(g !(print y) !x)
```

is lifted to:

```
let y = 42 in do y' <- print y
x' <- x
g' <- g y' x'
f g'
```

## The Type `Eff`

¶

Underneath, `Eff`

is an overloaded function which translates to an
underlying type `EffM`

:

```
EffM : (m : Type -> Type) -> (t : Type)
-> (List EFFECT)
-> (t -> List EFFECT) -> Type
```

This is more general than the types we have been writing so far. It is
parameterised over an underying computation context `m`

, a
result type `t`

as we have already seen, as well as a `List EFFECT`

and a
function type `t -> List EFFECT`

.

These additional parameters are the list of *input* effects, and a
list of *output* effects, computed from the result of an effectful
operation. That is: running an effectful program can change the set
of effects available! This is a particularly powerful idea, and we
will see its consequences in more detail later. Some examples of
operations which can change the set of available effects are:

- Updating a state containing a dependent type (for example adding an element to a vector).
- Opening a file for reading is an effect, but whether the file really
*is*open afterwards depends on whether the file was successfully opened. - Closing a file means that reading from the file should no longer be possible.

While powerful, this can make uses of the `EffM`

type hard to read.
Therefore the library provides an overloaded function `Eff`

There are the following three versions:

```
SimpleEff.Eff : (t : Type) -> (input_effs : List EFFECT) -> Type
TransEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->
(output_effs : List EFFECT) -> Type
DepEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->
(output_effs_fn : x -> List EFFECT) -> Type
```

So far, we have used only the first version, `SimpleEff.Eff`

, which
is defined as follows:

```
Eff : (x : Type) -> (es : List EFFECT) -> Type
Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
```

i.e. the set of effects remains the same on output. This suffices for
the `STATE`

example we have seen so far, and for many useful
side-effecting programs. We could also have written `treeTagAux`

with the expanded type:

```
treeTagAux : BTree a ->
EffM m (BTree (Int, a)) [STATE Int] (\x => [STATE Int])
```

Later, we will see programs which update effects:

```
Eff a xs xs'
```

which is expanded to

```
EffM m a xs (\_ => xs')
```

i.e. the set of effects is updated to `xs’`

(think of a transition
in a state machine). There is, for example, a version of `put`

which
updates the type of the state:

```
putM : y -> Eff () [STATE x] [STATE y]
```

Also, we have:

```
Eff t xs (\res => xs')
```

which is expanded to

```
EffM m t xs (\res => xs')
```

i.e. the set of effects is updated according to the result of the
operation `res`

, of type `t`

.

Parameterising `EffM`

over an underlying computation context allows us
to write effectful programs which are specific to one context, and in some
cases to write programs which *extend* the list of effects available using
the `new`

function, though this is beyond the scope of this tutorial.

[1] | The earlier paper [3] describes the essential implementation details, although the library presented there is an earlier version which is less powerful than that presented in this tutorial. |

[2] | In practice, `’name` simply introduces a new empty type |

[3] | (1, 2) Edwin Brady. 2013. Programming and reasoning with algebraic
effects and dependent types. SIGPLAN Not. 48, 9 (September
2013), 133-144. DOI=10.1145/2544174.2500581
http://dl.acm.org/citation.cfm?doid=2544174.2500581 |