Eta-expansion does The Trick

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' 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.

REFERENCES

• 1: J. Michael Ashley , Charles Consel, Fixpoint computation for polyvariant static analyses of higher-order applicative programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1431-1448, Sept. 1994 [doi>10.1145/186025.186037]
• 2: BARENDREGT, H. 1984. The Lambda Calculus Its Syntax and Semantics. North-Holland, Amsterdam, The Netherlands.
• 3: BERGER, W. AND SCHWICHTENBERG, H. 1991. An inverse of the evaluation functional for typed ~-calculus. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alomitos, Calif., 203-211.
• 4: Anders Bondorf, Automatic autoprojection of higher order recursive equations, Science of Computer Programming, v.17 n.1-3, p.3-34, Dec. 1991
• 5: Anders Bondorf, Improving binding times without explicit CPS-conversion, Proceedings of the 1992 ACM conference on LISP and functional programming, p.1-10, June 22-24, 1992, San Francisco, California, United States
• 6: Anders Bondorf , Olivier Danvy, Automatic autoprojection of recursive equations with global variable and abstract data types, Science of Computer Programming, v.16 n.2, p.151-195, Sept. 1991 [doi>10.1016/0167-6423(91)90002-F]
• 7: H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams, IV , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand , William Clinger , Jonathan Rees, Revised report on the algorithmic language scheme, ACM SIGPLAN Lisp Pointers, v.IV n.3, p.1-55, July, 1991 [doi>10.1145/382130.382133]
• 8: Charles Consel, Polyvariant binding-time analysis for applicative languages, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.66-77, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154638]
• 9: Charles Consel, A tour of Schism: a partial evaluation system for higher-order applicative languages, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.145-154, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154645]
• 10: Charles Consel , Olivier Danvy, For a better support of static data flow, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.496-519, June 1991, Cambridge, Massachusetts, United States
• 11: Charles Consel , Olivier Danvy, Tutorial notes on partial evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.493-501, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158707]
• 12: Olivier Danvy, Type-directed partial evaluation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.242-257, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237784]
• 13: Olivier Danvy , Andrzej Filinski, Abstracting control, Proceedings of the 1990 ACM conference on LISP and functional programming, p.151-160, June 27-29, 1990, Nice, France [doi>10.1145/91556.91622]
• 14: Olivier Danvy , Karoline Malmkjær , Jens Palsberg, The essence of eta-expansion in partial evaluation, Lisp and Symbolic Computation, v.8 n.3, p.209-227, Sept. 1995 [doi>10.1007/BF01019004]
• 15: Dirk Dussart , Fritz Henglein , Christian Mossin, Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time, Proceedings of the Second International Symposium on Static Analysis, p.118-135, September 25-27, 1995
• 16: Carsten K. Gomard, A self-applicable partial evaluator for the lambda calculus: correctness and pragmatics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.2, p.147-172, April 1992 [doi>10.1145/128861.128864]
• 17: GOMARD, C. K. AND JONES, N. D. 1991. A partial evaluator for the untyped lambda-calculus. J. Funct. Program. 1, 1, 21-69.
• 18: Nevin Charles Heintze, Set based program analysis, Carnegie Mellon University, Pittsburgh, PA, 1992
• 19: Fritz Henglein, Dynamic typing: syntax and proof theory, Science of Computer Programming, v.22 n.3, p.197-230, June 1994
• 20: HOLST, C. K. AND HUGHES, J. 1990. Towards binding-time improvement for free. In Functional Programming, Glasgow 1990, S. L. Peyton Jones, G. Hutton, and C. K. Hoist, Eds. Springer- Verlag, Berlin, 83-100.
• 21: JONES, N. D. 1988. Automatic program specialization: A re-examination from basic principles. In Partial Evaluation and Mimed Computation, D. Bjorner, A. P. Ershov, and N. D. Jones, Eds. North-Holland, Amsterdam, The Netherlands, 225-282.
• 22: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 23: JONES, N. D., SESTOFT, P., AND SONDERGAARD, H. 1989. MIX: A self-applicable partial evaluator for experiments in compiler generation. LISP Symbol. Comput. 2, 1, 9-50.
• 24: Julia L. Lawall , Olivier Danvy, Continuation-based partial evaluation, Proceedings of the 1994 ACM conference on LISP and functional programming, p.227-238, June 27-29, 1994, Orlando, Florida, United States
• 25: Julia L. Lawall , Olivier Danvy, Continuation-based partial evaluation, Proceedings of the 1994 ACM conference on LISP and functional programming, p.227-238, June 27-29, 1994, Orlando, Florida, United States
• 26: Karoline Malmkjær, Towards efficient partial evaluation, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.33-43, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154634]
• 27: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 28: Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
• 29: PALSBERG, J. 1993. Correctness of binding-time analysis. J. Funct. Program. 3, 3 (July}, 347-363.
• 30: Christine Paulin-Mohring , Benjamin Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, v.15 n.5-6, p.607-640, May/June 1993 [doi>10.1016/S0747-7171(06)80007-6]
• 31: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 32: REYNOLDS, J. C. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83, R. E. A. Mason, Ed. IFIP, Montvale, N.J., 513-523.
• 33: Erik Steven Ruf, Topics in online partial evaluation, Stanford University, Stanford, CA, 1993
• 34: Peter Sestoft, Replacing function parameters by global variables, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.39-53, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99374]
• 35: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 36: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]
• 37: WAND, M. 1993. Specifying the correctness of binding-time analysis. J. Funct. Program. 3, 3 (July), 365-387.
• 38: Daniel Weise , Roland Conybeare , Erik Ruf , Scott Seligman, Automatic online partial evaluation, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.165-191, June 1991, Cambridge, Massachusetts, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Evaluation strategies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Automatic analysis of algorithms

General Terms:
Languages, Theory

Keywords:
binding-time analysis and improvement, eta-expansion, partial evaluation, program specialization, static reduction