Understanding captured conversion

Question

I am trying to undertand how captured conversion works for wildcard types. There is a section in JLS explaining that:

Let G name a generic type declaration (§8.1.2, §9.1.2) with n type parameters A1,...,An with corresponding bounds U1,...,Un.

There exists a capture conversion from a parameterized type G<T1,...,Tn> (§4.5) to a parameterized type G<S1,...,Sn>, where, for 1 ≤ i ≤ n :

• If Ti is a wildcard type argument (§4.5.1) of the form ?, then Si is a fresh type variable whose upper bound is Ui[A1:=S1,...,An:=Sn] and whose lower bound is the null type (§4.1).

• If Ti is a wildcard type argument of the form ? extends Bi, then Si is a fresh type variable whose upper bound is glb(Bi, Ui[A1:=S1,...,An:=Sn]) and whose lower bound is the null type.

  glb(V1,...,Vm) is defined as V1 & ... & Vm.

  It is a compile-time error if, for any two classes (not interfaces) Vi and Vj, Vi is not a subclass of Vj or vice versa.

• If Ti is a wildcard type argument of the form ? super Bi, then Si is a fresh type variable whose upper bound is Ui[A1:=S1,...,An:=Sn] and whose lower bound is Bi.

• Otherwise, Si = Ti.

The thing that is not clear to me is Ui[A1:=S1,...,An:=Sn]. What does it mean? I could not find a definition for that searching through the JLS.

Answer 1

First: define substitution.

[A1:=S1,...,An:=Sn] is a substitution in JLS notation (§1.3), defined as:

The notation [F1:=T1,...,Fn:=Tn] denotes substitution of Fi by Ti for 1 ≤ i ≤ n.

Statement: [A1:=S1,...,An:=Sn] is the substitution of the type parameter (of G) Ai by the type variable Si for 1 ≤ i ≤ n. (also see footnote ^†)

Next: consider why we might need substitution in the first case. From §5.1.10 (highlighting added to drive home the next point):

Let G name a generic type declaration ... with n type parameters A1,...,An with corresponding bounds U1,...,Un.

That is:

• the bounds U1,...,Un correspond specifically to the type parameters A1,...,An.
• the unstated corollary: the bounds U1,...,Un do not correspond to the type variables S1,...,Sn.

Putting it together: I'm now stating the obvious as I'm sure you are ahead of me, but ...

Regarding the rule for "Ti is a wildcard type argument ... of the form ?")

Si is a fresh type variable whose upper bound is Ui [A1:=S1,...,An:=Sn]

• Si is a fresh type variable
• whose upper bound is Ui
• where the (this is the implied bit)
• type parameters A1,...,An that U1,...,Un correspond specifically to
• have been substituted by the type variables S1,...,Sn
• making U1,...,Un correspond to the type variables S1,...,Sn

TL;DR

i.e. It just means that the original upper bound Ui is also the upper bound for Si

Footnotes

^† It is helpful to recall from the JLS that type variables and type parameters are not the same thing (hence we can start to see why we need the substitution):

A type variable is an unqualified identifier used as a type in class, interface, method, and constructor bodies.

A type variable is introduced by the declaration of a type parameter of a generic class, interface, method, or constructor.

Answer 2

It means "substitution" of type variables with actual types. For example

List<T>[T:=String]    =>    List<String>

Enum<E extends Enum<E>>
    A1=E
    U1=Enum<E>

Enum<?> capture convertion to  Enum<S1>
    U1[A1:=S1]   =>   Enum<S1>
    S1's upper bound is Enum<S1>

The syntax is likely borrowed from lambda calculus