Russell's Hierarchy of Types isn't particularly where type theories came from, though it was an early reference to the word and obviously very adjacent to these

Russell's Hierarchy of Types isn't particularly where type theories came from, though it was an early reference to the word and obviously very adjacent to these developments. It is a type system employed to solve a particular problem, though. Types have existed for a long time as mechanisms to provide classification and structure to formal (and even informal) languages. Even just before Russell, Frege (and many of his contemporaries) made a huge deal of the fine distinctions in type between propositions, expressions of truth, proofs, and their ilk. What really made type theories blow up was the recognition that they corresponded with these very things: propositions, judgements, proofs. Mathematicians developed type theories as follow-on to Russell's (and others) work because they wanted to better describe what kinds of things counted as valid propositions and what kinds of corresponding proofs were formally admissible. They also were critically tied to conversations of syntax and semantics where mathematicians asked hard questions about why funny symbols on pages ought to have any sort of force of knowledge whatsoever. So what made types rich was a recognition of the richness in the structure of first- and higher-order logics. The recognition that the power of the semi-formal language of proofs employed by working mathematicians required sophisticated study in order to describe and formalize. And that doing so required a distinction between the object of mathematical work, the proof, and the intent or semantics, the judgement. Early PL type systems seem to have been convergent evolution. Here we were as computer scientists making and operating new formal languages and needing to describe certain properties of the syntax (but really: its ultimate semantic weight as it is operated by a machine) so that we could, e.g., make sure we used properly sized registers. Only as more sophisticated programming languages were developed that desired to simply the supposed programmer's task of working with abstraction did PL designers begin to converge toward, steal, and ultimately influence these languages of logic. The convergence, in my opinion, occurred because there truly are significant similarities in the kinds of mental processes accomplished by logicians and by programmers. So where do type systems come from, really? I think the good ones represent natural, parsimonious structuring of logic. We land on compositional systems because they're easy to reason about inductively. We land on sums and products because of archetypes from boolean logic, our belief about the "cheapness" of copying knowledge, and because of the natural urge to package together and make choices. We land on modules/quantifiers due to the value of abstraction in compartmentalizing and reusing ideas. We can relax and challenge some of these assumptions to come up with new sorts of logic (and many PL designers and logicians make their bread in this way). We can also imagine totally different approaches to logic (like: state machine transition matrices) which are more challenging for us to work with using human minds or communicate to others using human speech. In this way, our type theories and logics are tailored to how humans most comfortably perceive the world.