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.