How Many Numbers Can a Lambda-term Contain?

It is well known, that simply-typed lambda-terms can be used to represent numbers, as well as some other data types, in particular tuples of numbers. We prove, however, that in a lambda-term of a fixed type we can store only a fixed number of natural numbers, in such a way that they can be extracted using lambda-terms. More precisely, while representing k numbers in a closed lambda-term of some type we only require that there exist k closed lambda-terms M_1,...,M_k such that M_i takes as argument the lambda-term representing the k-tuple, and returns the i-th number in the tuple (we do not require that, using lambda-calculus, one can construct the representation of the k-tuple out of the k numbers in the tuple). Moreover, the same result holds when we allow that the numbers may be extracted approximately, up to some error (even when we only want to know whether a set is bounded or not). This work is closely related to my previous work on higher-order pushdown automata.