Formal model for defender method resolution

[Sam Pullara]

I find it unnatural that people are overriding interfaces to add Javadocs, but I guess it happens. If I was using someones library and I looked at their interface and there was no default, I wouldn't expect there to be a default. Having to go up the interface hierarchy to see if there is a default seems surprising. It wouldn't bother me though if interface B was illegal since it isn't just repeating something that was in its super interface.

Sam

On Jan 28, 2011, at 11:38 AM, Brian Goetz wrote:

> 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.)
>>> 
>>> 
>> 
>