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    :             { [STATE x] } Eff x
put    : x ->        { [STATE x] } Eff ()
putM   : y ->        { [STATE x] ==> [STATE y] } Eff ()
update : (x -> x) -> { [STATE x] } Eff ()

instance Handler State m

The last line, instance Handler State m, 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 ->   { [STDIO] } Eff ()
putStr   : String -> { [STDIO] } Eff ()
putStrLn : String -> { [STDIO] } Eff ()

getStr   :           { [STDIO] } Eff String
getChar  :           { [STDIO] } Eff Char

instance Handler StdIO IO
instance Handler StdIO (IOExcept a)

Examples

A program which reads the user’s name, then says hello, can be written as follows:

hello : { [STDIO] } Eff ()
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 : { [STDIO] } Eff ()
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 : { [STATE Int, STDIO] } Eff ()
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 explicitiy 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 -> { [EXCEPTION a ] } Eff b

instance           Handler (Exception a) Maybe
instance           Handler (Exception a) List
instance           Handler (Exception a) (Either a)
instance           Handler (Exception a) (IOExcept a)
instance Show a => Handler (Exception a) IO

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 paramaterised by an error type:

data Err = NotANumber | OutOfRange

parseNumber : Int -> String -> { [EXCEPTION Err] } Eff Int
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 Err context. It returns a value of the form Right x if successful:

*Exception> the (Either Err Int) $ run (parseNumber 42 "20")
Right 20 : Either Err Int

Or Left e on failure, carrying the appropriate exception:

*Exception> the (Either Err Int) $ run (parseNumber 42 "50")
Left OutOfRange : Either Err Int

*Exception> the (Either Err Int) $ run (parseNumber 42 "twenty")
Left NotANumber : Either Err 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 -> { [EXCEPTION Err] } Eff (Bounded x)
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 ->            { [RND] } Eff ()
rndInt : Integer -> Integer -> { [RND] } Eff Integer
rndFin : (k : Nat) ->          { [RND] } Eff (Fin (S k))

instance Handler Random m

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 -> { [STDIO] } Eff ()

For reference, the code for guess is given below:

guess : Int -> { [STDIO] } Eff ()
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 : { [RND, STDIO] } Eff ()
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 -> { [SELECT] } Eff a

instance Handler Selection Maybe
instance Handler Selection List

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 -> { [SELECT, EXCEPTION String] } Eff (Int, Int, Int)
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 :: idris 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 ->
             { [EXCEPTION String] } Eff (Vect m Int)
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 : { [STDIO] } Eff (p ** Vect p Int)

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. One way to implement this function, using -1 to indicate the end of input, is shown in Listing [readvec]. 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 : { [STDIO, EXCEPTION String] } Eff ()
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.

read_vec : { [STDIO] } Eff (p ** Vect p Int)
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 -> { [EXCEPTION String] } Eff Int
    parseNumber str
      = if all (\x => isDigit x || x == '-') (unpack str)
           then pure (cast str)
           else raise "Not a number"

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 -> { [EXCEPTION String, STATE Env] } Eff Integer
eval (Val x) = return x
eval (Add l r) = return $ !(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 => return 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 -> { [EXCEPTION String, STATE Env] } Eff Integer
        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 doen’t matter where RND appears in the list, as long as it is present:

eval : Expr -> { [EXCEPTION String, RND, STATE Env] } Eff Integer

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)
                         return 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 -> { [STDIO, EXCEPTION String, RND, STATE Env] } Eff Integer

Note that 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 = { [STDIO, EXCEPTION String, RND, STATE Env] } Eff t

eval : Expr -> EvalEff Integer