ABSTRACT
We introduce MetaML, a statically-typed multi-stage programming language extending Nielson and Nielson's two stage notation to an arbitrary number of stages. MetaML extends previous work by introducing four distinct staging annotations which generalize those published previously [25, 12, 7, 6]We give a static semantics in which type checking is done once and for all before the first stage, and a dynamic semantics which introduces a new concept of cross-stage persistence, which requires that variables available in any stage are also available in all future stages.We illustrate that staging is a manual form of binding time analysis. We explain why, even in the presence of automatic binding time analysis, explicit annotations are useful, especially for programs with more than two stages.A thesis of this paper is that multi-stage languages are useful as programming languages in their own right, and should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. To illustrate this we provide a simple three stage example, and an extended two-stage example elaborating a number of practical issues.
- 1.C. Consel and O. Danvy. For a better support of static data flow. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, Cambridge, Massachusetts, August 1991 (Lecture Notes in Computer Science, vol. 523}, pages 496-519. New York: ACM, Berlin: Springer-Verlag, 1991. Google ScholarDigital Library
- 2.Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In A CM Symposium on Principles of Programming Languages, pages 493-501, January 1993. Google ScholarDigital Library
- 3.Roberto Di Cosmo. Isomorphisms of Types: from )icalculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkh~user, 1995. Google ScholarDigital Library
- 4.Olivier Danvy. Type-directed partial evaluation. In A CM Symposium on Principles of Programming Languages, pages 242-257, Florida, January 1996. New York: ACM. Google ScholarDigital Library
- 5.Olivier Danvy, Karoline Malmkjaer, and Jens Palsberg. The essence of eta-expansion in partial evaluation. LISP and Symbolic Computation, 1(19), 1995. Google ScholarDigital Library
- 6.Rowan Davies. A temporal-logic approach to bindingtime analysis. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 184-195, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press. Google ScholarDigital Library
- 7.Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In 23rd Annual A CM Symposium on Principles of Programming Languages (POPL '96}, St.Petersburg Beach, Florida, January 1996. Google ScholarDigital Library
- 8.Nachum Dershowitz. Computing with rewrite systems. Information and Control, 65:122-157, 1985.Google ScholarCross Ref
- 9.Robert Gliick and Jesper J~rgeasen. Efficient multilevel generating extensions for program specialization. In Programming Languages, Implementations, Logics and Programs (PLILP'95), volume 982 of Lecture Notes in Computer Science. Springer-Verlag, 1995. Google ScholarDigital Library
- 10.Robert Gliick and jesper J~rgensen. Fasting bindingtime analysis for multi-level specialization. In Psi-g6: Andrei Ershov Second International Memorial Conference, Perspectives of System Informatics, volume 1181 of Lecture Notes in Computer Science. Springer-Verlag, 1996. Google ScholarDigital Library
- 11.Carsten K. Gomard and Nell D. Jones. A partial evaluatot for untyped lambda calculus. Journal of Functional Programming, 1(1):21-69, 1991.Google ScholarCross Ref
- 12.John Hatcliff and Robert Gliick. Reasoning about hierarchies of online specialization systems. In Olivier Danvy, Robert Gliick, and Peter Thiemann, editors, Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, pages 161-182. Springer-Verlag, 1996. Google ScholarDigital Library
- 13.J. Roger Hindley and Jonathan P. Seldin. introduction to Cobminators and A-Calculus. Number 1 in London Mathematical Society Student Texts. Cambridge University Press, 1986. Google ScholarDigital Library
- 14.Nell D. Jones. Mix ten years later. In Partial Evaluation and Semantics-Based Program Manipulation, New Haven, Connecticut (Sigplan Notices, vol. 26, no. 9, September 199I), pages 24-38. New York: ACM, New York: ACM, June 1995. Google ScholarDigital Library
- 15.Nell D. Jones, Carsten K Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993. Google ScholarDigital Library
- 16.Simon L. Peyton Jones and John Launchbury. Unboxed values as first class citizens in a non-strict functional language. In Functional Programming and Computer Architecture, September 91. Google ScholarDigital Library
- 17.Richard B. Kieburtz, Francoise Bellegarde, Jef Bell, James Hook, Jeffrey Lewis, Dino Oliva, Tim Sheard, Lisa Walton, and Tong Zhou. Calculating software generators from solution specifications. In TAPSOFT'95, volume 915 of LNCS, pages 546-560. Springer-Verlag, 1995. Google ScholarDigital Library
- 18.Richard B. Kieburtz, Laura McKinney, Jeffrey Bell, James Hook, Alex Kotov, Jeffrey Lewis, Dino Oliva, Tim Sheard, Ira Smith, and Lisa Walton. A software engineering experiment in software component generation. In 18th International Conference in Software Engineering, March 1996. Google ScholarDigital Library
- 19.John Launchbury and Amr Sabry. Monadic state: Axiomatization and type safety. In Proceedings of the International Conference on Functional Programmin9, Amsterdam, June 1997. Google ScholarDigital Library
- 20.Mark Leone and Peter Lee. Deferred compilation: The automation of run-time code generation. Technical Report CMU-CS-93-225, Carnegie Mellon University, Dec. 1993. Google ScholarDigital Library
- 21.Michael Lowry, Andrew Philpot, Thomas Pressburger, and Inn Underwood. Amphion: Automatic programming for scientific subroutine libraries. NASA Science Information Systems Newsletter, 31:22-25, 1994.Google Scholar
- 22.Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.Google ScholarCross Ref
- 23.Torben /E. Mogensen. Efficient self-interpretation in lambda calculus. Functional Programming, 2(3):345- 364, July 1992.Google ScholarCross Ref
- 24.F. Nielson. Correctness of code generation from a twolevel meta-language. In B. Robinet and R. Wilhelm, editors, Proceedings of the European Symposium on Programming (ESOP 86), volume 213 of LNCS, pages 30- 40, Saarbriicken, FRG, March 1986. Springer. Google ScholarDigital Library
- 25.F. Nielson and H. R. Nielson. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992. Google ScholarDigital Library
- 26.G. D. Plotkin. Call-by-name, call-by-value- and the lambda-calculus. Theoretical Computer Science, 1:125- 159, 1975.Google ScholarCross Ref
- 27.Tim Sheard. A type-directed, on-line partial evaluator for a polymorphic language. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, Amsterdam, June 1997. Google ScholarDigital Library
- 28.Tim Sheard and Neal Nelson. Type safe abstractions using program generators. Technical Report OGI-TR- 95-013, Oregon Graduate Institute of Science and Technology, 1995.Google Scholar
- 29.Tim Sheard and Mark Shields. Dynamic typing through staged type inference. In Proceedings of the Second A CM International Conference on Functional Programming, jun 1997. (submitted).Google Scholar
- 30.Brian C. Smith. Reflection and Semantics in a Procedural Language. PhD thesis, Massachusetts Institute of Technology, January 1982.Google Scholar
- 31.Peter Thiemann. Towards partial evaluation of full Scheme. In Gregor Kiczales, editor, Reflection 96, pages 95-106, San Francisco, CA, USA, April 1996.Google Scholar
- 32.Wright and Felleisen. A syntactic approach to type soundness. Information and Computation (formerly Information and Control), 115, 1994. Google ScholarDigital Library
Index Terms
- Multi-stage programming with explicit annotations
Recommendations
Multi-stage programming with explicit annotations
We introduce MetaML, a statically-typed multi-stage programming language extending Nielson and Nielson's two stage notation to an arbitrary number of stages. MetaML extends previous work by introducing four distinct staging annotations which generalize ...
MetaML and multi-stage programming with explicit annotations
Partial evaluation and semantics-based program manipulation
Comments