Navigation: Overview - Part A - Part B - Part C - Part D - Part E - Part F - Part G - Part H - Part J
Sections: 18 - 18.1 - 18.1.1 - 18.1.2 - 18.1.3 - 18.2 - 18.2.1 - 18.2.1.1 - 18.2.1.2 - 18.2.2 - 18.2.3 - 18.2.4 - 18.2.5 - 18.3 - 18.4 - 18.5 - 18.5.1 - 18.5.2 - 18.5.3 - 18.5.4 - 18.5.5 - 15.12.2.7 - 15.12.2.8
Version 0.6.2. Copyright © 2012 Oracle America, Inc. Legal Notice.
A variety of compile-time analyses require reasoning about types that are not yet known. Principal among these are generic method applicability testing and generic method invocation type inference. In general, we refer to the process of reasoning about unknown types as type inference.
At a high level, type inference consists of reducing compatibility assertions about expressions or types, called constraint formulas, to a set of bounds on inference variables. For example, given inference variable α, it might be determined that the constraint formula ⟨String[]
<: α[]
⟩ reduces to the lower bound String
<: α. As bounds are inferred, they are incorporated into a bound set. Ultimately, this bound set is resolved to produce an instantiation for each of the inference variables.
To infer a generic method's applicability, we assert that the arguments to the method are compatible with their corresponding formal parameter types, and reduce these constraints to a bound set. We then check that there exists a resolution of the resulting bounds.
To infer the type of a generic method invocation, we re-use the inferred bound set from method applicability testing, augmenting it with the results of asserting the compatibility of the method's return type with its target type. We also assert that any exceptions thrown by lambda expression bodies are contained by the throws
clauses of their target descriptors. After reduction, we resolve the inference variables and use them as type arguments to determine the invocation type of the method.
Type inference is also used to determine: i) a target function descriptor for a lambda expression that is assigned to a wildcard-parameterized functional interface; ii) whether an applicable method is more specific than another applicable, generic method; and iii) the validity of an unchecked conversion.
The following details of reduction are especially noteworthy:
When a generic method invocation or diamond constructor invocation appears as the argument to another invocation, the target type of the nested invocation is the targeted formal parameter type. If the target type contains inference variables, the inference variables and bounds from the nested invocation are "lifted" into the outer inference analysis, and dependencies between the outer and inner inference variables are inferred. Ultimately, information from an outermost invocation can be "pushed down" to nested invocations via these dependencies.
When a lambda expression appears as the argument to a generic invocation, and its target type includes inference variables, we proceed by:
Thus, lambda bodies can influence the instantiation of inference variables appearing in the targeted descriptor's return type, and lambda parameter types, if explicit, can influence the instantiation of inference variables appearing in the targeted descriptor's parameter types.
A method reference appearing as the argument to a generic invocation is handled in much the same way.
A variety of compile-time analyses require reasoning about types that are not yet known. Principal among these are generic method applicability testing (18.5.1) and generic method invocation type inference (18.5.2). In general, we refer to the process of reasoning about unknown types as type inference.
At a high level, type inference can be decomposed into three processes:
These processes interact closely: reduction can trigger incorporation; incorporation may lead to further reduction; and resolution may cause further incorporation.
We elaborate in the following sections.
Discussion and motivation:
This section introduces a new chapter to replace the current specification's definition of type argument inference in 15.12.2.7 and 15.12.2.8.In comparison to JLS 7, important changes to inference include:
- Adding support for lambda expressions and method references as method invocation arguments.
- Generalizing to define inference in terms of poly expressions, which may not have well-defined types until after inference is complete. This has the notable effect of improving inference for nested generic method and diamond constructor invocations.
- Describing how inference is used to handle wildcard-parameterized functional interface target types and most-specific method analysis.
- Clarifying the distinction between invocation applicability testing (which involves only the invocation arguments) and invocation type inference (which incorporates a target type).
- Delaying resolution of all inference variables, even those with lower bounds, until invocation type inference, in order to get better results.
- Improving inference behavior for interdependent (or self-dependent) variables.
- Eliminating bugs and potential sources of confusion. This revision more carefully and precisely handles the distinction between specific conversion contexts and subtyping, and describes reduction by paralleling the corresponding non-inference relations. Where there are intentional departures from the non-inference relations, these are explicitly identified as such.
- Laying a foundation for future evolution: enhancements to or new applications of inference will be easier to integrate into the specification.
This section defines inference variables, constraint formulas, and bounds, as the terms will be used throughout this chapter. It also presents the notation we will use.
Inference variables are meta-variables for types—that is, they are special names that allow us to reason about types abstractly. To distinguish them from type variables, we represent inference variables with Greek letters, principally α.
We'll loosely use the term "type" in this chapter to include type-like syntax that contains inference variables. We use the term proper type to exclude such "types" that mention inference variables. Assertions that involve inference variables are assertions about every proper type that can be produced by replacing each inference variable with a proper type.
Constraint formulas are assertions of compatibility or subtyping that may involve inference variables. The formulas may take one of the following forms:
throws
clauses, as derived from T.
Examples of constraint formulas:
- From
Collections.singleton("hi")
, we have the constraint⟨Through reduction, this will become the constraint"hi"
→ α⟩⟨String
<: α⟩- From
Arrays.asList(1, 2.0)
, we have the constraints⟨Through reduction, these will become the constraints1
→ α⟩
⟨2.0
→ α⟩⟨and thenint
→ α⟩
⟨double
→ α⟩⟨Integer
<: α⟩
⟨Double
<: α⟩- From the target type of the constructor invocation
List<Thread> lt = new ArrayList<>()
, we have the constraint⟨Through reduction, this eventually becomes the constraintArrayList<
α>
→List<Thread>
⟩⟨α =Thread
⟩
During the inference process, a set of bounds on inference variables is maintained. A single bound has one of the following forms:
A bound is satisfied by an inference variable substitution if, after applying the substitution, the assertion is true. (The bound false can never be satisfied.)
Some bounds relate an inference variable to a proper type. Let T be a proper type. Given a bound of the form α = T or T = α, we say T as an instantiation of α. Similarly, given a bound of the form α <: T, we say T is a proper upper bound of α, and given a bound of the form T <: α, we say T is a proper lower bound of α.
Other bounds relate two inference variables, or an inference variable to a type that contains inference variables. Such bounds, of the form S = T or S <: T, are called dependencies.
A bound of the form Expression → T represents a constraint formula that cannot be further reduced until one or more inference variables in T are instantiated.
An important intermediate result of inference is a bound set. It is sometimes convenient to refer to an empty bound set with the literal true; this is merely out of convenience, and the two are interchangeable.
Examples of bound sets:
- { α =
String
} contains a single bound, instantiating α asString
.- {
Integer
<: α,Double
<: α, α <:Object
} describes two proper lower bounds and one proper upper bound for α.- { α <:
Iterable<?>
, β <:Object
, α <:List<
β>
} describes a proper upper bound for each of α and β, along with a dependency between them.- { } contains no bounds nor dependencies, and can be referred to as true.
- { false } expresses the fact that no satisfactory instantiation exists.
When inference begins, a bound set is typically generated from a list of type parameter declarations P_{1}, ..., P_{p} and associated inference variables α_{1}, ..., α_{p}. Such a bound set is constructed as follows. For each l (1 ≤ l ≤ p):
Object
appears in the set.
&
in the TypeBound, the bound α_{l} <: T [P_{1}:=α_{1}, ..., P_{p}:=α_{p}] appears in the set; if this results in no proper upper bounds for α_{l} (only dependencies), then the bound α_{l} <: Object
also appears in the set.
Discussion and motivation:
The strategy described here of decomposing a TypeBound into individual types separated by&
, allowing some components to be treated as proper bounds and others as dependencies, is a slight enhancement to the JLS 7 behavior, which treats the bound as a monolithic intersection type.
Reduction is the process by which a set of constraint formulas (18.1.2) is simplified to produce a bound set (18.1.3). An initial bound set, describing known bounds and dependencies on inference variables of interest, is provided as input; this acts as the "current" bound set, which is periodically updated as further bounds are inferred.
Each constraint formula is considered in turn. The rules in this section outline how the formula is reduced to one or both of:
The results of a reduction step are always soundness-preserving: if an inference variable instantiation satisfies the reduced constraints and bounds, it will also satisfy the original constraint. On the other hand, reduction is not completeness-preserving: there may exist inference variable instantiations that satisfy the original constraint but do not satisfy a reduced constraint or bound. This is due to inherent limitations of the algorithm, along with a desire to avoid undue complexity. One effect is that there are expressions for which type argument inference fails to find a solution, but that can be well-typed if the programmer explicitly inserts appropriate types.
Discussion and motivation:
The reduction rules defined in JLS 7 are neither soundness- nor completeness-preserving. The reduction rules described here improve upon this by guaranteeing soundness and reducing the set of invocations which inference is unable to handle. The rules are also, of course, expanded to support the new language features.Unsoundness in JLS 7 arises, among other things, out of the fact that false and true results are treated interchangeably—neither has any impact on the current bound set. It is not a fundamental type safety problem, because the results of inference are checked for validity before an expression is considered well-typed. But it has the unfortunate effect of covering up bugs: if the spec misses an important constraint, there's not a hard line that says that's "wrong." The claim of soundness here raises the bar: if the rules miss a constraint that is necessary to guarantee that the initial constraint formula is true, that is a failing of the rules, and it must be corrected to make the spec internally consistent.
In addition, a soundness-preserving approach avoids the potential confusion that could arise if, say, inference unsoundly ignored certain difficult-to-analyze lambda expression arguments. (The effect might be that inference gets "lucky" in guessing valid type arguments in one scenario, only to fail when a seemingly unrelated adjustment changes the results.)
A constraint formula of the form ⟨Expression → T⟩ is reduced as follows: [jsr335-18.2.1-10]
(
Expression' )
, the constraint reduces to ⟨Expression' → T⟩. [jsr335-18.2.1-10-C1]
This bound set may contain new inference variables, as well as dependencies between these new variables and the inference variables in T.
?
Expression_{2} :
Expression_{3}, the constraint reduces to two constraint formulas, ⟨Expression_{2} → T⟩ and ⟨Expression_{3} → T⟩. [jsr335-18.2.1-10-C3]
Discussion and motivation:
By treating nested generic method invocations as poly expressions, we improve the behavior of inference for nested invocations. For example, the following is illegal in Java 7 but legal in Java 8:ProcessBuilder b = new ProcessBuilder(Collections.emptyList()); // Constructor expects a List<String>When both the outer and the nested invocation require inference, the problem is more difficult. For example:
List<String> ls = new ArrayList<>(Collections.emptyList());Our approach is to "lift" the bounds inferred for the nested invocation (simply { α <:
Object
} in the case ofemptyList
here) into the outer inference process (in this case, trying to infer β where the constructor is for typeArrayList<
β>
). We also infer dependencies between the nested inference variables and the outer inference variables (the constraint ⟨List<
α>
→Collection<
β>
⟩ would reduce to the dependency α = β). In this way, resolution of the inference variables in the nested invocation can wait until additional information can be inferred from the outer invocation (based on the assignment target, β =String
). An alternative strategy for handling nested invocations was considered and rejected: in certain cases, the inference variables of the outer call are resolved before considering the nested call; typing of the nested call is delayed until a proper target type can be provided. In other cases, the nested call is treated as a standalone invocation.This has the advantage of avoiding the extra complexity involved with reduction producing new inference variables and dependencies. But there are two problems with this approach:
- It is not powerful enough to handle situations in which information from both the outer and inner calls needs to be synthesized in order to choose in appropriate inference variable instantiation.
- There's not an obvious rule for choosing whether the outer or the inner call should be resolved first, and so the resulting behavior is very ad hoc.
A constraint formula of the form ⟨LambdaExpression → T⟩, where T mentions at least one inference variable, is reduced as follows, following the compatibility rules outlined in 15.27.3. [jsr335-18.2.1.2-10]
If T is an inference variable, the constraint reduces to the bound LambdaExpression → T. [jsr335-18.2.1.2-12]
Otherwise, if T is not a function type (9.8), the constraint reduces to false. [jsr335-18.2.1.2-14]
Otherwise, a target function descriptor for the expression must be determined, as described in 15.27.3. If no valid descriptor can be found, the constraint reduces to false. [jsr335-18.2.1.2-20]
Otherwise, if the lambda parameters' types are to be inferred, and at least one of the descriptor's parameter types is not a proper type, then the constraint reduces to the bound LambdaExpression → T. [jsr335-18.2.1.2-22]
Otherwise, the congruence of the LambdaExpression with the target function descriptor is asserted as follows: [jsr335-18.2.1.2-30]
void
and the lambda body is neither a statement expression nor a void-compatible block, the constraint reduces to false. [jsr335-18.2.1.2-30-D]
void
) type and the lambda body is a block that is not value-compatible, the constraint reduces to false. [jsr335-18.2.1.2-30-E]
void
) type R, assume the lambda's parameter types are the same as the descriptor parameter types. Then where the lambda body has the form Expression, the constraint ⟨Expression → R⟩; or where the lambda body is a block with return expressions Expression_{1}, ..., Expression_{m}, for all i, 1 ≤ i ≤ m, ⟨Expression_{i} → R⟩. [jsr335-18.2.1.2-30-F2]
Discussion and motivation:
The key piece of information to derive from a compatibility constraint involving a lambda expression is the set of bounds on inference variables appearing in the target descriptor's return type. This is crucial, because functional interfaces are often generic, and many methods operating on these types are generic, too.In the simplest case, a lambda expression may simply provide a lower bound for an inference variable:
<T> List<T> makeThree(Factory<T> factory) { ... } String s = makeThree(() -> "abc").get(2);In more complex cases, a result expression may be a poly expression—perhaps even another lambda expression—and so the inference variable might be passed through multiple constraint formulas with different target types before a bound is produced.
Most of the work described in this section precedes assertions about the result expressions; its purpose is to derive the lambda expression's function descriptor, and to check for expressions that are clearly disqualified from compatibility.
We do not attempt to produce bounds on inference variables that appear in the target descriptor's
throws
clause. This is because exception containment is not part of compatibility (15.27.3)—in particular, it must not influence method applicability (18.5.1). However, we do get bounds on these variables later, because invocation type inference (18.5.2) produces exception containment constraint formulas (18.2.5). If the target type is an inference variable, or if the target descriptor parameter types contain inference variables, we produce a delayed constraint (18.1.2). When more information about the target type can be inferred, a substitution can be performed to eliminate the blocking inference variables and allow further reduction. For example:<T> T id(T arg) { return arg; } Runnable r = id(() -> System.out.println("hi"));During applicability inference for
id
, it is impossible to determine what kind of functional interface is meant to be represented by the lambda expression. So a delayed constraint is produced:⟨() -> System.out.println("hi")
→ α⟩Later, when the target type of the
id
invocation is examined, we can resolve α =Runnable
, and then perform substitution to get the new constraint formula:⟨() -> System.out.println("hi")
→Runnable
⟩
A constraint formula of the form ⟨MethodReference → T⟩, where T mentions at least one inference variable, is reduced as follows, following the compatibility rules outlined in 15.28.1. [jsr335-18.2.1.3-10]
If T is neither a function type (9.8) nor an inference variable, or if T is a function type but does not have a function descriptor, the constraint reduces to false. [jsr335-18.2.1.3-12]
Otherwise, if T is an inference variable or if at least one of T's function descriptor parameter types is not a proper type, then the constraint reduces to the bound MethodReference → T. [jsr335-18.2.1.3-14]
Otherwise, if there does not exist a compile-time declaration for the method reference, as defined in 15.28.1, the constraint reduces to false. [jsr335-18.2.1.3-16]
If a compile-time declaration can be found there are three cases: [jsr335-18.2.1.3-40]
void
, the result is true. [jsr335-18.2.1.3-40-A]
This bound set may contain new inference variables, as well as dependencies between these new variables and the inference variables in T.
void
, the constraint reduces to false; otherwise, the constraint reduces to ⟨R' → R⟩. [jsr335-18.2.1.3-40-B]
Discussion and motivation:
Delayed constraints can be produced for method references just as they were for lambda expressions (18.2.1.2). The strategy used to determine a return type for a generic referenced method follows the same pattern as for generic method invocations (18.2.1). This may involve "lifting" bounds into the outer context and inferring dependencies between the two sets of inference variables.
A constraint formula of the form ⟨S → T⟩ is reduced as follows: [jsr335-18.2.2-10]
Discussion and motivation:
To do: we need to allow for unchecked conversion here. We may not be able to handle it in full generality, since unchecked conversion itself relies on inference (18.5.5); the situation is similar to a nested generic method invocation. Boxing T to T' is not completeness-preserving: for example, if T werelong
, S might be instantiated toInteger
, which could be unboxed and then widened tolong
. We avoid this problem is most cases by giving special treatment to inference-variable return types that we know are already constrained to be certain boxed primitive types. See 18.5.2.
A constraint formula of the form ⟨S <: T⟩ is reduced as follows:
<
A_{1},
...,
A_{n}>
, then let C<
B_{1},
...,
B_{n}>
be the parameterization of C for S, as defined below; if no such parameterization exists, the constraint reduces to false. Otherwise, the constraint reduces to the following new constraints: for all i, 1 ≤ i ≤ n, ⟨B_{i} <= A_{i}⟩.
[]
, then let S'[]
be the most specific array supertype of S, as defined below; if no such array supertype exists, the constraint reduces to false. Otherwise:
&
... &
I_{n}, the constraint reduces to the following new constraints: for all i, 1 ≤ i ≤ n, ⟨S <: I_{i}⟩.
A constraint formula of the form ⟨S <= T⟩, where S and T are type arguments, is reduced as follows:
?
or ? extends
Object
, the constraint reduces to true.
? extends
T', where T' is a type other than Object
:
? extends
S', the constraint reduces to ⟨S' <: T'⟩.
? super
T':
? super
S', the constraint reduces to ⟨T' <: S'⟩.
To do: define the parameterization of a class C for a type T; define the most specific array supertype of a type T.
A constraint formula of the form ⟨S = T⟩, where S and T are types, is reduced as follows:
<
B_{1},
...,
B_{n}>
and T = C<
A_{1},
...,
A_{n}>
, the constraint reduces to the following new constraints: for all i, 1 ≤ i ≤ n, ⟨B_{i} = A_{i}⟩.
[]
and T'[]
, the constraint reduces to ⟨S' = T'⟩.
&
... &
S_{m} and T_{1} &
... &
T_{n}: if m ≠ n, the constraint reduces to false; otherwise, for all i, 1 ≤ i ≤ n, ⟨S_{i} = T_{i}⟩.
A constraint formula of the form ⟨S = T⟩, where S and T are type arguments, is reduced as follows:
?
and T has the form ?
, the constraint reduces to true.
? extends
S' and T has the form ? extends
T', the constraint reduces to ⟨S' = T'⟩.
? super
S' and T has the form ? super
T', the constraint reduces to ⟨S' = T'⟩.
To do: the purpose of this section is to derive bounds on inference variables that appear in thethrows
clause of a functional interface descriptor. It mimics the checking of lambda expressions and method references above, deriving a target descriptor and then comparing the body's uncaught checked exceptions to the descriptor'sthrows
clause. It is also necessary to recursively traverse parenthesized expressions, conditional expressions, and return expressions of lambdas, because these may contain lambda expressions or method references that can influence inference variables.
Discussion and motivation:
Constraints on checked exceptions are handled separately from constraints on return types, because return type compatibility influences applicability of methods (18.5.1), while exceptions only influence the invocation type after overload resolution is complete (18.5.2). This could be simplified by including exception compatibility in the definition of lambda expression compatibility (15.27.3), but this would lead to possibly-surprising cases in which exceptions that can be thrown by a lambda body change overload resolution. The handling of the case in which more than one inference variable appears in a descriptor'sthrows
clause is not completeness-preserving. Either variable may, on its own, satisfy the constraint that each checked exception be declared, but we can't be sure which one is intended. So, for predictability, we constrain them both.
Whenever a bound set contains two or more bounds, it is possible that new bounds can be inferred based on the assertions of the original bounds. As bound sets are constructed and grown during inference, new bounds are incorporated by identifying complementary pairs of bounds and inferring further information in this way.
Specifically, for any pair of bounds in a bound set matching one of the following rules, a new constraint formula is inferred. In the rules, S and T are inference variables or types, and U is a proper type. For conciseness, a bound of the form α = T may also match a bound of the form T = α.
The resulting constraint formula is then reduced, and any new bounds are added to the bound set. This may trigger further incorporation; ultimately, the set will reach a fixed point and no further bounds can be inferred.
A bound set that is fully incorporated, if it does not contain the bound false, has the following properties:
Discussion and motivation:
The assertion that incorporation reaches a fixed point is not obvious. Building on the work of Kennedy and Pierce, On Decidability of Nominal Subtyping with Variance, this property can be proven by making the argument that the set of types that may appear in the bound set is finite. The argument relies on two assumptions:
- New capture variables are not generated when reducing subtyping constraints (18.2.3).
- Expansive inheritance paths are not pursued.
To do: each of these properties needs to be guaranteed via refinements to the specification.
Given a bound set that does not contain the bound false, a subset of the inference variables mentioned by the bound set may be resolved. This means that a satisfactory instantiation may be added to the set for each inference variable, until all the requested variables have instantiations. Dependencies in the bound set may require that the variables be resolved in a particular order, or that additional variables be resolved.
An inference variable α depends on the resolution of an inference variable β if α does not have an instantiation and, where T is either β or a type that mentions β, the bound set contains a bound of one of the following forms:
An inference variable α also depends on the resolution of an inference variable β if there exists an inference variable γ such that α depends on the resolution of γ and γ depends on the resolution of β.
Given a set of inference variables to resolve, let V be the union of this set and all variables upon which the resolution of at least one variable in this set depends.
If every variable in V has an instantiation, then the resolution procedure terminates. Otherwise, let { α_{1}, ..., α_{n} } be a non-empty subset of V such that i) for all i, 1 ≤ i ≤ n, if α_{i} depends on the resolution of a variable β, then either β has an instantiation or there is some j such that β = α_{j}; and ii) there exists no non-empty proper subset of { α_{1}, ..., α_{n} } with this property.
Then resolution proceeds by generating an instantiation for each of α_{1}, ..., α_{n}.
First, for all i (1 ≤ i ≤ n), define T_{i} as follows:
If incorporating the bounds α_{1} = T_{1}, ..., α_{n} = T_{n} with the current bound set produces a set that does not include false, then this is the new bound set; resolution proceeds by selecting a new set of variables to instantiate (if necessary), as described above.
Otherwise, if the resulting bound set does include false, then a second attempt is made to instantiate { α_{1}, ..., α_{n} }, as follows:
If the resulting type variables Z_{1}, ..., Z_{n} have well-formed bounds, then the new bound set is produced by incorporating α_{1} = Z_{1}, ..., α_{n} = Z_{n}. If the result contains the bound false, resolution fails. Otherwise, resolution proceeds by selecting a new set of variables to instantiate (if necessary), as described above.
Using the inference processes defined above, the following analyses are performed at compile-time.
Given a method invocation that provides no explicit type arguments, the following process, modeled after the applicability rules in 15.12.2.2, 15.12.2.3, & 15.12.2.4, determines whether a potentially-applicable generic method m is applicable: [jsr335-18.5.1-10]
To do: we need to do something here about the varargs accessibility constraint.
Discussion and motivation:
Consider the following method invocation and assignment:List<Number> ln = Arrays.asList(1, 2.0);A most-specific applicable method for the invocation must be identified as described in 15.12. The only potentially-applicable method (15.12.2.1) is declared as follows:
public static <T> List<T> asList(T... a)Trivially (because of its arity), this method is neither applicable by strict invocation (15.12.2.2) nor applicable by loose invocation (15.12.2.3). But since there are no other candidates, in a third phase the method is checked for applicability as a variable-arity method.
The initial bound set, B, is a trivial upper bound for a single inference variable, α:
{ α <:Object
}The initial constraint formula set is as follows:
{ ⟨1
→ α⟩, ⟨2.0
→ α⟩ }These are reduced to a new bound set, B':
{ α <:Object
,Integer
<: α,Double
<: α }Then, to test whether the method is applicable, we attempt to resolve these bounds. We succeed, producing the rather complex instantiation
α =Number & Comparable<? extends Number & Comparable<?>>
We have thus demonstrated that the method is applicable; since no other candidates exist, it is the most-specific applicable method. The type of the method, and its compatibility with the target type in the assignment, is not determined until further inference can occur, as described in the next section.
Consider a method invocation that provides no explicit type arguments, and a corresponding most-specific applicable generic method m. The following process is used to infer the invocation type (15.12.2.6) of the chosen method. [jsr335-18.5.2-10]
void
, then a compile-time error occurs; the invocation type of the method is undefined. [jsr335-18.5.2-10-C11]
To do: we need to figure out how this interacts with unchecked warnings and the resulting erasure of the invocation type (15.12.2.6).
To do: Should R be captured when targeting S?
To do: Need to describe how delayed constraints in B'' are reduced before proceeding to resolve all the inference variables.
Discussion and motivation:
It is important to note that two "rounds" of inference are involved in finding the type of a method invocation. This is necessary to allow a target type to influence the type of the invocation without allowing it to influence the choice of an applicable method. The first round produces a bound set and tests that a resolution exists, but does not commit to that resolution. The second round reduces additional constraints and then performs a second resolution, this time "for real."The distinction between these two rounds of inference was confused in previous iterations of the JLS (compare the discussion of inference in 15.12.2.2 vs. 15.12.2.6; also see 15.12.2.8, which makes ambiguous use of the term "now").
Let's revisit the example from the previous section:List<Number> ln = Arrays.asList(1, 2.0);The most-specific applicable method is declared as follows:
public static <T> List<T> asList(T... a)In order to complete type-checking of the method invocation, we must determine whether it is compatible with its target type,
List<Number>
.The bound set used to demonstrate applicability in the previous section, B', was:
{ α <:Object
,Integer
<: α ,Double
<: α }The new constraint formula set is as follows:
{ ⟨1
⊆_{throws} α⟩, ⟨2.0
⊆_{throws} α⟩, ⟨List<α>
→List<Number>
⟩ }The ⊆_{throws} constraints are trivially true, because they do not involve lambda expressions or method references. The assignability constraint produces an equality bound for α, which is included in the new bound set, B'':
{ α <:Object
,Integer
<: α ,Double
<: α, α =Number
}These bounds are trivially resolved:
α =Number
Finally, we perform a substitution on the declared return type of
asList
to determine that the invocation expression has typeList<Number>
; clearly, this is compatible with the target type.Note that this strategy for inference is different than JLS 7, which would have instantiated α based on its lower bounds (before even considering the invocation's target type), as we did in the previous section. This would result in a type error, since the resulting type is not a subtype of
List<Number>
.
Where a lambda expression with explicit parameter types P_{1}, ..., P_{n} targets a wildcard-parameterized functional interface, F<
A_{1}, ..., A_{m}>
, one or more of the wildcards in A_{1}, ..., A_{m} may be instantiated according to the following process: [jsr335-18.5.3-20]
? extends
U_{i}, then the initial bound set contains the bound α_{i} <: U_{i}. [jsr335-18.5.3-20-A2]
? super
L_{i}, then the initial bound set contains the bound L_{i} <: α_{i}. [jsr335-18.5.3-20-A3]
Object
. [jsr335-18.5.3-20-A4]
<
α_{1}, ..., α_{m}>
. If n ≠ k, no valid parameterization exists. [jsr335-18.5.3-20-B]
<
A'_{1}, ..., A'_{m}>
, is constructed as follows, for 1 ≤ i ≤ m: [jsr335-18.5.3-20-E]
<
A'_{1}, ..., A'_{m}>
is a well-formed type, this is the inferred parameterization. Otherwise, no valid parameterization exists. [jsr335-18.5.3-20-F]
Discussion and motivation:
In order to determine the descriptor of a wildcard-parameterized functional interface, we have to "instantiate" the wildcard type arguments with specific types. The "default" approach is to simply replace the wildcards with their bounds, as described in 9.8. But this produces spurious errors in cases in which a lambda expression has explicit parameter types that do not correspond to the wildcard bounds. For example:Predicate<? super Integer> p = (Number n) -> n.equals(23);The lambda expression in this example is a
Predicate<Number>
, which is a subtype ofPredicate<? super Integer>
but notPredicate<Integer>
. The analysis in this section is used to infer thatNumber
is an appropriate choice for the type argument toPredicate
. The analysis here, while described in terms of general type inference, is intentionally quite simple. The only constraints are equality constraints, which means that reduction amounts to simple pattern matching.A more powerful strategy might also infer constraints from the body of the lambda expression. But, given possible interactions with inference for surrounding and/or nested generic method invocations, this would introduce a lot of extra complexity.
This section must describe how inference is used to test whether a method m_{1} is more specific than generic method m_{2} given argument expressions exp_{1}, ..., exp_{n}.
The following demonstrates how inference might be used to implement checking for a legal unchecked conversion (the check is left unspecified in JLS 7). There are currently no cross-references mandating the use of this strategy from, for example, Chapter 5; for now, this section is just illustrative.
Unchecked conversions (5.1.9) are typically followed by widening reference conversions (5.1.5). When this occurs, the type resulting from the unchecked conversion is not expressed in the program, and must be inferred as follows.
Let S be the raw type to be converted, and let T be the type expected after widening reference conversion. Then:
Discussion and motivation:
This section addresses an existing specification bug: when an unchecked conversion is followed by widening, the implementation is left to figure out what the unchecked conversion produces, without any help from the specification. This has led to inconsistent behavior between compiler implementations. It turns out that this problem is a perfect fit for type inference.
Compare JLS 15.12.2.7
This section is deleted; it has been replaced by Chapter 18, principally 18.2 and 18.5.1.
Compare JLS 15.12.2.8
This section is deleted; it has been replaced by Chapter 18, principally 18.3, 18.4, and 18.5.2.