A Theory of Typed Hygienic Macros

A Theory of Typed Hygienic Macros, a dissertation by Dave Herman

We present the lambda_m-calculus, a semantics for a language of hygienic macros with a non-trivial theory. Unlike Scheme, where programs must be macro-expanded to be analyzed, our semantics admits reasoning about programs as they appear to programmers. Our contributions include a semantics of hygienic macro expansion, a formal definition of α-equivalence that is independent of expansion, and a proof that expansion preserves α-equivalence. The key technical component of our language is a type system similar to Culpepper and Felleisen's "shape types," but with the novel contribution of binding signature types, which specify the bindings and scope of a macro’s arguments.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I look forward to reading a

I look forward to reading a short, journal version.

Conference paper

Try this:

David Herman and Mitchell Wand. A Theory of Hygienic Macros. European Symposium On Programming (ESOP), 2008.

Thanks. That's ten times

Thanks. That's ten times more approachable.

Some advancements

The ESOP paper is a reasonable starting point, although the formalism has changed a bit since then. In particular, I've added recursion, pattern matching/case dispatch, and multi-arity binding forms. The type system now has recursive types and ad-hoc unions (necessary for the Scheme style of macros), and consequently a subtyping relation.

The dissertation is admittedly hefty. I do intend to write a gentler tech report or journal version.


An interesting comparison

can be made to the macro expansion hygiene in real world language, Nemerle:


(which is currently broken, as I see now... let's wait for administrators to fix this)