What are the benefits of Java's types erasure?

Question

I read a tweet today that said:

It's funny when Java users complain about type erasure, which is the only thing Java got right, while ignoring all the things it got wrong.

Thus my question is:

Are there benefits from Java's type erasure? What are the technical or programming style benefits it (possibly) offers other than the JVM implementations preference for backwards compatibility and runtime performance?

Answer 1

Type Erasure Is Good

Let's stick to the facts

A lot of the answers thus far are overly concerned with the Twitter user. It's helpful to keep focused on the messages and not the messenger. There is a fairly consistent message with even just the excerpts mentioned thus far:

It's funny when Java users complain about type erasure, which is the only thing Java got right, while ignoring all the things it got wrong.

I get huge benefits (e.g. parametricity) and nil cost (alleged cost is a limit of imagination).

new T is a broken program. It is isomorphic to the claim "all propositions are true." I am not big into this.

A goal: reasonable programs

These tweets reflect a perspective that is not interested in whether we can make the machine do something, but more whether we can reason that the machine will do something we actually want. Good reasoning is a proof. Proofs can be specified in formal notation or something less formal. Regardless of the specification language, they must be clear and rigorous. Informal specifications are not impossible to structure correctly, but are often flawed in practical programming. We end up with remediations like automated and exploratory tests to make up for the problems we have with informal reasoning. This is not to say that testing is intrinsically a bad idea, but the quoted Twitter user is suggesting that there is a much better way.

So our goal is to have correct programs that we can reason about clearly and rigorously in a way that corresponds with how the machine will actually execute the program. This, though, is not the only goal. We also want our logic to have a degree of expressivity. For example, there's only so much we can express with propositional logic. It's nice to have universal (∀) and existential (∃) quantification from something like first-order logic.

Using type systems for reasoning

These goals can be very nicely addressed by type systems. This is especially clear because of the Curry-Howard correspondence. This correspondence is often expressed with the following analogy: types are to programs as theorems are to proofs.

This correspondence is somewhat profound. We can take logical expressions, and translate them through the correspondence to types. Then if we have a program with the same type signature that compiles, we have proven that the logical expression is universally true (a tautology). This is because the correspondence is two-way. The transformation between the type/program and the theorem/proof worlds are mechanical, and can in many cases be automated.

Curry-Howard plays nicely into what we'd like to do with specifications for a program.

Are type systems useful in Java?

Even with an understanding of Curry-Howard, some people find it easy to dismiss the value of a type system, when it

1. is extremely hard to work with
2. corresponds (through Curry-Howard) to a logic with limited expressivity
3. is broken (which gets to the characterization of systems as "weak" or "strong").

Regarding the first point, perhaps IDEs make Java's type system easy enough to work with (that's highly subjective).

Regarding the second point, Java happens to almost correspond to a first-order logic. Generics give use the type system equivalent of universal quantification. Unfortunately, wildcards only give us a small fraction of existential quantification. But universal quantification is pretty good start. It's nice to be able to say that functions for List<A> work universally for all possible lists because A is completely unconstrained. This leads to what the Twitter user is talking about with respect to "parametricity."

An often-cited paper about parametricity is Philip Wadler's Theorems for free!. What's interesting about this paper is that from just the type signature alone, we can prove some very interesting invariants. If we were to write automated tests for these invariants we would be very much wasting our time. For example, for List<A>, from the type signature alone for flatten

<A> List<A> flatten(List<List<A>> nestedLists); 

we can reason that

flatten(nestedList.map(l -> l.map(any_function)))     ≡ flatten(nestList).map(any_function) 

That's a simple example, and you can probably reason about it informally, but it's even nicer when we get such proofs formally for free from the type system and checked by the compiler.

Not erasing can lead to abuses

From the perspective of language implementation, Java's generics (which correspond to universal types) play very heavily into the parametricity used to get proofs about what our programs do. This gets to the third problem mentioned. All these gains of proof and correctness require a sound type system implemented without defects. Java definitely has some language features that allow us to shatter our reasoning. These include but are not limited to:

• side-effects with an external system
• reflection

Non-erased generics are in many ways related to reflection. Without erasure there's runtime information that's carried with the implementation that we can use to design our algorithms. What this means is that statically, when we reason about programs, we don't have the full picture. Reflection severely threatens the correctness of any proofs we reason about statically. It's no coincidence reflection also leads to a variety of tricky defects.

So what are ways that non-erased generics might be "useful?" Let's consider the usage mentioned in the tweet:

<T> T broken { return new T(); } 

What happens if T doesn't have a no-arg constructor? In some languages what you get is null. Or perhaps you skip the null value and go straight to raising an exception (which null values seem to lead to anyway). Because our language is Turing complete, it's impossible to reason about which calls to broken will involve "safe" types with no-arg constructors and which ones won't. We've lost the certainty that our program works universally.

Erasing means we've reasoned (so let's erase)

So if we want to reason about our programs, we're strongly advised to not employ language features that strongly threaten our reasoning. Once we do that, then why not just drop the types at runtime? They're not needed. We can get some efficiency and simplicity with the satisfaction that no casts will fail or that methods might be missing upon invocation.

Erasing encourages reasoning.

Answer 2

Types are a construct used for writing programs in a manner that allows the compiler to check the correctness of a program. A type is a proposition on a value - the compiler verifies that this proposition is true.

During the execution of a program, there should be no need for type information - this has already been verified by the compiler. The compiler should be free to discard this information in order to perform optimisations on the code - make it run faster, generate a smaller binary etc. Erasure of type parameters facilitates this.

Java breaks static typing by allowing type information to be queried at runtime - reflection, instanceof etc. This allows you to construct programs that cannot be statically verified - they bypass the type system. It also misses opportunities for static optimisation.

The fact that type parameters are erased prevents some instances of these incorrect programs to be constructed, however, more incorrect programs would be disallowed if more type information was erased and the reflection and instanceof facilities were removed.

Erasure is important for upholding the property of "parametricity" of a data type. Say I have a type "List" parameterised over component type T. i.e. List<T>. That type is a proposition that this List type works identically for any type T. The fact that T is an abstract, unbounded type parameter means that we know nothing about this type, therefore are prevented from doing anything special for special cases of T.

e.g. say I have a List xs = asList("3"). I add an element: xs.add("q"). I end up with ["3","q"]. Since this is parametric, I can assume that List xs = asList(7); xs.add(8) ends up with [7,8] I know from the type that it doesn't do one thing for String and one thing for Int.

Furthermore, I know that the List.add function can not invent values of T out of thin air. I know that if my asList("3") has a "7" added to it, the only possible answers would be constructed out of the values "3" and "7". There is no possibility of a "2" or "z" being added to the list because the function would be unable to construct it. Neither of these other values would be sensible to add, and parametricity prevents these incorrect programs from being constructed.

Basically, erasure prevents some means of violating parametricity, thus eliminating possibilities of incorrect programs, which is the goal of static typing.