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.
Cite this item
Amin, N., & Tate, R. (2015). Java and Scala’s Type Systems are Unsound: The Existential Crisis of Null Pointers. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA 2016, Amsterdam, Netherlands. https://doi.org/10.1145/2983990.2984004
Click Copy to copy the citation, or select the text manually.
unsound-oopsla.pdf
Postprint
Accepted version
openaccess
214.96 KB
Adobe PDF
88298b0959bd9943935eed55d6b7c600