Hacker News Reader

I don't see the headline as misleading at all. There are two type systems in Java: the JVM's run-time type system, and Java's compile time type system. It's the latter that has been shown to be unsound. As the paper notes, it's fortunate that generics have been implemented with type erasure, because that is what saves the JVM from being unsound, too.

As for the problem itself: it really has nothing to do with inner classes (they are static in the example!). The problem is with this line:

    Constrain<U,? super T> constrain = null;

which leads the type system to assume that there is a type that is a superclass of T, which also is a subclass of B (from the 'Constrain' class) - even though no such type could possibly exist! The evil trick is in the 'null' - even though a type with the stated constraints is impossible, and so no actual 'real' value of this generic type could exist, 'null' is part of all types, so the compiler can't see the problem.

It really is a problem in the type system as defined in the standard, not just a compiler bug.

Do you have a spec reference for that (not trying to be a dick - i just want to understand what the type system believes it should be doing here as the value being assigned to a reference should not influence the type system behaviour)

This is explained in the article in a bit more detail. The point is not that the type system does something with the actual value - the point is that it would be impossible to create any code that results in such a value (other than null), since then you would have to provide an actual type that is somewhere between Integer and String - and that would obviously not pass the type checking. Using null avoids that.

Section 4.5 in the language spec deals with parameterized types; 4.5.1 deals with wildcards. Of course, there is no example in the specs that clearly points out what happens in this example - otherwise this wouldn't have remained undiscovered for so many years :)

If you can show, using the rules in the spec, that the sample program shouldn't pass type checking, then you'll have proved the article wrong :-)

Good point with the null, they have an example without the null keyword which is an even dirtier trick (because it is still null).

https://github.com/namin/unsound/blob/master/Nullless.java

Yes, it's all about nulls. I was curious to break it down from Curry-Howard correspondence (Types as Propositions) point of view. The line

  static class Constrain<A, B extends A> {}

reads as

  for all propositions A and B, such that B implies A, proposition Constrain<A, B> holds.

While, the line:

  Constrain<U,? super T> constrain = null;

kind of says:

  Admit that there exists type X, such that T implies X, for which Constrain<U, X> holds.

Even though no proof (read constructed instance) that X implies U is provided.

If we look at concrete execution instance with String and Integer:

String implies Object, Serializable, Comparable<String>, CharSequence. None of those imply/extend Integer, which is required for truthful Constrain<U, ? super T> proposition.

Basically, ex falso quodlibet :)

EDIT: spacing, formatting, wording.

The JVM's type system is sound. Java's type system is not (in the sense that a program with no casts can lead to a ClassCastException). This is possible because in the process of compiling Java to the Java Bytecode, some casts (that should, in theory, never cause ClassCastExceptions) are inserted.

Relevant quote from the paper:

> When executed, a ClassCastException is thrown inside the main method with the message “java.lang.Integer cannot be cast to java.lang.String”. The reason is that the JVM does not directly support generics, implementing them through type erasure and type casts. This is fortunate since it causes the JVM to catch the error before it can directly cause severe problems, such as accessing memory associated with a field that is not actually present (though it might be possible that it can indirectly cause problems).

Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type. That is the soundness guarantee, it cannot get stronger than that as the langauge allows down casts, and those are fundamentally unverifiable at compile time. Therefore the soundness of the complete type system /must/ consider the runtime behaviour.

This is literally a "the type system is unsound if we don't consider the required runtime semantics of the type system" paper.

Even ignoring this, the example they give is something the the typesystem correctly rejects, but what they want is a compile time failure that should be possible. I would say the if anything this is a compiler bug.

Actually shamsmall (in the thread) shows the it is a compiler bug, because their compiler does reject it any compile time.

That doesn't mean anything, really. Eclipse's compiler does not guarantee 1-to-1 correctness/equivalence with `javac` or any other compiler, so it's entirely possible that Eclipse is wrongfully rejecting this example, when it should actually accept it like `javac` does. So it is a "compiler bug", but in the other direction.

The paper actually explicitly acknowledges this, Section 3 pg. 3, if you read closely. In fact there is an even bigger danger lurking, which is that Java has non-deterministic type inference. It's not even necessarily a "compiler bug" that the first example, Unsound.java, is rejected:

> ... As a consequence, the method type-checks. Furthermore, even though type-argument inference in Java is undecidable, this type argument is identified by javac, version 1.8.0_25, which consequently accepts and compiles the code in Figure 1. However, constraint solving is generally a non-deterministic process, and type-argument inference itself is non-deterministic [35], so the Eclipse Compiler for Java, ecj version 3.11.1.v20150902-1521, and the current compiler for the upcoming Java 9, javac build 108, fail to type-check this code...

