Why do we have types? Pretty much to help modularise software into interchangeable parts.
But how does that work? Those parts are abstractions: something fixed encompassing something varying. Something is specified, but while allowing something to vary within that bound.
And an ideal type system would, one might expect, be able to specify exactly and completely. Is that not the value of types? that they can logically ensure particular meaning? We want to maximise that.
But these two are contradictory. You cannot simultaneously have interchangeble modules and perfectly specified types. The more interchangeable, the less specified: you have one, or the other. The interchangeability depends on the looseness of the specification – that is what abstraction is: it must leave out something, it does not say everything, otherwise nothing could vary.
The two are counterbalancing goods: the looseness of abstraction allows interchangeability, the rigidness of abstraction allows logical understanding/certainty. But the looseness also necessitates the possibility of error, and the rigidness also necessitates an unpliability of development – because each is really the opposite of the other.
~ ~ ~
In practice we resolve this in a few ways (all ‘externalise’ the variation, or pretend to, since that is not really possible).
First, we have sort-of decided that time and space are not primary: how much space a program uses is not fully explicitly coded, and how much time is practically entirely absent. This means performance can be an interchangeable aspect: different algorithms, of different performance, are substitutable, yet could still have (seemingly) fully specified types in code. The ‘looseness’ in the abstraction that allows interchangeability is just something we look away from.
Second, we are slack. We tend towards loose abstractions with a particular kind of risk distribution: we can gain a consistent productivity increase (by simplifying and sharing), but with a rare chance of big failure. See: ‘Programming is probabilistic’.
Third, we do not really care about getting exactly particular results. In fact, we do not really even know exactly what we want. You might want a particluar document, but do you care about the formatting? or whether it came from a particular hard-drive? So all software is only a rough idea, to some significant degree.
~ ~ ~
Type systems are ultimately pragmatic, empirical. We are not driving toward ever greater precision and power; it is a zero-sum-game in a sense: we are just shifting things around trying to find an optimal arrangement for what we happen to find ourselves doing (other fundamentals of software also seem like this . . .). Some interchangeability here, some logical certainty there.