Hygienic macros are generative

In normal functional programming, we can "substitute equals for equals" -- any two equivalent expressions are interchangeable, because they will always produce equivalent results. This allows for all sorts of refactoring, because you can pull out an expression from one lexical context, stick it in another context, and expect it to behave the same.

Any functional programmer who's been burned by programmed macros such as syntax-case will tell you that when they try to refactor their macros in simple ways -- in particular, separating out pieces of a complicated macro and moving them into helper functions -- the macros suddenly stop working!

This is because in a hygienic macro system, syntax transformers are not pure functions. The hygiene condition requires that, in order to avoid unwanted capture, every use of a syntax transformer must generate different binding occurrences of identifiers! This is analogous to applicativity vs. generativity in ML-style parameterized module systems: applicative functions generate the same output for the same input, whereas generative functions are guaranteed to have different results every time you invoke them.

In a sense, this reminds me of the balance between expressive power vs. local reasoning, because hygiene introduces a non-local effect that ruins the ability to understand a macro in isolation. (Happily, there are limitations on these effects; for example, the "freshness monad" is known to be commutative, meaning that it doesn't matter what order you generate fresh names in, because they're all distinct anyway.) I wonder what kind of reasoning tools can help mitigate the problems hygiene causes with understanding macros.