Consolidation of Haskell Programs

Semantic Fusion of maps, filters and folds

Alberto Sadde
Department of Computer Science, University of Oxford
Paper (pdf) Hackage Survey Source Code

Program consolidation is a recent, correct-by-construction program optimization calculus that exploits semantic relations between terms in multiple programs to obtain a consolidated program that is sound optimization of the sequential execution of the original programs. Inspired by its success in the imperative setting, where the focus is on domain-specific languages without side effects, in this paper we explore its applicability in the setting of a functional language. Motivated by the latest developments in logical verification for Haskell such as refinement types, we present our consolidation theory as a set of inference rules annotated with semantic information. Furthermore, following the renewed interest in improvement theory, an operational theory that aims to bring rigour to efficiency improvement proofs, we present a cost-annotated operational semantics for a call-by-value lambda calculus that we use to formally show that the consolidation rules, when applicable, yield efficiency improvements. We also present the results of a survey of the Haskell ecosystem and a series of benchmarks that show that exploiting semantic dependencies between inputs is a viable direction to optimise performance and memory consumption of a broad range of functional programs.