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

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.

REFERENCES

• 1: Thorsten Altenkirch , Bernhard Reus, Monadic Presentations of Lambda Terms Using Generalized Inductive Types, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.453-468, September 20-25, 1999
• 2: Françoise Bellegarde , James Hook, Substitution: a formal methods case study using monads and transformations, Science of Computer Programming, v.23 n.2-3, p.287-311, Dec. 1994
• 3: Richard S. Bird , Ross Paterson, de Bruijn notation as a nested datatype, Journal of Functional Programming, v.9 n.1, p.77-91, January 1999 [doi>10.1017/S0956796899003366]
• 4: Thierry Coquand, An algorithm for testing conversion in type theory, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 5: N. G. de Bruijn. Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation. Indagationes Mathematic, 34:381--392, 1972.
• 6: F. de Saussure. Course in General Linguistics. Duckworth, 1983. English translation by Roy Harris.
• 7: Peter Dybjer, Inductive sets and families in Martin-Lo¨f's type theory and their set-theoretic semantics, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 8: G. Gentzen. The collected papers of Gerhard Gentzen. North-Holland, 1969. Edited by Manfred Szabo.
• 9: G. Huet. The Constructive Engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. World Scientific Publishing, 1989. Commemorative Volume for Gift Siromoney.
• 10: Gérard Huet, The Zipper, Journal of Functional Programming, v.7 n.5, p.549-554, September 1997 [doi>10.1017/S0956796897002864]
• 11: Gérard Huet , Gordon Plotkin, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 12: Thomas Johnsson, Lambda lifting: transforming programs to recursive equations, Proc. of a conference on Functional programming languages and computer architecture, p.190-203, January 1985, Nancy, France
• 13: Proc. of a conference on Functional programming languages and computer architecture, January 1985
• 14: S. Kleene. Introduction to Metamathematics. van Nostrand Rheinhold, Princeton, 1952.
• 15: Zhaohui Luo, Computation and reasoning: a type theory for computer science, Oxford University Press, Inc., New York, NY, 1994
• 16: Conor McBride, Inverting Inductively Defined Relations in LEGO, Selected papers from the International Workshop on Types for Proofs and Programs, p.236-253, December 15-19, 1996
• 17: Conor McBride, Elimination with a Motive, Selected papers from the International Workshop on Types for Proofs and Programs, p.197-216, December 08-12, 2000
• 18: C. McBride. Epigram, 2004. http://www.dur.ac.uk/CARG/epigram.
• 19: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 20: James McKinna , Robert Pollack, Pure Type Systems Formalized, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.289-305, March 16-18, 1993
• 21: James Mckinna , Robert Pollack, Some Lambda Calculus and Type Theory Formalized, Journal of Automated Reasoning, v.23 n.3, p.373-409, November 1999 [doi>10.1023/A:1006294005493]
• 22: Dale Miller, Unification under a mixed prefix, Journal of Symbolic Computation, v.14 n.4, p.321-358, Oct. 1992 [doi>10.1016/0747-7171(92)90011-R]
• 23: Randy Pollack, Closure under alpha-conversion, Proceedings of the international workshop on Types for proofs and programs, p.313-332, January 1994, Nijmegen, The Netherlands
• 24: D. Prawitz. Natural Deduction-A proof theoretical study. Almquist and Wiksell, Stockholm, 1965.
• 25: Philip Wadler, How to replace failure by a list of successes, Proc. of a conference on Functional programming languages and computer architecture, p.113-128, January 1985, Nancy, France

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

General Terms:
Design, Languages, Reliability, Theory

Keywords:
abstract syntax, bound variables, de Bruijn representation, free variables, fresh names, haskell, implementing epigram, induction principles