Eta-Expansion Does The Trick (Revised Version)

Olivier Danvy
Karoline Malmkjær
Jens Palsberg

May 1996


Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such ``binding-time improvements'': non-standard use of continuation-passing style, eta-expansion, and a popular transformation called ``The Trick''. We provide a unified view of these binding-time improvements, from a typing perspective.

Just as a proper treatment of product values in partial evaluation requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the non-standard use of continuation-passing style encountered in partial evaluation. Eta-expansion thus acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it enables ``The Trick''.

In this paper, we extend Gomard and Jones's partial evaluator for the tex2html_wrap_inline22 -calculus, tex2html_wrap_inline22 -Mix, with products and disjoint sums; we point out how eta-expansion for (finite) disjoint sums enables The Trick; we generalize our earlier work by identifying that eta-expansion can be obtained in the binding-time analysis simply by adding two coercion rules; and we specify and prove the correctness of our extension to tex2html_wrap_inline22 -Mix.

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.