Non-determinism means something very specific here: it does not necessarily mean the compiler randomly rejects something based on whether it's a random day of the week or because `rand() % 4 == 0`. It means the compiler has no sound method for inferring the type of a value, given multiple choices, so it "just" picks one, in an ill specified way. It could pick the first one or the second, and whichever type it picks will influence further constraint generation/inference. See this paper, section 7.2:

http://www.cs.cornell.edu/~ross/publications/tamewild/tamewi...

The Eclipse compiler only coincidentally rejects one of these programs due to this type inference problem. Other valid, unsound programs are accepted by it, and these programs are unsound due to the same basic principles the original (rejected one) used. The Unsound9.java example should still work.

The fact a compiler is rejecting a valid program (a bug in the eclipse compiler) is essentially orthogonal to the fact the program it rejects may show the type system is unsound (a bug in the language itself, so to speak).

Furthermore your parent post is still simply wrong. You say:

> Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type.

But this is literally the point of the paper. They cast Integer to String, you cannot get this through downcasting alone. It is unsound. They are able to write a function of type "a" to "b" for any types "a" and "b". It's almost the textbook definition of being able to break the type system, from the viewpoint of Java-the-language. This same "cast anything to anything else" is also considered a breaking of the type system in Haskell, too, and being able to write a similar "coerce" function is Very Bad.

In fact, it's very similar in theory to the way you might construct or leverage such a "bug" in Haskell. They are essentially constructing an argument to the compiler -- in the form of a type, which is how the compiler thinks -- that there is an equality between two arbitrary types A and B, so we can coerce between them. The compiler needs some evidence that this equality, this argument that A and B are the same, is legitimate. Otherwise, it rejects the argument, because it's not that gullible (it rejects the program as "this program failed to type check"). Because the argument to the compiler is made in the form of a type, the compiler considers "evidence" for that argument, to be a value of that type. So if your type makes the argument that "Integer and String are equal", then you need to represent that argument as a type, and create evidence for it by creating a value of that type. Then the compiler thinks your argument is legitimate. (This is a core central component to e.g. constructive mathematics/constructive computerized theorem proving)

`null` inhabits every type, so every type contains `null`. Even the type that says "String equals Integer" has `null` as a value. Thus, we can "prove" to the compiler that yes, we can turn an Integer into a String, we have the argument (the type) and the evidence (the value) to prove it! But the evidence is actually bogus.

I honestly suggest you give the original paper and the surrounding references a good reading. It all seems very sound and straightforward to me as an argument (with a bit of PLT background), and frankly I can't make heads or tails of most of your complaints in this thread, though if you're unfamiliar with the field, teasing out the subtle parts is probably a bit difficult.

Just to further clarify, the existence (or not) an _explicit_ cast operator is not necessary to create an implicit cast that might fail. The dumbest case being due to the contra variant array semantics that say i can do this:

Object[] foo = new String[10] foo[0] = new Integer(1)

