Implementations of lazy functional languages ensure that computations are performed only when they are needed, and save the results so that they are not repeated. This frees the programmer to describe solutions at a high level, leaving details of control flow to the compiler. This freedom however places a heavy burden on the compiler; measurements show that over 70% of these saved results are never used again. A usage analysis that could statically detect values used at most once would enable these wasted updates to be avoided, and would be of great benefit. However, existing usage analyses either give poor results or have been applied only to prototype compilers or toy languages.
This thesis presents a sound, practical, type-based usage analysis that copes with all the language features of a modern functional language, including type polymorphism and user-defined algebraic data types, and addresses a range of problems that have caused difficulty for previous analyses, including poisoning, mutual recursion, separate compilation, and partial application and usage dependencies. In addition to well-typing rules, an inference algorithm is developed, with proofs of soundness and a complexity analysis.
In the process, the thesis develops simple polymorphism, a novel approach to polymorphism in the presence of subtyping that attempts to strike a balance between pragmatic concerns and expressive power. This thesis may be considered an extended experiment into this approach, worked out in some detail but not yet conclusive.
The analysis described was designed in parallel with a full implementation in the Glasgow Haskell Compiler, leading to informed design choices, thorough coverage of language features, and accurate measurements of its potential and effectiveness when used on real code. The latter demonstrate that the analysis yields moderate benefit in practice.
We present a novel inference algorithm for a type system featuring subtyping and usage (annotation) polymorphism. This algorithm infers simply-polymorphic types rather than the constrained-polymorphic types usual in such a setting; it achieves this by means of constraint approximation. The algorithm is motivated by practical considerations and experience of a previous system, and has been implemented in a production compiler with positive results. We believe the algorithm may well have applications in settings other than usage-type inference.
We present a sound type-based `usage analysis' for a realistic lazy functional language. Accurate information on the usage of program subexpressions in a lazy functional language permits a compiler to perform a number of useful optimisations. However, existing analyses are either ad-hoc and approximate, or defined over restricted languages.
Our work extends the Once Upon A Type system of Turner, Mossin, and Wadler (FPCA'95). Firstly, we add type polymorphism, an essential feature of typed functional programming languages. Secondly, we include general Haskell-style user-defined algebraic data types. Thirdly, we explain and solve the `poisoning problem', which causes the earlier analysis to yield poor results. Interesting design choices turn up in each of these areas.
Our analysis is sound with respect to a Launchbury-style operational semantics, and it is straightforward to implement. Good results have been obtained from a prototype implementation, and we intend to integrate the system into a production compiler.
Slides: Conference talk, longer talk,