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.
- 1
Edwin Brady. 2013. Programming and reasoning with algebraic effects and dependent types. SIGPLAN Not. 48, 9 (September 2013), 133-144. DOI=10.1145/2544174.2500581 https://dl.acm.org/citation.cfm?doid=2544174.2500581
- 2
Andrej Bauer, Matija Pretnar, Programming with algebraic effects and handlers, Journal of Logical and Algebraic Methods in Programming, Volume 84, Issue 1, January 2015, Pages 108-123, ISSN 2352-2208, http://math.andrej.com/wp-content/uploads/2012/03/eff.pdf
- 3
Ben Lippmeier. 2009. Witnessing Purity, Constancy and Mutability. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS ‘09), Zhenjiang Hu (Ed.). Springer-Verlag, Berlin, Heidelberg, 95-110. DOI=10.1007/978-3-642-10672-9_9 https://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
- 4
Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. SIGPLAN Not. 48, 9 (September 2013), 145-158. DOI=10.1145/2544174.2500590 https://dl.acm.org/citation.cfm?doid=2544174.2500590
- 5
Martin Hyland, Gordon Plotkin, John Power, Combining effects: Sum and tensor, Theoretical Computer Science, Volume 357, Issues 1–3, 25 July 2006, Pages 70-99, ISSN 0304-3975, (https://www.sciencedirect.com/science/article/pii/S0304397506002659)
- 6
Paul Blain Levy. 2004. Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, V. 2). Kluwer Academic Publishers, Norwell, MA, USA.
- 7
Plotkin, Gordon, and Matija Pretnar. “Handlers of algebraic effects.” Programming Languages and Systems. Springer Berlin Heidelberg, 2009. 80-94.
- 8
Pretnar, Matija. “Logic and handling of algebraic effects.” (2010).