Functional pearl: i am not a number--i am a free variable

Conor McBride, James McKinna

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 [5] 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 α-conversion. Further, we have ensured 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 hierarchical representation for names which naturally reflects the structure of the operations we implement. Name choice is safe and straightforward. Our technology combines easily with an approach to syntax manipulation inspired by Huet's 'zippers'[10].Without the ideas in this paper, we would have struggled to implement EPIGRAM [19]. Our example-constructing inductive elimination operators for datatype families-is but one of many where it proves invaluable.
Original languageEnglish
Title of host publicationHaskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on Haskell
PublisherAssociation for Computing Machinery
Number of pages9
ISBN (Print)1581138504
Publication statusPublished - Sept 2004
Event2004 ACM SIGPLAN workshop on Haskell - Snowbird, United States
Duration: 22 Sept 200422 Sept 2004


Conference2004 ACM SIGPLAN workshop on Haskell
Country/TerritoryUnited States


Dive into the research topics of 'Functional pearl: i am not a number--i am a free variable'. Together they form a unique fingerprint.

Cite this