
Higherorder Bindingtime Analysis
Kei Davis?
Abstract
The partial evaluation process requires a bindingtime analysis. Bindingtime analysis seeks to determine which parts of a program's result is determined when some part of the input is known. Domain projections provide a very general way to encode a description of which parts of a data structure are static (known), and which are dynamic (not static). For firstorder functional languages Launchbury [Lau91a] has developed an abstract interpretation technique for bindingtime analysis in which the basic abstract value is a projection. Unfortunately this technique does not generalise easily to higherorder languages. This paper develops such a generalisation: a projectionbased abstract interpretation suitable for higherorder bindingtime analysis.
Launchbury [Lau91b] has shown that bindingtime analysis and strictness analysis are equivalent problems at first order, and for projectionbased analyses have exactly the same safety condition. We argue that the same is true at higher order, and hence our development also leads to a higherorder projectionbased strictness analysis. The principal limitation of our technique is the restriction to monomorphic typing.
1 Introduction
For firstorder functional languages there exist both forward and backward abstract interpretation techniques in which the basic abstract value is a projection. Backward techniques [WH87, DW90] are useful for strictness analysis. Forward techniques can also give strictness information [Dav92], but here we are interested in their use for bindingtime analysis in partial evaluation. Launchbury [Lau91a] describes a forward technique which he implemented as part of the first selfapplicable, stronglytyped partial evaluator [Lau91c]. Unfortunately, neither the forward nor backward techniques generalise easily to higherorder languages. A higherorder projectionbased backward strictness analysis has been described [DW91]; this paper develops a higherorder forward technique suitable for higherorder binding
?Computing Science Department, University of Glasgow, Glasgow G12 8QQ, UK, [email protected].
time analysis, and briefly describes how to obtain the backward technique.
A domain projection is a continuous idempotent function that approximates the identity. The projections on a domain form a complete lattice, with the identity ID as the greatest element and the constant bottom function BOT as the least. A projection may be used to encode which components of values (data structures) are static (certainly available) and which are dynamic (possibly unavailable), by acting as the identity on static components and mapping dynamic components to ?. With this interpretation, underestimation (in the usual function ordering) of projections is safe: static objects may be safely regarded as dynamic, but not vice versa.
As a concrete example, let FST (x ; y) = (x ; ?). Then FST encodes the information that the first component of a pair is static and the second dynamic. If SND (x ; y) = (?;y) and swap (x ; y) = (y; x ) then the equation SND ffi swap = swap ffi FST shows that if the first component of the argument to swap is static and the second dynamic, then first component of the result is dynamic and the second static. Bearing in mind that the desired direction of information flow is from function argument to result (forward), and that underestimation is safe, the essence of the problem is, given function f and projection ffi , to find projection such that ffi f v f ffi ffi . More generally, given f we seek to find a function o from projections to projections such that (o ffi) ffi f v f ffi ffi for all ffi . Such a o will be called a projection abstraction of f . The constant BOT function is always a projection abstraction of f , but greater o are more informative; in fact, every continuous function has a greatest (most informative) projection abstraction [Dav92].
In Launchbury's development [Lau91a], an abstract semantics of a firstorder nonstrict functional language is given such that the abstract value of an expression e is a projection abstraction of >=ae:EOE[[ e ]] ae, or just EOE[[ e ]]the standard evaluation function mapping variable environments ae to values (here OE is an environment of firstorder functions). In that development the abstract value of a firstorder function definition is a projection abstraction of its standard value, so that abstract application is composition: in general if of and og are projection abstractions of f and g respectively then of ffi og is a projection abstraction of f ffi g, so the abstract value of EOE[[ f e ]] = OE[[ f ]] ffi EOE[[ e ]] is of ffi oe where of and oe are projection abstractions of OE[[ f ]] and EOE[[ e ]] respectively.
We take the central problem to be to find a projection abstraction of E [[ e ]] via a compositional abstract semantics. Some observations motivate our approach. Firstly, taking