Exercise 2.2
Find types for zero, one and two (see Exercise 1.10).
Let's remind ourselves of what these Church numerals are;
$$\begin{align} zero &:= λfx.x \\ \\ one &:= λfx.fx \\ \\ two &:= λfx.f(fx) \end{align}$$
$zero := λfx.x$
If $x:A$ and $f:B$, then the type of zero is
$$zero : B \to A \to A$$
$one := λfx.fx$
If $x:A$ then $f$ must have compatible type $f:A \to B$.
The type of one is
$$one : (A \to B) \to A \to B$$
$two := λfx.f(fx)$
If $x:A$ then $f$ must have compatible type $f:A \to B$. But $f$ is also applied to $(fx)$ so it must have type $A \to A$.
The type of two is
$$two : (A \to A) \to A \to A$$
