Collected comments / questions re type inference in 0.6.3
Stephan Herrmann
stephan.herrmann at berlin.de
Thu Oct 17 15:59:15 PDT 2013
On 10/16/2013 06:05 PM, Dan Smith wrote:
> On Oct 13, 2013, at 9:19 AM, Stephan Herrmann wrote:
>> I couldn't find a statement on how type inference supports
>> "pass-through" varargs semantics, where a provided array
>> is directly bound to the varargs array variable.
>> This way Java 8 would change the semantics in cases like this:
>> String[][] x = {{"X"}, {"Y"}};
>> List l = Arrays.asList(x);
>> In Java 7 'l' has two elements of type String[] but the new
>> inference seems to produce one element of type String[][].
>> Is this intended?
>
> In fact, I tried to add text to support the intended behavior (a list of length 2, as you say), where it was unclear before.
>
> See the discussion in Part F, 15.12.2.4: "The previous 'applicable variable arity method' terminology incorrectly hinted that, if a variable-arity method is applicable in any phase, it is applicable in and only in Phase 3. This overlooks the fact that variable arity methods can act as fixed-arity methods in Phases 1 and 2. What is relevant is the kinds of adaptations actually used to determine applicability, not the kinds of adaptations allowed by the method declaration."
Thanks, I indeed overlooked that discussion bullet.
I saw special mentioning in 15.12.2.1 ("the nth argument of the
method invocation is potentially compatible with either T or T[].")
and thought a similar rule might be missing from 18.5.1.
> In the Lambda Spec, none of this is substantially changed. We should probably clarify that 15.12.2.2 and 15.12.2.3 apply to all methods for which there are n formal parameters.
Yes, turning that note from the discussion into s.t. explicit
in the spec would be helpful.
>> However, for the case of B I'm not
>> sure about the intention: B1,...,Bn are introduced as the
>> bounds of type parameters P1,...,Pn, i.e., each Bi is a list of
>> bounds. The first bullet splits these into Bij, which is fine.
>> But what am I to make of a constraint ⟨θ Bi <: R⟩?
>> A list of types cannot be a subtype of a type, can it?
>> Is s.t. like "foreach j : Bij" implied here?
>
> Yes, it's a slight abuse, but I didn't invent it. :-) The intent is that Bi is an intersection type as implied by the bound. See, for example, 4.5, which also treats Bi as a type.
OK, with this unfolding it's much clearer :)
> Note that an intersection types do _not_ have "for all" behavior on the left side of subtyping: the constraint is that "there exists" an element of the list that is a subtype of R.
Thanks for mentioning!
>> Sect. 18.4. requires some type variables to "have well-formed bounds".
>> I could find no reference to well-formedness rules for type variables
>> in the given sense.
>
> I'll make a note to clean this up as best I can. The idea is that if capture would allow it (5.1.10), it's okay. One thing capture prohibits is two different unrelated classes as upper bounds. One thing it doesn't prohibit, but should, is a lower bound that is not a subtype of any upper bound. (Another to-do for another day: clarify the well-formedness rules for types.)
I think I can proceed with this statement for now.
> [...]
> One thing that needs tweaking (a known issue) is the use of lub in 18.4. The inputs to lub might not be fully defined types -- they might involve type variables whose bounds we are in the middle of instantiating. So I need to back off a bit on what we can do there, probably only taking the lub of the proper lower bounds. (glb is more of a syntactic operation, so we can get away with it in 5.1.10 and here.)
I'll keep that in mind if I get into trouble with this lub...
> [...]
> Type variables are definitely types. A type variable produced by capture may, for example, be the type of an expression. Chapter 4 needs to do a better job of acknowledging that some types (capture variables, intersection types, the 'null' type) are not Types -- they can't be written down in the syntax -- but are still types.
So, capitalization is semantically relevant? :)
> [...]
> See JLS 7 15.9.3. Overload resolution and inference have always been defined for class instance creations somewhat informally in terms of the behavior for methods. In the diamond case, we explicitly define a "method" that gets plugged in to the analysis.
>
> I've added a sentence to clarify that the "method" is as defined in 15.9.3.
OK, that a substantial substitution.
>> From Dan's last statement it seems that Java 8 will be significantly
>> more restrictive, rejecting some programs legal in Java 7.
>> Before implementing such semantics I need confirmation by the EG,
>> given that javac (b109) does *not* enforce the stricter semantics.
>> I might add that I'm actually in favor of gradually fading out some uses
>> of unchecked conversions, but this must happen in a coordinated way.
>
> What we're seeing is an old inconsistency that just hasn't been fixed yet. There are many other bugs, some reported and some not yet identified, of a similar scope. And Eclipse often prefers consistency with javac over consistency with the spec.
Even if we (committers) preferred the spec, most our users prefer consistency with javac,
including bug-compatibility. Particularly, if javac accepts an illegal program,
it's impossible to convince a user that the more restrictive compiler is better.
> There may be subtle differences between 7 and 8 due to 8's commitment to soundness; this is by design. I haven't encountered any cases that seem to be of serious concern to users. (In other words, 7 defaults to "true" during reduction, while 8 prefers "false". So in some corners, 7 is more powerful by pretending something is true even though it can't prove it, and then happening to get lucky. These corners are obscure.)
Judging from the number of bug reports and discussions in these bugs
I have the (not-validated) impression that combined use of parameterized and
some raw types is fairly wide-spread. It should be possible to mend these
programs by properly parameterizing all types, but I'd predict that users
will see a difference.
If we can tell our users that Java 8 will be stricter in those situations,
it may be easier to argue than if bug fixes in Java 7 compilers break existing
programs.
thanks,
Stephan
More information about the lambda-spec-experts
mailing list