Richard Bird and Ross Paterson.
*Journal of Functional Programming*, 9(1):77-91, January 1999.

de Bruijn notation is a coding of lambda terms in which each occurrence of
a bound variable *x* is replaced by a natural number, indicating the `distance'
from the occurrence to the abstraction that introduced *x*.
One might suppose that in any datatype for representing de Bruijn terms,
the distance restriction on numbers would have to maintained as an explicit
datatype invariant. However, by using a nested (or non-regular) datatype,
we can define a representation in which *all* terms are well-formed,
so that the invariant is enforced automatically by the type system.

Programming with nested types is only a little more difficult than programming with regular types, provided we stick to well-established structuring techniques. These involve expressing inductively defined functions in terms of an appropriate fold function for the type, and using fusion laws to establish their properties. In particular, the definition of lambda abstraction and beta reduction is particularly simple, and the proof of their associated properties is entirely mechanical.

gzipped PostScript, gzipped DVI, BibTeX. Haskell code (for Hugs 1.3c).

- Nested Datatypes,
Richard Bird and Lambert Meertens.
In
*Mathematics of Program Construction*, Marstrand, Sweden, June 1998, LNCS vol. 1422, pages 52-67.A preliminary exploration of the theory of nested (or non-regular) datatypes.

- Generalised Folds for Nested Datatypes,
Richard Bird and Ross Paterson.
*Formal Aspects of Computing*, to appear.The theory of the generalized folds, as used in this paper.

*Introduction to Functional Programming using Haskell*, Richard Bird. Second Edition, Prentice Hall, 1988.Contains the theorem prover used to construct the proofs in this paper.