The second Futamura projection for type-directed partial evaluation

ABSTRACT

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). Due to the differences between `traditional', syntax-directed partial evaluation and TDPE, this derivation involves several conceptual and technical steps. These include a suitable formulation of the second Futamura projection and techniques for using TDPE to specialize type-indexed programs. In the context of the second Futamura projection, we also compare and relate TDPE with conventional offline partial evaluation.

We demonstrate our technique with several examples, including compiler generation for Tiny, a prototypical imperative language.

REFERENCES

• 1: 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]
• 2: Olivier Danvy, Pragmatics of Type-Directed Partial Evaluation, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.73-94, February 12-16, 1996
• 3: Olivier Danvy, A Simple Solution to Type Specialization, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.908-917, July 13-17, 1998
• 4: Olivier Danvy, Type-Directed Partial Evaluation, Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, p.367-411, June 29-July 10, 1998
• 5: O. Danvy and M. Rhiger. Compiling actions by partial evaluation, revisited. Technical Report BRICS-RS-98-13, BRICS, Department of Computer Science, University of Aarhus, 1998.
• 6: Olivier Danvy , René Vestergaard, Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation, Proceedings of the 8th International Symposium on Programming Languages: Implementations, Logics, and Programs, p.182-197, September 24-27, 1996
• 7: Andrzej Filinski, Representing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.446-457, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.178047]
• 8: Andrzej Filinski, A Semantic Account of Type-Directed Partial Evaluation, Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming, p.378-395, September 29-October 01, 1999
• 9: Yoshihiko Futamura, Partial Evaluation of Computation Process—AnApproach to a Compiler-Compiler, Higher-Order and Symbolic Computation, v.12 n.4, p.381-391, December 1999 [doi>10.1023/A:1010095604496 ]
• 10: B. Grobauer and Z. Yang. The second Futamura projection for type-directed partial evaluation. Research Series RS-99- 40, BRICS, Department of Computer Science, University of Aaxhus, 1999.
• 11: C. K. Holst and J. Launchbury. Handwriting cogen to avoid problems with s~atic typing. In Draft Proceedings, ~th Annual Glasgow Workshop on Functional Programming, pages 210-218. Glasgow University, 1991.
• 12: N. D. Jones. Challenging problems in partial evaluation and mixed computation. In D. Bj0rner, A. P. Ershov, and N. D. Jones, editors, Partial Evaluation and Mixed Computation, pages 1-14. North-Holland, 1988.
• 13: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 14: N. D. Jones, P. Sestoft, and H. S0ndergaard. MIX: A selfapplicable partial evaluator for experiments in compiler generation. Lisp and Symbolic Computation, 2(1):9-50~ 1989.
• 15: Lawrence Paulson, Compiler generation from denotational semantics, Methods and tools for compiler construction, Cambridge University Press, New York, NY, 1984
• 16: M. Rhiger. Deriving a statically typed type-directed partial evaluator. In O. Danvy, editor, Proceedings of PEPM '99, Technical report BRICS-NS-99-1, BRICS, Department of Computer Science, University of Aarhus, pages 25-29, 1999.
• 17: M. Rhiger. Run-time code generation for type-directed partial evaluation. Progress report, BRICS PhD School, University of Aarhus. Available at http://www .brits. dk/-mrhiger, Dec. 1999.
• 18: Zhe Yang, Encoding types in ML-like languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.289-300, September 26-29, 1998, Baltimore, Maryland, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Experimentation, Management, Verification