A Fresh Approach to Representing Syntax with Static Binders in Functional Programming

Andrew M. Pitts
Cambridge University Computer Laboratory
Cambridge CB3 0FD, UK
Andrew.Pitts@cl.cam.ac.uk

Abstract

Tell category theorists about the concept of abstract syntax for a language and they may say ``that's just the initial algebra for a sum-of-products functor on the category of sets''. Despite what you might think, they are trying to be helpful, since the initiality property is the common denominator of both definitions by structural recursion and proofs by structural induction [5, Sect. 4.4].

In recent years we have learned how to extend this initial algebra view of abstract syntax to encompass languages with statically scoped binders. In the presence of such binders one wants to abstract away from the specific names of bound variables, either by quotienting parse trees by a suitable notion of alpha-equivalence, or by replacing conventional parse trees with ones containing de Bruijn indices [1]. By changing from the category of sets to other well-known, but still `set-like' categories of sheaves or presheaves, one can regain an initial algebra view of this even more than normally abstract syntax---the pay-off being new and automatically generated forms of structural recursion and induction that respect alpha-equivalence [2, 3].

One good test of these new ideas is to see if they give rise to new forms of functional programming. In fact they do. The paper [6] sketches a functional programming language for representing and manipulating syntactical structure involving binders, based on the mathematical model of variable-binding in [3, 4]. In this ML-like language there are new forms of type for names and name-binding that come along with facilities for declaring fresh names, for binding names in abstractions and for pulling apart such name-abstractions via pattern-matching. The key idea is that properly abstract uses of names, i.e. ones that do not descend below the level of alpha-conversion, can be imposed on the user by a static type system that deduces information about the freshness of names. Even though we appear to be giving users a `gensym' facility, the type system restricts the way it can be used to the extent that we keep within effect-free functional programming, in the sense that the usual laws of pure functional programming remain valid (augmented with new laws for names and name-abstractions).

In this talk I will introduce this new approach to representing languages static binders in functional programming and discuss some of the difficulties we have had verifying its semantic properties.

References

[1]
N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math., 34:381--392, 1972.

[2]
M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In 14th Annual Symposium on Logic in Computer Science, pages 193--202. IEEE Computer Society Press, Washington, 1999.

[3]
M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In 14th Annual Symposium on Logic in Computer Science, pages 214--224. IEEE Computer Society Press, Washington, 1999.

[4]
M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, ?:?--?, 2001. Special issue in honour of Rod Burstall. To appear.

[5]
J. Meseguer and J. A. Goguen. Initiality, induction and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 14, pages 459--541. Cambridge University Press, 1985.

[6]
A. M. Pitts and M. J. Gabbay. A metalanguage for programming with bound names modulo renaming. In R. Backhouse and J. N. Oliveira, editors, Mathematics of Program Construction. 5th International Conference, MPC2000, Ponte de Lima, Portugal, July 2000. Proceedings, volume 1837 of Lecture Notes in Computer Science, pages 230--255. Springer-Verlag, Heidelberg, 2000.

This document was translated from LATEX by HEVEA.