Type Specialisation for the Lambda-Calculus; or, A New Paradigm for Partial Evaluation based on Type Inference.

Abstract

We present a new paradigm for partial evaluation, inspired by type inference. Our partial evaluator is specified in terms of specialisation rules that prescribe how a source expression and type should be transformed into a residual expression and type. Static information is represented in the residual types, in contrast to traditional partial evaluators which effectively represent it in the transformed expression. Thus we break the link between staticness and unfolding: a variable can be static even if the specialiser does not substitute a value for it; static information is propagated by unification, not by substitution. As a result we obtain better static information flow, and consequently stronger specialisation, than traditional partial evaluators.

Our specialiser is very modular: each specialisation feature is tied to a particular type in the source language, with associated introduction and elimination rules. Each feature is specified independently, and features can be combined in arbitrary ways. This has led to a number of new results:

We can perform type specialisation --- there is no reason to expect source and residual types to be the same. Ours is the first specialiser which can obtain an arbitrary type in the residual program by specialising one universal type in the source program.
Dynamic functions can take partially static arguments and return partially static results; this is the key to optimal specialisation of typed programs, where the static information represents type information. Ours is the first optimal specialiser for a typed, higher-order language.
Ours is the first specialiser to support both higher-order functions and constructor specialisation. This combination is powerful: we can obtain closure analysis and firstification as a simple application.

Finally, although we describe our approach in terms of the lambda-calculus, the basic idea is quite general. Similar results should be obtainable for other typed languages, including imperative ones.

The paper is available here.