Projection Factorisations in Partial Evaluation

[摘要] Partial evaluation is becoming ever more promising as a programming tool. Early partial evaluators depended over much on the source program being written in a particular style, and needed certain ad hoc optimisations to produce good results. The practice of partial evaluation is now fairly well developed but the theoretical underpinnings are not equally well understood. A partial evaluator takes a program, together with some of the input to the program, and produces a new program. This new, or residual, program is an optimised version of the old, having taken the input data into account. Work undertaken at DIKU in Copenhagen has shown the importance of prior analysis of the program. This binding-time analysis discovers which values within the program may bo computed during partial evaluation-called static values and which values may not the dynamic values. In this thesis we propose using domain projections in binding-time analysis. This allows a greater level of data separation than before because values are no longer treated atomically. In particular, we are able to pinpoint static values within data structures containing both static and dynamic parts. An interesting consequence of using domain projections is that we are able to demonstrate an intimate relationship between binding-time analysis and strictness analysis. Dependent sum and product are familiar from constructive type theory. We give a less familiar domain-theoretic definition and show how projections determine particular dependent sums. The practical application of this result is to generate residual functions whose types depend on the static values from which they wore produced. Certain optimising techniques, such as tag removal and arity raising, arise as a direct, consequence. We extend the use of projections to polymorphic programs, giving a practical application of developments in the theory of polymorphism. Polymorphic functions are regarded as natural transformations between appropriate functors. This leads to three benefits: polymorphic functions are analysed once and the result reused; the static input to polymorphic functions is described by polymorphic projections, which reduces the search space of the analysis; and polymorphic functions are specialised to polymorphic values, leading to polymorphic residual functions.

[发布机构] University:University of Glasgow

[关键词] Computer science