4 ms·
I don't really think that unsound type systems are wrong, because I think it depends on the role of the types in the programming languages. Typescript, Java etc
by LeanderK 9y ago
I don't really think that unsound type systems are wrong, because I think it depends on the role of the types in the programming languages. Typescript, Java etc. don't have that sophisticated type systems and you can just check the types for yourself very quickly. You rely on the type-system to correct obvious mistakes, but not more.
In Languages like Haskell or completely dependently typed languages it would be morally wrong (in my opinion) to have an unsound type-system. Here the role of the types is different, you use types to compute types and need to trust the compiler in complicated situations that this is sound, just like you trust the compiler to do correct floating arithmetic. Checking the types per hand may be a real challenge, for example if your writing super polymorphic code. Sometimes you even have to prove that your code fits the type-signature (per induction etc.), here you want guarantees.