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.

翻译：在编译器、证明辅助工具和定理证明器的实现中，正确且高效地处理绑定标识符至关重要。当为带有绑定子的抽象语法选择表示形式时，实现者需要在具有内在作用域的类型安全性、效率以及通用性之间进行权衡。Maclaurin、Radul 和 Paszke 提出的"箔片"结合了 Barendregt 约定的高效实现与通过 Haskell 中高级类型系统特性（如秩-2 多态和广义代数数据类型）实现的内在作用域。另一方面，Kudasov 的自由作用域单子将内在作用域与 de Bruijn 索引相结合，作为嵌套数据类型，并采用 Sweirstra 的"数据类型的点菜"方法，以允许诸如高阶合一等算法的通用实现。在本文中，我们提出了两种使箔片更易实现的方法。首先，我们将自由作用域单子与箔片相结合，允许为任何给定其二阶签名的语言生成高效、类型安全且通用的带绑定子的抽象语法表示。其次，我们提供了 Template Haskell 函数，允许从一种朴素的表示生成作用域安全的表示。后一种方法使我们能够利用现有的工具（如 BNF Converter）非常快速地原型化语言的完整实现，包括解析、美观打印以及高效的内在作用域抽象语法。我们使用带有对和模式的 $\lambda\Pi$ 作为示例对象语言来演示这两种方法。最后，我们提供了基准测试，将我们的实现与箔片、使用嵌套 de Bruijn 索引的自由作用域单子以及一些传统实现进行比较。