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.