# 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: "a church number is a function that applies another function n times to an argument" 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?

1. 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.

2. 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.

You are looking for extrinsic types which were explained by John Reynolds in his paper on intrinsic and extrinsic semantics.

Briefly, there are two ways in which we can approach types for programs:

1. Intrinsic: a program without a typing is meaningless, i.e., we consider programs together with their types.
2. Extrinsic: a program without typing information is meaningful. We can assign one or many types to it to express that it has certain properties.

Statically typed functional languages such as ML and Haskell insist on intrinsic typing: they refuse to run a program unless they can determine that it has a type. Scheme is untyped, so it will run a program even if no type can be assigned to it, and any types that are assigned to Scheme programs are extrinsic (external) to Scheme.

Let us consider an example. In $\lambda$-calculus we may consider the identity function. There are many ways to write it, depending on a particular flavor of the calculus:

• untyped: $\lambda x . x$
• monomorphic: $(\lambda x : \mathsf{int} . x) : \mathsf{int} \to \mathsf{int}$
• polymorphic (System F): $(\Lambda A . \lambda x : A . x) : \forall A . A \to A$
• parametric polymorphism (ML): $(\lambda x . x) : \alpha \to \alpha$

Under the intrinsic view of types we would insist that $\lambda x . x$ by itself means nothing, and that typing information must be provided. Under the extrinsic view $\lambda x . x$ makes sense by itself, but can be assigned many different types – so long as we explain what it means "to assign a type". A simple way is to say that a type is the same thing as a subset $T \subseteq \Lambda_0$ of the set $\Lambda_0$ all closed terms in the untyped $\lambda$-calculus (a better definition would be that a type is a partial equivalence relation on the set of closed terms). Some types that come to mind are:

• the type of terms equal to a Church numeral $$C = \{t \in \Lambda_0 \mid \exists n : \mathbb{N} . f \equiv_{\beta\eta} \overline{n} \}$$ where $\overline{n}$ is the $n$-th Church numeral.
• given any $A \subseteq \Lambda_0$ and $B \subseteq \Lambda_0$, we can define the type of functions $$A \to B = \{ t \mid \forall u \in A . t u \in B\}$$.
• if $(A_i)_{i \in I}$ is a family of types, we can define their intersection type $\bigcap_{i \in I} A_i$.

Now it can be checked that $\lambda x . x$ has the following extrinsic types:

• $C$ because it equals $\overline{1}$,
• $C \to C$
• $A \to A$ for any $A \subseteq \Lambda_0$
• $\bigcap_{A \subseteq \Lambda_0} (A \to A)$

An example that John Reynold liked to give was this: given a real number $c \in \mathbb{R}$, what type does $\lambda x . \cos(c \cdot x)$ have? Under intrinsic semantics the type would presumably be $\mathbb{R} \to \mathbb{R}$ no matter what $c$ is. But under extrinsic semantics it always has the type $\mathbb{R} \to \mathbb{R}$ and also the extrinsic type $\mathbb{Z} \to \mathbb{Z}$ when $c = \pi/2$.

Here is a similar list:

• Bush is the name of a president.
• C is the name of a programming language.
• Red is the name of a color.
• Church is the name of a mathematician.

Does this amount to a categorization of English nouns?

• I don't quite follow your point.... – D.W. Jul 29 '15 at 20:53
• This answer is a bit too wry for my taste. – Andrej Bauer Jul 31 '15 at 16:07