Lambda the Ultimate

Conor McBride, James McKinna

In this paper, we show how to manipulate syntax with binding using a mixed representation of names for free variables (with respect to the task in hand) and de Bruijn indices for bound variables. By doing so, we retain the advantages of both representations: naming supports easy, arithmetic-­free manipulation of terms; de Bruijn indices eliminate the need for alpha-­conversion. Further, we have ensure that not only the user but also the implementation need never deal with de Bruijn indices, except within key basic operations. Moreover, we give a representation for names which readily supports a power structure naturally reflecting the structure of the implementation. Name choice is safe and straightforward. Our technology combines easily with an approach to syntax manipulation inspired by Huet's `zippers'. Without the technology in this paper, we could not have implemented Epigram. Our example---constructing inductive elimination opera­ tors for datatype families---is but one of many where it proves invaluable.

OT: Is it just me, or the page 7 contains an easter egg? Or rather a pun...