I am not a number: I am a free variable

I am not a number: I am a free variable

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.
A pretty technical paper, but fun to read.

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

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Relationship to CINNI?

I wonder if there's a connection to CINNI.

Have to find out

Great link, thanks! So far I am finding CINNI more accessible, and more compatible with my thinking.