which is the type error, even if the reported error is something akin to a "array store error" or something (it's been a long time since i did java programming :D)

> Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type.

Is it though? I always thought it was unsound due to, at a minimum, mutable covariant arrays. It's definitely possible to have a type error at runtime without using a cast.

I think they are referring to the fact that you will get a type error at runtime, instead of silently corrupting data or other undefined behavior.

But the static type system is what is being evaluated here. This is like saying that python has a sound type system because the interpreter throws type errors when you fuck up.

Java allows this

  Integer a = 0;
  Object c = a;
  String b = (String) c;

This code compiles but produces a runtime exception. The problem is here that you are allowed to upcast and this is perfectly valid code and it is developers responsibility to verify that upcast is actually valid.

The problem with the code in the paper is that Java 1.5 introduced generic types, that are in principle meant easy such situations and it appears that there are some corner cases where it does not work as expected (to more general populace).

For example consider this code

  static class Upcast {
    static <T extends String> String cast(T t) {
      return t;
    }
  }

  Integer a = 0;
  Object c = a;   
  String b = Upcast.cast(c);

This code does not compile, as we explicitly stated that we want an type that extends the String. Writing the last

  String b = Upcast.cast((String)c);

will make the code compile, but it will produce a compiler warning and runtime exception.

The paper demonstrates a more complex indirection to avoid the compiler warning but still produce a runtime exception.

Isn't the fundamental problem here the `?` wildcard type? It allows expressing impossible types like "a super-integer that extends string", and the compiler just trusts you such type exists if you say so.

Of course the whole generics system in Java is basically just "syntactic sugar" to save your from writing a ton casts, so it will just break at run-time.

With most type systems there's never a problem with being able to express nonexistent types. In some type systems, such "nonexistent types" itself are useful tools.

(Where by "nonexistent type" I mean "a type for which there cannot be an instance". "imaginary type" might be a better term, since the type itself exists in the type system.)

The problem here lies in the fact that Java lets you create an instance of any type you can write the signature for via `null`. This lies in conflict with the ability to specify nonexistent types (which is a relatively common ability in type systems and might not even be possible to excise without causing significant complexity).

> That is the soundness guarantee, it cannot get stronger than that as the langauge allows down casts, and those are fundamentally unverifiable at compile time.

An explicit downcast is allowed to fail at runtime. But if you can get a runtime cast failure in code that did not contain any cast, that's a soundness bug.

.NET doesn't get generics right, having type erasure is among the best features of Java.

The actual reason for why you feel the need for reification is because the type systems of both C# and Java are so poor that you end up in situations where you really need to do "isInstanceOf" checks and castings. But people are missing the forest from the trees here, because these are essentially holes in the type-system, only needed because the languages are not expressive enough. Because really, you don't really need to check whether something is an instance of "List<int>" at runtime, in a static language, unless your language sucks ;-)

As to why type erasure is among the best features of Java, that's because with reification it gets hard to support other languages. It's kind of ironic, but .NET CLR was once marketed as the multi-language runtime, but time has been on the JVM's side in that regard.

For example F# doesn't support higher-kinded types because the CLR doesn't support higher-kinded types and introducing support for HKT would mean for the F# compiler to basically do type erasure by itself, which would place it at a serious disadvantage versus the host language in terms of performance. Scala supports higher-kinded types, which means you can express in Scala types such as the Monad and the Applicative, which are essential for FP in static languages, without sacrificing performance or Java interoperability. Even OCaml supports higher-kinded types.

And this isn't just about static languages. Pick any dynamic language you can think of, take your pick from Ruby, Python, Clojure and Javascript and compare the performance of the implementations on the JVM versus the CLR. OK, it's sort of an unfair comparison, given the JVM implementations have had more resources invested in them, but you know, one of the reasons for why dynamic languages work better on top of the JVM is because the JVM's bytecode is basically dynamically typed, with the last barriers being brought down along with invokedynamic. But by introducing generics reification on the other hand you end up with more static info in the bytecode that dynamic languages have to work around.

The only clear advantage to reification is the specialization for primitives that the CLR is doing for things like the standard collections. But you know, this can be a job for the compiler, you don't actually need the runtime to do specialization (see Scala's miniboxing or Dotty) and even if the runtime does specialization, you don't need it to do .NET-like reification (at least the Java engineers claim that, having plans to do primitive specialization for Java 10 or something).

F# already does type erasure in some circumstances with Type Providers (erased vs. generated types).

F* runs on the CLR and has higher kinded polymorphism.

Also, while the JVM multi-language story is terrific, it's not like the CLI is severely wanting since it also has several world-class language implementations:

* C#

