Macros as Multi-Stage Computations: Type-Safe, Generative, Binding Macros in MacroML

Steve Ganz, Amr Sabry, and Walid Taha

To appear at International Conference on Functional Programming (ICFP01), Firenze, Italy, 3-5 September 2001


Abstract

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 suspicious 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 the proposed 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 run-time evaluation, and neither ``goes wrong'' in the usual sense.


Server START Conference Manager
Update Time 11 May 2001 at 15:31:50
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems