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
27 Put : b -> { a ==> b } State ()
29Each effect is associated with a *resource*, the type of which is
30given with the notation ``{ x ==> x’ }``. This notation gives the
31resource type expected by each operation, and how it updates when the
32operation is run. Here, it means:
34- ``Get`` takes no arguments. It has a resource of type ``a``, which
35 is not updated, and running the ``Get`` operation returns something
38- ``Put`` takes a ``b`` as an argument. It has a resource of type
39 ``a`` on input, which is updated to a resource of type
40 ``b``. Running the ``Put`` operation returns the element of the
43``Effect`` itself is a type synonym, declared as follows:
48 Effect = (result : Type) ->
49 (input_resource : Type) ->
50 (output_resource : result -> Type) -> Type
52That is, an effectful operation returns something of type ``result``,
53has an input resource of type ``input_resource``, and a function
54``output_resource`` which computes the output resource type from the
55result. We use the same syntactic sugar as with ``Eff`` to make effect
56declarations more readable. It is defined as follows in the library:
60 syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
61 syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
62 = eff inst (\b => outst)
63 syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
65In order to convert ``State`` (of type ``Effect``) into something
66usable in an effects list, of type ``EFFECT``, we write the following:
70 STATE : Type -> EFFECT
71 STATE t = MkEff t State
73``MkEff`` constructs an ``EFFECT`` by taking the resource type (here,
74the ``t`` which parameterises ``STATE``) and the effect signature
75(here, ``State``). For reference, ``EFFECT`` is declared as follows:
79 data EFFECT : Type where
80 MkEff : Type -> Effect -> EFFECT
82Recall that to run an effectful program in ``Eff``, we use one of the
83``run`` family of functions to run the program in a particular
84computation context ``m``. For each effect, therefore, we must explain
85how it is executed in a particular computation context for ``run`` to
86work in that context. This is achieved with the following type class:
90 class Handler (e : Effect) (m : Type -> Type) where
91 handle : resource -> (eff : e t resource resource') ->
92 ((x : t) -> resource' x -> m a) -> m a
94We have already seen some instance declarations in the effect
95summaries in Section :ref:`sect-simpleff`. An instance of ``Handler e
96m`` means that the effect declared with signature ``e`` can be run in
97computation context ``m``. The ``handle`` function takes:
99- The ``resource`` on input (so, the current value of the state for
102- The effectful operation (either ``Get`` or ``Put x`` for ``State``)
104- A *continuation*, which we conventionally call ``k``, and should be
105 passed the result value of the operation, and an updated resource.
107There are two reasons for taking a continuation here: firstly, this is
108neater because there are multiple return values (a new resource and
109the result of the operation); secondly, and more importantly, the
110continuation can be called zero or more times.
112A ``Handler`` for ``State`` simply passes on the value of the state,
113in the case of ``Get``, or passes on a new state, in the case of
114``Put``. It is defined the same way for all computation contexts:
118 instance Handler State m where
119 handle st Get k = k st st
120 handle st (Put n) k = k () n
122This gives enough information for ``Get`` and ``Put`` to be used
123directly in ``Eff`` programs. It is tidy, however, to define top level
124functions in ``Eff``, as follows:
128 get : { [STATE x] } Eff x
131 put : x -> { [STATE x] } Eff ()
132 put val = call (Put val)
134 putM : y -> { [STATE x] ==> [STATE y] } Eff ()
135 putM val = call (Put val)
137**An implementation detail (aside):** The ``call`` function converts
138an ``Effect`` to a function in ``Eff``, given a proof that the effect
139is available. This proof can be constructed automatically by , since
140it is essentially an index into a statically known list of effects:
144 call : {e : Effect} ->
145 (eff : e t a b) -> {auto prf : EffElem e a xs} ->
146 Eff t xs (\v => updateResTy v xs prf eff)
148This is the reason for the ``Can’t solve goal`` error when an effect
149is not available: the implicit proof ``prf`` has not been solved
150automatically because the required effect is not in the list of
153Such details are not important for using the library, or even writing
159The following listing summarises what is required to define the
164 data State : Effect where
166 Put : b -> { a ==> b } State ()
168 STATE : Type -> EFFECT
169 STATE t = MkEff t State
171 instance Handler State m where
172 handle st Get k = k st st
173 handle st (Put n) k = k () n
175 get : { [STATE x] } Eff x
178 put : x -> { [STATE x] } Eff ()
179 put val = call (Put val)
181 putM : y -> { [STATE x] ==> [STATE y] } Eff ()
182 putM val = call (Put val)
188Then listing below gives the definition of the ``STDIO``
189effect, including handlers for ``IO`` and ``IOExcept``. We omit the
190definition of the top level ``Eff`` functions, as this merely invoke
191the effects ``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.
193Note that in this case, the resource is the unit type in every case,
194since the handlers merely apply the ``IO`` equivalents of the effects
200 data StdIO : Effect where
201 PutStr : String -> { () } StdIO ()
202 GetStr : { () } StdIO String
203 PutCh : Char -> { () } StdIO ()
204 GetCh : { () } StdIO Char
206 instance Handler StdIO IO where
207 handle () (PutStr s) k = do putStr s; k () ()
208 handle () GetStr k = do x <- getLine; k x ()
209 handle () (PutCh c) k = do putChar c; k () ()
210 handle () GetCh k = do x <- getChar; k x ()
212 instance Handler StdIO (IOExcept a) where
213 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
214 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
215 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
216 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
219 STDIO = MkEff () StdIO
224The listing below gives the definition of the ``Exception``
225effect, including two of its handlers for ``Maybe`` and ``List``. The
226only operation provided is ``Raise``. The key point to note in the
227definitions of these handlers is that the continuation ``k`` is not
228used. Running ``Raise`` therefore means that computation stops with an
233 data Exception : Type -> Effect where
234 Raise : a -> { () } Exception a b
236 instance Handler (Exception a) Maybe where
237 handle _ (Raise e) k = Nothing
239 instance Handler (Exception a) List where
240 handle _ (Raise e) k = []
242 EXCEPTION : Type -> EFFECT
243 EXCEPTION t = MkEff () (Exception t)
249The following listing gives the definition of the ``Select``
250effect for writing non-deterministic programs, including a handler for
251``List`` context which returns all possible successful values, and a
252handler for ``Maybe`` context which returns the first successful
257 data Selection : Effect where
258 Select : List a -> { () } Selection a
260 instance Handler Selection Maybe where
261 handle _ (Select xs) k = tryAll xs where
263 tryAll (x :: xs) = case k x () of
267 instance Handler Selection List where
268 handle r (Select xs) k = concatMap (\x => k x r) xs
271 SELECT = MkEff () Selection
274Here, the continuation is called multiple times in each handler, for
275each value in the list of possible values. In the ``List`` handler, we
276accumulate all successful results, and in the ``Maybe`` handler we try
277the first value in the last, and try later values only if that fails.
282Result-dependent effects are no different from non-dependent effects
283in the way they are implemented. The listing below
284illustrates this for the ``FILE_IO`` effect. The syntax for state
285transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is
286computed from the result of the operation ``res``, follows that for
287the equivalent ``Eff`` programs.
291 data FileIO : Effect where
292 Open : String -> (m : Mode) ->
293 {() ==> {res} if res then OpenFile m else ()} FileIO Bool
294 Close : {OpenFile m ==> ()} FileIO ()
296 ReadLine : {OpenFile Read} FileIO String
297 WriteLine : String -> {OpenFile Write} FileIO ()
298 EOF : {OpenFile Read} FileIO Bool
300 instance Handler FileIO IO where
301 handle () (Open fname m) k = do h <- openFile fname m
305 handle (FH h) Close k = do closeFile h
308 handle (FH h) ReadLine k = do str <- fread h
310 handle (FH h) (WriteLine str) k = do fwrite h str
312 handle (FH h) EOF k = do e <- feof h
315 FILE_IO : Type -> EFFECT
316 FILE_IO t = MkEff t FileIO
318Note that in the handler for ``Open``, the types passed to the
319continuation ``k`` are different depending on whether the result is
320``True`` (opening succeeded) or ``False`` (opening failed). This uses
321``validFile``, defined in the ``Prelude``, to test whether a file
322handler 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