De Bruijn indices are a well known technique for programming with names and binders. They provide a representation that is both simple and canonical. However, programming errors tend to be really easy to make. We propose a safer programming interface implemented as a library. Whereas indexing the types of names and terms by a numerical bound is a famous technique, we index them by worlds, a different notion of index that is both finer and more abstract. While being more finely typed, our approach incurs no loss of expressiveness or efficiency. Via parametricity we obtain properties about functions polymorphic on worlds. For instance, well-typed world-polymorphic functions over open A-terms commute with any renaming of the free variables. Our whole development is conducted within Agda, from the code of the library, to its soundness proof and the properties of external functions. The soundness of our library is demonstrated via the construction of a logical relations argument.
展开▼
