Theory and practice of shortcut fusion

Thesis

There are a number of approaches for eliminating intermediate data structures in functional programs by rewriting a composition of recursive functions as a single recursive function. Such a transformation is called fusion. One such approach is to encapsulate a structured recursion scheme in two combinators for consumption and production of data, and use algebraic transformations to rewrite these where possible, letting local compiler optimisations fuse the remaining nonrecursive portions of the program. This approach is called shortcut fusion, which has been implemented using various recursion schemes in the programming language Haskell. Despite their obvious similarities, however, the relationship between these techniques has not been formalised.

In this thesis, three techniques, chosen for their success in practical applications and prominence in previous literature, are analysed. Their relationship is examined on three different levels: theory, practice, and pragmatics. Theoretically, the relationship between their underlying recursion schemes is examined. In the right setting, it is possible to compare them side-by-side, which makes clearer their differences in expressibility as well as the foundations for their correctness. On the practical level, the similarities in their implementations in Haskell can be generalised using the concept of data abstraction, and a general semantic framework is developed for shortcut fusion without reference to a specific recursion scheme. Finally, the pragmatics of these techniques are investigated, and it turns out that the these, too, are not dependent on the specific technique used.

The results from this analysis demonstrate that shortcut fusion is actually a single program transformation, defined by a general semantic framework that can be instantiated for a variety of recursion schemes. Furthermore, it is possible to use this information to create a declarative infrastructure for implementing shortcut fusion within a compiler. This results in a more robust program transformation that is less complicated to implement than before.

Authors: Harper, T

• DOI: 10.5287/ora-dezynp9n2
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: compiler optimisation; proof obligation; fusion; haskell; natural transformation
• Subjects: Functional programming (Computer science); Functional programming languages