Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers

We present short programs that 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 (down)casting. Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM. Nonetheless, we discuss broader implications of these findings on the field of programming languages.


Published in:
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Presented at:
OOPSLA 2016, Amsterdam, Netherlands, November 02 - 04, 2016
Year:
2015
Keywords:
Laboratories:




 Record created 2017-03-31, last modified 2018-09-13

Postprint:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)