* VB (criminally underrated; it's not just C# with another costume)

* F#

* F* (real dependent types)

* C++/CLI

* Nemerle (like C#, but with real macros and pattern-matching)

* PowerShell

* IronPython

> Because really, you don't really need to check whether something is an instance of "List<int>" at runtime, in a static language, unless your language sucks ;-)

So, I hate reflection with a burning passion, but this is wrong. You may not like doing it, but there are tons of legitimate use cases for RTTI.

My primary case is for runtime "light-up" of advanced features. For instance, if you deploy an application to a series of platforms that provide non-overlapping sets of capabilities, a fantastic way of dealing with this problem is to use RTTI to check whether the instance of the object is some specialized case at runtime, then cast to the specialized object to use the specific features (e.g., GPS, touch screen) that are only available on that platform.

The problem with .NET reflection is not that this dynamism exists, it's that everything is bundled together without an opt-out. I would love to have reflection split into small pieces that I could pick and choose from -- maybe I get RTTI, but I can't instantiate arbitrary generic types at runtime, for instance. Or I can't do RefEmit to JIT dynamically generated IL.

These play havoc with the runtime, forcing it to support incredibly elaborate systems just for simple features, so providing some guarantees would make the runtime's job way easier while also providing developer flexibility.

> The problem with .NET reflection is not that this dynamism exists, it's that everything is bundled together without an opt-out. I would love to have reflection split into small pieces that I could pick and choose from -- maybe I get RTTI, but I can't instantiate arbitrary generic types at runtime, for instance. Or I can't do RefEmit to JIT dynamically generated IL.

Something like mirrors?

C++'s ability to selectively turn off features drives me crazy, as I either need to convince myself to live without RTTI and exceptions or live without most of the libraries that exist.

Specially given the mentality of micro-benchmarking code lines without profiling.

It is also the cause of quite a few C++ warts, because the library code needs to be written assuming those features can be disabled.

> having type erasure is among the best features of Java

Until you try to use something like a List<int> without wasting incredible amounts of memory. This is even worse in a VM with custom value types (like the CLR), which also have to deal with boxing.

> For example F# doesn't support higher-kinded types because the CLR doesn't support higher-kinded types and introducing support for HKT would mean for the F# compiler to basically do type erasure by itself, which would place it at a serious disadvantage versus the host language in terms of performance.

So the solution is to push the performance disadvantage into the VM so all languages are equally screwed?

My original message contains your acknowledgement and answers to your question. Please re-read it.

Cheers,

To be fair, there's absolutely nothing wrong with type erasure, except when you allow runtime reflection.

If there is no reflection, then it shouldn't be possible to observe whether or not type erasure is done.

It really depends at what level -- because the erasure is done at the language level rather than the VM you _have_ to have a pile of runtime casts, even when those casts are no-ops :-/

I agree it works, i just don't think it's as elegant :D

Of course eventually everything is running on an untyped CPU and everything is just an integer so it's all erased in the end. Unless you have one of those silly mid-90s java cpus right?

Or maybe a LISP-machine

> silly mid-90s java cpus

They are still quite actual, here is one example.

http://www.imsystech.com/products/im3910-ic/

Well, that's a detail of how the VM works. My only point was that type erasure is not inherently bad, as plenty of languages do type erasure, like Haskell and OCaml. Of course you can always create conditions where it could become a problem.

But the example with C# "doing it right" is a little odd in that case, since Microsoft had the opportunity to build something new, that didn't have the same issues the JVM had. And they did, in some ways, but that doesn't mean tracking type parameters at the VM level is the only way to do it "right".

Even without full-blown reflection, the problem is that you don't have an "is instance of" operation for unerased types. Which is crucial to case/match as used in Scala and functional programming in general.

It is not crucial for functional programming, unless your functional programming language uses types as variant tags.

Both Haskell and OCaml use type erasure, and I doubt anyone would claim they aren't functional languages.

If they store a variant tag, that means they don't erase the bit of info that's needed for case matching. My point is that it's crucial to be able to tell at runtime to which (sub)type a value belongs. Other type information that isn't necessary for that can still be erased.

I think we're in agreement, and just tripping over terminology. In most functional languages, values in a variant are just values in that variant. They don't each have their own type, which means the variant tag isn't actually type information.

You can observe it on the JVM when you realise you can't overload a function with arguments that differ only in generic type.

Yes, my point was that there's nothing inherently wrong with type erasure. You can of course create conditions that would be problematic, like the design of Java and JVM does.

Haskell erases its generics and its type system's "generics" are superior to C#'s in every way. Erasure is not a problem.

Proper type specialization has its downsides in compile time and binary sizing. Ideally you would have the option of doing one or the other depending on your situation.

Not if done correctly -- for a JITted language the IL does not increase in size for generic types as the IL still only has a single version (with the type parameters). The JIT can share the code for the majority of Object/Reference instantiations (strictly it could share all object code if it put appropriate type metadata into the in memory class representation).

For value types you do need different copies for the various sizes of type parameter, but even then your heap overhead is reduced because you no longer need to box every value. E.g. you no longer need to make an object to wrap an int. So i suspect on balance you reduce the total space requirements.

FWIW, this is exactly how .NET does this. Generic instantiations are shared between all reference types (at runtime, you can sometimes see this leaking into visible abstractions in form of System.__Canon pseudo-type in call stacks etc), but separate instantiations are produced for every value type.

>.NET actually gets generics right, it's not done through erasure but actual correct type bindings.

Type erasure is one of the main reasons why there are so many different languages available on the JVM. It's also why there isn't a need for another runtime to run on top on the existing runtime just to support dynamic languages.