Infinite lists in Lambda calculus.... I have been learning Haskell for a number of months now and am now trying to understand the underpinning $\lambda$-calculus,  but I have run into a bit of a mental block! How would I go about writing a $λ$-term corresponding to an infinite list (for example  $[0, 1, 2, \dots]$)?
 A: The infinite list $[0, 1, 2, \dots]$ satisfies the following identity in Haskell (see here):
$$\tag{1}
[0,1,2, \dots] = 0 : \mathtt{map} \, (+1) \, [0,1,2,\dots]
$$
where $(+1)$ is the function computing the successor of an integer, and $:$ is the function that appends an element to the front of a list.
Indeed, $$\mathtt{map} \, (+1) \, [0,1,2,\dots] = [(+1) \, 0, (+1) \, 1, (+1) \, 2, \dots] = [1, 2, 3, \dots]$$ and clearly
$$0 : [1, 2, 3, \dots] = [0,1, 2, \dots]$$
therefore, Identity $(1)$ holds.
Can Identity $(1)$ be expressed in the $\lambda$-calculus? Yes!
Indeed:

*

*The natural number $0$ is represented in the $\lambda$-calculus by the Church numeral $\underline{0} = \lambda f. \lambda x. x$ (see here);

*The function $(+1)$ is represented in the $\lambda$-calculus by the $\lambda$-term $\mathsf{succ} = \lambda n. \lambda f. \lambda x. f(n f x)$ (see here);

*The function $:$ is represented in the $\lambda$-calculus by the $\lambda$-term $\mathsf{cons} = \lambda x. \lambda l. \lambda c. \lambda n. c x (l c n)$ (see here);

*The function $\mathtt{map}$ is represented in the $\lambda$-calculus by the $\lambda$-term $\mathsf{map} = \lambda f. \lambda l. \lambda c. l \, \lambda x. c (f x)$ (see here, unfortunately the author of the question has inexplicably deleted it, I hope he/she will undelete it).

Apparently, the only missing $\lambda$-term to represent $(1)$ in the $\lambda$-calculus is $[0,1,2,\dots]$, that is, the $\lambda$-term that we want to define! Let us denote it by $X$, as an unknown variable in a mathematical equation. Thus, $(1)$ can be rewritten as an equation in the $\lambda$-calculus
$$\tag{2}
X =_\beta \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, X)$$
where $=_\beta$ is $\beta$-equivalence, that is (roughly), the unoriented version of $\beta$-reduction.
If we can solve Equation $(2)$ (i.e. we find a $\lambda$-term $X$ such that $(2)$ holds), then such a $\lambda$-term represents the infinite list $[0,1,2,\dots]$.
Since $(\lambda x.N)x \to_\beta N$ for any $\lambda$-term $N$, Equation $(2)$ can be equivalently rewritten as
$$\tag{3}
X =_\beta (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)) X
$$
Equation $(3)$ is of interest because it says that the $\lambda$-term $X$ we are looking for is a fixed point of the $\lambda$-term $\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)$.
This is where the fixpoint combinator $Y$ of the $\lambda$-calculus becomes relevant, as correctly suggested by @MJD in his comment.
Indeed, $Y = \lambda f. (\lambda x. f(xx))(\lambda x. f(xx))$ is a "magic" $\lambda$-term such that, for every $\lambda$-term $M$,
$$\tag{4}
YM =_\beta  M(YM)$$
that is, $YM$ is a fixed point of any $\lambda$-term $M$.
Who cares? From Identity $(4)$, replace the generic $M$ with the $\lambda$-term $\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)$, so the following identity holds:
$$
Y(\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)) =_\beta (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)) \big( Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))\big)
$$
This shows that $X = Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$ is a solution of Equation $(3)$: just rewrite $(3)$ by replacing $X$ with $Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$.
And a solution of Equation $(3)$, and hence of Equation $(2)$, is what we are looking for!
Summing up, the infinite list $[0,1,2,\dots]$ is represented in the $\lambda$-calculus by the $\lambda$-term:
$$
Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$$

Digression. There are different ways to define the $\lambda$-terms $\mathsf{cons}$ and $\mathsf{map}$, depending on the way lists are encoded in the $\lambda$-calculus.
According to the encoding of lists presented here, a list $[N_1, \dots, N_k]$ is represented by the $\lambda$-term $$\lambda c. \lambda n.c N_1 (c N_2 (\dots(c N_k n)\dots))$$
and the definitions of $\mathsf{cons}$ and $\mathsf{map}$ above work for this encoding.
An alternative encoding of lists is presented here, it requires other (just slightly different) definitions of $\mathsf{cons}$ and $\mathsf{map}$.
Note that $Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$ always represents the infinite list $[0, 1, 2,\dots]$, provided that $\mathsf{cons}$ and $\mathsf{map}$ are suitable for the encoding of lists under consideration.
