Confusion over generics subtyping in java specs?

Question

I'm reading java specs https://docs.oracle.com/javase/specs/jls/se10/html/jls-4.html#jls-4.10.2 and this line confuses me:

D<U1 θ,...,Uk θ>, where D<U1,...,Uk> is a generic type which is a direct supertype of the generic type C and θ is the substitution [F1:=T1,...,Fn:=Tn].

is Uk θ here casting? and after substitution D becomes D<(U1)T1,...,(Uk)Tk>? If so why does the author omit the brackets in Uk θ as part of casting syntax? Thanks!

Archdiocese

Interestingly, the JLS mercifully decided to do away with this inscrutable construction; see, for example, the same section in JLS 17: docs.oracle.com/javase/specs/jls/se17/html/… – Florinda

Answer 1

Given a generic type declaration C<F1,...,Fn> (n > 0), the direct supertypes of the parameterized type C<T1,...,Tn>, where Ti (1 ≤ i ≤ n) is a type, are all of the following:

D<U1 θ,...,Uk θ>, where D<U1,...,Uk> is a generic type which is a direct supertype of the generic type C<F1,...,Fn> and θ is the substitution [F1:=T1,...,Fn:=Tn].

Let us see an example.

public class D<U1,U2> {
}

//Note the order of F3,F4.
class C<F1,F2,F3,F4> extends D<F4,F3>{

}

class Main{

    public static void main(String[] args) {

        C<Integer,String,Float,Number> obj = new C<>();

        D<Float ,Number> obj2 = obj; // Compilation error

        D<Number ,Float> obj3 = obj; //This is fine


    }
}

What do you think θ is here ?

θ = [F1:= Integer , F2:= String, F3:= Float, F4:= Number ]

Now D<Number,Float> is the correct supertype. But not D<Float,Number>. Why ?

Because of Ui θ. So what does this mean ?

Well , it just means substitute i.e. Scan U1 , U2 , ... till Uk and if you find any Fi , then replace it by Ti.

In our example , it means Scan F4 and F3 of class D. Did you have F4 and F3 in θ ? Yes. Then F4,F3 of D have to be as defined in θ.

Note : The answer is as per my understanding. I don't have any concrete reference of what Uk θ means in Java type semantics.

Ranchman

Thank you very much! That really makes a lot of sense! Just one tiny point I think is that there should be a constrain k <= n, although the java doc doesn't mention that whatsoever. Thanks again! – Archdiocese

Good point. Even I was thinking that. But then if you notice , they are applying θ on each U1, U2 ,... ,Uk. This clearly means that {U1, U2 ,... ,Uk} is subset of {F1,F2,..,Fn} as each Ui have to one of the F's as they are all type parameter and not type argument. This means k<=n. Again, this is my guess. Not very sure. – Ranchman

You're absolutely right, k <= n ought to be a prerequisite of using Uk θ so no need to explicitly denote that. – Archdiocese

Answer 2

Not casting. It's the mathy language used to describe a type.

In code, it's saying that if:

interface D<A, B> {}
interface C<A, B> extends D<A, B> {}

class Y implements D<String, Number> {}
class X implements C<String, Integer> {} // Note Integer is a subtype of Number

Then this compiles:

D d = new X();

Transcript

Thanks Bohemian your code is very insightful but I'm still bit confused. I learned from another post that := means assignment. However I can't find anything about the usage of Uk θ, it may be some sort of math transform notation but I still wonder is there any formal definition of that? – Archdiocese

@Archdiocese I greatly appreciate your question and your focus. I had the same question, and I too cannot find an answer. Perhaps my phrasing may help you. #69503323 – Florinda