We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments that map variables to expressions in some new scope. By statically tracking scopes, users of this library gain confidence that they have correctly maintained the subtle invariants that stem from using de Bruijn indices. Behind the scenes, Rebound uses environments to optimize the application of substitutions, while providing explicit access to these data structures when desired. We demonstrate that this library is expressive by using it to implement a wide range of language features with sophisticated uses of binding and several different operations that use this abstract syntax. Our examples include pi-forall, a tutorial implementation of a type checker for a dependently-typed programming language. Finally, we benchmark Rebound to understand its performance characteristics and find that it produces faster code than competing libraries.

翻译：本文介绍了Rebound库，该库支持在Haskell中实现作用域明确的项表示，并自动化了替换、α等价等与绑定结构相关的操作定义。我们设计的核心理念是使用一等环境，将变量映射到新作用域中的表达式。通过静态追踪作用域，该库的使用者能够确信自己正确维护了由德布鲁因索引使用所产生的微妙不变性。在底层实现中，Rebound利用环境优化替换操作的应用，同时允许用户在需要时显式访问这些数据结构。我们通过使用该库实现多种具有复杂绑定机制的语言特性及若干基于抽象语法的不同操作，证明了其强大的表达能力。示例包括pi-forall——一个依赖类型编程语言类型检查器的教学实现。最后，我们对Rebound进行基准测试以了解其性能特征，发现其生成的代码比同类竞争库更为高效。