Binding-time analysis for polymorphic types

Abstract

Offline partial evaluators specialise programs with annotations which distinguish specialisation-time (or static) computations from run-time ones. These annotations are generated by a binding-time analyser, via type inference in a suitable type-system. Henglein and Mossin developed a type system which allows polymorphism in binding-times, so that the same code can be specialised with different computations being static at different uses. We extend their work to permit polymorphism in types as well. This is particularly important for separately compiled libraries. Following Henglein and Mossin, binding-times are passed as parameters during specialisation, but types are not. Instead, we pass coercion functions when necessary, which makes specialisation less "interpretive" than it would otherwise be. We keep track of the coercions needed by assigning qualified types to polymorphic functions. We also consider hand-annotations to provide limited user control over the binding-time analysis, which our prototype implementation showed to be necessary. © Springer-Verlag Berlin Heidelberg 2001.