Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell)

TL;DR

This paper demonstrates how equational reasoning, a key feature of functional programming, can be integrated directly into Haskell and verified with Liquid Haskell, making formal proofs accessible within the language.

Contribution

It introduces a method to perform and check equational proofs directly in Haskell using Liquid Haskell, bridging the gap between manual reasoning and formal verification.

Findings

Equational proofs can be embedded and verified within Haskell.

Liquid Haskell effectively checks the correctness of equational reasoning.

Proofs in Haskell resemble traditional textbook derivations.

Abstract

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how equational reasoning can be performed directly and seamlessly within Haskell itself, and be checked using Liquid Haskell. In particular, language learners --- to whom external theorem provers are out of reach --- can benefit from having their proofs mechanically checked. Concretely, we show how the equational proofs and derivations from Graham's textbook can be recast as proofs in Haskell (spoiler: they look essentially the same).