Hygiene is an essential aspect of Scheme’s macro system that prevents unintended variable capture. However, previous work on hygiene has focused on algorithmic implementation rather than precise, mathematical definition of what constitutes hygiene. This is in stark contrast with lexical scope, alpha-equivalence and capture-avoiding substitution, which also deal with preventing unintended variable capture but have widely applicable and well-understood mathematical definitions.
This paper presents such a precise, mathematical definition of hygiene. It reviews various kinds of hygiene violation and presents examples of how they occur. From these examples, we develop a practical algorithm for hygienic macro expansion. We then present algorithm-independent, mathematical criteria for whether a macro expansion algorithm is hygienic. This characterization corresponds closely to existing hygiene algorithms and sheds light on aspects of hygiene that are usually overlooked in informal definitions.
Hygiene; Macros; Nominal logic
. Towards the essence of hygiene. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15. ACM, New York, NY, USA, January 2015. ISBN 978-1-4503-3300-9. doi: 10.1145/2676726.2677013.
@inproceedings{adams2015hygiene,
author = {Adams, Michael D.},
title = {Towards the Essence of Hygiene},
booktitle = {Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = {2015},
series = {POPL '15},
address = {New York, NY, USA},
month = jan,
publisher = {ACM},
isbn = {978-1-4503-3300-9},
doi = {10.1145/2676726.2677013},
}