Towards the Essence of Hygiene

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 captureavoiding 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 defin...

• Type: Journal
• Year: 2015
• Where: POPL
• Authors: Michael D. Adams
• Keywords: POPL 2015, Programming Languages