One of the biggest problems during this work was the lack of research in transforming strict functional languages. This is not without reason: as we have seen in many parts of this work, transformations may have unexpected consequences on termination behaviour and other side effects. It seems that most researchers avoid these somewhat annoying problems in order to focus more on the transformation aspects rather than on these “secondary” issues: they choose lazy languages.
We have to admit that solving at least some of the covered problems in a clean and general way prevented us from covering more interesting fields of automated program transformation in the detail they would have deserved. Still, it seems that the “side effects” caused by our work, the implementation of a partial evaluator that can cope with higher-order functions and side effects easily while allowing many optimisations and retaining a very elegant implementation, was worth the effort. This is even more true if we consider that other important transformations like common sub-expression elimination or functionality for program analysis like termination inference greatly benefit from this approach: “squeezing out” all statically computable parts from a program reveals a huge amount of information that we can exploit. One could imagine, for example, improving an extended version of this system that conducts exception analysis to find places where uncaught exceptions could be raised — an application in the field of software verification rather than transformation. A powerful and correct partial evaluator seems to be useful for much more than “just” partial evaluation.
How powerful is our monadic approach to partial evaluation really? Unfortunately, the tight time constraints and limited scope of this work did not allow us to give a more formal treatment of this approach. Although we have found and presented references to interesting theoretical work on this question (for example []), it would be very important to prove our specific partial evaluator correct. We have mentioned formal tools (e.g. denotational semantics) that might be very helpful for this task. Our design decisions, especially the one to stick as close as possible to a language specification that is formally well-defined ([]), might pay off in future work.
From the developer’s intuitive point of view it seems to be justified to claim that the only limitation of this partial evaluator is termination inference, a generally undecidable problem, and that it performs optimally within this limit. So far, it was not possible to find any counter-example to this claim, and the way the partial evaluator evolved was based on thorough considerations:
If we consider the high level of declarativity in the implementation, it should not be too difficult to come up with a formal treatment of this partial evaluator. This might be interesting future work: as we can learn from e.g. chapter 5.5 and 8.8 in [], partial evaluation of functional programs seems to currently still face many problems, be it side effects, termination of the partial evaluator, linearity constraints for function applications or higher-order functions. We hope that our approach, which is significantly supported by the underlying implementation language LambdaProlog, contributes some solutions to annoying problems in this field. Future work may illuminate more formal aspects.
Besides the correctness issues concerning the partial evaluator, we have also tried to develop suitable criteria that allow safe application of other transformations. It seems that some questions concerning correct application of recursive folding are clearer now: we have identified sum types as crucial aspect and have presented a way which may give a bit more generality in deciding whether recursive folding is safe (see section 4.1.2). It seems that this has not yet been explicitly treated in the literature we know.
This could have been the major point of this thesis, but the idea to use partial evaluation to improve control has lured us away from this topic quite far. It is definitely clear that this aspect is the one which has to be strongly improved before advanced transformations can be applied to real-world problems, in which search space sizes are very often not tractable for our current methods. Our partial evaluator probably adds less to this topic than to others like correctness and transformation itself.
One contribution of this thesis may be seen in the demonstration that moving to a higher-order logic can lead to significant improvements in our application domain: we have hopefully succeeded in convincing the reader of the clarity and conciseness of programs written in the language LambdaProlog. We therefore suggest that this language be more widely applied, especially in the field of program transformation.
Monads as implementation technique have been gaining quite some momentum in functional languages and have been successfully applied to many very diverse problems. It seems likely that they may have a similar success in higher-order logic languages: we can hardly imagine how to “beat” the clarity and conciseness of the monadic approach that lead to our implementation of the partial evaluator — taking out only a single clause would seem to make it inherently incomplete. It should be noted that several other approaches had been tried by us before, but none came only close to the current solution. This big step forward gives us confidence that this implementation technique may be highly beneficial in many more cases.
Having given a broad overview of various transformation techniques, there should be plenty of ideas that the reader may try out in our transformation framework: on the practical side the fold/unfold strategy is surely a worthy candidate for implementation. But also theoretical work, especially what concerns correctness proofs and improvements in controlling search, could help make this framework even better.
Due to the size of the topic, it was not possible to cover alternative approaches to program transformation in any detail. We would like to point out two publications which seem to go fundamentally different ways to automated transformation than we have described so far. The interested reader may therefore consider [] and []. The first publication approaches program transformations from the field of rewrite rules and completion techniques. The second one takes up the idea of attribute grammars to transforming declarative programs.
Who knows, the answer to many of our questions may be found in approaches that we have considered least promising so far…