Type-directed partial evaluation

Publisher Website
Google Scholar
Abstract
We present a strikingly simple partial evaluator, that is type-directed and rei es a compiled program into the text of a re-sidual, specialized program. Our partial evaluator is concise (a few lines) and it handles the agship examples of o-line monovariant partial evaluation. Its source programs are constrained in two ways: they must be closed and mono-morphically typable. Thus dynamic free variables need to be factored out in a \dynamic initial environment". Type-directed partial evaluation uses no symbolic evaluation for specialization, and naturally processes static computational e ects. Our partial evaluator is the part of an o ine partial eval-uator that residualizes static values in dynamic contexts. Its restriction to the simply typed lambda-calculus coincides with Berger and Schwichtenberg's \inverse of the evaluation functional" (LICS'91), which is an instance of normalization in a logical setting. As such, type-directed partial evaluation essentially achieves lambda-calculus normalization. We ex-tend it to produce specialized programs that are recursive and that use disjoint sums and computational e ects. We also analyze its limitations: foremost, it does not handle in-ductive types. This paper therefore bridges partial evaluation and-calculus normalization through higher-order abstract syn-tax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler op-timization, and run-time code generation (including decom-pilation). It also o ers a simple solution to denotational semantics-based compilation and compiler generation.

This publication has 0 references indexed in Scilit: