Simple Effects¶
So far we have seen how to write programs with locally mutable state
using the STATE
effect. To recap, we have the definitions below
in a module Effect.State
module Effect.State
STATE : Type -> EFFECT
get : Eff x [STATE x]
put : x -> Eff () [STATE x]
putM : y -> Eff () [STATE x] [STATE y]
update : (x -> x) -> Eff () [STATE x]
Handler State m where { ... }
The last line, Handler State m where { ... }
, means that the STATE
effect is usable in any computation context m
. That is, a program
which uses this effect and returns something of type a
can be
evaluated to something of type m a
using run
, for any
m
. The lower case State
is a data type describing the
operations which make up the STATE
effect itself—we will go into
more detail about this in Section Creating New Effects.
In this section, we will introduce some other supported effects,
allowing console I/O, exceptions, random number generation and
non-deterministic programming. For each effect we introduce, we will
begin with a summary of the effect, its supported operations, and the
contexts in which it may be used, like that above for STATE
, and
go on to present some simple examples. At the end, we will see some
examples of programs which combine multiple effects.
All of the effects in the library, including those described in this section, are summarised in Appendix Effects Summary.
Console I/O¶
Console I/O is supported with the STDIO
effect, which allows reading and writing characters and strings to and
from standard input and standard output. Notice that there is a
constraint here on the computation context m
, because it only
makes sense to support console I/O operations in a context where we
can perform (or at the very least simulate) console I/O:
module Effect.StdIO
STDIO : EFFECT
putChar : Char -> Eff () [STDIO]
putStr : String -> Eff () [STDIO]
putStrLn : String -> Eff () [STDIO]
getStr : Eff String [STDIO]
getChar : Eff Char [STDIO]
Handler StdIO IO where { ... }
Handler StdIO (IOExcept a) where { ... }
Examples¶
A program which reads the user’s name, then says hello, can be written as follows:
hello : Eff () [STDIO]
hello = do putStr "Name? "
x <- getStr
putStrLn ("Hello " ++ trim x ++ "!")
We use trim
here to remove the trailing newline from the
input. The resource associated with STDIO
is simply the empty
tuple, which has a default value ()
, so we can run this as
follows:
main : IO ()
main = run hello
In hello
we could also use !
-notation instead of x <-
getStr
, since we only use the string that is read once:
hello : Eff () [STDIO]
hello = do putStr "Name? "
putStrLn ("Hello " ++ trim !getStr ++ "!")
More interestingly, we can combine multiple effects in one program. For example, we can loop, counting the number of people we’ve said hello to:
hello : Eff () [STATE Int, STDIO]
hello = do putStr "Name? "
putStrLn ("Hello " ++ trim !getStr ++ "!")
update (+1)
putStrLn ("I've said hello to: " ++ show !get ++ " people")
hello
The list of effects given in hello
means that the function can
call get
and put
on an integer state, and any functions which
read and write from the console. To run this, main
does not need
to be changed.
Aside: Resource Types¶
To find out the resource type of an effect, if necessary (for example
if we want to initialise a resource explicitly with runInit
rather
than using a default value with run
) we can run the
resourceType
function at the REPL:
*ConsoleIO> resourceType STDIO
() : Type
*ConsoleIO> resourceType (STATE Int)
Int : Type
Exceptions¶
The EXCEPTION
effect is declared in module Effect.Exception
. This allows programs
to exit immediately with an error, or errors to be handled more
generally:
module Effect.Exception
EXCEPTION : Type -> EFFECT
raise : a -> Eff b [EXCEPTION a]
Handler (Exception a) Maybe where { ... }
Handler (Exception a) List where { ... }
Handler (Exception a) (Either a) where { ... }
Handler (Exception a) (IOExcept a) where { ... }
Show a => Handler (Exception a) IO where { ... }
Example¶
Suppose we have a String
which is expected to represent an integer
in the range 0
to n
. We can write a function parseNumber
which returns an Int
if parsing the string returns a number in the
appropriate range, or throws an exception otherwise. Exceptions are
parameterised by an error type:
data Error = NotANumber | OutOfRange
parseNumber : Int -> String -> Eff Int [EXCEPTION Error]
parseNumber num str
= if all isDigit (unpack str)
then let x = cast str in
if (x >=0 && x <= num)
then pure x
else raise OutOfRange
else raise NotANumber
Programs which support the EXCEPTION
effect can be run in any
context which has some way of throwing errors, for example, we can run
parseNumber
in the Either Error
context. It returns a value of
the form Right x
if successful:
*Exception> the (Either Error Int) $ run (parseNumber 42 "20")
Right 20 : Either Error Int
Or Left e
on failure, carrying the appropriate exception:
*Exception> the (Either Error Int) $ run (parseNumber 42 "50")
Left OutOfRange : Either Error Int
*Exception> the (Either Error Int) $ run (parseNumber 42 "twenty")
Left NotANumber : Either Error Int
In fact, we can do a little bit better with parseNumber
, and have
it return a proof that the integer is in the required range along
with the integer itself. One way to do this is define a type of
bounded integers, Bounded
:
Bounded : Int -> Type
Bounded x = (n : Int ** So (n >= 0 && n <= x))
Recall that So
is parameterised by a Bool
, and only So
True
is inhabited. We can use choose
to construct such a value
from the result of a dynamic check:
data So : Bool -> Type = Oh : So True
choose : (b : Bool) -> Either (So b) (So (not b))
We then write parseNumber
using choose
rather than an
if/then/else
construct, passing the proof it returns on success as
the boundedness proof:
parseNumber : (x : Int) -> String -> Eff (Bounded x) [EXCEPTION Error]
parseNumber x str
= if all isDigit (unpack str)
then let num = cast str in
case choose (num >=0 && num <= x) of
Left p => pure (num ** p)
Right p => raise OutOfRange
else raise NotANumber
Random Numbers¶
Random number generation is also implemented by the library, in module
Effect.Random
:
module Effect.Random
RND : EFFECT
srand : Integer -> Eff () [RND]
rndInt : Integer -> Integer -> Eff Integer [RND]
rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]
Handler Random m where { ... }
Random number generation is considered side-effecting because its
implementation generally relies on some external source of randomness.
The default implementation here relies on an integer seed, which can
be set with srand
. A specific seed will lead to a predictable,
repeatable sequence of random numbers. There are two functions which
produce a random number:
rndInt
, which returns a random integer between the given lower- and upper bounds.
rndFin
, which returns a random element of a finite set- (essentially a number with an upper bound given in its type).
Example¶
We can use the RND
effect to implement a simple guessing game. The
guess
function, given a target number, will repeatedly ask the
user for a guess, and state whether the guess is too high, too low, or
correct:
guess : Int -> Eff () [STDIO]
For reference, the code for guess
is given below:
guess : Int -> Eff () [STDIO]
guess target
= do putStr "Guess: "
case run {m=Maybe} (parseNumber 100 (trim !getStr)) of
Nothing => do putStrLn "Invalid input"
guess target
Just (v ** _) =>
case compare v target of
LT => do putStrLn "Too low"
guess target
EQ => putStrLn "You win!"
GT => do putStrLn "Too high"
guess target
Note that we use parseNumber
as defined previously to read user input, but
we don’t need to list the EXCEPTION
effect because we use a nested run
to invoke parseNumber
, independently of the calling effectful program.
To invoke this, we pick a random number within the range 0–100,
having set up the random number generator with a seed, then run
guess
:
game : Eff () [RND, STDIO]
game = do srand 123456789
guess (fromInteger !(rndInt 0 100))
main : IO ()
main = run game
If no seed is given, it is set to the default
value. For a less
predictable game, some better source of randomness would be required,
for example taking an initial seed from the system time. To see how to
do this, see the SYSTEM
effect described in Effects Summary.
Non-determinism¶
The listing below gives the definition of the non-determinism effect, which allows a program to choose a value non-deterministically from a list of possibilities in such a way that the entire computation succeeds:
import Effects
import Effect.Select
SELECT : EFFECT
select : List a -> Eff a [SELECT]
Handler Selection Maybe where { ... }
Handler Selection List where { ... }
Example¶
The SELECT
effect can be used to solve constraint problems, such
as finding Pythagorean triples. The idea is to use select
to give
a set of candidate values, then throw an exception for any combination
of values which does not satisfy the constraint:
triple : Int -> Eff (Int, Int, Int) [SELECT, EXCEPTION String]
triple max = do z <- select [1..max]
y <- select [1..z]
x <- select [1..y]
if (x * x + y * y == z * z)
then pure (x, y, z)
else raise "No triple"
This program chooses a value for z
between 1
and max
, then
values for y
and x
. In operation, after a select
, the
program executes the rest of the do
-block for every possible
assignment, effectively searching depth-first. If the list is empty
(or an exception is thrown) execution fails.
There are handlers defined for Maybe
and List
contexts, i.e.
contexts which can capture failure. Depending on the context m
,
triple
will either return the first triple it finds (if in
Maybe
context) or all triples in the range (if in List
context). We can try this as follows:
main : IO ()
main = do print $ the (Maybe _) $ run (triple 100)
print $ the (List _) $ run (triple 100)
vadd
revisited¶
We now return to the vadd
program from the introduction. Recall the
definition:
vadd : Vect n Int -> Vect n Int -> Vect n Int
vadd [] [] = []
vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
Using , we can set up a program so that it reads input from a user,
checks that the input is valid (i.e both vectors contain integers, and
are the same length) and if so, pass it on to vadd
. First, we
write a wrapper for vadd
which checks the lengths and throw an
exception if they are not equal. We can do this for input vectors of
length n
and m
by matching on the implicit arguments n
and
m
and using decEq
to produce a proof of their equality, if
they are equal:
vadd_check : Vect n Int -> Vect m Int ->
Eff (Vect m Int) [EXCEPTION String]
vadd_check {n} {m} xs ys with (decEq n m)
vadd_check {n} {m=n} xs ys | (Yes Refl) = pure (vadd xs ys)
vadd_check {n} {m} xs ys | (No contra) = raise "Length mismatch"
To read a vector from the console, we implement a function of the following type:
read_vec : Eff (p ** Vect p Int) [STDIO]
This returns a dependent pair of a length, and a vector of that
length, because we cannot know in advance how many integers the user
is going to input. We can use -1
to indicate the end of input:
read_vec : Eff (p ** Vect p Int) [STDIO]
read_vec = do putStr "Number (-1 when done): "
case run (parseNumber (trim !getStr)) of
Nothing => do putStrLn "Input error"
read_vec
Just v => if (v /= -1)
then do (_ ** xs) <- read_vec
pure (_ ** v :: xs)
else pure (_ ** [])
where
parseNumber : String -> Eff Int [EXCEPTION String]
parseNumber str
= if all (\x => isDigit x || x == '-') (unpack str)
then pure (cast str)
else raise "Not a number"
This uses a variation on parseNumber
which does not require a
number to be within range.
Finally, we write a program which reads two vectors and prints the result of pairwise addition of them, throwing an exception if the inputs are of differing lengths:
do_vadd : Eff () [STDIO, EXCEPTION String]
do_vadd = do putStrLn "Vector 1"
(_ ** xs) <- read_vec
putStrLn "Vector 2"
(_ ** ys) <- read_vec
putStrLn (show !(vadd_check xs ys))
By having explicit lengths in the type, we can be sure that vadd
is only being used where the lengths of inputs are guaranteed to be
equal. This does not stop us reading vectors from user input, but it
does require that the lengths are checked and any discrepancy is dealt
with gracefully.
Example: An Expression Calculator¶
To show how these effects can fit together, let us consider an evaluator for a simple expression language, with addition and integer values.
data Expr = Val Integer
| Add Expr Expr
An evaluator for this language always returns an Integer
, and
there are no situations in which it can fail!
eval : Expr -> Integer
eval (Val x) = x
eval (Add l r) = eval l + eval r
If we add variables, however, things get more interesting. The evaluator will need to be able to access the values stored in variables, and variables may be undefined.
data Expr = Val Integer
| Var String
| Add Expr Expr
To start, we will change the type of eval
so that it is effectful,
and supports an exception effect for throwing errors, and a state
containing a mapping from variable names (as String
) to their
values:
Env : Type
Env = List (String, Integer)
eval : Expr -> Eff Integer [EXCEPTION String, STATE Env]
eval (Val x) = pure x
eval (Add l r) = pure $ !(eval l) + !(eval r)
Note that we are using !
-notation to avoid having to bind
subexpressions in a do
block. Next, we add a case for evaluating
Var
:
eval (Var x) = case lookup x !get of
Nothing => raise $ "No such variable " ++ x
Just val => pure val
This retrieves the state (with get
, supported by the STATE Env
effect) and raises an exception if the variable is not in the
environment (with raise
, supported by the EXCEPTION String
effect).
To run the evaluator on a particular expression in a particular
environment of names and their values, we can write a function which
sets the state then invokes eval
:
runEval : List (String, Integer) -> Expr -> Maybe Integer
runEval args expr = run (eval' expr)
where eval' : Expr -> Eff Integer [EXCEPTION String, STATE Env]
eval' e = do put args
eval e
We have picked Maybe
as a computation context here; it needs to be
a context which is available for every effect supported by
eval
. In particular, because we have exceptions, it needs to be a
context which supports exceptions. Alternatively, Either String
or
IO
would be fine, for example.
What if we want to extend the evaluator further, with random number
generation? To achieve this, we add a new constructor to Expr
,
which gives a random number up to a maximum value:
data Expr = Val Integer
| Var String
| Add Expr Expr
| Random Integer
Then, we need to deal with the new case, making sure that we extend
the list of events to include RND
. It doesn’t matter where RND
appears in the list, as long as it is present:
eval : Expr -> Eff Integer [EXCEPTION String, RND, STATE Env]
eval (Random upper) = rndInt 0 upper
For test purposes, we might also want to print the random number which has been generated:
eval (Random upper) = do val <- rndInt 0 upper
putStrLn (show val)
pure val
If we try this without extending the effects list, we would see an error something like the following:
Expr.idr:28:6:When elaborating right hand side of eval:
Can't solve goal
SubList [STDIO]
[(EXCEPTION String), RND, (STATE (List (String, Integer)))]
In other words, the STDIO
effect is not available. We can correct
this simply by updating the type of eval
to include STDIO
.
eval : Expr -> Eff Integer [STDIO, EXCEPTION String, RND, STATE Env]
Note
Using STDIO
will restrict the number of contexts in
which eval
can be run
to those which support
STDIO
, such as IO
. Once effect lists get longer, it
can be a good idea instead to encapsulate sets of effects in
a type synonym. This is achieved as follows, simply by
defining a function which computes a type, since types are
first class in Idris:
EvalEff : Type -> Type
EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]
eval : Expr -> EvalEff Integer