Olivier Danvy
ABSTRACT
We present a strikingly simple partial evaluator, that is type-directed and reifies a compiled program into the text of a residual, specialized program. Our partial evaluator is concise (a few lines) and it handles the flagship examples of offline monovariant partial evaluation. Its source programs are constrained in two ways: they must be closed and monomorphically typable. Thus dynamic free variables need to be factored out in a "dynamic initial environment". Type-directed partial evaluation uses no symbolic evaluation for specialization, and naturally processes static computational effects.Our partial evaluator is the part of an offline partial evaluator that residualizes static values in dynamic contexts. Its restriction to the simply typed lambda-calculus coincides with Berger and Schwichtenberg's "inverse of the evaluation functional" (LICS'91), which is an instance of normalization in a logical setting. As such, type-directed partial evaluation essentially achieves lambda-calculus normalization. We extend it to produce specialized programs that are recursive and that use disjoint sums and computational effects. We also analyze its limitations: foremost, it does not handle inductive types.This paper therefore bridges partial evaluation and λ-calculus normalization through higher-order abstract syntax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler optimization, and rut-time code generation (including decompilation). It also offers a simple solution to denotational semantics-based compilation and compiler generation.
- 1.Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free reduction proof. In Peter Dybjer and Randy Pollack, editors, Informal Proceedings of the Joint CLICS- TYPES Workshop on Categomes and Type Theory, Ggteborg, Sweden, May 1995. Report 85, Programming Methodology Group, Chalmers University and the University of GSteborg. Google Scholar
Digital Library
- 2.Henk Barendregt. The Lambda Calculus Its Syntax and Semantics. North-Holland, 1984.Google Scholar
- 3.Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed )#-calculus. In Proceedings of the S#xth Annual IEEE Symposium on Logic in Computer Science, pages 203-2tl, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press.Google ScholarCross Ref
- 4.Lars Birkedal and Morten Welinder. Partial evaluation of Standard ML. Master's thesis, D1KU, Computer Science Department, University of Copenhagen, August 1993. DIKU report 93/22.Google Scholar
- 5.Hans-J. Boehm, editor. Proceedings of the Twenty- F#rst Annual A CM Symposium on Pmnciples of Programmzng Languages, Portland, Oregon, January 1994. ACM Press. Google Scholar
- 6.Anders Bondorf. Self-Applicable Partial Evaluation. PhD thesis, DtKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, 1990. DIKU Report 90-17.Google Scholar
- 7.Anders Bondorf. Improving binding times without explicit cps-conversion. In William Clinger, editor, Proceed#ngs of the 1992 A CM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 1-10, San Francisco, California, June 1992. ACM Press. Google ScholarDigital Library
- 8.Anders Bondorf and Olivier Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming, 16:151-195, 1991. Google ScholarDigital Library
- 9.Anders Bondorf and Jesper Jorgensen. Efficient analyses for realistic off-line partial evaluation. Journal of Functional Programming, 3(3):315-346, 1993.Google ScholarCross Ref
- 10.William Clinger and Jonathan Rees (editors). Revisecl4 report on the algorithmic language Scheme. LISP Poznters, IV(3):1-55, July-September 1991. Google ScholarDigital Library
- 11.Charles Consel. Analyse de Programmes, Evaluation Partielle et Gdndrat#on de Comp#lateurs. PhD thesis, Universit# Pierre et Marie Curie (Paris VI), Paris, France, June 1989.Google Scholar
- 12.Charles Consel. Polyvariant binding-time analysis for applicative languages. In David A. Schmidt, editor, Proceedings of the Second A CM SIGPLAN S#mpos:um on Partial Evaluation and Semantics-Based Program Manipulatzon, pages 66-77, Copenhagen, Denmark, June 1993. ACM Press. Google ScholarDigital Library
- 13.Charles Consel and Olivier Danvy. From interpreting to compiling binding times. In Neil D. Jones, editor, Proceedings of the Third European Symposium on Programmzng, number 432 in Lecture Notes in Computer Science, pages 88-105, Copenhagen, Denmark, May 1990. Google ScholarDigital Library
- 14.Charles Consel and Olivier Danvy. Static and dynamic semantics processing. In Robert (Corky) Cartwright, editor, Procee&ngs of the Eighteenth Annual A CM Symposium on Principles o} Programming Languages, pages 14-24, Orlando, Florida, January 1991. ACM Press. Google ScholarDigital Library
- 15.Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual A CM Symposium on Principles of Programming Languages, pages 493-501, Charleston, South Carolina, January 1993. ACM Press. Google ScholarDigital Library
- 16.Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 A CM Conference on L#sp and Functional Programming, pages 151-160, Nice, France, June 1990. ACM Press. Google ScholarDigital Library
- 17.Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361-391, December 1992.Google ScholarCross Ref
- 18.Olivier Danvy, Karoline Malmkjaer, and Jens Palsberg. The essence of eta-expansion in partial evaluation. LISP and Symbohc Computation, 8(3):209-227, 1995. An earlier version appeared in the proceedings of the 1994 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. Google ScholarDigital Library
- 19.Olivier Danvy, Karoline Malmkjaer, and Jens Palsberg. Eta-expansion does The Trick. Technical report BRICS RS-95-41, DAIMI, Computer Science Department, Aarhus University, Aarhus, Denmark, August 1995.Google Scholar
- 20.Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Guy L. Steele Jr., editor, Proceed#ngs of the Twenty-Third Annual A CM Symposium on Princzples of Programming Languages, St. Petersburg Beach, Florida, January 1996. ACM Press. Google ScholarDigital Library
- 21.Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and Peter Mager, editors, Proceedings of the Fifteenth Annual A CM Symposium on Principles of Programming Languages, pages 180- 190, San Diego, California, January 1988. Google ScholarDigital Library
- 22.Andrzej Filinski. Representing monads. In Boehm {5}, pages 446-457. Google ScholarDigital Library
- 23.Andrzej FiIinski. Controlling Effects. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, 1995.Google Scholar
- 24.Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essenhals of Programming Languages. The MIT Press and McGraw-Hill, 1991. Google ScholarDigital Library
- 25.Yoshihito Futamura. Partial evaluation of computation process - an approach to a compiler-compiler. Systems, Computers, Controls 2, 5, pages 45-50, 1971.Google Scholar
- 26.Robert Glfick and Jesper J0rgensen. Efficient multilevel generating extensions for program specialization. In S. D. Swierstra and M. Hermenegildo, editors, Seventh International Symposium on Programming Language Implementation and Logic Programming, number 982 in Lecture Notes in Computer Science, p#ges 259- 278, Utrecht, The Netherlands, September 1995. Google ScholarDigital Library
- 27.Mayer Goldberg. Recursive Apphcation Survival #n the A-Calculus. PhD thesis, Computer Science Department, Indiana lIniversity, Bloomington, Indiana, 1996. Forthcoming. Google ScholarDigital Library
- 28.John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Boehm {5}, pages 458- 471. Google ScholarDigital Library
- 29.Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming, 22(3):197-230, 1993. Special Issue on ESOP'92, the Fourth European Symposium on Programming, Rennes, February 1992. Google ScholarDigital Library
- 30.G#rard Huet. R#solution d'fiquations dans les tangages d'ordre 1, 2, .., w. Th#se d't#tat, Universit# de Paris VII, Paris, France, 1976.Google Scholar
- 31.C. Barry Jay and Neil Ghani. The virtues of eta-expansion. Journal of Functional Programming, 5(3):135- 154, 1995.Google Scholar
- 32.Neil D. Jones, editor. Semant, cs-D,rected Compiler Generation, number 94 in Lecture Notes in Computer Science, Aarhus, Denmark, 1980.Google Scholar
- 33.Nell D. Jones. Challenging problems in partial evaluation and mixed computation. In Partial Evaluation and M,xed Computation, pages 1-14. North-Holland, 1988.Google Scholar
- 34.Neil D. Jones. Mix ten years after. In William L. Scherlis, editor, Proceedzngs o} the A CM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 24-38, La Jolla, California, June 1995. Google ScholarDigital Library
- 35.Neil D. Jones, Carsten K. Gomard, Anders Bondorf, Olivier Danvy, and Torben #. Mogensen. A selfapplicable partial evaluator for the lambda calculus. In K. C. Tai and Alexander L. Wolf, editors, Proceedings of the 1990 IEEE International Conference on Computer Languages, pages 49-58, New Orleans, Louisiana, March 1990.Google ScholarCross Ref
- 36.Nell D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall International Series in Computer Science. Prentice-Hall, 1993. Google ScholarDigital Library
- 37.John Launchbury. Projectzon Factorisations #n Part#at Evaluation. Distinguished Dissertations in Computer Science. Cambridge University Press, 1991. Google ScholarDigital Library
- 38.Julia L. Lawall and Olivier Danvy. Continuationbased partial evaluation. In Carolyn L. Talcott, editor, Proceedings of the 199# A CM Conference on L#sp and Functional Programming, LISP Pointers, Vol. VII, No. 3, Orlando, Florida, June 1994. ACM Press. Google ScholarDigital Library
- 39.Ralph Loader. Normalisation by translation. Technical report, Computing Laboratory, Oxford University, April 1995.Google Scholar
- 40.Karoline Malmkjaer, Nevin Heintze, and Olivier Danvy. ML partial evaluation using set-based analysis. In John Reppy. editor, Record of the 199# A CM SIG- PLAN Workshop on ML and its Apphcat#ons, Rapport de recherche N~ 2265, INR{A, pages 112-119, Orlando, Florida, June 1994. Also appears as Technical report CMU-CS-94-129.Google Scholar
- 41.Torben }E. Mogensen. B#nding Time Aspects of Part, al Evatuat,on. PhD thesis, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, March 1989.Google Scholar
- 42.Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55-92, 199t. Google ScholarDigital Library
- 43.Peter D. Mosses. SIS -- semantics implementation system, reference manual and user guide. Technical Report MD-30, DAIMI, Computer Science Department, Aarhus University, Aarhus, Denmark, 1979.Google Scholar
- 44.Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992. Google ScholarDigital Library
- 45.Larry Paulson. Compiler generation from denotational semantics. In Bernard Lorho, editor, Methods and Tools for Compiler Construction, pages 219-250. Cambridge University Press, t984. Google ScholarDigital Library
- 46.Frank Pfenning. Logic programming in the LF logical framework. In G#rard Huet and Gordon Plotkin, editors, Logical _Frameworks, pages 149-181. Cambridge University Press, 1991. Google ScholarDigital Library
- 47.John C. Reynolds. The essence of Algol. In van Vliet, editor, International Symposium on Algorithmic Languages, pages 345-372, Amsterdam, 1982. North- Holland.Google Scholar
- 48.Erik Ruf. Topics in Online Partial Evaluation. PhD thesis, Stanford University, Stanford, California, February 1993. Technical report CSL-TR-93-563. Google ScholarDigital Library
- 49.Guy L. Steele Jr. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978. Google ScholarDigital Library
- 50.Philip Wadter. The essence of functional programming (tutorial). In Andrew W. Appel, editor, Proceedings of the Nineteenth Annual A CM Symposium on Principles of Programming Languages, pages 1-14, Albuquerque, New Mexico, January 1992. ACM Press. Google ScholarDigital Library
- 51.Daniel Weise, Roland Conybeare, Erik Ruf, and Score Seligman. Aueomatic online partial evaluation. In John Hughes, editor, Proceedings of the F#fth A CM Conference on Functional Programming and Computer Architecture, number 523 in Lecture Notes in Computer Science, pages 165-191, Cambridge, Massachusetts, August 1991. Google ScholarDigital Library
Index Terms
- Type-directed partial evaluation
Recommendations
The Second Futamura Projection for Type-Directed Partial Evaluation
A generating extension of a program specializes the program with respect to part of the input. Applying a partial evaluator to the program trivially yields a generating extension, but specializing the partial evaluator with respect to the program often ...
Formalizing a correctness property of a type-directed partial evaluator
PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program VerificationThis paper presents our experience of formalizing Danvy's type-directed partial evaluator (TDPE) for the call-by-name lambda calculus in the proof assistant Coq. Following the previous approach by Coquand and Ilik, we characterize TDPE as a composition ...
The second Futamura projection for type-directed partial evaluation
The second Futamura projection describes the automatic generation of non-trivial generating extensions by applying a partial evaluator to itself. We derive an ML implementation of the second Futamura projection for Type-Directed Partial Evaluation (TDPE)...
Comments