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.
State¶
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 typea
, whichis not updated, and running the
Get
operation returns something of typea
.
Put
takes ab
as an argument. It has a resource of typea
on input, which is updated to a resource of typeb
. Running thePut
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 : Type -> EFFECT
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 State
)
- The
The effectful operation (either
Get
orPut x
forState
)- A continuation, which we conventionally call
k
, and should be passed the result value of the operation, and an updated resource.
- A continuation, which we conventionally call
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.
Summary¶
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 : Type -> EFFECT
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 : EFFECT
STDIO = MkEff () StdIO
Exceptions¶
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 : Type -> EFFECT
EXCEPTION t = MkEff () (Exception t)
Non-determinism¶
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 : EFFECT
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 : Type -> EFFECT
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.