Declarative modeling of finite mathematics

A common foundation of finite arithmetic, hereditarily finite sets and sequences, binary trees and graphs is described as a progressive refinement of Haskell type classes.We derive as instances symbolic implementations of arithmetic operations in terms of rooted ordered trees representing hereditarily finite sets and sequences. Conversely, arithmetic implementations of pairs, powersets, von Neumann ordinals shade new light on the bi-interpretability between Peano arithmetic and a theory of hereditarily finite sets.As another instance, rooted ordered binary trees representing a simplified form of the type language of Goedel's System T are shown as directly emulating arithmetic and finite set operations.The main contribution of the paper is a fully constructive unification of paradigms - a chain of type classes does it all: Peano arithmetic, sets, sequences, binary trees, bitstrings. Another contribution is that we do it "efficiently" (i.e. in time and space asymptotically comparable with standard binary representations).The Haskell code in the paper is available at http://logic.cse.unt.edu/tarau/research/2010/shared.hs.