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

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 functiona l 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 th ese problems can be addressed by formally viewing macros as multi-stage com putations. This view eliminates the need for freshness conditions and tests on variable names, and provides a compositional interpretation that can se rve as a basis for designing a sound type system for languages supporting m acros, or even for compilation. To illustrate our approach, we develop and present Macro-ML, an extension o f ML that supports inlining, recursive macros, and the definition of new bi nding 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 giv en by an interpretation into MetaML, a statically-typed multi-stage program ming 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".