unsound
unsound copied to clipboard
Artifact for OOPSLA'16 Paper on Unsoundness of Java and Scala
Artifact for Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers
We provide the three programs as listed in the paper (Amin and Tate, OOPSLA'16 forthcoming), and step-by-step instructions on how to compile and run them. We also offer an interactive playground.
-
Unsound.java
for Java 8 -
Unsound9.java
for Java 9 -
unsound.scala
for Scala
These short programs demonstrate the unsoundness of Java and Scala’s current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without casting. Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM
Getting Started Guide
You need JDK 8, JDK 9, Scala 2.11.8.
You need to be able to use javac
, java
, scalac
, scala
.
You need to be able to switch between JDK 8 and JDK 9.
We give further pointers within the step by step instructions below.
Step-by-Step Instructions
Java
JDK 8 (Download)
Step 1: Check version
java -version
java version "1.8.0_25"
Java(TM) SE Runtime Environment (build 1.8.0_25-b17)
Java HotSpot(TM) 64-Bit Server VM (build 25.25-b02, mixed mode)
If necessary, switch to JDK 8:
export JAVA_HOME=$(/usr/libexec/java_home -v 1.8) ; PATH=$JAVA_HOME/bin:$PATH
Step 2: Compile
javac Unsound.java
(compiles OK)
Step 3: Run
java Unsound
Exception in thread "main" java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
at Unsound.main(Unsound.java:15)
JDK 9 (Download)
Step 1: Check version
java -version
java version "9-ea"
Java(TM) SE Runtime Environment (build 9-ea+121)
Java HotSpot(TM) 64-Bit Server VM (build 9-ea+121, mixed mode)
If necessary, switch to JDK 9:
export JAVA_HOME=$(/usr/libexec/java_home -v 9) ; PATH=$JAVA_HOME/bin:$PATH
Step 2: Compile
javac Unsound9.java
(compiles OK)
Note that Unsound.java
does not compile with JDK 9.
javac Unsound.java
Unsound.java:12: error: method upcast in class Bind<A> cannot be applied to given types;
return bind.upcast(constrain, t);
^
required: Constrain<U,B>,B
found: Constrain<U,CAP#1>,T
reason: inference variable B has incompatible bounds
upper bounds: U
lower bounds: T
where U,T,B,A are type-variables:
U extends Object declared in method <T,U>coerce(T)
T extends Object declared in method <T,U>coerce(T)
B extends U declared in method <B>upcast(Constrain<A,B>,B)
A extends Object declared in class Bind
where CAP#1 is a fresh type-variable:
CAP#1 extends U super: T from capture of ? super T
1 error
Step 3: Run
java Unsound9
Exception in thread "main" java.lang.ClassCastException: java.lang.Integer (in module: java.base) cannot be cast to java.lang.String (in module: java.base)
at Unsound9.main(Unsound9.java:25)
Scala (Download)
Step 1: Check version
scala -version
Scala code runner version 2.11.8 -- Copyright 2002-2016, LAMP/EPFL
java -version
java version "1.8.0_25"
Java(TM) SE Runtime Environment (build 1.8.0_25-b17)
Java HotSpot(TM) 64-Bit Server VM (build 25.25-b02, mixed mode)
Scala does not support JDK 9 yet, so switch back to JDK 8 if necessary.
You can also switch back to an earlier JDK, e.g. 6, to try the steps with more previous versions of Scala (download list).
The earliest version we could get to work with JDK 8 is 2.10.2, and all the releases we sampled in between up to the current milestone 2.12.0-M4 reproduce the remaining steps.
The example does not compile in Scala 2.9.3 and earlier due to restrictions on dependent method types. In unsound_legacy.scala
, we give an example without dependent method types that exhibits the same issue using only features already available in Scala 2.5.0.
Step 2: Compile
scalac unsound.scala
(compiles OK)
Step 3: Run
scala unsound
java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
at unsound$.main(unsound.scala:14)
at unsound.main(unsound.scala)
at ...