On Tuesday, 21 November 2017 at 09:12:25 UTC, Ola Fosheim Grostad
wrote:
On Tuesday, 21 November 2017 at 06:03:33 UTC, Meta wrote:
I'm not clear on whether he means that Java's type system is
unsound, or that the type checking algorithm is unsound. From
what I can tell, he's asserting the former but describing the
latter.
He claims that type systems with existential rules,
hierarchical relations between types and null can potentially
be unsound. His complaint is that if Java had been correctly
implemented to the letter of the spec then this issue could
have led to heap corruption if exploited by a malicious
programmer.
Runtime checks are part of the type system though, so it isn't
unsound as implemented as generated JVM does runtime type
checks upon assignment.
AFAIK the complaint assumes that information from generic
constraints isn't kept on a separate level.
It is a worst case analysis of the spec...
I don't quite understand the logic here, because it seems to be
backwards reasoning. Constrain<U,? super T> is a valid type
because null inhabits it? That doesn't make sense to me. He also
cites the "implicit constraint" that X extends U where X is ?
super T, but X does not meet that constraint (Constrain<U, X
extends U>) so how can the type checker deduce that X extends U?