Compiled generics for functional programming languages
thesisposted on 29.03.2022, 03:51 authored by Matthew Roberts
"We address the problem of extending existing functional language compilers to support generic programming constructs, such as those that arise in term rewriting and datatype generic programs. In particular, we present a compiler capable of compiling a wide range of generic programs in a way which substantially reduces the execution overhead traditionally associated with such programs, without requiring type classes. We explicitly build upon a baseline functional compiler by extending it to support a universal spine view of data and by adding a mechanism for building polymorphic functions from monomorphic ones. This work employs variants of standard pattern compilation and lambda lifting translations that render these generic extensions into efficient code while making only modest modifications to our baseline compiler and its run-time. We show that type inference (with annotations for higher-ranked types and polymorphic recursion) can be maintained, by building all the mechanisms needed for type inference of generic programs on top of an existing variant of Damas and Milner's algorithm W. We demonstrate that this compiler achieves type safe and efficient compiled generic programs by showing the breadth of generic programs that we can encode with it and by benchmarking the execution speed and memory use of the programs output by the compiler. The generic programs we demonstrate are generic transformations, generic queries, generic traversals, generic equality, generic show plus a large number of variants of these. We also provide a proof of the soundness of the type system which underpins the compiler. In summary, the primary outcome of this research is a new compiler for generic programs which uses a unique combination of encoding techniques and which generates efficient generic code. For each of our extensions (polymorphic functions with specific behaviour and the explicit spine view) we provide new algorithms for pattern compilation, type inference and conversion to primitive operations. These can be easily incorporated into existing functional language compilers.