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
159Listing :ref:`eff-statedef` summarises what is required to define the
164 :caption: Complete State Effect Definition
166 data State : Effect where
168 Put : b -> { a ==> b } State ()
170 STATE : Type -> EFFECT
171 STATE t = MkEff t State
173 instance Handler State m where
174 handle st Get k = k st st
175 handle st (Put n) k = k () n
177 get : { [STATE x] } Eff x
180 put : x -> { [STATE x] } Eff ()
181 put val = call (Put val)
183 putM : y -> { [STATE x] ==> [STATE y] } Eff ()
184 putM val = call (Put val)
190Listing :ref:`eff-stdiodef` gives the definition of the ``STDIO``
191effect, including handlers for ``IO`` and ``IOExcept``. We omit the
192definition of the top level ``Eff`` functions, as this merely invoke
193the effects ``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.
195Note that in this case, the resource is the unit type in every case,
196since the handlers merely apply the ``IO`` equivalents of the effects
201 :caption: Console I/O Effect Definition
203 data StdIO : Effect where
204 PutStr : String -> { () } StdIO ()
205 GetStr : { () } StdIO String
206 PutCh : Char -> { () } StdIO ()
207 GetCh : { () } StdIO Char
209 instance Handler StdIO IO where
210 handle () (PutStr s) k = do putStr s; k () ()
211 handle () GetStr k = do x <- getLine; k x ()
212 handle () (PutCh c) k = do putChar c; k () ()
213 handle () GetCh k = do x <- getChar; k x ()
215 instance Handler StdIO (IOExcept a) where
216 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
217 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
218 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
219 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
222 STDIO = MkEff () StdIO
229 :caption: Exception Effect Definition
231 data Exception : Type -> Effect where
232 Raise : a -> { () } Exception a b
234 instance Handler (Exception a) Maybe where
235 handle _ (Raise e) k = Nothing
237 instance Handler (Exception a) List where
238 handle _ (Raise e) k = []
240 EXCEPTION : Type -> EFFECT
241 EXCEPTION t = MkEff () (Exception t)
243Listing :ref:`eff-exceptdef` gives the definition of the ``Exception``
244effect, including two of its handlers for ``Maybe`` and ``List``. The
245only operation provided is ``Raise``. The key point to note in the
246definitions of these handlers is that the continuation ``k`` is not
247used. Running ``Raise`` therefore means that computation stops with an
255 :caption: Non-determinism Effect Definition
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
273Listing :ref:`eff-selectdef` gives the definition of the ``Select``
274effect for writing non-deterministic programs, including a handler for
275``List`` context which returns all possible successful values, and a
276handler for ``Maybe`` context which returns the first successful
279Here, the continuation is called multiple times in each handler, for
280each value in the list of possible values. In the ``List`` handler, we
281accumulate all successful results, and in the ``Maybe`` handler we try
282the first value in the last, and try later values only if that fails.
287Result-dependent effects are no different from non-dependent effects
288in the way they are implemented. Listing :ref:`eff-filedef`
289illustrates this for the ``FILE_IO`` effect. The syntax for state
290transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is
291computed from the result of the operation ``res``, follows that for
292the equivalent ``Eff`` programs.
294Note that in the handler for ``Open``, the types passed to the
295continuation ``k`` are different depending on whether the result is
296``True`` (opening succeeded) or ``False`` (opening failed). This uses
297``validFile``, defined in the ``Prelude``, to test whether a file
298handler refers to an open file or not.
302 :caption: File I/O Effect Definition
304 data FileIO : Effect where
305 Open : String -> (m : Mode) ->
306 {() ==> {res} if res then OpenFile m else ()} FileIO Bool
307 Close : {OpenFile m ==> ()} FileIO ()
309 ReadLine : {OpenFile Read} FileIO String
310 WriteLine : String -> {OpenFile Write} FileIO ()
311 EOF : {OpenFile Read} FileIO Bool
313 instance Handler FileIO IO where
314 handle () (Open fname m) k = do h <- openFile fname m
318 handle (FH h) Close k = do closeFile h
321 handle (FH h) ReadLine k = do str <- fread h
323 handle (FH h) (WriteLine str) k = do fwrite h str
325 handle (FH h) EOF k = do e <- feof h
328 FILE_IO : Type -> EFFECT
329 FILE_IO t = MkEff t FileIO
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