.JAVA File Format – Type inference

Inference variables (18.1.1)

Inference variables are placeholders for types, written with Greek letters such as α and β so as not to be confused with type variables. In this chapter “type” includes type-like syntax that mentions inference variables; a proper type mentions none.

Constraint formulas (18.1.2)

A constraint formula states a compatibility or subtyping fact that may mention inference variables:

For example, Collections.singleton("hi") gives ‹"hi" → α›, which reduces to ‹String <: α›. Arrays.asList(1, 2.0) gives ‹1 → α› and ‹2.0 → α›, which become ‹Integer <: α› and ‹Double <: α›. List<Thread> lt = new ArrayList<>() gives ‹ArrayList<α> → List<Thread>›, which becomes ‹α = Thread›.

Bounds (18.1.3)

With T a proper type, α = T makes T an instantiation of α; α <: T makes it a proper upper bound and T <: α a proper lower bound. Other bounds of the form S = T or S <: T are dependencies. A set of bounds is a bound set; the empty set is also called true.

Inference usually starts with a bound set made from the type parameters P1, ..., Pp and fresh variables α1, ..., αp. A parameter with no bound gives αl <: Object; otherwise each type T in its bound gives αl <: T[P1:=α1, ..., Pp:=αp], with αl <: Object added if that leaves no proper upper bound.

Expression compatibility (18.2.1)

‹Expression → T›: if T is proper, true or false by loose invocation compatibility; otherwise a standalone expression of type S reduces to ‹S → T›. A poly expression depends on its form:

This is how nested generic calls are inferred together: the bounds of an inner call are lifted into the outer one. List<String> ls = new ArrayList<>(Collections.emptyList()); compiles because the inner variable is tied to the outer by a dependency and resolved once the outer target is known.

A lambda, ‹LambdaExpression → T› with T mentioning a variable: false if T is not a functional interface, or if no valid function type comes from the ground target type T′ (15.27.3), or if the lambda is not congruent with it (different parameter count; an implicitly typed lambda with non-proper parameter types; a void result with a body that is neither a statement expression nor a void-compatible block; a non-void result with a block that is not value-compatible). Otherwise it reduces to all of these: for explicit parameter types F1, ..., Fn against G1, ..., Gn, ‹Fi = Gi› and ‹T′ <: T›; and for a return type R, assuming the lambda’s parameter types are the function type’s, false if R is proper and a result expression is not assignment-compatible with R, otherwise ‹e → R› for the expression body or for each result expression. No bounds come from the function type’s throws clause at this stage.

A method reference, ‹MethodReference → T›: false if T is not a functional interface with a function type, or if no method is potentially applicable. An exact method reference reduces its parameters to ‹Pi → Fi› (with P1 as the receiver via ‹P1 <: ReferenceType› when n = k + 1) and its result to ‹R′ → R›, where R′ is the captured return type; false if R is non-void and the method is void. An inexact one requires proper parameter types, finds the compile-time declaration (15.13.1), and reduces its return type, lifting a generic method’s bounds as above where the type arguments are elided.

Type compatibility (18.2.2)

‹S → T› is decided in order:

1. Both proper: true if S is compatible with T in a loose invocation context, else false.
2. S primitive: box it to S′ and reduce ‹S′ → T›.
3. T primitive: box it to T′ and reduce ‹S = T′›.
4. T is parameterised G<T1, ..., Tn> and no supertype of S has the form G<...> but raw G is a supertype of S: true (unchecked conversion).
5. The same for an array type G<T1, ..., Tn>[]k.
6. Otherwise ‹S <: T›.

Subtyping and containment (18.2.3)

‹S <: T›: if both are proper, true if S is a subtype of T. If S is the null type, true; if T is the null type, false. If S is a variable α, the bound α <: T; if T is a variable α, the bound S <: α. Otherwise by the form of T:

• Parameterised class or interface, or an inner class of one, with type arguments A1, ..., An: find the corresponding supertype of S with arguments B1, ..., Bn, or false if there is none, and reduce ‹Bi <= Ai› for each.
• Any other class or interface type: true if it is among S’s supertypes.
• Array type T′[]: find the most specific array supertype S′[] of S, or false. If neither is primitive, ‹S′ <: T′›; otherwise true only if they are the same primitive type.
• Type variable: true if S is an intersection type containing T; otherwise, if T has a lower bound B, ‹S <: B›; otherwise false.
• Intersection type I1 & ... & In: ‹S <: Ii› for each.

‹S <= T›, for type arguments:

Type equality (18.2.4)

‹S = T› for types: true or false if both are proper; false if either is the null type; the bound α = T or S = α if one is a variable and the other is not primitive. Class or interface types with the same erasure reduce to ‹Bi = Ai› for their type arguments; array types reduce to ‹S′ = T′›; intersection types pair each element with its counterpart. Anything else is false.

For type arguments: both types, as above; both ?, true; ? against ? extends T′, ‹Object = T′› (and the reverse); ? extends S′ against ? extends T′ and ? super S′ against ? super T′, ‹S′ = T′›; anything else false.

Checked exceptions (18.2.5)

‹LambdaExpression →throws T› and ‹MethodReference →throws T›: let E1, ..., En be the non-proper types in the function type’s throws clause, and X1, ..., Xm the checked exceptions the body or referenced method can throw. If n = 0, the result is false if some Xi is not a subtype of a proper thrown type, and otherwise true. If n > 0, each Xi that is not a subtype of a proper thrown type gives ‹Xi <: Ej› for every j, and every Ej gets the bound throws Ej. These are kept apart from return types because return types affect which method is applicable, and thrown exceptions must not.

Complementary pairs (18.3.1)

