7So far we have seen how to write programs with locally mutable state
8using the ``STATE`` effect. To recap, we have the definitions below
9in a module ``Effect.State``
15 STATE : Type -> EFFECT
17 get : { [STATE x] } Eff x
18 put : x -> { [STATE x] } Eff ()
19 putM : y -> { [STATE x] ==> [STATE y] } Eff ()
20 update : (x -> x) -> { [STATE x] } Eff ()
22 instance Handler State m
24The last line, ``instance Handler State m``, means that the ``STATE``
25effect is usable in any computation context ``m``. That is, a program
26which uses this effect and returns something of type ``a`` can be
27evaluated to something of type ``m a`` using ``run``, for any
28``m``. The lower case ``State`` is a data type describing the
29operations which make up the ``STATE`` effect itself—we will go into
30more detail about this in Section :ref:`sect-impleff`.
32In this section, we will introduce some other supported effects,
33allowing console I/O, exceptions, random number generation and
34non-deterministic programming. For each effect we introduce, we will
35begin with a summary of the effect, its supported operations, and the
36contexts in which it may be used, like that above for ``STATE``, and
37go on to present some simple examples. At the end, we will see some
38examples of programs which combine multiple effects.
40All of the effects in the library, including those described in this
41section, are summarised in Appendix :ref:`sect-appendix`.
46Console I/O is supported with the ``STDIO``
47effect, which allows reading and writing characters and strings to and
48from standard input and standard output. Notice that there is a
49constraint here on the computation context ``m``, because it only
50makes sense to support console I/O operations in a context where we
51can perform (or at the very least simulate) console I/O:
59 putChar : Char -> { [STDIO] } Eff ()
60 putStr : String -> { [STDIO] } Eff ()
61 putStrLn : String -> { [STDIO] } Eff ()
63 getStr : { [STDIO] } Eff String
64 getChar : { [STDIO] } Eff Char
66 instance Handler StdIO IO
67 instance Handler StdIO (IOExcept a)
72A program which reads the user’s name, then says hello, can be written
77 hello : { [STDIO] } Eff ()
78 hello = do putStr "Name? "
80 putStrLn ("Hello " ++ trim x ++ "!")
82We use ``trim`` here to remove the trailing newline from the
83input. The resource associated with ``STDIO`` is simply the empty
84tuple, which has a default value ``()``, so we can run this as
92In ``hello`` we could also use ``!``-notation instead of ``x <-
93getStr``, since we only use the string that is read once:
97 hello : { [STDIO] } Eff ()
98 hello = do putStr "Name? "
99 putStrLn ("Hello " ++ trim !getStr ++ "!")
101More interestingly, we can combine multiple effects in one
102program. For example, we can loop, counting the number of people we’ve
107 hello : { [STATE Int, STDIO] } Eff ()
108 hello = do putStr "Name? "
109 putStrLn ("Hello " ++ trim !getStr ++ "!")
111 putStrLn ("I've said hello to: " ++ show !get ++ " people")
114The list of effects given in ``hello`` means that the function can
115call ``get`` and ``put`` on an integer state, and any functions which
116read and write from the console. To run this, ``main`` does not need
122To find out the resource type of an effect, if necessary (for example
123if we want to initialise a resource explicitiy with ``runInit`` rather
124than using a default value with ``run``) we can run the
125``resourceType`` function at the REPL:
129 *ConsoleIO> resourceType STDIO
131 *ConsoleIO> resourceType (STATE Int)
138effect is declared in module ``Effect.Exception``. This allows programs
139to exit immediately with an error, or errors to be handled more
145 module Effect.Exception
147 EXCEPTION : Type -> EFFECT
149 raise : a -> { [EXCEPTION a ] } Eff b
151 instance Handler (Exception a) Maybe
152 instance Handler (Exception a) List
153 instance Handler (Exception a) (Either a)
154 instance Handler (Exception a) (IOExcept a)
155 instance Show a => Handler (Exception a) IO
160Suppose we have a ``String`` which is expected to represent an integer
161in the range ``0`` to ``n``. We can write a function ``parseNumber``
162which returns an ``Int`` if parsing the string returns a number in the
163appropriate range, or throws an exception otherwise. Exceptions are
164paramaterised by an error type:
168 data Err = NotANumber | OutOfRange
170 parseNumber : Int -> String -> { [EXCEPTION Err] } Eff Int
172 = if all isDigit (unpack str)
173 then let x = cast str in
174 if (x >=0 && x <= num)
176 else raise OutOfRange
177 else raise NotANumber
179Programs which support the ``EXCEPTION`` effect can be run in any
180context which has some way of throwing errors, for example, we can run
181``parseNumber`` in the ``Either Err`` context. It returns a value of
182the form ``Right x`` if successful:
186 *Exception> the (Either Err Int) $ run (parseNumber 42 "20")
187 Right 20 : Either Err Int
189Or ``Left e`` on failure, carrying the appropriate exception:
193 *Exception> the (Either Err Int) $ run (parseNumber 42 "50")
194 Left OutOfRange : Either Err Int
196 *Exception> the (Either Err Int) $ run (parseNumber 42 "twenty")
197 Left NotANumber : Either Err Int
199In fact, we can do a little bit better with ``parseNumber``, and have
200it return a *proof* that the integer is in the required range along
201with the integer itself. One way to do this is define a type of
202bounded integers, ``Bounded``:
206 Bounded : Int -> Type
207 Bounded x = (n : Int ** So (n >= 0 && n <= x))
209Recall that ``So`` is parameterised by a ``Bool``, and only ``So
210True`` is inhabited. We can use ``choose`` to construct such a value
211from the result of a dynamic check:
215 data So : Bool -> Type = Oh : So True
217 choose : (b : Bool) -> Either (So b) (So (not b))
219We then write ``parseNumber`` using ``choose`` rather than an
220``if/then/else`` construct, passing the proof it returns on success as
221the boundedness proof:
225 parseNumber : (x : Int) -> String -> { [EXCEPTION Err] } Eff (Bounded x)
227 = if all isDigit (unpack str)
228 then let num = cast str in
229 case choose (num >=0 && num <= x) of
230 Left p => pure (num ** p)
231 Right p => raise OutOfRange
232 else raise NotANumber
237Random number generation is also implemented by the library, in module
246 srand : Integer -> { [RND] } Eff ()
247 rndInt : Integer -> Integer -> { [RND] } Eff Integer
248 rndFin : (k : Nat) -> { [RND] } Eff (Fin (S k))
250 instance Handler Random m
252Random number generation is considered side-effecting because its
253implementation generally relies on some external source of randomness.
254The default implementation here relies on an integer *seed*, which can
255be set with ``srand``. A specific seed will lead to a predictable,
256repeatable sequence of random numbers. There are two functions which
257produce a random number:
259- ``rndInt``, which returns a random integer between the given lower
262- ``rndFin``, which returns a random element of a finite set
263 (essentially a number with an upper bound given in its type).
268We can use the ``RND`` effect to implement a simple guessing game. The
269``guess`` function, given a target number, will repeatedly ask the
270user for a guess, and state whether the guess is too high, too low, or
275 guess : Int -> { [STDIO] } Eff ()
277For reference, the code for ``guess`` is given below:
282 guess : Int -> { [STDIO] } Eff ()
284 = do putStr "Guess: "
285 case run {m=Maybe} (parseNumber 100 (trim !getStr)) of
286 Nothing => do putStrLn "Invalid input"
289 case compare v target of
290 LT => do putStrLn "Too low"
292 EQ => putStrLn "You win!"
293 GT => do putStrLn "Too high"
296Note that we use ``parseNumber`` as defined previously to read user input, but
297we don’t need to list the ``EXCEPTION`` effect because we use a nested ``run``
298to invoke ``parseNumber``, independently of the calling effectful program.
300To invoke this, we pick a random number within the range 0–100,
301having set up the random number generator with a seed, then run
306 game : { [RND, STDIO] } Eff ()
307 game = do srand 123456789
308 guess (fromInteger !(rndInt 0 100))
313If no seed is given, it is set to the ``default`` value. For a less
314predictable game, some better source of randomness would be required,
315for example taking an initial seed from the system time. To see how to
316do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.
322The listing below gives the definition of the non-determinism
323effect, which allows a program to choose a value non-deterministically
324from a list of possibilities in such a way that the entire computation
334 select : List a -> { [SELECT] } Eff a
336 instance Handler Selection Maybe
337 instance Handler Selection List
342The ``SELECT`` effect can be used to solve constraint problems, such
343as finding Pythagorean triples. The idea is to use ``select`` to give
344a set of candidate values, then throw an exception for any combination
345of values which does not satisfy the constraint:
349 triple : Int -> { [SELECT, EXCEPTION String] } Eff (Int, Int, Int)
350 triple max = do z <- select [1..max]
353 if (x * x + y * y == z * z)
355 else raise "No triple"
357This program chooses a value for ``z`` between ``1`` and ``max``, then
358values for ``y`` and ``x``. In operation, after a ``select``, the
359program executes the rest of the ``do``-block for every possible
360assignment, effectively searching depth-first. If the list is empty
361(or an exception is thrown) execution fails.
363There are handlers defined for ``Maybe`` and ``List`` contexts, i.e.
364contexts which can capture failure. Depending on the context ``m``,
365``triple`` will either return the first triple it finds (if in
366``Maybe`` context) or all triples in the range (if in ``List``
367context). We can try this as follows:
372 main = do print $ the (Maybe _) $ run (triple 100)
373 print $ the (List _) $ run (triple 100)
378We now return to the ``vadd`` program from the introduction. Recall the
383 vadd : Vect n Int -> Vect n Int -> Vect n Int
385 vadd (x :: idris xs) (y :: ys) = x + y :: vadd xs ys
387Using , we can set up a program so that it reads input from a user,
388checks that the input is valid (i.e both vectors contain integers, and
389are the same length) and if so, pass it on to ``vadd``. First, we
390write a wrapper for ``vadd`` which checks the lengths and throw an
391exception if they are not equal. We can do this for input vectors of
392length ``n`` and ``m`` by matching on the implicit arguments ``n`` and
393``m`` and using ``decEq`` to produce a proof of their equality, if
398 vadd_check : Vect n Int -> Vect m Int ->
399 { [EXCEPTION String] } Eff (Vect m Int)
400 vadd_check {n} {m} xs ys with (decEq n m)
401 vadd_check {n} {m=n} xs ys | (Yes Refl) = pure (vadd xs ys)
402 vadd_check {n} {m} xs ys | (No contra) = raise "Length mismatch"
404To read a vector from the console, we implement a function of the
409 read_vec : { [STDIO] } Eff (p ** Vect p Int)
411This returns a dependent pair of a length, and a vector of that
412length, because we cannot know in advance how many integers the user
413is going to input. One way to implement this function, using ``-1`` to
414indicate the end of input, is shown in Listing [readvec]. This uses a
415variation on ``parseNumber`` which does not require a number to be
418Finally, we write a program which reads two vectors and prints the
419result of pairwise addition of them, throwing an exception if the
420inputs are of differing lengths:
424 do_vadd : { [STDIO, EXCEPTION String] } Eff ()
425 do_vadd = do putStrLn "Vector 1"
426 (_ ** xs) <- read_vec
428 (_ ** ys) <- read_vec
429 putStrLn (show !(vadd_check xs ys))
431By having explicit lengths in the type, we can be sure that ``vadd``
432is only being used where the lengths of inputs are guaranteed to be
433equal. This does not stop us reading vectors from user input, but it
434does require that the lengths are checked and any discrepancy is dealt
439 read_vec : { [STDIO] } Eff (p ** Vect p Int)
440 read_vec = do putStr "Number (-1 when done): "
441 case run (parseNumber (trim !getStr)) of
442 Nothing => do putStrLn "Input error"
444 Just v => if (v /= -1)
445 then do (_ ** xs) <- read_vec
449 parseNumber : String -> { [EXCEPTION String] } Eff Int
451 = if all (\x => isDigit x || x == '-') (unpack str)
453 else raise "Not a number"
455Example: An Expression Calculator
456=================================
458To show how these effects can fit together, let us consider an
459evaluator for a simple expression language, with addition and integer
464 data Expr = Val Integer
467An evaluator for this language always returns an ``Integer``, and
468there are no situations in which it can fail!
472 eval : Expr -> Integer
474 eval (Add l r) = eval l + eval r
476If we add variables, however, things get more interesting. The
477evaluator will need to be able to access the values stored in
478variables, and variables may be undefined.
482 data Expr = Val Integer
486To start, we will change the type of ``eval`` so that it is effectful,
487and supports an exception effect for throwing errors, and a state
488containing a mapping from variable names (as ``String``) to their
494 Env = List (String, Integer)
496 eval : Expr -> { [EXCEPTION String, STATE Env] } Eff Integer
497 eval (Val x) = return x
498 eval (Add l r) = return $ !(eval l) + !(eval r)
500Note that we are using ``!``-notation to avoid having to bind
501subexpressions in a ``do`` block. Next, we add a case for evaluating
506 eval (Var x) = case lookup x !get of
507 Nothing => raise $ "No such variable " ++ x
508 Just val => return val
510This retrieves the state (with ``get``, supported by the ``STATE Env``
511effect) and raises an exception if the variable is not in the
512environment (with ``raise``, supported by the ``EXCEPTION String``
515To run the evaluator on a particular expression in a particular
516environment of names and their values, we can write a function which
517sets the state then invokes ``eval``:
521 runEval : List (String, Integer) -> Expr -> Maybe Integer
522 runEval args expr = run (eval' expr)
523 where eval' : Expr -> { [EXCEPTION String, STATE Env] } Eff Integer
524 eval' e = do put args
527We have picked ``Maybe`` as a computation context here; it needs to be
528a context which is available for every effect supported by
529``eval``. In particular, because we have exceptions, it needs to be a
530context which supports exceptions. Alternatively, ``Either String`` or
531``IO`` would be fine, for example.
533What if we want to extend the evaluator further, with random number
534generation? To achieve this, we add a new constructor to ``Expr``,
535which gives a random number up to a maximum value:
539 data Expr = Val Integer
544Then, we need to deal with the new case, making sure that we extend
545the list of events to include ``RND``. It doen’t matter where ``RND``
546appears in the list, as long as it is present:
550 eval : Expr -> { [EXCEPTION String, RND, STATE Env] } Eff Integer
552 eval (Random upper) = rndInt 0 upper
554For test purposes, we might also want to print the random number which
559 eval (Random upper) = do val <- rndInt 0 upper
563If we try this without extending the effects list, we would see an
564error something like the following:
568 Expr.idr:28:6:When elaborating right hand side of eval:
571 [(EXCEPTION String), RND, (STATE (List (String, Integer)))]
573In other words, the ``STDIO`` effect is not available. We can correct
574this simply by updating the type of ``eval`` to include ``STDIO``.
578 eval : Expr -> { [STDIO, EXCEPTION String, RND, STATE Env] } Eff Integer
580Note that using ``STDIO`` will restrict the number of contexts in
581which ``eval`` can be ``run`` to those which support ``STDIO``, such
582as ``IO``. Once effect lists get longer, it can be a good idea instead
583to encapsulate sets of effects in a type synonym. This is achieved as
584follows, simply by defining a function which computes a type, since
585types are first class in Idris:
589 EvalEff : Type -> Type
590 EvalEff t = { [STDIO, EXCEPTION String, RND, STATE Env] } Eff t
592 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