You can't usefully define a type $\mathsf{list}$ that doesn't indicate the type of its elements. That doesn't mean that you can't have lists that contain things of different types: it's still a $\tau \, \mathsf{list}$, but you can put the “contain things of different types” part in the $\tau$.
(These basic ideas were already in D.W. and varkor's answers. It's important to realize that these answers aren't contradictory! They're looking at different aspects of the bigger picture.)
If the type system lets you define a type $\mathsf{list}$ that can contain elements of any type, then consider the return type of a destructor like $\mathsf{head}$ or $\mathsf{nth}$, or the type of the function argument to $\mathsf{fold}$. You have no information on the type of the elements, so they would have to allow any type. This means that for example $\lambda x. \mathsf{head}(\mathsf{cons}(x, \mathsf{nil}))$ will not give you back a value of the same type as $x$ (or $x \, \mathsf{option}$, so that $\mathsf{head}$ can return $\mathsf{None}$ on empty lists). But then what do you get back from $\mathsf{head}$?
- If $\mathsf{head}$ allows the caller to specify any return type, then the type system is pretty much useless, since it allows arbitrary coercions between types through $\lambda x. \mathsf{head}(\mathsf{cons}(x, \mathsf{nil}))$. It's useless for logic since the Curry-Howard correspondence maps an arbitrary coercion between types to having every proposition imply every other proposition, so you have an inconsistent logic.
- If not, then you can't get back a value of the original type through $\lambda x. \mathsf{head}(\mathsf{cons}(x, \mathsf{nil}))$. So you may be able to build lists, but you can't get elements out of them.
A real-life example which in fact demonstrates both behaviors above is early versions of Java, before it had generics. Java has both a static type system and a dynamic type system. In the static type system, any¹ value can be transparently coerced to Object
, because Object
is considered a supertype of everything. So you can put any value in a List
. But what you get back out of it is the original value cast to Object
, not the original value itself. In the dynamic type system, you can coerce any type to any other type, so in practice, to get a value out of a list, you coerce it to the desired type. But having coercions defeats the purpose of a type system. This problem is the main reason why Java acquired generics: they allow the language to have $\tau \, \mathsf{list}$ instead of $\mathsf{list}$ (or in Java notation, List<T>
instead of List
).
Just because a list has a type of elements — $\tau \, \mathsf{list}$ is a list of elements of type $\tau$ — doesn't mean that you can't arrange to put values of different types in the same list. Pretty much any language that allows defining a list type does it by allowing algebraic data type definitions, something like this:
$$ \tau \, \mathsf{list} ::= \mathsf{nil} \mid \mathsf{cons} \: \tau \: (\tau \, \mathsf{list}) $$
Suppose you want to put both integers and strings in the same list. Define a type
$$ U ::= \mathsf{I} \: \mathsf{int} \mid \mathsf{S} \: \mathsf{string} $$
Now $U \, \mathsf{list}$ is the type of lists that can contain a mixture of integers and strings, e.g. $[\mathsf{I}(3), \mathsf{S}(\texttt{"foo"}), \mathsf{I}(4)]$.
You can make heterogeneous lists this way to the extent that the type system allows heterogeneous types. Note that “heterogeneous lists” isn't quite correct: the list itself is homogeneous: it's a list of elements of type $U$. The heterogeneity is in the type $U$. To put an element in the list, you apply a constructor of $U$ first. After you get an element out of the list, apply a destructor of $U$ to get the original value with its original type.
You can do this with any type that the language supports. If you want a completely heterogeneous list, you need a language that supports an “any” type. That's Object
in Java, for example. Strongly typed can have an “any” type if they carry the necessary type information at runtime. Java does it all the time. Languages that are statically typed (such as OCaml and other ML dialects, Haskell, Clean, Swift or Rust) can do it with a $\mathsf{dyn}$ type whose runtime representation contains the type of the value. With such a type, $\mathsf{dyn} \, \mathsf{list}$ is a list type that can contain a value of any type. This type coexists with other list types such as $\mathsf{int} \, \mathsf{list}$ (where the list elements don't carry runtime type information).
A related approach to building heterogeneous data structures is existential types. Existential types let you package a type with a value of that type: $(\exists \tau : P(\tau). a)$ where $a$ is an expression of some type $T$ such that $P(T)$ is true. For example, $\mathsf{dyn}$ can be modeled as a special case where $P$ is true of all types (an unbounded existential). A common use for existential types is to say that $\tau$ is a record, module or class with some particular elements or methods, without giving all the details: existential types are a way to model abstract types. With a bounded existential, you can still do some useful things with the value even without runtime type information (e.g. you can call the methods that $P$ describes), but not get the original type. A list whose elements have an existential type $T_E = (\exists \tau \ldots)$ can be seen as a heterogeneous list (because its elements have different “real” types), but it's still homogeneous in the sense that if you retrieve a value from the list, all you know is its package type $T_E$.
If the language has dependent types, you can package a value with its type in a way that allows recovering the original value: $\mathsf{package} ::= \sum_{\tau:\mathsf{TYPE}} \tau$ where $\mathsf{TYPE}$ is the type of types. This is a dependent sum type where the first component happens to be a type. The $\mathsf{package}$ type is a way to implement unbounded existentials in a dependently typed language. You can construct bounded existentials by adding constraints on $\tau$. Once again, you can build heterogeneous lists in the sense that a $\mathsf{package} \, \mathsf{list}$ contains elements whose “real” types are different, but the list itself is homogeneous in the sense that each list element has the type $\mathsf{package}$. As with existential types, you can't extract a value from a list and directly recover its “real” type. It's possible to destruct a value of type $\mathsf{package}$ by applying the second-element projection, but all you know about the result is that its type is the first-element projection: $p : \mathsf{package} \vdash \pi_2(p) : \pi_1(p)$.
So far, we've seen that in a non-degenerate type system, lists are homogeneous. It's possible to build heterogeneous lists, but the list type constructor itself is homogeneous: the heterogeneity comes from the element type. In a language that has both algebraic datatypes and types that depend on an integer (or something isomorphic to the naturals), it is possible to define a truly heterogenenous list type. Given a type family $(T_n)_{n \in \mathbb{N}}$, you can define the type of lists whose $n$th element has the type $T_n$. Here's such a definition in the language of the calculus of inductive constructions, specifically in Coq syntax. First, I define an example of a family of types indexed by an integer: tuple A n
is the type of n
-element tuples whose components all have the type A
. To keep the definition simple, all tuples have an additional value U
at the beginning of unit type. Then I define the inductive type hlist_
which is parametrized by both a type family T
and an integer n
, which is a heterogeneous list whose k
th element has the type n + k
. The parameter n
is necessary to keep the definition constructive. Finally I show some example terms of type hlist (tuple bool)
, that is, lists whose n
th element is an nth
-element tuple of bool
values (with U
prepended).
Inductive unit : Type := U : unit.
Fixpoint tuple (A : Type) (n : nat) : Type :=
match n with
| 0 => unit
| S m => (tuple A m) * A
end.
Inductive hlist_ (T : nat -> Type) n :=
| Hnil : hlist_ T n
| Hcons : (T n) -> hlist_ T (S n) -> hlist_ T n.
Definition hlist T := hlist_ T 0.
Check (Hcons (tuple bool) 0 U (Hnil _ _) : hlist (tuple bool)).
Check (Hcons (tuple bool) 0 U (Hcons _ 1 (U, true) (Hnil _ _)) : hlist (tuple bool)).
Check (Hcons (tuple bool) 0 U (Hcons _ 1 (U, true) (Hcons _ 2 (U, true, true) (Hnil _ _))) : hlist (tuple bool)).
¹ Except for some primitive data types, actually, but that's not important here. When I say “any” about Java in this answer, I mean objects only, not primitive data types.