×

zbMATH — the first resource for mathematics

Local algebraic effect theories. (English) Zbl 07245567
Summary: Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. We present an alternative approach where the type system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimisations and reasoning tools.
MSC:
68N18 Functional programming and lambda calculus
Software:
Eff; Haskell; QuickCheck; z3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ahman, D. (2017) Fibred Computational Effects. Ph.D. thesis, School of Informatics, University of Edinburgh.
[2] Ahman, D. (2018) Handling fibred algebraic effects. PACMPL2(POPL), 7:1-7:29.
[3] Bauer, A. & Pretnar, M. (2014) An effect system for algebraic effects and handlers. Log. Methods Comput. Sci.10(4), 1-29. · Zbl 1448.68203
[4] Bauer, A. & Pretnar, M. (2015) Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program.84(1), 108-123. · Zbl 1304.68025
[5] Bauer, A., Hofmann, M., Pretnar, M. & Yallop, J. (2016) From theory to practice of algebraic effects and handlers. Dagstuhl Rep.6(3), 44-58.
[6] Biernacki, D., Piróg, M., Polesiuk, P. & Sieczkowski, F. (2018) Handle with care: Relational interpretation of algebraic effects and handlers. PACMPL2(POPL), 8:1-8:30.
[7] Brady, E. (2013) Programming and reasoning with algebraic effects and dependent types. In Morrisett, G. & Uustalu, T. (eds), ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA, September 25-27, 2013. ACM, pp. 133-144. · Zbl 1323.68097
[8] Chandrasekaran, S. K., Leijen, D., Pretnar, M. & Schrijvers, T. (2018) Algebraic effect handlers go mainstream. Dagstuhl Rep.8(4), 104-125.
[9] Claessen, K. & Hughes, J. (2000) Quickcheck: A lightweight tool for random testing of haskell programs. In Odersky, M. & Wadler, P. (eds), Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP’00), Montreal, Canada, September 18-21, 2000. ACM, pp. 268-279.
[10] De Moura, L. M. & Bjørner, N. (2008) Z3: An efficient SMT solver. In TACAS. Lecture Notes in Computer Science, vol. 4963. Springer, pp. 337-340.
[11] Forster, Y., Kammar, O., Lindley, S. & Pretnar, M. (2017) On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. PACMPL1(ICFP), 13:1-13:29.
[12] Gibbons, J. & Hinze, R. (2011) Just do it: Simple monadic equational reasoning. In Chakravarty, M. M. T., Hu, Z. & Danvy, O. (eds), Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011. ACM, pp. 2-14. · Zbl 1323.68207
[13] Hillerström, D. & Lindley, S. (2016) Liberating effects with rows and handlers. In Chapman, J. & Swierstra, W. (eds), Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016. ACM, pp. 15-27.
[14] Kammar, O. & Plotkin, G. D. (2012). Algebraic foundations for effect-dependent optimisations. In Field, J. & Hicks, M. (eds), Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. ACM, pp. 349-360. · Zbl 1321.68200
[15] Kammar, O. & Pretnar, M. (2017) No value restriction is needed for algebraic effects and handlers. J. Funct. Program.27, e7. · Zbl 1418.68034
[16] Kammar, O., Lindley, S. & Oury, N. (2013) Handlers in action. In Morrisett, G. & Uustalu, T. (eds), ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA, September 25-27, 2013. ACM, pp. 145-158. · Zbl 1323.68126
[17] Leijen, D. (2017) Type directed compilation of row-typed algebraic effects. In Castagna, G. & Gordon, A. D. (eds), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM, pp. 486-499. · Zbl 1380.68097
[18] Levy, P. B., Power, J. & Thielecke, H. (2003) Modelling environments in call-by-value programming languages. Inf. Comput.185(2), 182-210. · Zbl 1069.68073
[19] Mclaughlin, C., Mckinna, J. & Stark, I. (2018) Triangulating context lemmas. In Andronick, J. & Felty, A. P. (eds), Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018. ACM, pp. 102-114.
[20] Moggi, E. (1991) Notions of computation and monads. Inf. Comput.93(1), 55-92. · Zbl 0723.68073
[21] Plotkin, G. D. & Power, J. (2001) Adequacy for algebraic effects. In Honsell, F. & Miculan, M. (eds), Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2030. Springer, pp. 1-24. · Zbl 0986.68055
[22] Plotkin, G. D. & Power, J. (2003) Algebraic operations and generic effects. Appl. Categorical Struct. 11(1), 69-94. · Zbl 1023.18006
[23] Plotkin, G. D. & Pretnar, M. (2008) A logic for algebraic effects. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA. IEEE Computer Society, pp. 118-129.
[24] Plotkin, G. D. & Pretnar, M. (2009) Handlers of algebraic effects. In Castagna, G. (ed), Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5502. Springer, pp. 80-94.
[25] Plotkin, G. D. & Pretnar, M. (2013) Handling algebraic effects. Log. Methods Comput. Sci.9(4), 1-36. · Zbl 1314.68191
[26] Pretnar, M. (2010) Logic and Handling of Algebraic Effects. Ph.D. thesis, University of Edinburgh, UK.
[27] Pretnar, M. (2015) An introduction to algebraic effects and handlers. Invited tutorial paper. Electr. Notes Theor. Comput. Sci.319, 19-35. · Zbl 1351.68079
[28] Saleh, A. H., Karachalias, G., Pretnar, M. & Schrijvers, T. (2018) Explicit effect subtyping. In Ahmed, A. (ed), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801. Springer, pp. 327-354. · Zbl 1418.68065
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.