An important thing to get right in simply typed lambda calculus is how you represent data. The way you represent it determines what kinds of recursion you can do. The "trick" in this answer is to represent lists as folds. Let's review how this works by recalling the equations for $\mathbf{foldr}$:
- $\mathbf{foldr}\ f\ b\ \mathbf{nil} = a$
- $\mathbf{foldr}\ f\ b\ (\mathbf{cons}\ x\ xs) = f\ x\ (\mathbf{foldr}\ f\ b\ xs)$
where
\begin{align*}
f &: \alpha\to\beta\to\beta\\
b &: \beta \\
x &: \alpha \\
xs &: \mathbf{list}\ \alpha
\end{align*}
An audacious idea is to try to come up with definitions for $\mathbf{nil}$ and $\mathbf{cons}$ so that the following equation holds:
$$xs\ f\ b = \mathbf{foldr}\ f\ b\ xs$$
That way, we know $\mathbf{foldr}$ doesn't need any additional recursion to be defined.
The following works as pure lambda terms:
- $\mathbf{nil} = \lambda f.\lambda b. b$
- $\mathbf{cons}\ x\ xs = \lambda f.\lambda b. f\ x\ (xs\ f\ b)$
Notice how they are essentially the equations for $\mathbf{foldr}$ but with the $f$ and $b$ arguments coming last.
However, there is an issue: what should the types be for the arguments $f$ and $b$? We could give them types this way:
- $\mathbf{nil} = \lambda (f:\alpha\to\beta\to\beta).\lambda (b:\beta). b$
- $\mathbf{cons}\ (x:\alpha)\ (xs:\mathbf{list}\ \alpha) = \lambda (f:\alpha\to\beta\to\beta).\lambda (b:\beta). f\ x\ (xs\ f\ b)$
But for this to work, we need to say what $\beta$ is. What we have actually defined is something like a type $\mathbf{list}\ \alpha\ \beta$, which are lists that only allow folds with a specific $\beta$. To remedy this, it seems we have to extend our notion of the simply typed lambda calculus to include dependent types.
Let's introduce the simplest type of pi types, the one that appears in vanilla Haskell. We may prefix a type with $\forall \beta$ to indicate a function that takes an additional type argument, where the type of a type is ${*}$, known as a kind, and where the rest of the type may depend on that type. Now, set
\begin{align*}
&\mathbf{list}\ \alpha = \forall \beta. (\alpha \to \beta \to \beta) \to \beta \to \beta \\
&\mathbf{nil} : \mathbf{list}\ \alpha
= \lambda (\beta:{*}). \lambda (f:\alpha\to\beta\to\beta).\lambda (b:\beta). b \\
&\mathbf{cons}\ (x:\alpha)\ (xs:\mathbf{list}\ \alpha) : \mathbf{list}\ \alpha= \lambda (\beta:{*}).\lambda (f:\alpha\to\beta\to\beta).\lambda (b:\beta). f\ x\ (xs\ f\ b)
\end{align*}
With these, we may define
\begin{align*}
\mathbf{foldr} &: \forall\alpha.\forall\beta. (\alpha \to \beta \to \beta) \to \beta \to \mathbf{list}\ \alpha \to \beta \\
&=\lambda (\alpha:{*}).\lambda(\beta:{*}).\lambda (f:\alpha \to \beta \to \beta).\lambda (b:\beta).\lambda(xs:\mathbf{list}\ \alpha).\\
&\quad \quad xs\ f\ b
\end{align*}
It's also easy to define $\mathbf{map}$ since we can make use of $\mathbf{foldr}$:
\begin{align*}
\mathbf{map} &: \forall\alpha.\forall\beta. (\alpha \to \beta) \to \mathbf{list}\ \alpha \to \mathbf{list}\ \beta \\
&= \lambda(\alpha:{*}).\lambda(\beta:{*}).\lambda (f:\alpha\to\beta). \lambda(xs:\mathbf{list}\ \alpha).\\
&\quad\quad \mathbf{foldr}\ (\lambda x.\lambda ys. \mathbf{cons}\ (f\ x)\ ys)\ \mathbf{nil}\ xs
\end{align*}
Note: Commonly type arguments are passed implicitly. To be explicit, we would want to instead write the body of this definition as
\begin{align*}
\mathbf{foldr}\ \alpha\ (\mathbf{list}\ \beta)\ (\lambda x.\lambda ys. \mathbf{cons}\ (f\ x)\ ys)\ \mathbf{nil}\ xs
\end{align*}
Another important function for manipulating lists (since it's how you can implement destructuring by cases for a programming language) is
\begin{align*}
\mathbf{cases} &: \forall\alpha.\forall\beta. \beta \to (\alpha \to \beta) \to \mathbf{list}\ \alpha \to \beta
\end{align*}
with the equations
- $\mathbf{cases}\ b\ f\ \mathbf{nil} = b$
- $\mathbf{cases}\ b\ f\ (\mathbf{cons}\ x\ xs) = f\ x$
It's a nice little exercise to figure out how to define this using $\mathbf{foldr}$. (By the way, these equations are another starting point for defining lists, but if you use them I'm pretty sure you can't define $\mathbf{foldr}$ without a fixed point combinator.)
Summary: To define these lists in a useful way, you have to extend the simply typed lambda calculus with a simple kind of type polymorphism -- this is System F.
Lists are an example of inductive types (data). Infinite lists are actually very different, and are examples of coinductive types (codata). (Haskell's ubiquitous laziness essentially makes everything be simultaneously data and codata, which is why its lists can be infinite.)
Both the simply typed lambda calculus and System F are strongly normalizing, so it's impossible to define infinite lists. The issue is that infinite lists don't have a normal form (they're infinite!) since you can keep evaluating tails. For example, if $\mathbf{zeros}$ is the infinite list with $\mathbf{zeros} = \mathbf{cons}\ 0\ \mathbf{zeros}$, then
$$\mathbf{zeros} = \mathbf{cons}\ 0\ (\mathbf{cons}\ 0\ (\mathbf{cons}\ 0\ (\mathbf{cons}\ 0\ \dots)))$$
That is, we can't even define any infinite lists at all.
We can get around this by introducing certain pure lambda terms (involving $Y$) and axiomatically asserting what their types are. The tradeoff is that, while we now would have infinite lists, we lose strong normalization. If we're careful with how we normalize (for example, weak head normal form) and with which axioms we introduce, then everything will still be well-behaved.
