7So far we have seen how to write programs with locally mutable state
8using the ``STATE`` effect. To recap, we have the definitions in
9Listing :ref:`eff-state` in a module ``Effect.State``.
13 :caption: State Effect
17 STATE : Type -> EFFECT
19 get : { [STATE x] } Eff x
20 put : x -> { [STATE x] } Eff ()
21 putM : y -> { [STATE x] ==> [STATE y] } Eff ()
22 update : (x -> x) -> { [STATE x] } Eff ()
24 instance Handler State m
26The last line, ``instance Handler State m``, means that the ``STATE``
27effect is usable in any computation context ``m``. That is, a program
28which uses this effect and returns something of type ``a`` can be
29evaluated to something of type ``m a`` using ``run``, for any
30``m``. The lower case ``State`` is a data type describing the
31operations which make up the ``STATE`` effect itself—we will go into
32more detail about this in Section :ref:`sect-impleff`.
34In this section, we will introduce some other supported effects,
35allowing console I/O, exceptions, random number generation and
36non-deterministic programming. For each effect we introduce, we will
37begin with a summary of the effect, its supported operations, and the
38contexts in which it may be used, like that above for ``STATE``, and
39go on to present some simple examples. At the end, we will see some
40examples of programs which combine multiple effects.
42All of the effects in the library, including those described in this
43section, are summarised in Appendix :ref:`sect-appendix`.
48Console I/O (Listing :ref:`eff-stdio`) is supported with the ``STDIO``
49effect, which allows reading and writing characters and strings to and
50from standard input and standard output. Notice that there is a
51constraint here on the computation context ``m``, because it only
52makes sense to support console I/O operations in a context where we
53can perform (or at the very least simulate) console I/O.
57 :caption: Console I/0 Effect
63 putChar : Char -> { [STDIO] } Eff ()
64 putStr : String -> { [STDIO] } Eff ()
65 putStrLn : String -> { [STDIO] } Eff ()
67 getStr : { [STDIO] } Eff String
68 getChar : { [STDIO] } Eff Char
70 instance Handler StdIO IO
71 instance Handler StdIO (IOExcept a)
76A program which reads the user’s name, then says hello, can be written
81 hello : { [STDIO] } Eff ()
82 hello = do putStr "Name? "
84 putStrLn ("Hello " ++ trim x ++ "!")
86We use ``trim`` here to remove the trailing newline from the
87input. The resource associated with ``STDIO`` is simply the empty
88tuple, which has a default value ``()``, so we can run this as
96In ``hello`` we could also use ``!``-notation instead of ``x <-
97getStr``, since we only use the string that is read once:
101 hello : { [STDIO] } Eff ()
102 hello = do putStr "Name? "
103 putStrLn ("Hello " ++ trim !getStr ++ "!")
105More interestingly, we can combine multiple effects in one
106program. For example, we can loop, counting the number of people we’ve
111 hello : { [STATE Int, STDIO] } Eff ()
112 hello = do putStr "Name? "
113 putStrLn ("Hello " ++ trim !getStr ++ "!")
115 putStrLn ("I've said hello to: " ++ show !get ++ " people")
118The list of effects given in ``hello`` means that the function can
119call ``get`` and ``put`` on an integer state, and any functions which
120read and write from the console. To run this, ``main`` does not need
126To find out the resource type of an effect, if necessary (for example
127if we want to initialise a resource explicitiy with ``runInit`` rather
128than using a default value with ``run``) we can run the
129``resourceType`` function at the REPL:
133 *ConsoleIO> resourceType STDIO
135 *ConsoleIO> resourceType (STATE Int)
141Listing :ref:`eff-exception` gives the definition of the ``EXCEPTION``
142effect, declared in module ``Effect.Exception``. This allows programs
143to exit immediately with an error, or errors to be handled more
148 :caption: Exception Effect
150 module Effect.Exception
152 EXCEPTION : Type -> EFFECT
154 raise : a -> { [EXCEPTION a ] } Eff b
156 instance Handler (Exception a) Maybe
157 instance Handler (Exception a) List
158 instance Handler (Exception a) (Either a)
159 instance Handler (Exception a) (IOExcept a)
160 instance Show a => Handler (Exception a) IO
165Suppose we have a ``String`` which is expected to represent an integer
166in the range ``0`` to ``n``. We can write a function ``parseNumber``
167which returns an ``Int`` if parsing the string returns a number in the
168appropriate range, or throws an exception otherwise. Exceptions are
169paramaterised by an error type:
173 data Err = NotANumber | OutOfRange
175 parseNumber : Int -> String -> { [EXCEPTION Err] } Eff Int
177 = if all isDigit (unpack str)
178 then let x = cast str in
179 if (x >=0 && x <= num)
181 else raise OutOfRange
182 else raise NotANumber
184Programs which support the ``EXCEPTION`` effect can be run in any
185context which has some way of throwing errors, for example, we can run
186``parseNumber`` in the ``Either Err`` context. It returns a value of
187the form ``Right x`` if successful:
191 *Exception> the (Either Err Int) $ run (parseNumber 42 "20")
192 Right 20 : Either Err Int
194Or ``Left e`` on failure, carrying the appropriate exception:
198 *Exception> the (Either Err Int) $ run (parseNumber 42 "50")
199 Left OutOfRange : Either Err Int
201 *Exception> the (Either Err Int) $ run (parseNumber 42 "twenty")
202 Left NotANumber : Either Err Int
204In fact, we can do a little bit better with ``parseNumber``, and have
205it return a *proof* that the integer is in the required range along
206with the integer itself. One way to do this is define a type of
207bounded integers, ``Bounded``:
211 Bounded : Int -> Type
212 Bounded x = (n : Int ** So (n >= 0 && n <= x))
214Recall that ``So`` is parameterised by a ``Bool``, and only ``So
215True`` is inhabited. We can use ``choose`` to construct such a value
216from the result of a dynamic check:
220 data So : Bool -> Type = Oh : So True
222 choose : (b : Bool) -> Either (So b) (So (not b))
224We then write ``parseNumber`` using ``choose`` rather than an
225``if/then/else`` construct, passing the proof it returns on success as
226the boundedness proof:
230 parseNumber : (x : Int) -> String -> { [EXCEPTION Err] } Eff (Bounded x)
232 = if all isDigit (unpack str)
233 then let num = cast str in
234 case choose (num >=0 && num <= x) of
235 Left p => pure (num ** p)
236 Right p => raise OutOfRange
237 else raise NotANumber
242Random number generation is also implemented by the library, in module
243``Effect.Random``. Listing :ref:`eff-random` gives its definition.
247 :caption: Random Number Effect
253 srand : Integer -> { [RND] } Eff ()
254 rndInt : Integer -> Integer -> { [RND] } Eff Integer
255 rndFin : (k : Nat) -> { [RND] } Eff (Fin (S k))
257 instance Handler Random m
259Random number generation is considered side-effecting because its
260implementation generally relies on some external source of randomness.
261The default implementation here relies on an integer *seed*, which can
262be set with ``srand``. A specific seed will lead to a predictable,
263repeatable sequence of random numbers. There are two functions which
264produce a random number:
266- ``rndInt``, which returns a random integer between the given lower
269- ``rndFin``, which returns a random element of a finite set
270 (essentially a number with an upper bound given in its type).
275We can use the ``RND`` effect to implement a simple guessing game. The
276``guess`` function, given a target number, will repeatedly ask the
277user for a guess, and state whether the guess is too high, too low, or
282 guess : Int -> { [STDIO] } Eff ()
284For reference, the code for ``guess`` is given in Listing
285:ref:`eff-game`. Note that we use ``parseNumber`` as defined
286previously to read user input, but we don’t need to list the
287``EXCEPTION`` effect because we use a nested ``run`` to invoke
288``parseNumber``, independently of the calling effectful program.
290To invoke these, we pick a random number within the range 0–100,
291having set up the random number generator with a seed, then run
296 game : { [RND, STDIO] } Eff ()
297 game = do srand 123456789
298 guess (fromInteger !(rndInt 0 100))
303If no seed is given, it is set to the ``default`` value. For a less
304predictable game, some better source of randomness would be required,
305for example taking an initial seed from the system time. To see how to
306do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.
310 :caption: Guessing Game
312 guess : Int -> { [STDIO] } Eff ()
314 = do putStr "Guess: "
315 case run {m=Maybe} (parseNumber 100 (trim !getStr)) of
316 Nothing => do putStrLn "Invalid input"
319 case compare v target of
320 LT => do putStrLn "Too low"
322 EQ => putStrLn "You win!"
323 GT => do putStrLn "Too high"
329Listing :ref:`eff-select` gives the definition of the non-determinism
330effect, which allows a program to choose a value non-deterministically
331from a list of possibilities in such a way that the entire computation
336 :caption: Non-determinism Effect
343 select : List a -> { [SELECT] } Eff a
345 instance Handler Selection Maybe
346 instance Handler Selection List
351The ``SELECT`` effect can be used to solve constraint problems, such
352as finding Pythagorean triples. The idea is to use ``select`` to give
353a set of candidate values, then throw an exception for any combination
354of values which does not satisfy the constraint:
358 triple : Int -> { [SELECT, EXCEPTION String] } Eff (Int, Int, Int)
359 triple max = do z <- select [1..max]
362 if (x * x + y * y == z * z)
364 else raise "No triple"
366This program chooses a value for ``z`` between ``1`` and ``max``, then
367values for ``y`` and ``x``. In operation, after a ``select``, the
368program executes the rest of the ``do``-block for every possible
369assignment, effectively searching depth-first. If the list is empty
370(or an exception is thrown) execution fails.
372There are handlers defined for ``Maybe`` and ``List`` contexts, i.e.
373contexts which can capture failure. Depending on the context ``m``,
374``triple`` will either return the first triple it finds (if in
375``Maybe`` context) or all triples in the range (if in ``List``
376context). We can try this as follows:
381 main = do print $ the (Maybe _) $ run (triple 100)
382 print $ the (List _) $ run (triple 100)
387We now return to the ``vadd`` program from the introduction. Recall the
392 vadd : Vect n Int -> Vect n Int -> Vect n Int
394 vadd (x :: idris xs) (y :: ys) = x + y :: vadd xs ys
396Using , we can set up a program so that it reads input from a user,
397checks that the input is valid (i.e both vectors contain integers, and
398are the same length) and if so, pass it on to ``vadd``. First, we
399write a wrapper for ``vadd`` which checks the lengths and throw an
400exception if they are not equal. We can do this for input vectors of
401length ``n`` and ``m`` by matching on the implicit arguments ``n`` and
402``m`` and using ``decEq`` to produce a proof of their equality, if
407 vadd_check : Vect n Int -> Vect m Int ->
408 { [EXCEPTION String] } Eff (Vect m Int)
409 vadd_check {n} {m} xs ys with (decEq n m)
410 vadd_check {n} {m=n} xs ys | (Yes Refl) = pure (vadd xs ys)
411 vadd_check {n} {m} xs ys | (No contra) = raise "Length mismatch"
413To read a vector from the console, we implement a function of the
418 read_vec : { [STDIO] } Eff (p ** Vect p Int)
420This returns a dependent pair of a length, and a vector of that
421length, because we cannot know in advance how many integers the user
422is going to input. One way to implement this function, using ``-1`` to
423indicate the end of input, is shown in Listing [readvec]. This uses a
424variation on ``parseNumber`` which does not require a number to be
427Finally, we write a program which reads two vectors and prints the
428result of pairwise addition of them, throwing an exception if the
429inputs are of differing lengths:
433 do_vadd : { [STDIO, EXCEPTION String] } Eff ()
434 do_vadd = do putStrLn "Vector 1"
435 (_ ** xs) <- read_vec
437 (_ ** ys) <- read_vec
438 putStrLn (show !(vadd_check xs ys))
440By having explicit lengths in the type, we can be sure that ``vadd``
441is only being used where the lengths of inputs are guaranteed to be
442equal. This does not stop us reading vectors from user input, but it
443does require that the lengths are checked and any discrepancy is dealt
447 :caption: Reading a vector from the console.
449 read_vec : { [STDIO] } Eff (p ** Vect p Int)
450 read_vec = do putStr "Number (-1 when done): "
451 case run (parseNumber (trim !getStr)) of
452 Nothing => do putStrLn "Input error"
454 Just v => if (v /= -1)
455 then do (_ ** xs) <- read_vec
459 parseNumber : String -> { [EXCEPTION String] } Eff Int
461 = if all (\x => isDigit x || x == '-') (unpack str)
463 else raise "Not a number"
465Example: An Expression Calculator
466---------------------------------
468To show how these effects can fit together, let us consider an
469evaluator for a simple expression language, with addition and integer
474 data Expr = Val Integer
477An evaluator for this language always returns an ``Integer``, and
478there are no situations in which it can fail!
482 eval : Expr -> Integer
484 eval (Add l r) = eval l + eval r
486If we add variables, however, things get more interesting. The
487evaluator will need to be able to access the values stored in
488variables, and variables may be undefined.
492 data Expr = Val Integer
496To start, we will change the type of ``eval`` so that it is effectful,
497and supports an exception effect for throwing errors, and a state
498containing a mapping from variable names (as ``String``) to their
504 Env = List (String, Integer)
506 eval : Expr -> { [EXCEPTION String, STATE Env] } Eff Integer
507 eval (Val x) = return x
508 eval (Add l r) = return $ !(eval l) + !(eval r)
510Note that we are using ``!``-notation to avoid having to bind
511subexpressions in a ``do`` block. Next, we add a case for evaluating
516 eval (Var x) = case lookup x !get of
517 Nothing => raise $ "No such variable " ++ x
518 Just val => return val
520This retrieves the state (with ``get``, supported by the ``STATE Env``
521effect) and raises an exception if the variable is not in the
522environment (with ``raise``, supported by the ``EXCEPTION String``
525To run the evaluator on a particular expression in a particular
526environment of names and their values, we can write a function which
527sets the state then invokes ``eval``:
531 runEval : List (String, Integer) -> Expr -> Maybe Integer
532 runEval args expr = run (eval' expr)
533 where eval' : Expr -> { [EXCEPTION String, STATE Env] } Eff Integer
534 eval' e = do put args
537We have picked ``Maybe`` as a computation context here; it needs to be
538a context which is available for every effect supported by
539``eval``. In particular, because we have exceptions, it needs to be a
540context which supports exceptions. Alternatively, ``Either String`` or
541``IO`` would be fine, for example.
543What if we want to extend the evaluator further, with random number
544generation? To achieve this, we add a new constructor to ``Expr``,
545which gives a random number up to a maximum value:
549 data Expr = Val Integer
554Then, we need to deal with the new case, making sure that we extend
555the list of events to include ``RND``. It doen’t matter where ``RND``
556appears in the list, as long as it is present:
560 eval : Expr -> { [EXCEPTION String, RND, STATE Env] } Eff Integer
562 eval (Random upper) = rndInt 0 upper
564For test purposes, we might also want to print the random number which
569 eval (Random upper) = do val <- rndInt 0 upper
573If we try this without extending the effects list, we would see an
574error something like the following:
578 Expr.idr:28:6:When elaborating right hand side of eval:
581 [(EXCEPTION String), RND, (STATE (List (String, Integer)))]
583In other words, the ``STDIO`` effect is not available. We can correct
584this simply by updating the type of ``eval`` to include ``STDIO``.
588 eval : Expr -> { [STDIO, EXCEPTION String, RND, STATE Env] } Eff Integer
590Note that using ``STDIO`` will restrict the number of contexts in
591which ``eval`` can be ``run`` to those which support ``STDIO``, such
592as ``IO``. Once effect lists get longer, it can be a good idea instead
593to encapsulate sets of effects in a type synonym. This is achieved as
594follows, simply by defining a function which computes a type, since
595types are first class in Idris:
599 EvalEff : Type -> Type
600 EvalEff t = { [STDIO, EXCEPTION String, RND, STATE Env] } Eff t
602 eval : Expr -> EvalEff Integer
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