Effects

From version 0.9.12 Idris includes a library for side-effect management, Effects.
To use it, you will need to add the -p effects flag when invoking Idris, which makes the effect package available. The following information is available about Effects

  • A tutorial on programming with side-effects in Idris

The papers and talks below describe an earlier version of the effects package, available from Idris 0.9.7-0.9.11 (and still available in a deprecated oldeffects package).

  • A paper which describes how to use Effects as well as how to create new side-effects and how it is implemented.
  • A talk on managing effects, with slides and a video, as part of a mini-course.
  • The source code of the library itself.

Additionally, some examples from the above paper are available to download.