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
sumofproducts 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 alphaequivalence, or by replacing
conventional parse trees with ones containing de Bruijn
indices [1]. By changing from the category of
sets to other wellknown, but still `setlike' categories of sheaves
or presheaves, one can regain an initial algebra view of this even
more than normally abstract syntaxthe payoff being new and
automatically generated forms of structural recursion and induction
that respect alphaequivalence [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 variablebinding
in [3, 4]. In this MLlike language
there are new forms of type for names and namebinding that come along
with facilities for declaring fresh names, for binding names in
abstractions and for pulling apart such nameabstractions via
patternmatching. The key idea is that properly abstract uses of
names, i.e. ones that do not descend below the level of
alphaconversion, 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 effectfree functional programming, in the sense that the usual
laws of pure functional programming remain valid (augmented with new
laws for names and nameabstractions).
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 ChurchRosser theorem.
Indag. Math., 34:381392, 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
193202. 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
214224. 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 459541. 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 230255. SpringerVerlag, Heidelberg, 2000.
This document was translated from L^{A}T_{E}X by
H^{E}V^{E}A.