7We have now seen several side-effecting operations provided by the
8``Effects`` library, and examples of their use in Section
9:ref:`sect-simpleff`. We have also seen how operations may *modify*
10the available effects by changing state in Section
11:ref:`sect-depeff`. We have not, however, yet seen how these
12operations are implemented. In this section, we describe how a
13selection of the available effects are implemented, and show how new
14effectful operations may be provided.
19Effects are described by *algebraic data types*, where the
20constructors describe the operations provided when the effect is
21available. Stateful operations are described as follows:
25 data State : Effect where
26 Get : State a a (\x => a)
27 Put : b -> State () a (\x => b)
29``Effect`` itself is a type synonym, giving the required type for an
35 Effect = (result : Type) ->
36 (input_resource : Type) ->
37 (output_resource : result -> Type) -> Type
39Each effect is associated with a *resource*. The second argument to
40an effect signature is the resource type on *input* to an operation,
41and the third is a function which computes the resource type on
42*output*. Here, it means:
44- ``Get`` takes no arguments. It has a resource of type ``a``, which is not updated, and running the ``Get`` operation returns something of type ``a``.
46- ``Put`` takes a ``b`` as an argument. It has a resource of type ``a`` on input, which is updated to a resource of type ``b``. Running the ``Put`` operation returns the element of the unit type.
48The effects library provides an overloaded function ``sig``
49which can make effect signatures more concise, particularly when the
50result has no effect on the resource type. For ``State``, we can
55 data State : Effect where
57 Put : b -> sig State () a b
59There are four versions of ``sig``, depending on whether we
60are interested in the resource type, and whether we are updating the
61resource. Idris will infer the appropriate version from usage.
65 NoResourceEffect.sig : Effect -> Type -> Type
66 NoUpdateEffect.sig : Effect -> (ret : Type) ->
67 (resource : Type) -> Type
68 UpdateEffect.sig : Effect -> (ret : Type) ->
69 (resource_in : Type) ->
70 (resource_out : Type) -> Type
71 DepUpdateEffect.sig : Effect -> (ret : Type) ->
72 (resource_in : Type) ->
73 (resource_out : ret -> Type) -> Type
75In order to convert ``State`` (of type ``Effect``) into something
76usable in an effects list, of type ``EFFECT``, we write the following:
80 STATE : Type -> EFFECT
81 STATE t = MkEff t State
83``MkEff`` constructs an ``EFFECT`` by taking the resource type (here,
84the ``t`` which parameterises ``STATE``) and the effect signature
85(here, ``State``). For reference, ``EFFECT`` is declared as follows:
89 data EFFECT : Type where
90 MkEff : Type -> Effect -> EFFECT
92Recall that to run an effectful program in ``Eff``, we use one of the
93``run`` family of functions to run the program in a particular
94computation context ``m``. For each effect, therefore, we must explain
95how it is executed in a particular computation context for ``run`` to
96work in that context. This is achieved with the following interface:
100 interface Handler (e : Effect) (m : Type -> Type) where
101 handle : resource -> (eff : e t resource resource') ->
102 ((x : t) -> resource' x -> m a) -> m a
104We have already seen some implementation declarations in the effect
105summaries in Section :ref:`sect-simpleff`. An implementation of ``Handler e
106m`` means that the effect declared with signature ``e`` can be run in
107computation context ``m``. The ``handle`` function takes:
109- The ``resource`` on input (so, the current value of the state for ``State``)
111- The effectful operation (either ``Get`` or ``Put x`` for ``State``)
113- A *continuation*, which we conventionally call ``k``, and should be passed the result value of the operation, and an updated resource.
115There are two reasons for taking a continuation here: firstly, this is
116neater because there are multiple return values (a new resource and
117the result of the operation); secondly, and more importantly, the
118continuation can be called zero or more times.
120A ``Handler`` for ``State`` simply passes on the value of the state,
121in the case of ``Get``, or passes on a new state, in the case of
122``Put``. It is defined the same way for all computation contexts:
126 Handler State m where
127 handle st Get k = k st st
128 handle st (Put n) k = k () n
130This gives enough information for ``Get`` and ``Put`` to be used
131directly in ``Eff`` programs. It is tidy, however, to define top level
132functions in ``Eff``, as follows:
136 get : Eff x [STATE x]
139 put : x -> Eff () [STATE x]
140 put val = call (Put val)
142 putM : y -> Eff () [STATE x] [STATE y]
143 putM val = call (Put val)
145**An implementation detail (aside):** The ``call`` function converts
146an ``Effect`` to a function in ``Eff``, given a proof that the effect
147is available. This proof can be constructed automatically by , since
148it is essentially an index into a statically known list of effects:
152 call : {e : Effect} ->
153 (eff : e t a b) -> {auto prf : EffElem e a xs} ->
154 Eff t xs (\v => updateResTy v xs prf eff)
156This is the reason for the ``Can’t solve goal`` error when an effect
157is not available: the implicit proof ``prf`` has not been solved
158automatically because the required effect is not in the list of
161Such details are not important for using the library, or even writing
167The following listing summarises what is required to define the
172 data State : Effect where
174 Put : b -> sig State () a b
176 STATE : Type -> EFFECT
177 STATE t = MkEff t State
179 Handler State m where
180 handle st Get k = k st st
181 handle st (Put n) k = k () n
183 get : Eff x [STATE x]
186 put : x -> Eff () [STATE x]
187 put val = call (Put val)
189 putM : y -> Eff () [STATE x] [STATE y]
190 putM val = call (Put val)
196Then listing below gives the definition of the ``STDIO``
197effect, including handlers for ``IO`` and ``IOExcept``. We omit the
198definition of the top level ``Eff`` functions, as this merely invoke
199the effects ``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.
201Note that in this case, the resource is the unit type in every case,
202since the handlers merely apply the ``IO`` equivalents of the effects
208 data StdIO : Effect where
209 PutStr : String -> sig StdIO ()
210 GetStr : sig StdIO String
211 PutCh : Char -> sig StdIO ()
212 GetCh : sig StdIO Char
214 Handler StdIO IO where
215 handle () (PutStr s) k = do putStr s; k () ()
216 handle () GetStr k = do x <- getLine; k x ()
217 handle () (PutCh c) k = do putChar c; k () ()
218 handle () GetCh k = do x <- getChar; k x ()
220 Handler StdIO (IOExcept a) where
221 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
222 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
223 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
224 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
227 STDIO = MkEff () StdIO
232The listing below gives the definition of the ``Exception``
233effect, including two of its handlers for ``Maybe`` and ``List``. The
234only operation provided is ``Raise``. The key point to note in the
235definitions of these handlers is that the continuation ``k`` is not
236used. Running ``Raise`` therefore means that computation stops with an
241 data Exception : Type -> Effect where
242 Raise : a -> sig (Exception a) b
244 Handler (Exception a) Maybe where
245 handle _ (Raise e) k = Nothing
247 Handler (Exception a) List where
248 handle _ (Raise e) k = []
250 EXCEPTION : Type -> EFFECT
251 EXCEPTION t = MkEff () (Exception t)
257The following listing gives the definition of the ``Select``
258effect for writing non-deterministic programs, including a handler for
259``List`` context which returns all possible successful values, and a
260handler for ``Maybe`` context which returns the first successful
265 data Selection : Effect where
266 Select : List a -> sig Selection a
268 Handler Selection Maybe where
269 handle _ (Select xs) k = tryAll xs where
271 tryAll (x :: xs) = case k x () of
275 Handler Selection List where
276 handle r (Select xs) k = concatMap (\x => k x r) xs
279 SELECT = MkEff () Selection
282Here, the continuation is called multiple times in each handler, for
283each value in the list of possible values. In the ``List`` handler, we
284accumulate all successful results, and in the ``Maybe`` handler we try
285the first value in the list, and try later values only if that fails.
290Result-dependent effects are no different from non-dependent effects
291in the way they are implemented. The listing below
292illustrates this for the ``FILE_IO`` effect. The syntax for state
293transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is
294computed from the result of the operation ``res``, follows that for
295the equivalent ``Eff`` programs.
299 data FileIO : Effect where
300 Open : (fname: String)
302 -> sig FileIO Bool () (\res => case res of
305 Close : sig FileIO () (OpenFile m)
307 ReadLine : sig FileIO String (OpenFile Read)
308 WriteLine : String -> sig FileIO () (OpenFile Write)
309 EOF : sig FileIO Bool (OpenFile Read)
311 Handler FileIO IO where
312 handle () (Open fname m) k = do h <- openFile fname m
316 handle (FH h) Close k = do closeFile h
319 handle (FH h) ReadLine k = do str <- fread h
321 handle (FH h) (WriteLine str) k = do fwrite h str
323 handle (FH h) EOF k = do e <- feof h
326 FILE_IO : Type -> EFFECT
327 FILE_IO t = MkEff t FileIO
329Note that in the handler for ``Open``, the types passed to the
330continuation ``k`` are different depending on whether the result is
331``True`` (opening succeeded) or ``False`` (opening failed). This uses
332``validFile``, defined in the ``Prelude``, to test whether a file
333handler refers to an open file or not.
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