posted on 2022-03-29, 03:51authored byMatthew 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.
History
Table of Contents
1. Introduction -- 2. Generic functions -- 3. Encoding generic functions -- 4. A baseline functional language compiler -- 5. Compiling and typing polymorphic functions with specific behaviour -- 6. Compiling and typing structure agnosticism -- 7. Evaluating expressiveness -- 8. Evaluating compilation -- 9. Evaluating the type system -- 10. Conclusion.
Notes
This dissertation is presented for the degree of Doctor of Philosophy".
"March 2011
Bibliography: pages 183-190
Awarding Institution
Macquarie University
Degree Type
Thesis PhD
Degree
PhD, Macquarie University, Faculty of Science, Department of Computing
Department, Centre or School
Department of Computing
Year of Award
2011
Principal Supervisor
Dominic Verity
Additional Supervisor 1
Tony Sloane
Rights
Copyright disclaimer: http://www.copyright.mq.edu.au
Copyright Matthew Roberts 2011.