Effects is an Idris package that implements resource-dependent algebraic effects. This allows a developer to control at a fine-a-grained level the side affects (state, logging, IO) for effectful programs. A tutorial and more background on their use is available on line.
When writting my Idris libraries I have used Effects to manage exceptions, state, logging, and IO. Here are some tips in my experiences in using Effects.
In an effectful function the effects used are declared in a
List data structure of type
List EFFECT. An effectful main function will look like:
fooMain : Eff () [FILE_IO, STDIO, SYSTEM] fooMain = do ...
The top most list of effects will determine the complete set of effects allowed in sub-effectful programs. Good practice will be
In this list the order in which effects appear will have an effect on the order in which sub lists can be created for effectful programs called. An engineering tip will be to create a global list of effects that allows for the list of effects to be passed around to all effectful programs. It also saves on typing.
Most, if not all, of my projects have a file called
Effs.idr. This file is used to control the imports of effects, and creation of effectful utility functions for working with state, logging, and IO. This allows me to keep track of the effects I use and isolate the majority of utility functions to a single file.
If you are creating a library to be used by others that contains effectful functions, be proactive and label the effects that are native to your library. For example, the file, stdio, log, and system effects are shared by all effectful programs and need not be labelled. The use of effects such as exception and state will be custom to your library. This advice holds if you are using only a single instance of the State effect, as it will be guaranteed that a user might use a library that has their own effect. Label it.
These labels should be unique and a simple naming scheme can be =
The only place in which you would not want to label your state effect if you know that the effect will be run in isolation from the main effectful program.
With the use of labels can come messy looking code and forgetfulness of label names. The latter especially if you hide the list of effects.
Take for example:
FooEffs : List EFFECT FooEffs = [ FILE_IO (), SYSTEM, STDIO , 'foost ::: STATE FState , 'fopts ::: STATE FOpts , 'foosymtbl ::: STATE SymTbl , 'fooerr ::: Exception FooError] fooMain : Eff () FooEffs fooMain = do as <- getArgs opts <- processArgs as case opts of Nothing => 'fooerr :- raise InvalidOpts Just os => do 'fopts :- put os st <- doInit case st of Nothing => 'fooerr :- raise InvalidState Just s => do 'foost :- put st doStuff ...
A good trick is to re-domain the effects such that the effectful functions are accessed using the form =
namespace Foo raise : FooError -> Eff b ['fooerr ::: Exception FooError] raise err = 'fooerr :- Exception.raise err
Accessing state becomes:
getFState : Eff FState ['foost ::: STATE FState] getFState = 'foost :- get updateFState : (FState -> FState) -> Eff () ['foost ::: STATE FState] updateFState u = 'foost :- update (\st => u st) setFState : FState -> Eff () ['foost ::: STATE FState] setFState newST = 'foost :- put newST
And option accessors will have type:
getFOptions : Eff FOpts ['fopts ::: STATE FOpts] putFOptions : FOpts -> Eff () ['fopts ::: STATE FOpts]
The program from above now becomes:
fooMain : Eff () FooEffs fooMain = do as <- getArgs opts <- processArgs as case opts of Nothing => Foo.raise InvalidOpts Just os => do setFOptions os st <- doInit case st of Nothing => Foo.raise InvalidState Just s => do setFState s doStuff ...
An added benefit of this approach is that it adds a level of indirection in case you wish to update how you deal with your state affects... Which leads on to the final hint for using effects.
If you find that you are using multiple state effects in your program that you define yourself, consider collapsing them into a single record and write some wrapper effectful functions to obtain the requisite state from the global state.