Author:

Keywords:

Science & Technology, Technology, Physical Sciences, Computer Science, Software Engineering, Computer Science, Theory & Methods, Mathematics, Applied, Logic, Computer Science, Mathematics, Science & Technology - Other Topics, Monads, Effect handlers, Equational reasoning, Nondeterminism, State, Contextual equivalence, HANDLERS, G0D1419N#54969407

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 abstract 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.