Foundations of Haskell’s Rewrite Rules Based on Higher-Kinded Polymorphic Rewrite Systems

The aim of this paper is to establish theoretical foundations of GHC’s rewrite rules. The Glasgow Haskell Compiler (GHC) has the feature of rewrite rules to specify optimising transformations. Rewrite rules have been widely used in many libraries. However, there has been no theory to formalise the rules and establish their correctness. We present System \(\textrm{F}_\textrm{RE}\) —the polymorphic \({\lambda }\) -calculus System \(\textrm{F}_\omega \) extended with higher-order term rewriting and equational reasoning to model GHC’s rewrite rules. We develop a theory and methods for verifying correctness of rewrite rules. The key to our method is to guarantee the rewriting properties of local confluence and strong normalisation. We prove the Rule Meaning Preservation Theorem that gives a simple criterion for establishing correctness of rewrite rules, which is suited for mechanical checking.