Java and scala's type systems are unsound: the existential crisis of null pointers

super T> constrain = null; Bind<U> bind = new Bind<U>(); return bind.upcast(constrain, t); } public static void main(String[] args) { String zero = Unsound.<Integer, String>coerce(0); } } [0] N. Amin, R. Tate "Java and Scala's type systems are unsound: the existential crisis of null pointers", https://dl.acm.org/doi/pdf/10.1145/2983990.2984004

code execution, and more... I don't think there are any invariants that a C compiler can enforce. Scheme, Python, Lua, Javascript etc. OTOH, have no static (= compile-time) type checking, yet they maintain some invariants! An object that has pointers to it will not be freed; An object's type is known, and will not change (well, some class transmutation is allowed but some not, an int will not turn into an array); Some types are immutable; You can never divide a string / string! etc... Moreover, by maintaining run-time metadata about object's types, they can tell you specifically that an operation raised a TypeError. Thus these languages are strongly typed at run time. IOW, I'm arguing that anything that blows up at run time is checked IFF it tells you it was a type error. This is meaningful compared to C segfaults that tell you nothing :-) --- The Java paper https://dl.acm.org/doi/pdf/10.1145/2983990.2984004 shows an interesting subtlety. "Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM" — yet they present unsound programs that "type-checks according to the Java Language Specification and is compiled by javac, version 1.8.0_25". What gives? If a bad program compiles, how come JVM is still sound? See, Java has two type systems! - JVM is the runtime, intended to be capable of loading even untrusted bytecode yet still maintain some type invariants. It manages memory and type metadata, and for this bad program will correctly identify type violation at run-time: "When executed, a ClassCastExceptionis thrown inside the main method with the message “java.lang.Integer cannot be cast to java.lang.String”" - The compilers uses a distinct more complex static type system. The question of soundness is: can any program that passed the compiler cause JVM run-time type errors? + Java language allows you to write type casts. These are deliberate "trust me" holes in the *static* type system, whose specified semantics is: JVM will check type at run time and raise exception if not as programmer promised. As https://typing-is-hard.ch/#what-about-unsafe-casts says, since these are deliberate, and fall back to meaningful run-time type checking(!), let's ignore them — redefine "soundness" as: can a program with no exclicit casts cause a run-time type error? + Generics only exist in static type system! They are invisible to JVM (aka "type erasure"), they compile into dynamically checked casts. Their soundness goal was that the compiler can prove these implicit casts will never fail — e.g. you can only put candies into ArrayList<Candy>, so arr.get(0).eat() is guaranteed to give you a candy you can eat. That paper demonstrates a simple 17-line program with no explicit casts that compiles yet causes run time type error. --- If you think what type soundness means, ALL statically typed languages have 2 type systems! There are execution semantics — what it means to, say, compute number + number. And there is a static language of talking about types that aims to predict / prove the types that will be involved at run time. Static checking fails if they don't match. Dynamic checking largely fails when you don't do it :-) But also when you erased info you needed to do it.