Home » forums » LtU Forum

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.

By Jacques Carette at 2010-06-20 15:21 | LtU Forum | previous forum topic | next forum topic | other blogs | 14329 reads

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.

By dmbarbour at Sun, 2010-06-20 15:35 | login or register to post comments

Conference paper

Try this:

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

By Frank Atanassow at Sun, 2010-06-20 19:28 | login or register to post comments

Thanks. That's ten times

Thanks. That's ten times more approachable.

By dmbarbour at Sun, 2010-06-20 20:05 | login or register to post comments

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.

Dave

By Dave Herman at Sun, 2010-06-20 22:13 | login or register to post comments

An interesting comparison

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

http://nemerle.org/metaprogramming.pdf

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

By catbert at Sun, 2010-06-20 20:09 | login or register to post comments