I've been thinking about this (and will probably try to put together an essay about it at some point). I think that the types you learn in programming 101 and t

I've been thinking about this (and will probably try to put together an essay about it at some point). I think that the types you learn in programming 101 and the advanced types (the kinds of things written about in type theory books and papers) are related, but different beasts. If we drop down to the lowest level, basic-programming-types are about one thing - interpreting what is otherwise a pile of bits in memory. Without any notion of the difference, how would you interpret the difference between characters and integers and floating points? There is nothing about the ones and zeroes to tell you. So the first thing you learn is to write something like `char a = 'b';` Dependent types (and related type theory constructs) do get used for this in languages built from the ground up with that as a theoretical foundation, but they have their basis in ideas that are more related to formal verification and logic. And that's where the divide comes in. Using types to pick a codec for some bytes and using them to verify systems are very, very different mindsets. And we simply call both "types".