Really good write up. I'd add a couple of touch points:
- The art of designing type systems you describe is also heavily constrained by the practical limits of language. We could easily add more and more 'types' to a programming environment to cover more use cases, but at some point it makes the 'language' difficult when there's too many. Which is why turn to different languages for different uses.
- There's a bunch of different categories of types. This thread is full of discussion of functions and lambda calculus which is important as function types are some of the most complex, especially for 'trying to figure out at compile time' as you describe. But there's also common types like a 1 byte char, 4 byte unsigned int, or memory pointer that are more based on hardware and established standards, as well as user defined types and 'classes' which bring their own practical complexity and approaches.
- The art of designing type systems you describe is also heavily constrained by the practical limits of language. We could easily add more and more 'types' to a programming environment to cover more use cases, but at some point it makes the 'language' difficult when there's too many. Which is why turn to different languages for different uses.
- There's a bunch of different categories of types. This thread is full of discussion of functions and lambda calculus which is important as function types are some of the most complex, especially for 'trying to figure out at compile time' as you describe. But there's also common types like a 1 byte char, 4 byte unsigned int, or memory pointer that are more based on hardware and established standards, as well as user defined types and 'classes' which bring their own practical complexity and approaches.