Java Generics are Turing Complete

TL;DR

This paper proves that Java's subtype checking is undecidable by reducing the halting problem to it, demonstrating its Turing completeness and implications for recognizing recursive languages.

Contribution

It establishes that Java's subtype checking is Turing complete and undecidable, answering a longstanding open question and extending previous results on Java's type system capabilities.

Findings

Subtype checking in Java is undecidable due to Turing completeness.

Java's type checker can recognize any recursive language.

A parser generator for fluent interfaces demonstrates the practical implications.

Abstract

This paper describes a reduction from the halting problem of Turing machines to subtype checking in Java. It follows that subtype checking in Java is undecidable, which answers a question posed by Kennedy and Pierce in 2007. It also follows that Java's type checker can recognize any recursive language, which improves a result of Gil and Levy from 2016. The latter point is illustrated by a parser generator for fluent interfaces.