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

Abstract

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
Pages1-9
Number of pages9
ISBN (Print)1581138504
DOIs
Publication statusPublished - Sep 2004
Event2004 ACM SIGPLAN workshop on Haskell - Snowbird, United States
Duration: 22 Sep 200422 Sep 2004

Conference

Conference2004 ACM SIGPLAN workshop on Haskell
CountryUnited States
CitySnowbird
Period22/09/0422/09/04

Fingerprint 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

    McBride, C., & McKinna, J. (2004). Functional pearl: i am not a number--i am a free variable. In Haskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on Haskell (pp. 1-9). Association for Computing Machinery. https://doi.org/10.1145/1017472.1017477