A predicate transformer semantics for effects (functional pearl)

Abstract

Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

References

1. Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017. Dijkstra Monads for Free. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, 515–529.
2. João Alpuim and Wouter Swierstra. 2018. Embedding the refinement calculus in Coq. Science of Computer Programming 164 (2018), 37–48.
3. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. 2015. Indexed containers. Journal of Functional Programming 25 (2015).
4. Ralph-Johan Back and Joakim von Wright. 2012. Refinement calculus: a systematic introduction. Springer Graduate Texts in Computer Science.
5. R. J. R. Back and J. von Wright. 1989. Refinement Concepts Formalized in Higher Order Logic. Formal Aspects of Computing 2 (1989).
6. Richard Bird. 2010. Pearls of Functional Algorithm Design. Cambridge University Press.
7. Richard Bird and Oege de Moor. 1996. The algebra of programming. Prentice Hall.
8. Sylvain Boulmé. 2007. Intuitionistic refinement calculus. In Typed Lambda Calculi and Applications. Springer, 54–69.
9. Ana Bove and Venanzio Capretta. 2005. Modelling general recursion in type theory. Mathematical Structures in Computer Science 15, 4 (2005), 671–708.
10. Ana Bove, Alexander Krauss, and Matthieu Sozeau. 2016. Partiality and recursion in interactive theorem provers – an overview. Mathematical Structures in Computer Science 26, 1 (2016), 38–88.
11. Edwin Brady. 2013a. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.
12. Edwin Brady. 2013b. Programming and Reasoning with Algebraic Effects and Dependent Types. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). ACM, 133–144.
13. M. J. Butler, J. Grundy, T. Långbacka, R. Ruksenas, and J. von Wright. 1997. The Refinement Calculator: Proof Support for Program Refinement. In Proc. Conf. Formal Methods Pacific’97, Springer Series in Discrete Mathematics and Theoretical Computer Science, L. Groves and S. Reeves (Eds.). 40–61.
14. Venanzio Capretta. 2005. General Recursion via Coinductive Types. Logical Methods in Computer Science 1, 2 (2005), 1–28.
15. Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. 2017. The end of history? Using a proof assistant to replace language design with library design. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Schloss Dagstuhl-Leibniz-Zentrum für Informatik.
16. The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual, version 8.7. ADT Coq (Action for Technological Development). http://coq.inria.fr
17. Edsger W. Dijkstra. 1975. Guarded commands, non-determinacy and formal. derivation of programs. Commun. ACM 18, 8 (1975), 453–457.
18. Brijesh Dongol, Victor B.F. Gomes, and Georg Struth. 2015. A Program Construction and Verification Tool for Separation Logic. In Mathematics of Program Construction (LNCS), Vol. 9129. Springer, 137–158.
19. Jeremy Gibbons. 2013. Unifying Theories of Programming with Monads. In Unifying Theories of Programming, Burkhart Wolff, Marie-Claude Gaudel, and Abderrahmane Feliachi (Eds.). Springer, 23–67.
20. Jeremy Gibbons and Ralf Hinze. 2011. Just Do It: Simple Monadic Equational Reasoning. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP ’11). ACM, 2–14.
21. Peter Hancock and Anton Setzer. 2000a. Interactive Programs in Dependent Type Theory. In Computer Science Logic: 14th InternationalWorkshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21 – 26, 2000 Proceedings, Peter G. Clote and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 317–331.
22. Peter Hancock and Anton Setzer. 2000b. Specifying interactions with dependent types. In Workshop on Subtyping and Dependent Types in Programming. INRIA, Ponte de Lima, Portugal, Article 5, 13 pages.
23. Graham Hutton and Diana Fulger. 2008. Reasoning about effects: Seeing the wood through the trees. (2008).
24. Martin Hyland, Gordon Plotkin, and John Power. 2006. Combining effects: Sum and tensor. Theoretical Computer Science 357, 1-3 (2006), 70–99.
25. Shin-ya Katsumata and Tetsuya Sato. 2013. Preorders on monads and coalgebraic simulations. In International Conference on Foundations of Software Science and Computational Structures. Springer, 145–160.
26. Oleg Kiselyov and Hiromi Ishii. 2015. Freer Monads, More Extensible Effects. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell (Haskell ’15). ACM, 94–105.
27. Sheng Liang, Paul Hudak, and Mark Jones. 1995. Monad transformers and modular interpreters. In Conference record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 333–343.
28. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martinez, Catalin Hritcu, Exequiel Rivas, and Éric Tanter. 2019. Dijkstra Monads for All. (2019). arXiv: cs.PL/1903.01237
29. Conor McBride. 2015. Turing-completeness totally free. In International Conference on Mathematics of Program Construction. Springer, 257–275.
30. Carroll Morgan. 1994. Programming from specifications. Prentice Hall,.
31. Aleksandar Nanevski and Greg Morrisett. 2005. Dependent Type Theory of Stateful Higher-Order Functions. Technical Report TR-24-05. Harvard University.
32. Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. 2006. Polymorphism and Separation in Hoare Type Theory. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). ACM, 62–73.
33. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. 2008. Ynot: Dependent Types for Imperative Programs. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). ACM, 229–240.
34. Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers University of Technology.
35. Gordon Plotkin and John Power. 2002. Notions of computation determine monads. In International Conference on Foundations of Software Science and Computation Structures. Springer, 342–356.
36. Gordon Plotkin and John Power. 2003. Algebraic operations and generic effects. Applied categorical structures 11, 1 (2003), 69–94.
37. Matija Pretnar. 2010. Logic and handling of algebraic effects. Ph.D. Dissertation. The University of Edinburgh.
38. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with value-dependent types. In Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 266–278.
39. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago ZanellaBéguelin. 2016. Dependent Types and Multi-monadic Effects in F*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, New York, NY, USA, 256–270.
40. Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying Higher-order Programs with the Dijkstra Monad. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’13). ACM, 387–398.
41. Wouter Swierstra. 2008. Data types à la carte. Journal of Functional Programming 18, 4 (2008), 423–436.
42. Wouter Swierstra. 2009a. A functional specification of effects. Ph.D. Dissertation. University of Nottingham.
43. Wouter Swierstra. 2009b. A Hoare Logic for the State Monad. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 440–451.
44. Wouter Swierstra and João Alpuim. 2016. From Proposition to Program - Embedding the Refinement Calculus in Coq. In Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings (LNCS), Vol. 9613. Springer, 29–44.
45. Wouter Swierstra and Thorsten Altenkirch. 2007. Beauty in the Beast: a functional semantics for the awkward squad. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop (Haskell ’07). ACM, 25–36.
46. Janis Voigtländer. 2008. Asymptotic Improvement of Computations over Free Monads. In Mathematics of Program Construction, Philippe Audebaud and Christine Paulin-Mohring (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 388–403.
47. Philip Wadler. 1987. A critique of Abelson and Sussman or why calculating is better than scheming. ACM SIGPLAN Notices 22, 3 (1987), 83–94.
48. Nicolas Wu, Tom Schrijvers, and Ralf Hinze. 2014. Effect Handlers in Scope. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell (Haskell ’14). ACM, 1–12.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Functional languages

• Theory of computation

  • Logic

    • Constructive mathematics

    • Logic and verification

    • Type theory

  • Semantics and reasoning

    • Program reasoning

      • Program specifications

    • Program semantics