Free Foil: Generating Efficient and Scope-Safe Abstract Syntax

TL;DR

This work tackles the problem of efficiently and safely representing abstract syntax with binders, comparing the foil approach to prior methods such as de Bruijn indices and HOAS. It proposes two practical directions: (i) integrating the foil with free scoped monads to yield type-safe, generic ASTs parameterized by a second-order signature, and (ii) using Template Haskell to derive a scope-safe foil representation from naïve syntax, enabling rapid prototyping with BNF Converter. Demonstrations on a $λΠ$ language with pairs and patterns show how each route can realize scope-safe substitution and generic recursion, with benchmarks indicating that Template Haskell generation often yields the best performance among foil-based approaches, while free foil remains competitive. Overall, the paper offers a practical framework for accessible, scalable, scope-safe abstract syntax generation, outlines clear trade-offs between genericity and performance, and suggests paths for unifying the approaches toward higher-order unification and beyond.

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 à 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ïve 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.

Figures (14)

• Figure 1: The foil representation for terms in $\lambda\Pi$ with pairs and patterns. haskellTerm and haskellName are parametrized by a phantom type parameter that indicates the scope (untyped context) of the term. haskellPattern is parametrized by two phantom parameters: first parameter indicates the smaller outer scope while the second parameter indicates the larger inner scope, extended with the variables bound in the pattern.
• Figure 2: Sinkability proof for $\lambda\Pi$ terms. This definition ensures that renaming is scope-safe for haskellTerm and only serves as a formal justification to use a zero cost function haskellsink instead of haskellsinkabilityProof in the user code.
• Figure 3: Scope-safe implementation of the substitution for the foil representation of terms in $\lambda\Pi$ with pairs and patterns. The foil helps maintain the correct implementation, making sure binders and scopes are handled properly.
• Figure 4: The haskellCoSinkable type class, its instance for haskellBinder, and a general version of haskellextendRenaming.
• Figure 5: The foil representation for a complex pattern type with corresponding haskellCoSinkable instance and haskellwithPattern.

Theorems & Definitions (1)

• Remark 3.1