Formal model for defender method resolution

[Brian Goetz]

Thinking more, the logical thing to do is require that a covariant 
override of an extension method in an interface must also provide a new 
default.  The cases where the old default will still be OK (even when it 
is type-correct, which is already rare) under a covariant override seem 
pretty limited.

However, it is a common behavior currently to override a method in an 
interface solely to provide new Javadoc (or annotations).  Currently 
these are a no-op from a language semantics perspective, and I believe 
this is a behavior we should continue to respect.  Hence the current 
implementation (and formal model) interprets

interface A { T m() default k }
interface B extends A { T m() }  // non-covariant override

as B inheriting A's default, rather than B overriding A's default with 
some magic "no default".  (This is different from the "obvious" analogy 
to concrete classes, where it is permitted to reabstract a concrete 
method.  But such reabstraction for defaults would introduce a lot of 
additional complexity for relatively little value.)

Some people find this "sub-inheritance" (inheritance of part of a 
signature) disturbing, because there is no precedent for it in Java.

What do people think?  Do you find this interpretation of B (m() 
continues to use A's default) confusing or natural (or both)?

On 1/24/2011 11:26 AM, Brian Goetz wrote:
> Dan Smith has pointed out a hole in the Featherweight Defenders
> document; there is an unsound disconnect introduced when we allow
> covariant overriding but don't require the implementation to be replaced
> (rules T-IntNoDef and T-ClassAbs).  This would allow the following failure:
>
>     k1 : Object
>     intf A { Object m() default k1 }
>     intf B extends A { String m() }
>
> Here, the default for A is going to produce a result that does not meet
> B's interface contract.  I believe what is needed is additional
> constraints on T-IntNoDef to include a
>     \Gamma(mdef(I_i))<: T
> constraint (for the cases where mdef(I_i) is not nil).
>
> I think this is all that is needed to plug this hole.
>
> On 1/19/2011 12:48 PM, Brian Goetz wrote:
>> At
>>      http://cr.openjdk.java.net/~briangoetz/lambda/featherweight-defenders.pdf
>>
>> I have posted a draft of a formal model for resolution of defender
>> methods.  This is written in the style of "Featherweight Java"
>> (Igarashi, Pierce, et al), in which a number of real-world language
>> concerns are abstracted away, in order to simplify the formalism for the
>> portion of the language of interest, notably the typing and resolution
>> of defender methods.
>>
>> Hopefully this will serve as a basis for discussion of the proposal.
>>
>> The T- and S- rules are implemented by the compiler and are used for
>> typing; the R- rules are implemented by the VM to do method selection.
>> (The primary computed item of interest is mres(C), which is the method
>> resolution for a given class -- while this is not used in any further
>> production (it would be used if the operational semantics were
>> specified), it is in fact the whole point of this exercise.)
>>
>>
>