← All papers
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
cs.PL
Jan 28, 2020 · v7
TL;DR
Implements and evaluates a hygienic macro system as a core component of Lean 4.
Abstract
In interactive theorem provers, the weights of extensible syntax and tactic languages have grown to rival the logical core. This paper proposes a hygienic macro system inspired by Scheme for these languages. The system addresses restrictive syntax extension mechanisms that cause unnecessary redundancy in libraries and accidental name capture in tactic languages that often produces unexpected behavior. The authors describe type-directed macro expansion yielding a single, uniform system offering multiple abstraction levels from simple syntax sugars to elaboration of built-in syntax. The system was implemented in Lean 4 and is simple enough to be integrated into other systems.
Problem
Interactive theorem provers suffer from restrictive syntax extension mechanisms that cause library redundancy, and tactic languages are prone to accidental name capture producing unexpected behavior.
Approach
A hygienic macro system inspired by Scheme is proposed for theorem proving languages. Type-directed macro expansion yields a single uniform system offering multiple abstraction levels, from simple syntax sugars to elaboration of built-in syntax. The system prevents accidental name capture in tactic languages.
Results
The system was implemented in Lean 4 and is simple enough to be integrated into other systems. It replaces multiple ad-hoc extension mechanisms with a single principled framework that avoids name-capture bugs.