Expanding a bit on the following questions and their answers:
Give Lambda Calculus Term for Haskell Function
Infinite lists in Lambda calculus....
I really like the answers to the two questions, but it got me thinking: Is it possible to find a solution for these in typed lambda-calculus? My question is not straight about how to do it, since I think that would be a nice exercise to try, however, I would like to know if there is such a solution and more likely why. We have three cases here:
- Infinite list - I guess here the answer would be no, because of the fixed-point combinator. However, I'm not really sure why? I guess the problem is the value that is mapped to itself by the function but would be nice to get a "real" clarification on that one.
- Foldr - I think here it should be fine, since there is no fix-point combinator, but it doesn't seem like "strong enough" reasoning.
- Map - Here I think the same logic applies as for folder.
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}$:
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:
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:
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
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.