Free Foil: Generating Efficient and Scope-Safe Abstract Syntax
Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva

TL;DR
This paper introduces two methods to enhance the efficiency and scope-safety of abstract syntax representations with binders, combining free scoped monads with the foil and providing Template Haskell tools for quick prototyping.
Contribution
It proposes marrying free scoped monads with the foil and offers Template Haskell functions to generate scope-safe syntax from naive representations, improving efficiency and usability.
Findings
Achieved more affordable, type-safe abstract syntax representations.
Enabled quick language prototyping with existing tools.
Benchmarked performance improvements over traditional methods.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNatural Language Processing Techniques · Speech and dialogue systems · Topic Modeling
