State Will do

The main strength of purely functional languages like Haskell is that they make reasoning about programs easy with a technique called equational reasoning. This ease of reasoning also extends to effectful programs provided the side-effects are modelled in a purely functional manner, for instance with monads. This paper uses equational reasoning to reason about the modelling of the side-effects themselves. In particular, we consider non-determinism, which is a key side-effect in Prolog and other logic-programming systems. Non-determinism is typically modelled by the list monad, but efficient implementations of Prolog and other non-deterministic systems use a much more low-level approach based on mutable state. In this way we model those lower-level implementations with the state monad and use equational reasoning to show its correctness with respect to the high-level list-based model. We also show how this result can be further generalized to other models of non-determinism.status: publishe