The Unsound Playground: Java and Scala's Type Systems are Unsound

It was unsound from the first version with respect to arrays. If B is a subtype of A, then Java allows you to pass as an argument (or return) an array of B where an array of A is specified in the type signature.

To see why this is broken, consider a method that takes an array of Animal and sets the first element to be a Cat instance. Java's type system will allow you to call this method with an array of Dog which will blow up at runtime on the assignment to the array element.

I noticed this immediately when I first started using Java (version 1.0.4!) as I had just read the classic 1985 OO type systems paper by Cardelli. I didn't have an OO background and was surprised that a "modern" language like Java would have this flaw in its type system given that the problem was well known years before.

I used IntelliJ to convert the Java code into Kotlin and the compiler came up with the following errors. It does seem to do a better job of handling types:

Error:(3, 39) Kotlin: Type argument is not within its bounds: should be subtype of 'U'

Error:(5, 21) Kotlin: Type inference failed: 'B' cannot capture 'in T'. Type parameter has an upper bound 'U' that cannot be satisfied capturing 'in' projection

Error:(5, 28) Kotlin: Type mismatch: inferred type is Unsound.Constrain<U, in T>? but Unsound.Constrain<U, ???> was expected

In related news: Radu Grigore "Java generics are Turing complete" POPL'17 Preprint: https://arxiv.org/pdf/1605.05274

Scala is broken by implicit constraints as well.

Makes me wonder how Dotty would hold up under similar conditions, or whether this sort of calculus on type constraints cannot guarantee a correct return.

A sound type system is one that prevents illegal operations. Using a null reference is an illegal operation, and Java doesn't prevent this. Hasn't Java's type system been unsound all along?

