Eta-Expansion Does The Trick

Olivier Danvy, Karoline Malmkjær, Jens Palsberg

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearch


    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' partial evaluator for the &lgr;-calculus, &lgr;-Mix, with products and disjoint sums; we point out how eta-expansion for (finite) disjoint sums enable The Trick; we generalize our earlier work by identifying the eta-expansion can be obtained in the binding-time analysis simple by adding two coercion rules; and we specify and prove the correctness of our extension to &lgr;-Mix.
    Original languageEnglish
    Book seriesB R I C S Report Series
    Number of pages29
    Publication statusPublished - 1996


    Dive into the research topics of 'Eta-Expansion Does The Trick'. Together they form a unique fingerprint.

    Cite this