Papers › Free Foil: Generating Efficient and Scope-Safe Abstract Syntax
Free Foil: Generating Efficient and Scope-Safe Abstract Syntax
Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
Handling bound identifiers correctly and efficiently is critical in implementations of compilers, proof assistants, and theorem provers. When choosing a representation for abstract syntax with binders, implementors face a trade-off between type safety with intrinsic scoping, efficiency, and generality. The "foil" by Maclaurin, Radul, and Paszke combines an efficient implementation of the Barendregt convention with intrinsic scoping through advanced type system features in Haskell, such as rank-2 polymorphism and generalized algebraic data types. Free scoped monads of Kudasov, on the other hand, combine intrinsic scoping with de Bruijn indices as nested data types with Sweirstra's data types \`a la carte approach to allow generic implementation of algorithms such as higher-order unification. In this paper, we suggest two approaches of making the foil more affordable. First, we marry free scoped monads with the foil, allowing to generate efficient, type-safe, and generic abstract syntax representation with binders for any language given its second-order signature. Second, we provide Template Haskell functions that allow generating the scope-safe representation from a na\"ive one. The latter approach enables us to use existing tools like BNF Converter to very quickly prototype complete implementation of languages, including parsing, pretty-printing, and efficient intrinsically scoped abstract syntax. We demonstrate both approaches using λΠ with pairs and patterns as our example object language. Finally, we provide benchmarks comparing our implementation against the foil, free scoped monads with nested de Bruijn indices, and some traditional implementations.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections