Eta-Expansion Does The Trick (Revised Version)

  • Olivier Danvy
  • Karoline Malmkjær
  • Jens Palsberg

Abstract

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": nonstandard 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 nonstandard 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 article, we extend Gomard and Jones's partial evaluator
for the lambda-calculus, lambda-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 lambda-Mix.


Keywords: Partial evaluation, binding-time analysis, program specialization,
binding-time improvement, eta-expansion, static reduction.

Published
1996-01-17
How to Cite
Danvy, O., Malmkjær, K., & Palsberg, J. (1996). Eta-Expansion Does The Trick (Revised Version). BRICS Report Series, 3(17). https://doi.org/10.7146/brics.v3i17.19979