git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/docs/effects/conclusions.rst
76 lines 3.2 kB history raw
1.. _sect-further:
3***************
4Further Reading
5***************
7This tutorial has given an introduction to writing and reasoning about
8side-effecting programs in Idris, using the ``Effects`` library.
9More details about the *implementation* of the library, such as how
10``run`` works, how handlers are invoked, etc, are given in a separate
11paper [1]_.
13Some libraries and programs which use ``Effects`` can be found in the
14following places:
16- http://github.com/edwinb/SDL-idris — some bindings for the SDL media
17 library, supporting graphics in particular.
19- http://github.com/edwinb/idris-demos — various demonstration
20 programs, including several examples from this tutorial, and a “Space
21 Invaders” game.
23- https://github.com/SimonJF/IdrisNet2 — networking and socket
24 libraries.
26- http://github.com/edwinb/Protocols — a high level communication
27 protocol description language.
29The inspiration for the ``Effects`` library was Bauer and Pretnar’s
30Eff language [2]_, which describes a langauge based on algebraic
31effects and handlers. Other recent languages and libraries have also
32been built on this ideas, for example [3]_ and [4]_. The theoretical
33foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.
37.. [1] Edwin Brady. 2013. Programming and reasoning with algebraic
38 effects and dependent types. SIGPLAN Not. 48, 9 (September
39 2013), 133-144. DOI=10.1145/2544174.2500581
40 http://doi.acm.org/10.1145/2544174.2500581
42.. [2] Andrej Bauer, Matija Pretnar, Programming with algebraic
43 effects and handlers, Journal of Logical and Algebraic Methods
44 in Programming, Volume 84, Issue 1, January 2015, Pages
45 108-123, ISSN 2352-2208,
46 http://dx.doi.org/10.1016/j.jlamp.2014.02.001.
47 (http://www.sciencedirect.com/science/article/pii/S2352220814000194)
49.. [3] Ben Lippmeier. 2009. Witnessing Purity, Constancy and
50 Mutability. In Proceedings of the 7th Asian Symposium on
51 Programming Languages and Systems (APLAS '09), Zhenjiang Hu
52 (Ed.). Springer-Verlag, Berlin, Heidelberg,
53 95-110. DOI=10.1007/978-3-642-10672-9_9
54 http://dx.doi.org/10.1007/978-3-642-10672-9_9
56.. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in
57 action. SIGPLAN Not. 48, 9 (September 2013),
58 145-158. DOI=10.1145/2544174.2500590
59 http://doi.acm.org/10.1145/2544174.2500590
61.. [5] Martin Hyland, Gordon Plotkin, John Power, Combining effects:
62 Sum and tensor, Theoretical Computer Science, Volume 357,
63 Issues 1–3, 25 July 2006, Pages 70-99, ISSN 0304-3975,
64 http://dx.doi.org/10.1016/j.tcs.2006.03.013.
65 (http://www.sciencedirect.com/science/article/pii/S0304397506002659)
67.. [6] Paul Blain Levy. 2004. Call-By-Push-Value: A
68 Functional/Imperative Synthesis (Semantics Structures in
69 Computation, V. 2). Kluwer Academic Publishers, Norwell, MA,
70 USA.
72.. [7] Plotkin, Gordon, and Matija Pretnar. "Handlers of algebraic
73 effects." Programming Languages and Systems. Springer Berlin
74 Heidelberg, 2009. 80-94.
76.. [8] Pretnar, Matija. "Logic and handling of algebraic effects." (2010).