Bounds involving capture (18.3.2)

A bound G<α1, ..., αn> = capture(G<A1, ..., An>) implies bounds on the variables from the declared bounds of G’s parameters. Let Bi be the bound of the i-th parameter, θ the substitution of the variables for the parameters, and R a type that is not a variable. Then for each i:

Invocation applicability inference (18.5.1)

To test whether a potentially applicable generic method m applies to an invocation with no explicit type arguments: let θ map the type parameters to fresh variables. B0 is the bound set from their declared bounds, with throws αi added for each parameter in m’s throws clause, giving B1. A constraint set C comes from the formal parameter types F1, ..., Fn and the arguments e1, ..., ek:

C is reduced and incorporated with B1 to give B2. The method is applicable if B2 has no false and all its variables can be resolved. That resolution only shows that an answer exists; its results are not kept.

List<Number> ln = Arrays.asList(1, 2.0);   // public static <T> List<T> asList(T... a)

// B2 after reducing the arguments: { α <: Object, Integer <: α, Double <: α }
// The method is applicable, since those bounds resolve to
//   α = Number & Comparable<? extends Number & Comparable<?>>
// With the target type, B3 adds α = Number, and the result is List<Number>

Invocation type inference (18.5.2)

Several rounds of inference are needed, so that the target type can affect the type of an invocation without affecting which method is chosen.

Poly method invocations (18.5.2.1). For a target T, B3 is derived from B2. Let R be m’s return type. If unchecked conversion was needed, reduce ‹|R| → T›. If R θ is a wildcard-parameterised G<A1, ..., An>, use fresh variables β1, ..., βn with ‹G<β1, ..., βn> → T› and the bound G<β1, ..., βn> = capture(G<A1, ..., An>). If R θ is a variable α and T is a non-wildcard reference type with wildcard-parameterised or conflicting lower bounds on α, or T is a parameterisation of G where α’s bound makes it raw, or T is primitive and a wrapper class is an instantiation, upper or lower bound of α: resolve α and reduce ‹U → T› with U the capture of its instantiation. Otherwise reduce ‹R θ → T›. The invocation is compatible with T if B3 has no false and resolves.

Additional argument constraints (18.5.2.2). The set C holds, for each argument ei not pertinent to applicability, ‹ei → Fi θ›, and, by the form of ei: for a lambda, ‹ei →throws Fi θ› with the search applied to the lambda body and its result expressions; for a method reference, ‹ei →throws Fi θ›; for a poly creation or invocation, that inner inference’s own C; for parenthesised, conditional and switch expressions, the same rules on their parts.

While C is not empty, a subset is chosen in which no constraint’s input variable can influence the output variable of another. If none exists, there is a cycle: from the constraints in it that depend on nothing outside it, take one whose expression is furthest left. The chosen input variables are resolved, the substitution is applied to every constraint, and the result is reduced and incorporated, producing B4. If B4 has no false, its variables are resolved to T1, ..., Tp, and the invocation type is m’s type with θ′ = [P1:=T1, ..., Pp:=Tp] applied, or with the return and thrown types erased if unchecked conversion was needed. If B4 has false or resolution fails, it is a compile-time error.

The output variables of a constraint are the variables in T that are not input variables.

Functional interface parameterisation (18.5.3)

When a lambda with explicit parameter types P1, ..., Pn targets a wildcard-parameterised F<A1, ..., Am>, take the function type of F<α1, ..., αm> with parameter types Q1, ..., Qk. If n ≠ k there is no parameterisation. Otherwise reduce ‹Pi = Qi› to a bound set B; false means none. Each A′i is B’s instantiation of αi if it has one, otherwise Ai. The result must be well-formed and a subtype of the original; wildcards left over are replaced as described for the function type. So Predicate<? super Integer> p = (Number n) -> n.equals(23); makes Predicate<Number>.

More specific method inference (18.5.4)

To test whether m1 is more specific than a generic m2 for arguments e1, ..., ek, let S1, ..., Sk be m1’s parameter types (its own type parameters stay as type variables) and T1, ..., Tk be m2’s after θ. Start from m2’s bound set, then for each i:

• If Ti is proper: true if Si is more specific than Ti for ei, otherwise false.
• If they are not both functional interface types, or one interface is a superinterface or subinterface of the other: ‹Si <: Ti›.
• Otherwise compare their function types: same type parameters and parameter count, equal bounds and parameter types, and return types compared as follows. For an explicitly typed lambda or an exact method reference, a void RT is true; a primitive RS against a reference RT is true when every result is a standalone primitive (and the reverse with reference results); otherwise ‹RS <: RT θ′›. Parenthesised, conditional and switch arguments are handled through their parts.

For a variable arity comparison a final ‹Sk+1 <: Tk+1› is added. Reducing and incorporating everything with m2’s bound set must give no false and resolve, for m1 to be more specific.

Record pattern inference (18.5.5)

A record pattern for a generic record R that names no type arguments has them inferred from the type T being matched. T must be checked-cast convertible to raw R. Variables α1, ..., αn stand for R’s parameters, with their declared bounds in B0. T′ is derived from T: for a parameterised T, its capture with each capture variable replaced by a fresh variable β carrying its bounds; T unchanged for any other class or interface type. For a type variable or intersection type, the rule applies to each bound.

If T′ is a parameterisation of G and R<α1, ..., αn> has a supertype R′ that is one too, ‹T′ = R′› is reduced and incorporated. With no false, the variables are resolved, skipping the lower-bound step so that fresh type variables are introduced directly; the type of the pattern is the upward projection of the result. For op instanceof Mapper(var in, var out) with op a UnaryOperator<? extends CharSequence>, this gives Mapper<? extends CharSequence>.