论文标题
箔：避免捕获的替代，没有锋利的边缘
The Foil: Capture-Avoiding Substitution With No Sharp Edges
论文作者
论文摘要
正确地操纵编译器中的程序术语非常困难，因为需要避免名称捕获。从“格拉斯哥Haskell编译器Inliner的秘密”中的剑杆是一种尖端的技术，用于快速，无状态捕获的替代，用于用明确名称表示的表达式。但是，这是一个锋利的工具：它的不变性很棘手，需要在使用它的整个编译器中维护。我们描述了使用Haskell类型系统在静态上强制强制执行Rapier的箔纸，这是静态强制执行的，可以防止一类难以找到的错误，但没有添加任何运行时的开销。
Correctly manipulating program terms in a compiler is surprisingly difficult because of the need to avoid name capture. The rapier from "Secrets of the Glasgow Haskell Compiler inliner" is a cutting-edge technique for fast, stateless capture-avoiding substitution for expressions represented with explicit names. It is, however, a sharp tool: its invariants are tricky and need to be maintained throughout the whole compiler that uses it. We describe the foil, an elaboration of the rapier that uses Haskell's type system to enforce the rapier's invariants statically, preventing a class of hard-to-find bugs, but without adding any run-time overheads.
