When writing a program, especially in a high level language such as Haskell, the programmer is faced with a tension between abstraction and efficiency. A program that is easy to understand often fails to be efficient, while a more efficient solution often compromises clarity. Fortunately Haskell permits us to reason about programs, so that we can start out with a program that is clear but inefficient, and transform it into a program that is efficient, but perhaps less readable. Indeed, such a transformational style of programming is as old as the subject of functional programming itself. Programs developed in this style continue to suffer from a lack of readability, however: typically a functional programmer will develop his program on the back of an envelope, and only record the final result in his code. Of course he could document his ideas in comments, but as we all know, this is rarely done. Furthermore, when the programmer finds himself in a similar situation, using the same technique to develop a new piece of code, there is no way he can reuse the development recorded as a comment. We claim that there is a handful of techniques that functional programmers routinely use to transform their programs, and that these techniques can themselves be coded as meta programs, allowing one to reuse the same optimisation technique on different pieces of code. In these lectures we shall explore this claim, and ways in which such meta programs might be implemented. The structure of these notes is as follows. We first discuss three motivating examples, to clarify what type of optimisation we have in mind, and how an inefficient program might be annotated with transformations that effect the optimisation. Next, we discuss how the application of transformations can be mechanised. Our main design decision at this point is that transformations are never applied backwards. These ideas are then put to practice in a series of practical assignments, with a toy transformation system especially developed to accompany these notes. Finally, we discuss the matching problem in some detail, and explain how we have chosen to circumvent the undecidability inherent in matching of λ-terms. Throughout, we shall take a cavalier attitude towards semantics. In particular, we have chosen to ignore all issues of strictness: some of our transformation rules ought to state side conditions about strictness. While it is admittedly incorrect to ignore such side conditions, they would clutter the presentation and detract from the main thesis of these lectures.
展开▼
