Free Foil: Generating Efficient and Scope-Safe Abstract Syntax

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 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 $\lambda\Pi$ 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.