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.