Is there any meaning behind the classification of "λ-terms" in classes such as "church number" and "church list"? λ-calculus terms can be informally/intuitively categorized, such as:

(λ f x . (f (f (f x))))) is a church natural (3)
(λ a b . a) is a church boolean (true)
(λ c n . (c 1 (c 2 (c 3 n)))) is a church list ([1,2,3])
(λ s z . (s (λ s z . (s (λ s z . (s (λ s z . z))))))) is a peano natural (3)

That is, while the untyped lambda calculus obviously doesn't have explicit types, one can certainly recognize patterns on terms and categorize them based on their behavior - as if those had a type. When you say: &quot;a church number is a function that applies another function n times to an argument&quot; you are informally characterizing a wide range of λ-terms. My question is: is there any way to formalize that intuition? Any system/theory that meaningfully categorizes (untyped) λ-terms?
Several observations can be made based on your remarks:


In System F, every data type can be given an encoding using polymorphic types, e.g. $\mathrm{Bool}$ can be defined as the type
$$\forall A.A\rightarrow A\rightarrow A$$
On the other hand, certain terms (not all of course) can be given a principal type in system F, e.g.
$$\lambda ab.a $$
can be given the type $\forall AB.A\rightarrow B \rightarrow A$. But you can now notice that this is a generalization of the type $\forall A.A \rightarrow A \rightarrow A$, and this happens to be the most general type it shares with $\lambda a b.b$, which is of course the polymorphic encoding of $\mathrm{Bool}$. In this way, one can always attempt to assign the most general type to a term, and then check to see if this happens to be (a generalization of) the polymorphic encoding of a datatype.
Intersection type systems are usually undecidable type systems assigning types to pure $\lambda$-terms that have the remarkable property of classifying their behavior: in particular the most simple such system is complete for strong normalization: a term has a type iff it is SN.


In intersection type systems, it is always possible to interpret the set of all types of a term (ordered by the sub-typing relation) as a representation of the behavior of that term. In particular, there is a close correspondence between the various domain theory models of the pure $\lambda$-calculus and various intersection typing systems. See for example Intersection Types and Lambda Theories for an overview.