6 ms·

The JVM's type system is sound. Java's type system is not (in the sense that a program with no casts can lead to a ClassCastException). This is possible because

The JVM's type system is sound. Java's type system is not (in the sense that a program with no casts can lead to a ClassCastException). This is possible because in the process of compiling Java to the Java Bytecode, some casts (that should, in theory, never cause ClassCastExceptions) are inserted. Relevant quote from the paper: > When executed, a ClassCastException is thrown inside the main method with the message “java.lang.Integer cannot be cast to java.lang.String”. The reason is that the JVM does not directly support generics, implementing them through type erasure and type casts. This is fortunate since it causes the JVM to catch the error before it can directly cause severe problems, such as accessing memory associated with a field that is not actually present (though it might be possible that it can indirectly cause problems).

olliej 10y ago
Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type. That is the soundness guarantee, it cannot get stronger than that as the langauge allows down casts, and those are fundamentally unverifiable at compile time. Therefore the soundness of the complete type system /must/ consider the runtime behaviour. This is literally a "the type system is unsound if we don't consider the required runtime semantics of the type system" paper. Even ignoring this, the example they give is something the the typesystem correctly rejects, but what they want is a compile time failure that should be possible. I would say the if anything this is a compiler bug.
- olliej 10y ago
  Actually shamsmall (in the thread) shows the it is a compiler bug, because their compiler does reject it any compile time.
  - aseipp 10y ago
    That doesn't mean anything, really. Eclipse's compiler does not guarantee 1-to-1 correctness/equivalence with `javac` or any other compiler, so it's entirely possible that Eclipse is wrongfully rejecting this example, when it should actually accept it like `javac` does. So it is a "compiler bug", but in the other direction. The paper actually explicitly acknowledges this, Section 3 pg. 3, if you read closely. In fact there is an even bigger danger lurking, which is that Java has non-deterministic type inference. It's not even necessarily a "compiler bug" that the first example, Unsound.java, is rejected: > ... As a consequence, the method type-checks. Furthermore, even though type-argument inference in Java is undecidable, this type argument is identified by javac, version 1.8.0_25, which consequently accepts and compiles the code in Figure 1. However, constraint solving is generally a non-deterministic process, and type-argument inference itself is non-deterministic [35], so the Eclipse Compiler for Java, ecj version 3.11.1.v20150902-1521, and the current compiler for the upcoming Java 9, javac build 108, fail to type-check this code... Non-determinism means something very specific here: it does not necessarily mean the compiler randomly rejects something based on whether it's a random day of the week or because `rand() % 4 == 0`. It means the compiler has no sound method for inferring the type of a value, given multiple choices, so it "just" picks one, in an ill specified way. It could pick the first one or the second, and whichever type it picks will influence further constraint generation/inference. See this paper, section 7.2: http://www.cs.cornell.edu/~ross/publications/tamewild/tamewild-tate-pldi11-tr.pdf http://www.cs.cornell.edu/~ross/publications/tamewild/tamewi... The Eclipse compiler only coincidentally rejects one of these programs due to this type inference problem. Other valid, unsound programs are accepted by it, and these programs are unsound due to the same basic principles the original (rejected one) used. The Unsound9.java example should still work. The fact a compiler is rejecting a valid program (a bug in the eclipse compiler) is essentially orthogonal to the fact the program it rejects may show the type system is unsound (a bug in the language itself, so to speak). Furthermore your parent post is still simply wrong. You say: > Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type. But this is literally the point of the paper. They cast Integer to String, you cannot get this through downcasting alone. It is unsound. They are able to write a function of type "a" to "b" for any types "a" and "b". It's almost the textbook definition of being able to break the type system, from the viewpoint of Java-the-language. This same "cast anything to anything else" is also considered a breaking of the type system in Haskell, too, and being able to write a similar "coerce" function is Very Bad. In fact, it's very similar in theory to the way you might construct or leverage such a "bug" in Haskell. They are essentially constructing an argument to the compiler -- in the form of a type, which is how the compiler thinks -- that there is an equality between two arbitrary types A and B, so we can coerce between them. The compiler needs some evidence that this equality, this argument that A and B are the same, is legitimate. Otherwise, it rejects the argument, because it's not that gullible (it rejects the program as "this program failed to type check"). Because the argument to the compiler is made in the form of a type, the compiler considers "evidence" for that argument, to be a value of that type. So if your type makes the argument that "Integer and String are equal", then you need to represent that argument as a type, and create evidence for it by creating a value of that type. Then the compiler thinks your argument is legitimate. (This is a core central component to e.g. constructive mathematics/constructive computerized theorem proving) `null` inhabits every type, so every type contains `null`. Even the type that says "String equals Integer" has `null` as a value. Thus, we can "prove" to the compiler that yes, we can turn an Integer into a String, we have the argument (the type) and the evidence (the value) to prove it! But the evidence is actually bogus. I honestly suggest you give the original paper and the surrounding references a good reading. It all seems very sound and straightforward to me as an argument (with a bit of PLT background), and frankly I can't make heads or tails of most of your complaints in this thread, though if you're unfamiliar with the field, teasing out the subtle parts is probably a bit difficult.
