Dan Sommers writes:
How would I "think of types as collections of their instances"?
The canonical example of a type as a collection of instances is an enumeration, the simplest (useful) example of which is bool = {False, True}. In pre-big-integer Python, in principle you could do the same thing with the collection of all 2^64-bit bit patterns, with addition defined by a 2^64 x 2^64 tables with rows and columns indexed by the bit patterns and the results in the table cells. So a type is a tuple of a set and operations, which can also be defined as sets of the above form. Floats would have the same underlying set and different tables.
For example, in what sense is the type list a collection of instances of lists?
This involves infinite sets, but in principle can be thought of in the same way.
In my mind, a type is a description/container/shortand for a collection of properties or behaviors of instances of that type.
That's one way to think about it, of course. But the strong intuitions about the numeric tower (a natural number *is* an integer, an integer *is* a real number, and so on) as well as some useful but (intuitively) more artificial ideas such as a bool *is* a natural number are just as well expressed as set inclusions. This is useful in type theory, but explaining "how" is way beyond the scope of this post (and this whole list, in fact).