Advocates for pure functional languages such as Haskell have long argued that a key benefit of these languages is the ability to reason equationally, using basic mathematics to reason about, verify, and derive programs. Consequently, introductory textbooks often place considerable emphasis on the use of equational reasoning to prove properties of programs. Graham, for example, concludes the chapter on equational reasoning in Programming in Haskell with the remark, ``Mathematics is an excellent tool for guiding the development of efficient programs with simple proofs!''
In this pearl, we mechanize equational reasoning in Haskell using an expressive type system. In particular, we demonstrate how Liquid Haskell, which brings refinement types to Haskell, can effectively check pen-and-paper proofs. Doing so remains faithful to the traditional techniques for verifying and deriving programs, while enjoying the added benefit of being mechanically checked for correctness. Moreover, this approach is well-suited to beginners because the language of proofs is simply Haskell itself.
To demonstrate the applicability of our approach, we present a series of examples that replay equational reasoning, program optimizations, and program calculations from the literature. Concretely, the paper is structured as follows:
Equational Reasoning: We prove properties about familiar functions on lists, and compare them with standard textbook proofs. In each case, the proofs are strikingly similar! This approach opens up machine-checked equational reasoning to ordinary Haskell users, without requiring expertise in theorem provers.
Optimized Function Derivations: Another common theme in Haskell textbooks is to derive efficient implementations from high-level specifications, as described by Bird and Graham. We demonstrate how Liquid Haskell supports the derivation of correct-by-construction programs by using equational proofs that themselves serve as efficient implementations.
Calculating Correct Compilers: As an extended case study we use equational reasoning to derive a correct-by-construction compiler for a simple language of numeric expressions, following Graham's book.
We conclude that, even though these proofs can be performed in external tools such as Agda, Coq, Dafny, Isabelle or Lean, equational reasoning using Liquid Haskell is unique in that the proofs are literally just Haskell functions. It can therefore be used by any Haskell programmer or learner.