Can lists be defined in a special way so that they contain things of different type?
The short answer is that $\tau\ \text{list}$ is defined as a type constructor, along with rules for formation and elimination, and so we could similarly define a type constructor that allowed terms of different types to form a single &quot;variably-typed list&quot;. However, lists cannot take different types in the definition given, simply because they are defined with respect to a single type. In either case, adding lists, or variably-typed lists, involves extending the simply-typed $\lambda$-calculus, as lists of any kind do not exist in the usual presentation.
If we have a slightly richer type system than the simply-typed $\lambda$-calculus, we can encode variably-typed lists using standard $\tau\ \text{list}$s.

If we have a form of subtyping, we can store terms of different types, as long as they share a supertype. However, when we project elements out of the list, we can no longer tell specifically what type they were to begin with (this may be familiar from object-oriented programming), so this is a little limited.
If we have dependent sum types (also called $\Sigma$-types) and a universe type $\mathcal U$ (i.e. a &quot;type of types&quot;), we can form the type $(\Sigma_{A : \mathcal U} A)\ \text{list}$, whose elements are pairs consisting of a type $A$ and a term of that type.

Finally, I'll just note that polymorphism doesn't help us if we want heterogeneous lists: it just allows us to manipulate homogeneous lists for different $\tau$ more effectively. Polymorphic types have to be uniform in some sense, which is why we need dependency here instead.

To answer a follow-up question: if we have two variably-sorted lists using the dependent type approach, we can concatenate and flatten lists just as with ordinary lists.

The $\mathrm{List}$ monad has an operation $\mathrm{join}$ (in the language of Haskell), so given a list of variably-typed lists, $$l = [[(A, a), (B, b)], [(C, c), (D, d)]] : (\Sigma_{X : \mathcal U} X)\ \text{list list}$$ we can perform $\mathrm{join}$ to get a new list: $$\mathrm{join}(l) = [(A, a), (B, b), (C, c), (D, d)] : (\Sigma_{X : \mathcal U} X)\ \text{list}$$
Similarly, $\tau\ \text{list}$ can be equipped with a concatenation operation $+\!+$, so given the two lists in the previous example, we can concatenate them for a similar result:
$$[(A, a), (B, b)]\ {+\!+}\ [(C, c), (D, d)] = [(A, a), (B, b), (C, c), (D, d)] : (\Sigma_{X : \mathcal U} X)\ \text{list}$$