A Theory of Hygienic Macros
Hygienic macro systems, such as Scheme’s, automatically rename variables to prevent unintentional variable capture—in short, they “just work.” Yet hygiene has never been formally presented as a specification rather than an algorithm. According to folklore
- PDF / 616,836 Bytes
- 15 Pages / 430 x 660 pts Page_size
- 84 Downloads / 215 Views
Abstract. Hygienic macro systems, such as Scheme’s, automatically rename variables to prevent unintentional variable capture—in short, they “just work.” Yet hygiene has never been formally presented as a specification rather than an algorithm. According to folklore, the definition of hygienic macro expansion hinges on the preservation of alpha-equivalence. But the only known notion of alpha-equivalence for programs with macros depends on the results of macro expansion! We break this circularity by introducing explicit binding specifications into the syntax of macro definitions, permitting a definition of alpha-equivalence independent of expansion. We define a semantics for a first-order subset of Scheme-like macros and prove hygiene as a consequence of confluence.
The subject of macro hygiene is not at all decided, and more research is needed to precisely state what hygiene formally means and [precisely which] assurances it provides. —Oleg Kiselyov [1]
1
What Are Hygienic Macros?
Programming languages with hygienic macros automatically rename variables to prevent subtle but common bugs arising from unintentional variable capture— the experience of the practical programmer is that hygienic macros “just work.” Numerous macro expansion algorithms for Scheme have been developed over many years [2,3,4,5,6], and the Scheme standard has included hygienic macros since R4 RS [7]. Yet to date, a formal specification for hygiene has been an elusive goal. Intuitively, macro researchers have always understood hygiene to mean preserving α-equivalence. In particular, performing an α-conversion of a bound variable should not result in a macro expansion that accidentally captures the renamed variable. But this idea has never been made precise. Why should such a simple idea be so hard to formalize? The problem is this: since the only known binding forms in Scheme are the core forms, the binding structure of a Scheme expression does not become apparent until after it has been fully expanded to core Scheme. Thus α-equivalence is only well-defined for Scheme programs that have been fully expanded, with no remaining instances of S. Drossopoulou (Ed.): ESOP 2008, LNCS 4960, pp. 48–62, 2008. © Springer-Verlag Berlin Heidelberg 2008
A Theory of Hygienic Macros
49
macros. So if the conventional wisdom is correct, the definition of hygienic macro expansion relies on α-equivalence, but the definition of α-equivalence relies on the results of macro expansion! This circularity is clearly paradoxical, and the definition of hygiene has consequently remained a mystery. But in practice, well-behaved macros follow regular binding disciplines consistently, independent of their particular expansion. For example, Scheme’s let construct can be macro-defined using lambda, yet programmers rely on knowing the binding structure of let without actually thinking about its expansion. If the semantics of macros only had access to this binding structure in such a way that we could reason formally about the scope of Scheme programs without resorting to operational reas
Data Loading...
