Functional pearl: i am not a number--i am a free variable
Functional pearl: i am not a number--i am a free variable
复制标题
DOI：
10.1145/1017472.1017477
复制
发表时间：
2004-09
期刊：
影响因子：
--
通讯作者：
Conor McBride;James McKinna
中科院分区：
文献类型：
--
作者：
Conor McBride;James McKinna
在本文中，我们显示了如何使用自由变量的名称的混合表示（相对于手头任务）和De Bruijn索引[5]来操纵语法[5]。两种表示：命名支持术语的轻松，无算术的操纵；索引，除了主要的基本操作外，我们提供了一个自然反映我们实现的操作结构的名称的层次表示。 '[10]。这是家庭，但事实证明它是无价的。
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.