> That’s the whole idea of static type checking: in return for restricting yourself to a controlled subset of the language that isn’t “too dynamic”, you gain the ability to type-check your code without running it.
Eh, you are mixing up distinctions.
All that's required of _static_ typing is that your static type specification finishes running before you start your program.
Whether that static type specification language is Turing complete or not is a completely separate issue. And, yes, you are right that it's generally useful for that language to be decidable. But see eg Haskell's UndecidableInstances.
Eh, you are mixing up distinctions.
All that's required of _static_ typing is that your static type specification finishes running before you start your program.
Whether that static type specification language is Turing complete or not is a completely separate issue. And, yes, you are right that it's generally useful for that language to be decidable. But see eg Haskell's UndecidableInstances.