4

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!

Number945
  • 4,631
  • 8
  • 45
  • 83
mzoz
  • 1,273
  • 1
  • 14
  • 28
  • Interestingly, the JLS mercifully decided to do away with this inscrutable construction; see, for example, the same section in JLS 17: https://docs.oracle.com/javase/specs/jls/se17/html/jls-4.html#jls-4.10.2 – Laird Nelson Oct 09 '21 at 05:01

2 Answers2

3

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.

Number945
  • 4,631
  • 8
  • 45
  • 83
  • 1
    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! – mzoz Jul 21 '18 at 05:34
  • 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. – Number945 Jul 21 '18 at 06:03
  • You're absolutely right, `k <= n` ought to be a prerequisite of using `Uk θ` so no need to explicitly denote that. – mzoz Jul 21 '18 at 12:08
1

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();
Bohemian
  • 412,405
  • 93
  • 575
  • 722
  • 1
    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? – mzoz Jul 21 '18 at 04:56
  • @mzoz 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. https://stackoverflow.com/questions/69502823/in-the-java-language-specification-version-11-section-4-10-2-how-do-i-read-u%e2%82%96 – Laird Nelson Oct 09 '21 at 04:59