Selective eta-expansion is a powerful ldquobinding-time improvementrdquo,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 interfacingstatic higher-order values in dynamic contexts anddynamic higher-order values in static contexts. They contribute to twodistinct binding-time improvements.
We present two extensions of Gomard's monovariant binding-time analysis for the pure lambda-calculus. Our extensions annotateand 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 ldquocps-basedrdquo partial evaluation.
We also outline the counterpart of eta-expansion for partially static data structures.