Shin-Cheng Mu. Tech. Report TR-IIS-19-003, Institute of Information Science, Academia Sinica, June 2019.
[PDF]
Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively less attention has been paid to reasoning about monadic programs. In this report we derive a backtracking algorithm for problem specifications that use a monadic unfold to generate possible solutions, which are filtered using a scanl-like predicate. We develop theorems that convert a variation of scanl to a foldr that uses the state monad, as well as theorems constructing hylomorphism. The algorithm is used to solve the n-queens puzzle, our running example. The aim is to develop theorems and patterns useful for the derivation of monadic programs, focusing on the intricate interaction between state and non-determinism.