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:
Acm Sigplan Notices, 51, 10, 838-848
Presented at:
ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Amsterdam, NETHERLANDS, NOV 02-04, 2016
Year:
2016
Publisher:
New York, Assoc Computing Machinery
ISSN:
0362-1340
Keywords:
Laboratories:




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

Postprint:
Download fulltext
PDF

Rate this document:

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