LISP and Symbolic Computation, 8(3)209-227
The Essence of Eta-Expansion in Partial EvaluationOlivier Danvy, Computer Science Department, Aarhus University, Ny Munkegade, DK-8000 Aarhus C, Denmark
Karoline Malmkjær, Computer Science Department, Aarhus University, Ny Munkegade, DK-8000 Aarhus C, Denmark
Jens Palsberg, Computer Science Department, Aarhus University, Ny Munkegade, DK-8000 Aarhus C, Denmark
|
Abstract: Selective eta-expansion is a powerful "binding-time
improvement", i.e., a source-program modification that makes a partial
evaluator yield better results. But like most binding-time
improvements, the exact problem it solves and the reason why have not
been formalized and are only understood by few. In this paper, we describe the problem and the effect of eta-redexes in terms of monovariant binding-time propagation: eta-redexes preserve the static data flow of a source program by interfacing static higher-order values in dynamic contexts and dynamic higher-order values in static contexts. They contribute to two distinct binding-time improvements. We present two extensions of Gomard's monovariant binding-time analysis for the pure lambda-calculus. Our extensions annotate and eta-expand lambda-terms. The first one eta-expands static higher-order values in dynamic contexts. The second also eta-expands dynamic higher-order values in static contexts. As a significant application, we show that our first binding-time analysis suffices to reformulate the traditional formulation of a CPS transformation into a modern one-pass CPS transformer. This binding-time improvement is known, but it is still left unexplained in contemporary literature, e.g., about "cps-based" partial evaluation. We also outline the counterpart of eta-expansion for partially static data structures. Keywords: two-level lambda-calculus, binding-time analysis, coercions |
[local copy]
![[picture of journal cover]](../LISP.JPG)