Exception in thread "main" java.lang.Error: Unresolved compilation problem: The method upcast(Unsound.Constrain<U,B>, B) in the type Unsound.Bind<U> is not applicable for the arguments (Unsound.Constrain<U,capture#1-of ? super T>, T)

at Unsound.coerce(Unsound.java:13) at Unsound.main(Unsound.java:17)

Exception in thread "main" java.lang.Error: Unresolved compilation problem: The method upcast(Unsound.Constrain<U,B>, B) in the I get compilation why trying this in eclipse on Java 8 but strange when I compile it outside of it, it goes through.

type Unsound.Bind<U> is not applicable for the arguments (Unsound.Constrain<U,capture#1-of ? super T>, T)

at Unsound.coerce(Unsound.java:13) at Unsound.main(Unsound.java:17)

The headline is misleading as the type system is sound, but the general idea of generics is that the type bindings and constraints should result in a guarantee that there won't be any failing casts at runtime. And they're interpreting the failure to catch all detectable errors statically as a sign of unsoundness, which is not a correct assertion.

The Java language's half-assed generics implementation works by type erasure - so everything is boxed to Object. Because of that erasure my guess is that they're not handling inner class type binding correctly (maybe they're not able to? I don't know their compiler internals - fundamentally it _should_ be possible). If anything i'd argue that this is a compiler bug.

Anyway, the end result is a type safe (and entirely sound) runtime and language -- if it were not sound it would be possible to write code that _should_ trigger a type failure, either at compile or at runtime, but that doesn't. That is what it means to have an unsound type system, for example all C-derived languages have unsound type systems. Remember the Java has no guarantees of full static safety (the ability to downcast Object to anything ensures that they can never be fully statically typed), so as long as you're guaranteed the the runtime will never let an invalid cast or conversion happen its still correct. Another way of triggering this would be to use introspection to instantiate an instance of a generic class. Because the VM is unaware of generics you'll just get an Object interface through which you could trigger the same faults.

Footnote: .NET actually gets generics right, it's not done through erasure but actual correct type bindings. The VM is itself aware of parametric types and instances of said types and so can statically verify the IL itself, so even if you make an unsafe language that targets .NET the VM would reject illformed/unsound IL, before running it: this is VM equivalent of a static failure: it's not waiting for a dynamic cast to fail at runtime.

TLDR: We always knew null'a could float around and cause NPEs, but many assumed they couldn't convince the compiler to unsafely convert, e.g., a String to an Integer. However, since null can inhabit any type, we can use null as a proof of any proposition, for example that there exists some super type of Integer which is a subtype of String. Of course, if such a type exists we should be able to traffic an Integer to a String.

The example on the page is pretty straightforward. I encourage everyone to reason it out.

There have been some fantastic conversations on Hacker News about type systems. I've learned a lot about the different arguments for dynamic typing, versus strict typing, versus gradual typing. Java's type system may or may not have represented new thinking when it was under development in the early 1990s, but it certainly seems a bit dated in the year 2016. The limits of the Java type system have been discussed both here on HackerNews and also elsewhere, many times.

For those who want to consider arguments against Java's style of strict typing, 2 things I would recommend include "Agility & Robustness: Clojure spec, by Stuart Halloway":

https://www.youtube.com/watch?v=VNTQ-M_uSo8

He offers a chart that shows the strengths and weaknesses of strict typing versus unit tests versus the run-time checks offered by Spec. It's worth a look.

The discussions around gradual typing have been interesting, but to see how far the limits of this can be pushed, I would suggest everyone check out the Qi/Shen programming language:

https://en.wikipedia.org/wiki/Qi_(programming_language)

"Qi makes use of the logical notation of sequent calculus to define types. This type notation, under Qi’s interpretation, is actually a Turing complete language in its own right. This notation allows Qi to assign extensible type systems to Common Lisp libraries and is thought of as an extremely powerful feature of the language."

This next quote is from someone who has spent a long time experimenting with different Lisps:

"Qi (and its successor Shen) really push the limits of what we might call a Fluchtpunkt Lisp. I suspect it requires a categorization of its own. A few years ago I was looking for a Lisp to dive into and my searching uncovered two extremely interesting options: Clojure and Qi. I eventually went with Clojure, but in the intervening time I’ve managed to spend quality time with Qi and I love what I’ve seen so far. Qi’s confluence of features, including an optional type system (actually, its type system might be more accurately classified as “skinnable”), pattern matching, and an embedded logic engine based on Prolog, make it a very compelling choice indeed."

http://blog.fogus.me/2011/05/03/the-german-school-of-lisp-2/

Mark Taver, who created Shen, posted a comment and then turned it into an essay here:

"The underlined sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages – that they are losing something, a degree of freedom that the writer identifies as hampering creativity. Is this true? I will argue, to a degree – yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel's incompleteness proof [9] [11], is that the human ability to recognise truth transcends our ability to capture it formally. In computing terms our ability to recognise something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work. That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding. ...That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding. The invitation of adding types was thus taken up by myself, and the journey to making this program type secure in Shen emphasises the conclusion in this paragraph"

http://www.shenlanguage.org/library/shenpaper.pdf

I'm only quoting two favorites of mine, but of course I could post a hundred examples, all making a similar point. Java's style of strict typing is both weak and incomplete, and yet overly rigid at the same time. It's worth noting how many other strategies exist, that deliver more robustness, with greater flexibility.

In case it makes reading easier for people, here's the code with the "A, B, T, U" replaced with what they would expand to. The "that can't work" comes out pretty clear with the equivalent of "Integer-superclass which extends String" which is obvious nonsense.

    class Unsound {
      static class Constrain<AString, BSuperInteger extends AString> {}
      static class Bind<AString> {
        <BSuperInteger extends AString>
        AString upcast(Constrain<AString, BSuperInteger> constrain, BSuperInteger b) {
          return b;
        }
      }
      static <TInteger, UString> UString coerce(TInteger t) {
        Constrain<UString, ? super TInteger> constrain = null;
        Bind<UString> bind = new Bind<UString>();
        return bind.upcast(constrain, t);
      }
      public static void main(String[] args) {
        String zero = Unsound.<Integer, String>coerce(0);
      }
    }

I left the T, U, A, B as part of the name, so it's easier to map back to the original.

I wish people would stop insisting on single-character type variables. They have a purpose - name them meaningfully, like everything else.

I ran the example and I got the same result. The result that is provided, and the one I got, makes sense. Can someone explain to me what is "broken" about this?

Broken down you:

Create 3 classes - Unsound: Unsound contains a static generic method. Two types are requested (T and U). T is the parameter and the U is the return type. From now on T will be called CoerceInputType and U will be called CoerceOutputType - Constrain: A class that has two generic types it requests. A being the first type, and B who is the second type. A restriction is placed on B saying that B extends A. We will call A ConstraintType and B ExtendedConstraintType - Bind: A class that takes one generic parameter of type A. Here we will call A BindType

What is happening here?

Your execution stack:

   - *Call* Unsound.coerce. Tell it CoerceInputType is an Integer and CoerceOutputType is a String. You pass into coerce a value of '0' with the type CoerceInputType (an Integer class) and accept a result with the return type CoerceOutputType (a String class) 
   - *Assign* In Unsound.coerce you define a type Constraint<CoerceOutputType, ANYTHING extends CoerceInputType>. This means that these type annotations will be propagated through anything this is passed into. 
   - *Assign* you create an instance of bind with the type CoerceOutputType.

What this currently looks like

   <Output, AnyType that extends Input> Output ourFunction(Input i) {
      return i
   } 

What happens: You get an exception as Integer is not castable to a String. You can look further down to the only link in this page to see where that cast is coming from in the bytecode.

The authors seem to be surprised that this will not execute? Or maybe that this doesnt? This is completely expected behavior. Maybe not to someone who hasen't worked in Java and is coming from another VM but for me this is not surprising. Why? Here's a list:

The ways you can trigger a type change:

   1. Auto boxing
   2. Casting

For integers and strings, these two type conversions will not work. Here is a much more direct explanation of what's happening here:

   class Test {
      public static void main(String[] args) {
         String a = "Hello World";
         Integer b = 10;
         a = b;
      }
   }

Running this you will get the following error:

   test.java:5: error: incompatible types: Integer cannot be converted to String
   		a = b;
   		    ^
   1 error

This is because Integer cannot auto (un)box to String. This exception happens at compile time. I'll get into why in a bit.

You might also ask, "But gravypod, what about an explicit cast, will that work?" No, it will not!

   test.java:5: error: incompatible types: Integer cannot be converted to String
   		a =(String) b;
   		            ^
   1 error

This will not work at compile time as well.

Now for the next section: why will this not be picked up at compile time? Well that's a hard one to answer, the basic answer is the method isn't existent yet. Or to be closer to the truth, the method's types don't exist yet. When you use generics you're creating a method that will work on a base set of types. There isn't necessarily hard type checking on generics though. These are mainly there for the programmer, not the runtime. The runtime will operate on any data and is just expecting casting to change between types.

When run though a decompiler this is the output of Unsound.class: http://hastebin.com/sitamomogu.java

All that has happened is the compiler couldn't follow the type annotations at compile time and it was left for runtime. This should be improved, but I don't see what is broken. The time of the error just shifted. This is the same thing that happens with null. The error is not compile time when you are going to have an NPE. Instead they are runtime.

Here is example code that compiles perfectly fine:

   public class Test {
   	public static void main(String[] args) {
   		String a = null;
   		System.out.println(a.getClass().getSimpleName());
   	}
   }

When run you will get this exception:

   Exception in thread "main" java.lang.NullPointerException
   	at Test.main(Test.java:7)

I don't think that this is broken behavior as this is consistent with the way the JVM is meant to operate. Types are suggestions to the VM. This to me is a side effect of auto (un)boxing.

Maybe I'm wrong. I hope someone could tell me why if so.

Edit: Please read https://news.ycombinator.com/item?id=13051036 as this explanation is much more elegant and gets the idea across in a simpler way.

The code doesn't seem to change on click.

EDIT: Don't downvote, is anyone else having this problem?