Creating New Effects

We have now seen several side-effecting operations provided by the Effects library, and examples of their use in Section Simple Effects. We have also seen how operations may modify the available effects by changing state in Section Dependent Effects. We have not, however, yet seen how these operations are implemented. In this section, we describe how a selection of the available effects are implemented, and show how new effectful operations may be provided.


Effects are described by algebraic data types, where the constructors describe the operations provided when the effect is available. Stateful operations are described as follows:

data State : Effect where
     Get :      { a }       State a
     Put : b -> { a ==> b } State ()

Each effect is associated with a resource, the type of which is given with the notation { x ==> x’ }. This notation gives the resource type expected by each operation, and how it updates when the operation is run. Here, it means:

  • Get takes no arguments. It has a resource of type a, which

    is not updated, and running the Get operation returns something of type a.

  • Put takes a b as an argument. It has a resource of type

    a on input, which is updated to a resource of type b. Running the Put operation returns the element of the unit type.

Effect itself is a type synonym, declared as follows:

Effect : Type
Effect = (result : Type) ->
         (input_resource : Type) ->
         (output_resource : result -> Type) -> Type

That is, an effectful operation returns something of type result, has an input resource of type input_resource, and a function output_resource which computes the output resource type from the result. We use the same syntactic sugar as with Eff to make effect declarations more readable. It is defined as follows in the library:

syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
       = eff inst (\b => outst)
syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)

In order to convert State (of type Effect) into something usable in an effects list, of type EFFECT, we write the following:

STATE t = MkEff t State

MkEff constructs an EFFECT by taking the resource type (here, the t which parameterises STATE) and the effect signature (here, State). For reference, EFFECT is declared as follows:

data EFFECT : Type where
     MkEff : Type -> Effect -> EFFECT

Recall that to run an effectful program in Eff, we use one of the run family of functions to run the program in a particular computation context m. For each effect, therefore, we must explain how it is executed in a particular computation context for run to work in that context. This is achieved with the following type class:

