Higher-order Binding-time Analysis

Kei Davis?

Abstract

The partial evaluation process requires a binding-time analysis. Binding-time 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 first-order 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 higher-order languages. This paper develops such a generalisation: a projection-based abstract interpretation suitable for higher-order binding-time analysis.

Launchbury [Lau91b] has shown that binding-time analysis and strictness analysis are equivalent problems at first order, and for projection-based 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 higher-order projection-based strictness analysis. The principal limitation of our technique is the restriction to monomorphic typing.

1 Introduction

For first-order 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 self-applicable, strongly-typed partial evaluator [Lau91c]. Unfortunately, neither the forward nor backward techniques generalise easily to higher-order languages. A higher-order projection-based backward strictness analysis has been described [DW91]; this paper develops a higherorder forward technique suitable for higher-order 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 first-order non-strict 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 first-order functions). In that development the abstract value of a first-order 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