Macros as multi-stage computations: type-safe, generative, binding macros in MacroML

ABSTRACT

With few exceptions, macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of contemporary typed functional languages: static typing and static scoping. At a deeper level, there is a need for a simple, usable semantics for macros. This paper argues that these problems can be addressed by formally viewing macros as multi-stage computations. This view eliminates the need for freshness conditions and tests on variable names, and provides a compositional interpretation that can serve as a basis for designing a sound type system for languages supporting macros, or even for compilation. To illustrate our approach, we develop and present MacroML, an extension of ML that supports inlining, recursive macros, and the definition of new binding constructs. The latter is subtle, and is the most novel addition in a statically typed setting. The semantics of a core subset of MacroML is given by an interpretation into MetaML, a statically-typed multi-stage programming language. It is then easy to show that MacroML is stage- and type-safe: macro expansion does not depend on runtime evaluation, and both stages do not "go wrong.

REFERENCES

• 1: Zena M. Ariola , Amr Sabry, Correctness of monadic state: an imperative call-by-need calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.62-74, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268952]
• 2: BARENDREGT, H. P. The Lambda Calculus: Its Syntax and Semantics, revised ed, vol. 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1984.
• 3: BENAISSA, Z. E.-A., MOGGI, E., TAHA, W., AND SHEARD, T. Logical modalities and multi-stage programming. In Federated Logic Conference (FLoe,) Satellite Workshop on Intuitionistic Modal Logics and Applications (IMLA) (1999).
• 4: Cristiano Calcagno , Eugenio Moggi , Walid Taha, Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.25-36, July 09-15, 2000
• 5: Luca Cardelli , Florian Matthes , Martín Abadi, Extensible Grammars for Language Specialization, Proceedings of the Fourth International Workshop on Database Programming Languages - Object Models and Languages, p.11-31, August 30-September 01, 1993
• 6: CURRY, H. B., AND FEYS, R. Combinatory Logic, Volume I. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1958. Second printing 1968.
• 7: R. Davies, A temporal-logic approach to binding-time analysis, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.184, July 27-30, 1996
• 8: Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.258-270, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237788]
• 9: R. Kent Dybvig , Robert Hieb , Carl Bruggeman, Syntactic abstraction in Scheme, Lisp and Symbolic Computation, v.5 n.4, p.295-326, Dec. 1992 [doi>10.1007/BF01806308]
• 10: Levent Erkök , John Launchbury, Recursive monadic bindings, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.174-185, September 2000
• 11: Matthias Felleisen, On the expressive power of programming languages, Science of Computer Programming, v.17 n.1-3, p.35-75, Dec. 1991
• 12: Marcelo Fiore , Gordon Plotkin , Daniele Turi, Abstract Syntax and Variable Binding, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.193, July 02-05, 1999
• 13: Robert Glück , Jesper Jørgensen, Efficient Multi-level Generating Extensions for Program Specialization, Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs, p.259-278, September 20-22, 1995
• 14: Robert Glück , Jesper Jørgensen, Fast Binding-Time Analysis for Multi-Level Specialization, Proceedings of the Second International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.261-272, June 25-28, 1996
• 15: Robert Glück , Jesper Jørgensen, An Automatic Program Generator for Multi-Level Specialization, Lisp and Symbolic Computation, v.10 n.2, p.113-158, July 1997 [doi>10.1023/A:1007763000430]
• 16: G0MARD, C. K., AND JONES, N. D. A partial evaluator for untyped lambda calculus. Journal of Functional Programming 1, 1 (1991), 21-69.
• 17: GRIFFIN, T. G. Notational definitions--a formal account. In Proceedings of the Third Symposium on Logic in Computer Science (1988).
• 18: Masatomo Hashimoto , Atsushi Ohori, A typed context calculus, Theoretical Computer Science, v.266 n.1-2, p.249-272, 09/06/2001 [doi>10.1016/S0304-3975(00)00174-2]
• 19: Martin Hofmann, Semantical Analysis of Higher-Order Abstract Syntax, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.204, July 02-05, 1999
• 20: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 21: Eugene Kohlbecker , Daniel P. Friedman , Matthias Felleisen , Bruce Duba, Hygienic macro expansion, Proceedings of the 1986 ACM conference on LISP and functional programming, p.151-161, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319859]
• 22: Jeffrey R. Lewis , John Launchbury , Erik Meijer , Mark B. Shields, Implicit parameters: dynamic scoping with static types, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.108-118, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325708]
• 23: Ian A. Mason, Computing with Contexts, Higher-Order and Symbolic Computation, v.12 n.2, p.171-201, September 1999 [doi>10.1023/A:1010052222987]
• 24: MIILLER, D. An extension to NIL to handle bound variables in data structures: Preliminary report. In Informal Proceedings of the Logical Frameworks BRA Workshop (June 1990). Available as UPenn CIS technical report MS-CIS-90-59.
• 25: John C. Mitchell, On abstraction and the expressive power of programming languages, Selected papers of the conference on Theoretical aspects of computer software, p.141-163, October 1993, Sendai, Japan
• 26: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 27: MOGGI, E. A categorical account of two-level languages. In Mathematics Foundations of Program Semantics (1997). Elsevier Science.
• 28: Eugenio Moggi, Functor Categories and Two-Level Languages, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure, p.211-225, March 28-April 04, 1998
• 29: Eugenio Moggi , Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, An Idealized MetaML: Simpler, and More Expressive, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.193-207, March 22-28, 1999
• 30: MONNIER, S., AND SHA0, Z. Inlirung as staged computation. Tech. Rep. YALEU/DCS/TR-l 193, Department of Computer Science. Yale University, Mar. 2000.
• 31: Andrew Moran , David Sands, Improvement in a lazy context: an operational theory for call-by-need, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292547]
• 32: Flemming Nielson , Hanne Riis Nielson, Two-level semantics and code generation, Theoretical Computer Science, v.56 n.1, p.59-133, Jan. 1988 [doi>10.1016/0304-3975(86)90006-X]
• 33: Chris Okasaki , Peter Lee, Purely functional data structures, 1996
• 34: Dino P. Oliva , John D. Ramsdell , Mitchell Wand, The VLISP verified PreScheme compiler, Lisp and Symbolic Computation, v.8 n.1-2, p.111-182, March 1995 [doi>10.1007/BF01128408]
• 35: Oregon Graduate Institute Technical Reports. P.C. Box 91000, Portland. OR 972911000,IJSA. Available online front ftp://cse.ogi.edu/pub/tech-repo~s/README.html. Last viewed August 1999.
• 36: Emir Pasalic , Tim Sheard , Walid Taha, DalI: An Untyped CBV Operational Semantics and Equational Theoryofr Datatypes with Binders(Technical Development), Oregon Graduate Institute School of Science & Engineering, 2000
• 37: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 38: Andrew M. Pitts , Murdoch Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.230-255, July 03-05, 2000
• 39: PLOTKIN, G. D. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science 1 (1975), 125-159.
• 40: Amr Sabry, What is a purely functional language?, Journal of Functional Programming, v.8 n.1, p.1-22, January 1998 [doi>10.1017/S0956796897002943]
• 41: SANDS, D. Computing with contexts: A simple approach. In Second Workshop on HigherOrder Operational Techniques in Semantics (HOOTS II), A. 0. Gordon. A. NI. Pitts, and C. L. Talcott, Eds., vol. 10 of Electron,( Notes in Theoretical Computer Science. Elsevier Science Publishers B.V., 1998.
• 42: SHEARD, T. Using MetahIL: A staged programming language. Lecture Notes in Computer Science 1608 1 207-239.
• 43: Mark Shields , Tim Sheard , Simon Peyton Jones, Dynamic typing as staged type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.289-302, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268970]
• 44: Walid Mohamed Taha , Tim Sheard, Multistage programming: its theory and applications, 1999
• 45: Walid Taha, A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract), Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.34-43, January 22-23, 2000, Boston, Massachusetts, United States
• 46: Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, Multi-Stage Programming: Axiomatization and Type Safety, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.918-929, July 13-17, 1998
• 47: TAHA, W., AND MAKHOLM, H. Tag elimination - or type specialisation is a type-indexed effect. In Subtyping and Dependent Types in Programming. APPSEM Workshop. INRIA technical report, 2000.
• 48: Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.203-217, June 12-13, 1997, Amsterdam, The Netherlands
• 49: THIEMANN, P. AND DUSSART, D. Partial evaluation for higher-order languages with state. Available online from http://www.informatik.uni_freiburgdethiemanri/papers index,html. 1996
• 50: Mitchell Wand, Embedding type structure in semantics, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.1-6, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318602]
• 51: Mitchell Wand, The Theory of Fexprs is Trivial, Lisp and Symbolic Computation, v.10 n.3, p.189-199, May 1998 [doi>10.1023/A:1007720632734]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.3 Language Constructs and Features

General Terms:
Algorithms, Languages