4 ms·
It has zero impact on a static type system, but it has huge impact on any run-time type checking. So, for example, you can't really do dynamic typing and type
by mumblemumble 5y ago
It has zero impact on a static type system, but it has huge impact on any run-time type checking.
So, for example, you can't really do dynamic typing and type erasure. More generally, you can't do any dynamic type checking, including casts when types have been erased. OCaml does a more complete version of type erasure, and also lacks a casting operation. Because you can't safely cast if the run-time can't dynamically verify that the cast is valid.
(Tangentially, and Java is a great example of this - static and dynamic typing are not a binary. There are actually quite a few different kinds of type disciplines, and, in practice, it's common for languages to do some things statically and some dynamically.)
The soundness problem for Java is that, with the way it did generics, they don't really fit cleanly into Java's original type discipline. There are some things that tradition would have dictated be handled dynamically, but can't be in the case of generics because generic types only have partial run-time type information. At the same time, they weren't handed by the compiler, either, presumably because, historically, they fell outside the type checker's bailiwick. So they ended up being nobody's responsibility, and just not checked.
Nowadays we do generally get warnings for the most common situations where this happens, but there's no real way to fix them. You just silence the warning with an annotation to tell the compiler, "Trust me, I know what I'm doing." Meaning that, yeah, there's even a little bit of weak typing in Java. At least as of Java 5.