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) -> ... -> Eff t effs
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 -> Eff (BTree (Int, a)) [STATE Int]
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 : Eff t [STATE t]
145 put : t -> Eff () [STATE t]
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 -> Eff (BTree (Int, a)) [STATE Int]
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 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 -> Eff (BTree (Int, a)) [STATE Int]
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} -> Eff a xs -> a
231 run : Applicative m => {env : Env m xs} -> Eff a xs -> m a
233The ``env`` argument is implicit, and initialised automatically where
234possible using default values given by implementations of the following
239 interface Default a where
242Implementations 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`` implementation) the resource environment can be given explicitly
247using one of the following functions:
251 runPureInit : Env id xs -> Eff a xs -> a
252 runInit : Applicative m => Env m xs -> Eff a xs -> 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.:
275 treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE (Int, Int)]
277Doing this, however, ties the two states together throughout (as well
278as not indicating which integer is which). It would be nice to be able
279to call effectful programs which guaranteed only to access one of the
280states, for example. In a larger application, this becomes
281particularly important.
283The library therefore allows effects in general to be *labelled* so
284that they can be referred to explicitly by a particular name. This
285allows multiple effects of the same type to be included. We can count
286leaves and update the tag separately, by labelling them as follows:
290 treeTagAux : BTree a -> Eff (BTree (Int, a))
292 'Leaves ::: STATE Int]
294The ``:::`` operator allows an arbitrary label to be given to an
295effect. This label can be any type—it is simply used to identify an
296effect uniquely. Here, we have used a symbol type. In general
297``’name`` introduces a new symbol, the only purpose of which is to
298disambiguate values [2]_.
300When an effect is labelled, its operations are also labelled using the
301``:-`` operator. In this way, we can say explicitly which state we
302mean when using ``get`` and ``put``. The tree tagging program which
303also counts leaves can be written as follows:
308 'Leaves :- update (+1)
310 treeTagAux (Node l x r) = do
315 pure (Node l' (i, x) r')
317The ``update`` function here is a combination of ``get`` and ``put``,
318applying a function to the current state.
322 update : (x -> x) -> Eff () [STATE x]
324Finally, our top level ``treeTag`` function now returns a pair of the
325number of leaves, and the new tree. Resources for labelled effects are
326initialised using the ``:=`` operator (reminiscent of assignment in an
331 treeTag : (i : Int) -> BTree a -> (Int, BTree (Int, a))
332 treeTag i x = runPureInit ['Tag := i, 'Leaves := 0]
333 (do x' <- treeTagAux x
334 leaves <- 'Leaves :- get
337To summarise, we have:
339- ``:::`` to convert an effect to a labelled effect.
341- ``:-`` to convert an effectful operation to a labelled effectful operation.
343- ``:=`` to initialise a resource for a labelled effect.
345Or, more formally with their types (slightly simplified to account
346only for the situation where available effects are not updated):
350 (:::) : lbl -> EFFECT -> EFFECT
351 (:-) : (l : lbl) -> Eff a [x] -> Eff a [l ::: x]
352 (:=) : (l : lbl) -> res -> LRes l res
354Here, ``LRes`` is simply the resource type associated with a labelled
355effect. Note that labels are polymorphic in the label type ``lbl``.
356Hence, a label can be anything—a string, an integer, a type, etc.
361In many cases, using ``do``-notation can make programs unnecessarily
362verbose, particularly in cases where the value bound is used once,
363immediately. The following program returns the length of the
364``String`` stored in the state, for example:
368 stateLength : Eff Nat [STATE String]
369 stateLength = do x <- get
372This seems unnecessarily verbose, and it would be nice to program in a
373more direct style in these cases. provides ``!``-notation to help with
374this. The above program can be written instead as:
378 stateLength : Eff Nat [STATE String]
379 stateLength = pure (length !get)
381The notation ``!expr`` means that the expression ``expr`` should be
382evaluated and then implicitly bound. Conceptually, we can think of
383``!`` as being a prefix function with the following type:
389Note, however, that it is not really a function, merely syntax! In
390practice, a subexpression ``!expr`` will lift ``expr`` as high as
391possible within its current scope, bind it to a fresh name ``x``, and
392replace ``!expr`` with ``x``. Expressions are lifted depth first, left
393to right. In practice, ``!``-notation allows us to program in a more
394direct style, while still giving a notational clue as to which
395expressions are effectful.
397For example, the expression:
401 let y = 42 in f !(g !(print y) !x)
407 let y = 42 in do y' <- print y
415Underneath, ``Eff`` is an overloaded function which translates to an
416underlying type ``EffM``:
420 EffM : (m : Type -> Type) -> (t : Type)
422 -> (t -> List EFFECT) -> Type
424This is more general than the types we have been writing so far. It is
425parameterised over an underlying computation context ``m``, a
426result type ``t`` as we have already seen, as well as a ``List EFFECT`` and a
427function type ``t -> List EFFECT``.
429These additional parameters are the list of *input* effects, and a
430list of *output* effects, computed from the result of an effectful
431operation. That is: running an effectful program can change the set
432of effects available! This is a particularly powerful idea, and we
433will see its consequences in more detail later. Some examples of
434operations which can change the set of available effects are:
436- Updating a state containing a dependent type (for example adding an element to a vector).
438- Opening a file for reading is an effect, but whether the file really
439 *is* open afterwards depends on whether the file was successfully
442- Closing a file means that reading from the file should no longer be
445While powerful, this can make uses of the ``EffM`` type hard to read.
446Therefore the library provides an overloaded function ``Eff``
447There are the following three versions:
451 SimpleEff.Eff : (t : Type) -> (input_effs : List EFFECT) -> Type
452 TransEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->
453 (output_effs : List EFFECT) -> Type
454 DepEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->
455 (output_effs_fn : x -> List EFFECT) -> Type
457So far, we have used only the first version, ``SimpleEff.Eff``, which
458is defined as follows:
462 Eff : (x : Type) -> (es : List EFFECT) -> Type
463 Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
465i.e. the set of effects remains the same on output. This suffices for
466the ``STATE`` example we have seen so far, and for many useful
467side-effecting programs. We could also have written ``treeTagAux``
468with the expanded type:
472 treeTagAux : BTree a ->
473 EffM m (BTree (Int, a)) [STATE Int] (\x => [STATE Int])
475Later, we will see programs which update effects:
485 EffM m a xs (\_ => xs')
487i.e. the set of effects is updated to ``xs’`` (think of a transition
488in a state machine). There is, for example, a version of ``put`` which
489updates the type of the state:
493 putM : y -> Eff () [STATE x] [STATE y]
499 Eff t xs (\res => xs')
505 EffM m t xs (\res => xs')
507i.e. the set of effects is updated according to the result of the
508operation ``res``, of type ``t``.
510Parameterising ``EffM`` over an underlying computation context allows us
511to write effectful programs which are specific to one context, and in some
512cases to write programs which *extend* the list of effects available using
513the ``new`` function, though this is beyond the scope of this tutorial.
515.. [1] The earlier paper [3]_ describes the essential implementation
516 details, although the library presented there is an earlier version
517 which is less powerful than that presented in this tutorial.
519.. [2] In practice, ``’name`` simply introduces a new empty type
521.. [3] Edwin Brady. 2013. Programming and reasoning with algebraic
522 effects and dependent types. SIGPLAN Not. 48, 9 (September
523 2013), 133-144. DOI=10.1145/2544174.2500581
524 http://dl.acm.org/citation.cfm?doid=2544174.2500581
528.. |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