The HERMIT in the tree: Mechanizing program transformations in the GHC core language

Abstract. This paper describes our experience using the HERMIT tool-kit to apply well-known transformations to the internal core language of the Glasgow Haskell Compiler. HERMIT provides several mechanisms to support writing general-purpose transformations: a domain-specific lan-guage for strategic programming specialized to GHC’s core language, a library of primitive rewrites, and a shell-style–based scripting language for interactive and batch usage. There are many program transformation techniques that have been de-scribed in the literature but have not been mechanized and made avail-able inside GHC — either because they are too specialized to include in a general-purpose compiler, or because the developers ’ interest is in theory rather than implementation. The mechanization process can often reveal pragmatic obstacles that are glossed over in pen-and-paper proofs; under-standing and removing these obstacles is our concern. Using HERMIT, we implement eleven examples of three program transformations, report on our experience, and describe improvements made in the process