Can lists be defined in a special way so that they contain things of different type?

In https://www.seas.harvard.edu/courses/cs152/2019sp/lectures/lec18-monads.pdf it is written that

A type $\tau$ list is the type of lists with elements of type $\tau$

Why must a list contain elements of the same type? Why can't it contain elements of different types?
Is there a way of defining a list polymorphically in the typed lambda calculus, so that it takes elements of any type?

Can we then use the List monad on lists, defined polymorphically?

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 "variably-typed list". 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 "type of types"), 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}$$

StackExchange Computer Science Q#129264, answer score: 4