Further Reading¶
This tutorial has given an introduction to writing and reasoning about
side-effecting programs in Idris, using the Effects
library.
More details about the implementation of the library, such as how
run
works, how handlers are invoked, etc, are given in a separate
paper [1].
Some libraries and programs which use Effects
can be found in the
following places:
https://github.com/edwinb/SDL-idris — some bindings for the SDL media library, supporting graphics in particular.
https://github.com/edwinb/idris-demos — various demonstration programs, including several examples from this tutorial, and a “Space Invaders” game.
https://github.com/SimonJF/IdrisNet2 — networking and socket libraries.
https://github.com/edwinb/Protocols — a high level communication protocol description language.
The inspiration for the Effects
library was Bauer and Pretnar’s
Eff language [2], which describes a language based on algebraic
effects and handlers. Other recent languages and libraries have also
been built on this ideas, for example [3] and [4]. The theoretical
foundations are also well-studied see [5], [6], [7], [8].