- olliej 10y ago
  Just to further clarify, the existence (or not) an _explicit_ cast operator is not necessary to create an implicit cast that might fail. The dumbest case being due to the contra variant array semantics that say i can do this: Object[] foo = new String[10] foo[0] = new Integer(1) which is the type error, even if the reported error is something akin to a "array store error" or something (it's been a long time since i did java programming :D)
- moon_priestess 10y ago
  > Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type. Is it though? I always thought it was unsound due to, at a minimum, mutable covariant arrays. It's definitely possible to have a type error at runtime without using a cast.
  - johncolanduoni 10y ago
    I think they are referring to the fact that you will get a type error at runtime, instead of silently corrupting data or other undefined behavior.
    - UncleMeat 10y ago
      But the static type system is what is being evaluated here. This is like saying that python has a sound type system because the interpreter throws type errors when you fuck up.
      - eveningcoffee 10y ago
        Java allows this Integer a = 0; Object c = a; String b = (String) c; This code compiles but produces a runtime exception. The problem is here that you are allowed to upcast and this is perfectly valid code and it is developers responsibility to verify that upcast is actually valid. The problem with the code in the paper is that Java 1.5 introduced generic types, that are in principle meant easy such situations and it appears that there are some corner cases where it does not work as expected (to more general populace). For example consider this code static class Upcast { static <T extends String> String cast(T t) { return t; } } Integer a = 0; Object c = a; String b = Upcast.cast(c); This code does not compile, as we explicitly stated that we want an type that extends the String. Writing the last String b = Upcast.cast((String)c); will make the code compile, but it will produce a compiler warning and runtime exception. The paper demonstrates a more complex indirection to avoid the compiler warning but still produce a runtime exception.
- vesinisa 10y ago
  Isn't the fundamental problem here the `?` wildcard type? It allows expressing impossible types like "a super-integer that extends string", and the compiler just trusts you such type exists if you say so. Of course the whole generics system in Java is basically just "syntactic sugar" to save your from writing a ton casts, so it will just break at run-time.
  - Manishearth 10y ago
    With most type systems there's never a problem with being able to express nonexistent types. In some type systems, such "nonexistent types" itself are useful tools. (Where by "nonexistent type" I mean "a type for which there cannot be an instance". "imaginary type" might be a better term, since the type itself exists in the type system.) The problem here lies in the fact that Java lets you create an instance of any type you can write the signature for via `null`. This lies in conflict with the ability to specify nonexistent types (which is a relatively common ability in type systems and might not even be possible to excise without causing significant complexity).
- lmm 10y ago
  > That is the soundness guarantee, it cannot get stronger than that as the langauge allows down casts, and those are fundamentally unverifiable at compile time. An explicit downcast is allowed to fail at runtime. But if you can get a runtime cast failure in code that did not contain any cast, that's a soundness bug.

olliej 10y ago

Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type. That is the soundness guarantee, it cannot get stronger than that as the langauge allows down casts, and those are fundamentally unverifiable at compile time. Therefore the soundness of the complete type system /must/ consider the runtime behaviour. This is literally a "the type system is unsound if we don't consider the required runtime semantics of the type system" paper. Even ignoring this, the example they give is something the the typesystem correctly rejects, but what they want is a compile time failure that should be possible. I would say the if anything this is a compiler bug.

olliej 10y ago
Actually shamsmall (in the thread) shows the it is a compiler bug, because their compiler does reject it any compile time.
- aseipp 10y ago
  That doesn't mean anything, really. Eclipse's compiler does not guarantee 1-to-1 correctness/equivalence with `javac` or any other compiler, so it's entirely possible that Eclipse is wrongfully rejecting this example, when it should actually accept it like `javac` does. So it is a "compiler bug", but in the other direction. The paper actually explicitly acknowledges this, Section 3 pg. 3, if you read closely. In fact there is an even bigger danger lurking, which is that Java has non-deterministic type inference. It's not even necessarily a "compiler bug" that the first example, Unsound.java, is rejected: > ... As a consequence, the method type-checks. Furthermore, even though type-argument inference in Java is undecidable, this type argument is identified by javac, version 1.8.0_25, which consequently accepts and compiles the code in Figure 1. However, constraint solving is generally a non-deterministic process, and type-argument inference itself is non-deterministic [35], so the Eclipse Compiler for Java, ecj version 3.11.1.v20150902-1521, and the current compiler for the upcoming Java 9, javac build 108, fail to type-check this code... Non-determinism means something very specific here: it does not necessarily mean the compiler randomly rejects something based on whether it's a random day of the week or because `rand() % 4 == 0`. It means the compiler has no sound method for inferring the type of a value, given multiple choices, so it "just" picks one, in an ill specified way. It could pick the first one or the second, and whichever type it picks will influence further constraint generation/inference. See this paper, section 7.2: http://www.cs.cornell.edu/~ross/publications/tamewild/tamewild-tate-pldi11-tr.pdf http://www.cs.cornell.edu/~ross/publications/tamewild/tamewi... The Eclipse compiler only coincidentally rejects one of these programs due to this type inference problem. Other valid, unsound programs are accepted by it, and these programs are unsound due to the same basic principles the original (rejected one) used. The Unsound9.java example should still work. The fact a compiler is rejecting a valid program (a bug in the eclipse compiler) is essentially orthogonal to the fact the program it rejects may show the type system is unsound (a bug in the language itself, so to speak). Furthermore your parent post is still simply wrong. You say: > Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type. But this is literally the point of the paper. They cast Integer to String, you cannot get this through downcasting alone. It is unsound. They are able to write a function of type "a" to "b" for any types "a" and "b". It's almost the textbook definition of being able to break the type system, from the viewpoint of Java-the-language. This same "cast anything to anything else" is also considered a breaking of the type system in Haskell, too, and being able to write a similar "coerce" function is Very Bad. In fact, it's very similar in theory to the way you might construct or leverage such a "bug" in Haskell. They are essentially constructing an argument to the compiler -- in the form of a type, which is how the compiler thinks -- that there is an equality between two arbitrary types A and B, so we can coerce between them. The compiler needs some evidence that this equality, this argument that A and B are the same, is legitimate. Otherwise, it rejects the argument, because it's not that gullible (it rejects the program as "this program failed to type check"). Because the argument to the compiler is made in the form of a type, the compiler considers "evidence" for that argument, to be a value of that type. So if your type makes the argument that "Integer and String are equal", then you need to represent that argument as a type, and create evidence for it by creating a value of that type. Then the compiler thinks your argument is legitimate. (This is a core central component to e.g. constructive mathematics/constructive computerized theorem proving) `null` inhabits every type, so every type contains `null`. Even the type that says "String equals Integer" has `null` as a value. Thus, we can "prove" to the compiler that yes, we can turn an Integer into a String, we have the argument (the type) and the evidence (the value) to prove it! But the evidence is actually bogus. I honestly suggest you give the original paper and the surrounding references a good reading. It all seems very sound and straightforward to me as an argument (with a bit of PLT background), and frankly I can't make heads or tails of most of your complaints in this thread, though if you're unfamiliar with the field, teasing out the subtle parts is probably a bit difficult.
olliej 10y ago
Just to further clarify, the existence (or not) an _explicit_ cast operator is not necessary to create an implicit cast that might fail. The dumbest case being due to the contra variant array semantics that say i can do this: Object[] foo = new String[10] foo[0] = new Integer(1) which is the type error, even if the reported error is something akin to a "array store error" or something (it's been a long time since i did java programming :D)
moon_priestess 10y ago
> Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type. Is it though? I always thought it was unsound due to, at a minimum, mutable covariant arrays. It's definitely possible to have a type error at runtime without using a cast.
- johncolanduoni 10y ago
  I think they are referring to the fact that you will get a type error at runtime, instead of silently corrupting data or other undefined behavior.
  - UncleMeat 10y ago
    But the static type system is what is being evaluated here. This is like saying that python has a sound type system because the interpreter throws type errors when you fuck up.
    - eveningcoffee 10y ago
      Java allows this Integer a = 0; Object c = a; String b = (String) c; This code compiles but produces a runtime exception. The problem is here that you are allowed to upcast and this is perfectly valid code and it is developers responsibility to verify that upcast is actually valid. The problem with the code in the paper is that Java 1.5 introduced generic types, that are in principle meant easy such situations and it appears that there are some corner cases where it does not work as expected (to more general populace). For example consider this code static class Upcast { static <T extends String> String cast(T t) { return t; } } Integer a = 0; Object c = a; String b = Upcast.cast(c); This code does not compile, as we explicitly stated that we want an type that extends the String. Writing the last String b = Upcast.cast((String)c); will make the code compile, but it will produce a compiler warning and runtime exception. The paper demonstrates a more complex indirection to avoid the compiler warning but still produce a runtime exception.
vesinisa 10y ago
Isn't the fundamental problem here the `?` wildcard type? It allows expressing impossible types like "a super-integer that extends string", and the compiler just trusts you such type exists if you say so. Of course the whole generics system in Java is basically just "syntactic sugar" to save your from writing a ton casts, so it will just break at run-time.
- Manishearth 10y ago
  With most type systems there's never a problem with being able to express nonexistent types. In some type systems, such "nonexistent types" itself are useful tools. (Where by "nonexistent type" I mean "a type for which there cannot be an instance". "imaginary type" might be a better term, since the type itself exists in the type system.) The problem here lies in the fact that Java lets you create an instance of any type you can write the signature for via `null`. This lies in conflict with the ability to specify nonexistent types (which is a relatively common ability in type systems and might not even be possible to excise without causing significant complexity).
lmm 10y ago
> That is the soundness guarantee, it cannot get stronger than that as the langauge allows down casts, and those are fundamentally unverifiable at compile time. An explicit downcast is allowed to fail at runtime. But if you can get a runtime cast failure in code that did not contain any cast, that's a soundness bug.