class Handler (e : Effect) (m : Type -> Type) where
      handle : resource -> (eff : e t resource resource') ->
               ((x : t) -> resource' x -> m a) -> m a

We have already seen some instance declarations in the effect summaries in Section Simple Effects. An instance of Handler e m means that the effect declared with signature e can be run in computation context m. The handle function takes:

  • The resource on input (so, the current value of the state for


  • The effectful operation (either Get or Put x for State)

  • A continuation, which we conventionally call k, and should be

    passed the result value of the operation, and an updated resource.

There are two reasons for taking a continuation here: firstly, this is neater because there are multiple return values (a new resource and the result of the operation); secondly, and more importantly, the continuation can be called zero or more times.

A Handler for State simply passes on the value of the state, in the case of Get, or passes on a new state, in the case of Put. It is defined the same way for all computation contexts:

instance Handler State m where
     handle st Get     k = k st st
     handle st (Put n) k = k () n

This gives enough information for Get and Put to be used directly in Eff programs. It is tidy, however, to define top level functions in Eff, as follows:

get : { [STATE x] } Eff x
get = call Get

put : x -> { [STATE x] } Eff ()
put val = call (Put val)

putM : y -> { [STATE x] ==> [STATE y] } Eff ()
putM val = call (Put val)

An implementation detail (aside): The call function converts an Effect to a function in Eff, given a proof that the effect is available. This proof can be constructed automatically by , since it is essentially an index into a statically known list of effects:

call : {e : Effect} ->
       (eff : e t a b) -> {auto prf : EffElem e a xs} ->
       Eff t xs (\v => updateResTy v xs prf eff)

This is the reason for the Can’t solve goal error when an effect is not available: the implicit proof prf has not been solved automatically because the required effect is not in the list of effects xs.

Such details are not important for using the library, or even writing new effects, however.


The following listing summarises what is required to define the STATE effect:

data State : Effect where
     Get :      { a }       State a
     Put : b -> { a ==> b } State ()

STATE t = MkEff t State

instance Handler State m where
     handle st Get     k = k st st
     handle st (Put n) k = k () n

get : { [STATE x] } Eff x
get = call Get

put : x -> { [STATE x] } Eff ()
put val = call (Put val)

putM : y -> { [STATE x] ==> [STATE y] } Eff ()
putM val = call (Put val)

Console I/O

Then listing below gives the definition of the STDIO effect, including handlers for IO and IOExcept. We omit the definition of the top level Eff functions, as this merely invoke the effects PutStr, GetStr, PutCh and GetCh directly.

Note that in this case, the resource is the unit type in every case, since the handlers merely apply the IO equivalents of the effects directly.

data StdIO : Effect where
     PutStr : String -> { () } StdIO ()
     GetStr : { () } StdIO String
     PutCh : Char -> { () } StdIO ()
     GetCh : { () } StdIO Char

instance Handler StdIO IO where
    handle () (PutStr s) k = do putStr s; k () ()
    handle () GetStr     k = do x <- getLine; k x ()
    handle () (PutCh c)  k = do putChar c; k () ()
    handle () GetCh      k = do x <- getChar; k x ()

instance Handler StdIO (IOExcept a) where
    handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
    handle () GetStr     k = do x <- ioe_lift $ getLine; k x ()
    handle () (PutCh c)  k = do ioe_lift $ putChar c; k () ()
    handle () GetCh      k = do x <- ioe_lift $ getChar; k x ()

STDIO = MkEff () StdIO


The listing below gives the definition of the Exception effect, including two of its handlers for Maybe and List. The only operation provided is Raise. The key point to note in the definitions of these handlers is that the continuation k is not used. Running Raise therefore means that computation stops with an error.

data Exception : Type -> Effect where
     Raise : a -> { () } Exception a b

instance Handler (Exception a) Maybe where
     handle _ (Raise e) k = Nothing

instance Handler (Exception a) List where
     handle _ (Raise e) k = []

EXCEPTION t = MkEff () (Exception t)


The following listing gives the definition of the Select effect for writing non-deterministic programs, including a handler for List context which returns all possible successful values, and a handler for Maybe context which returns the first successful value.

data Selection : Effect where
     Select : List a -> { () } Selection a

instance Handler Selection Maybe where
     handle _ (Select xs) k = tryAll xs where
         tryAll [] = Nothing
         tryAll (x :: xs) = case k x () of
                                 Nothing => tryAll xs
                                 Just v => Just v

instance Handler Selection List where
     handle r (Select xs) k = concatMap (\x => k x r) xs

SELECT = MkEff () Selection

Here, the continuation is called multiple times in each handler, for each value in the list of possible values. In the List handler, we accumulate all successful results, and in the Maybe handler we try the first value in the last, and try later values only if that fails.

File Management

Result-dependent effects are no different from non-dependent effects in the way they are implemented. The listing below illustrates this for the FILE_IO effect. The syntax for state transitions { x ==> {res} x’ }, where the result state x’ is computed from the result of the operation res, follows that for the equivalent Eff programs.

data FileIO : Effect where
     Open  : String -> (m : Mode) ->
             {() ==> {res} if res then OpenFile m else ()} FileIO Bool
     Close : {OpenFile m ==> ()}                           FileIO ()

     ReadLine  :           {OpenFile Read}  FileIO String
     WriteLine : String -> {OpenFile Write} FileIO ()
     EOF       :           {OpenFile Read}  FileIO Bool

instance Handler FileIO IO where
    handle () (Open fname m) k = do h <- openFile fname m
                                    if !(validFile h)
                                             then k True (FH h)
                                             else k False ()
    handle (FH h) Close      k = do closeFile h
                                    k () ()

    handle (FH h) ReadLine        k = do str <- fread h
                                         k str (FH h)
    handle (FH h) (WriteLine str) k = do fwrite h str
                                         k () (FH h)
    handle (FH h) EOF             k = do e <- feof h
                                         k e (FH h)

FILE_IO t = MkEff t FileIO

Note that in the handler for Open, the types passed to the continuation k are different depending on whether the result is True (opening succeeded) or False (opening failed). This uses validFile, defined in the Prelude, to test whether a file handler refers to an open file or not.