Abstract
Equational reasoning is one of the most important tools of functional programming. To facilitate its application to monadic programs, Gibbons and Hinze have proposed a simple axiomatic approach using laws that characterise the computational effects without exposing their implementation details. At the same time Plotkin and Pretnar have proposed algebraic effects and handlers, a mechanism of layered abstractions by which effects can be implemented in terms of other effects.
This paper performs a case study that connects these two strands of research. We consider two ways in which the nondeterminism and state effects can interact: the high-level semantics where every nondeterministic branch has a local copy of the state, and the low-level semantics where a single sequentially threaded state is global to all branches.
We give a monadic account of the folklore technique of handling local state in terms of global state, provide a novel axiomatic characterisation of global state and prove that the handler satisfies Gibbons and Hinze’s local state axioms by means of a novel combination of free monads and contextual equivalence. We also provide a model for global state that is necessarily non-monadic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The proof can be found at https://github.com/KoenP/LocalAsGlobal.
- 2.
Gibbons and Hinze [4] were mistaken in their claim that the type \( s \rightarrow [( a , s )]\) constitutes a model of their backtrackable state laws; it is not a model because its
does not commute with itself. One could consider a relaxed semantics that admits \( s \rightarrow [( a , s )]\), but that is not the focus of this paper.
does not commute with itself. One could consider a relaxed semantics that admits References
Aït-Kaci, H.: Warren’s Abstract Machine: A Tutorial Reconstruction (1991)
Bauer, A., Pretnar, M.: An effect system for algebraic effects and handlers. Logical Methods Comput. Sci. 10(4) (2014). https://doi.org/10.2168/LMCS-10(4:9)2014
Gale, Y.: ListT done right alternative (2007). https://wiki.haskell.org/ListT_done_right_alternative
Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: Danvy, O. (ed.) International Conference on Functional Programming, pp. 2–14. ACM Press (2011)
Gill, A., Kmett, E.: The monad transformer library (2014). https://hackage.haskell.org/package/mtl
Hinze, R.: Prolog’s control constructs in a functional setting - axioms and implementation. Int. J. Found. Comput. Sci. 12(2), 125–170 (2001). https://doi.org/10.1142/S0129054101000436
Hutton, G., Fulger, D.: Reasoning about effects: seeing the wood through the trees. In: Symposium on Trends in Functional Programming (2007)
Kiselyov, O.: Laws of monadplus (2015). http://okmij.org/ftp/Computation/monads.html#monadplus
Kiselyov, O., Ishii, H.: Freer monads, more extensible effects. In: Reppy, J.H. (ed.) Symposium on Haskell, pp. 94–105. ACM Press (2015)
Lukšič, V., Pretnar, M.: Local algebraic effect theories (2019, submitted)
Moggi, E.: Computational lambda-calculus and monads. In: Parikh, R. (ed.) Logic in Computer Science, pp. 14–23. IEEE Computer Society Press (1989)
Plotkin, G., Pretnar, M.: Handlers of algebraic effects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 80–94. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_7
Volkov, N.: The list-t package (2014). http://hackage.haskell.org/package/list-t
Wadler, P.: Monads for functional programming. In: Broy, M. (ed.) Program Design Calculi: Marktoberdorf Summer School, pp. 233–264. Springer, Heidelberg (1992). https://doi.org/10.1007/978-3-662-02880-3_8
Wu, N., Schrijvers, T., Hinze, R.: Effect handlers in scope. In: Voigtländer, J. (ed.) Symposium on Haskell, pp. 1–12. ACM Press (2012)
Acknowledgements
We would like to thank Matija Pretnar, the members of IFIP WG 2.1, the participants of Shonan meeting 146 and the MPC reviewers for their insightful comments. We would also like to thank the Flemish Fund for Scientific Research (FWO) for their financial support.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Pauwels, K., Schrijvers, T., Mu, SC. (2019). Handling Local State with Global State. In: Hutton, G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science(), vol 11825. Springer, Cham. https://doi.org/10.1007/978-3-030-33636-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-33636-3_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-33635-6
Online ISBN: 978-3-030-33636-3
eBook Packages: Computer ScienceComputer Science (R0)