7Many programs, even pure programs, can benefit from locally mutable
8state. For example, consider a program which tags binary tree nodes
9with a counter, by an inorder traversal (i.e. counting depth first,
10left to right). This would perform something like the following:
14We can describe binary trees with the following data type ``BTree``
15and ``testTree`` to represent the example input above:
20 | Node (BTree a) a (BTree a)
22 testTree : BTree String
23 testTree = Node (Node Leaf "Jim" Leaf)
25 (Node (Node Leaf "Alice" Leaf)
27 (Node Leaf "Bob" Leaf))
29Then our function to implement tagging, beginning to tag with a
30specific value ``i``, has the following type:
34 treeTag : (i : Int) -> BTree a -> BTree (Int, a)
39Naïvely, we can implement ``treeTag`` by implementing a helper
40function which propagates a counter, returning the result of the count
45 treeTagAux : (i : Int) -> BTree a -> (Int, BTree (Int, a))
46 treeTagAux i Leaf = (i, Leaf)
47 treeTagAux i (Node l x r)
48 = let (i', l') = treeTagAux i l in
50 let (i'', r') = treeTagAux (i' + 1) r in
53 treeTag : (i : Int) -> BTree a -> BTree (Int, a)
54 treeTag i x = snd (treeTagAux i x)
56This gives the expected result when run at the REPL prompt:
60 *TreeTag> treeTag 1 testTree
61 Node (Node Leaf (1, "Jim") Leaf)
63 (Node (Node Leaf (3, "Alice") Leaf)
65 (Node Leaf (5, "Bob") Leaf)) : BTree (Int, String)
67This works as required, but there are several problems when we try to
68scale this to larger programs. It is error prone, because we need to
69ensure that state is propagated correctly to the recursive calls (i.e.
70passing the appropriate ``i`` or ``i’``). It is hard to read, because
71the functional details are obscured by the state propagation. Perhaps
72most importantly, there is a common programming pattern here which
73should be abstracted but instead has been implemented by hand. There
74is local mutable state (the counter) which we have had to make
77Introducing ``Effects``
78=======================
80Idris provides a library, ``Effects`` [3]_, which captures this
81pattern and many others involving effectful computation [1]_. An
82effectful program ``f`` has a type of the following form:
86 f : (x1 : a1) -> (x2 : a2) -> ... -> { effs } Eff t
88That is, the return type gives the effects that ``f`` supports
89(``effs``, of type ``List EFFECT``) and the type the computation
90returns ``t``. So, our ``treeTagAux`` helper could be written with the
95 treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
97That is, ``treeTagAux`` has access to an integer state, because the
98list of available effects includes ``STATE Int``. ``STATE`` is
99declared as follows in the module ``Effect.State`` (that is, we must
100``import Effect.State`` to be able to use it):
104 STATE : Type -> EFFECT
106It is an effect parameterised by a type (by convention, we write
107effects in all capitals). The ``treeTagAux`` function is an effectful
108program which builds a new tree tagged with ``Ints``, and is
109implemented as follows:
113 treeTagAux Leaf = pure Leaf
114 treeTagAux (Node l x r)
115 = do l' <- treeTagAux l
119 pure (Node l' (i, x) r')
121There are several remarks to be made about this implementation.
122Essentially, it hides the state, which can be accessed using ``get``
123and updated using ``put``, but it introduces several new features.
124Specifically, it uses ``do``-notation, binding variables with ``<-``,
125and a ``pure`` function. There is much to be said about these
126features, but for our purposes, it suffices to know the following:
128- ``do`` blocks allow effectful operations to be sequenced.
130- ``x <- e`` binds the result of an effectful operation ``e`` to a
131 variable ``x``. For example, in the above code, ``treeTagAux l`` is
132 an effectful operation returning ``BTree (Int, a)``, so ``l’`` has
133 type ``BTree (Int, a)``.
135- ``pure e`` turns a pure value ``e`` into the result of an effectful
138The ``get`` and ``put`` functions read and write a state ``t``,
139assuming that the ``STATE t`` effect is available. They have the
140following types, polymorphic in the state ``t`` they manage:
144 get : { [STATE t] } Eff t
145 put : t -> { [STATE t] } Eff ()
147A program in ``Eff`` can call any other function in ``Eff`` provided
148that the calling function supports at least the effects required by
149the called function. In this case, it is valid for ``treeTagAux`` to
150call both ``get`` and ``put`` because all three functions support the
153Programs in ``Eff`` are run in some underlying *computation context*,
154using the ``run`` or ``runPure`` function. Using ``runPure``, which
155runs an effectful program in the identity context, we can write the
156``treeTag`` function as follows, using ``put`` to initialise the
161 treeTag : (i : Int) -> BTree a -> BTree (Int, a)
162 treeTag i x = runPure (do put i
165We could also run the program in an impure context such as ``IO``,
166without changing the definition of ``treeTagAux``, by using ``run``
167instead of ``runPure``:
171 treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
174 treeTag : (i : Int) -> BTree a -> IO (BTree (Int, a))
175 treeTag i x = run (do put i
178Note that the definition of ``treeTagAux`` is exactly as before. For
179reference, this complete program (including a ``main`` to run it) is
180shown in Listing [introprog].
190 | Node (BTree a) a (BTree a)
192 instance Show a => Show (BTree a) where
194 show (Node l x r) = "[" ++ show l ++ " "
198 testTree : BTree String
199 testTree = Node (Node Leaf "Jim" Leaf)
201 (Node (Node Leaf "Alice" Leaf)
203 (Node Leaf "Bob" Leaf))
205 treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
206 treeTagAux Leaf = pure Leaf
207 treeTagAux (Node l x r) = do l' <- treeTagAux l
211 pure (Node l' (i, x) r')
213 treeTag : (i : Int) -> BTree a -> BTree (Int, a)
214 treeTag i x = runPure (do put i; treeTagAux x)
217 main = print (treeTag 1 testTree)
222Each effect is associated with a *resource*, which is initialised
223before an effectful program can be run. For example, in the case of
224``STATE Int`` the corresponding resource is the integer state itself.
225The types of ``runPure`` and ``run`` show this (slightly simplified
226here for illustrative purposes):
230 runPure : {env : Env id xs} -> { xs } Eff a -> a
231 run : Applicative m => {env : Env m xs} -> { xs } Eff a -> m a
233The ``env`` argument is implicit, and initialised automatically where
234possible using default values given by instances of the following type
239 class Default a where
242Instances of ``Default`` are defined for all primitive types, and many
243library types such as ``List``, ``Vect``, ``Maybe``, pairs, etc.
244However, where no default value exists for a resource type (for
245example, you may want a ``STATE`` type for which there is no
246``Default`` instance) the resource environment can be given explicitly
247using one of the following functions:
251 runPureInit : Env id xs -> { xs } Eff a -> a
252 runInit : Applicative m => Env m xs -> { xs } Eff a -> m a
254To be well-typed, the environment must contain resources corresponding
255exactly to the effects in ``xs``. For example, we could also have
256implemented ``treeTag`` by initialising the state as follows:
260 treeTag : (i : Int) -> BTree a -> BTree (Int, a)
261 treeTag i x = runPureInit [i] (treeTagAux x)
266What if we have more than one state, especially more than one state of
267the same type? How would ``get`` and ``put`` know which state they
268should be referring to? For example, how could we extend the tree
269tagging example such that it additionally counts the number of leaves
270in the tree? One possibility would be to change the state so that it
271captured both of these values, e.g.:
276 -> { [STATE (Int, Int)] } Eff (BTree (Int, a))
278Doing this, however, ties the two states together throughout (as well
279as not indicating which integer is which). It would be nice to be able
280to call effectful programs which guaranteed only to access one of the
281states, for example. In a larger application, this becomes
282particularly important.
284The library therefore allows effects in general to be *labelled* so
285that they can be referred to explicitly by a particular name. This
286allows multiple effects of the same type to be included. We can count
287leaves and update the tag separately, by labelling them as follows:
292 -> {['Tag ::: STATE Int,
293 'Leaves ::: STATE Int]} Eff (BTree (Int, a))
295The ``:::`` operator allows an arbitrary label to be given to an
296effect. This label can be any type—it is simply used to identify an
297effect uniquely. Here, we have used a symbol type. In general
298``’name`` introduces a new symbol, the only purpose of which is to
299disambiguate values [2]_.
301When an effect is labelled, its operations are also labelled using the
302``:-`` operator. In this way, we can say explicitly which state we
303mean when using ``get`` and ``put``. The tree tagging program which
304also counts leaves can be written as follows:
309 'Leaves :- update (+1)
311 treeTagAux (Node l x r) = do
316 pure (Node l' (i, x) r')
318The ``update`` function here is a combination of ``get`` and ``put``,
319applying a function to the current state.
323 update : (x -> x) -> { [STATE x] } Eff ()
325Finally, our top level ``treeTag`` function now returns a pair of the
326number of leaves, and the new tree. Resources for labelled effects are
327intialised using the ``:=`` operator (reminisicent of assignment in an
332 treeTag : (i : Int) -> BTree a -> (Int, BTree (Int, a))
333 treeTag i x = runPureInit ['Tag := i, 'Leaves := 0]
334 (do x' <- treeTagAux x
335 leaves <- 'Leaves :- get
338To summarise, we have:
340- ``:::`` to convert an effect to a labelled effect.
342- ``:-`` to convert an effectful operation to a labelled effectful
345- ``:=`` to initialise a resource for a labelled effect.
347Or, more formally with their types (slightly simplified to account
348only for the situation where available effects are not updated):
352 (:::) : lbl -> EFFECT -> EFFECT
353 (:-) : (l : lbl) -> { [x] } Eff a -> { [l ::: x] } Eff a
354 (:=) : (l : lbl) -> res -> LRes l res
356Here, ``LRes`` is simply the resource type associated with a labelled
357effect. Note that labels are polymorphic in the label type ``lbl``.
358Hence, a label can be anything—a string, an integer, a type, etc.
363In many cases, using ``do``-notation can make programs unnecessarily
364verbose, particularly in cases where the value bound is used once,
365immediately. The following program returns the length of the
366``String`` stored in the state, for example:
370 stateLength : { [STATE String] } Eff Nat
371 stateLength = do x <- get
374This seems unnecessarily verbose, and it would be nice to program in a
375more direct style in these cases. provides ``!``-notation to help with
376this. The above program can be written instead as:
380 stateLength : { [STATE String] } Eff Nat
381 stateLength = pure (length !get)
383The notation ``!expr`` means that the expression ``expr`` should be
384evaluated and then implicitly bound. Conceptually, we can think of
385``!`` as being a prefix function with the following type:
389 (!) : { xs } Eff a -> a
391Note, however, that it is not really a function, merely syntax! In
392practice, a subexpression ``!expr`` will lift ``expr`` as high as
393possible within its current scope, bind it to a fresh name ``x``, and
394replace ``!expr`` with ``x``. Expressions are lifted depth first, left
395to right. In practice, ``!``-notation allows us to program in a more
396direct style, while still giving a notational clue as to which
397expressions are effectful.
399For example, the expression:
403 let y = 42 in f !(g !(print y) !x)
409 let y = 42 in do y' <- print y
414Syntactic Sugar and ``Eff``
415===========================
417By now, you may be wondering about the syntax we are using for
418``Eff``, because it doesn’t look like a normal type! (If not, you may
419safely skip this section and return to it later.) In fact, the type of
420``Eff`` is the following:
425 List EFFECT -> (x -> List EFFECT) -> Type
427This is more general than the types we have been writing so far. It is
428parameterised over a result type ``x``, as we have already seen, but
429also a ``List EFFECT`` and a function type ``x -> List EFFECT``.
431These additional parameters are the list of *input* effects, and a
432list of *output* effects, computed from the result of an effectful
433operation. That is: running an effectful program can change the set
434of effects available! This is a particularly powerful idea, and we
435will see its consequences in more detail later. Some examples of
436operations which can change the set of available effects are:
438- Updating a state containing a dependent type (for example adding an
439 element to a vector).
441- Opening a file for reading is an effect, but whether the file really
442 *is* open afterwards depends on whether the file was successfully
445- Closing a file means that reading from the file should no longer be
448While powerful, this can make uses of the ``Eff`` type hard to read.
449Therefore, the library provides syntactic sugar which is translated
462i.e. the set of effects remains the same on output. This suffices for
463the ``STATE`` example we have seen so far, and for many useful
464side-effecting programs. We could also have written ``treeTagAux``
465with the expanded type:
469 treeTagAux : BTree a ->
470 Eff (BTree (Int, a)) [STATE Int] (\x => [STATE Int])
472Later, we will see programs which update effects:
484i.e. the set of effects is updated to ``xs’`` (think of a transition
485in a state machine). There is, for example, a version of ``put`` which
486updates the type of the state:
490 putM : y -> { [STATE x] ==> [STATE y] } Eff ()
496 { xs ==> {res} xs' } Eff a
502 Eff a xs (\res => xs')
504i.e. the set of effects is updated according to the result of the
507.. [1] The earlier paper [3]_ describes the essential implementation
508 details, although the library presented there is an earlier version
509 which is less powerful than that presented in this tutorial.
511.. [2] In practice, ``’name`` simply introduces a new empty type
513.. [3] Edwin Brady. 2013. Programming and reasoning with algebraic
514 effects and dependent types. SIGPLAN Not. 48, 9 (September
515 2013), 133-144. DOI=10.1145/2544174.2500581
516 http://doi.acm.org/10.1145/2544174.2500581
518.. |image| image:: ../image/effects-tree.png
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list