On Sat, Dec 7, 2013 at 1:30 AM, Peter Thiemann <
thiem...@informatik.uni-freiburg.de> wrote:
> On 12/4/13 11:59 PM, Mark Miller wrote:
>
>> The
>> position Tom and I take is that, aside from -0.0, JS ===
>> guarantees full observational equivalence, i.e., for any
>> program containing the fragment
>>
>> if (x === y) {
>> .... x ....
>> }
>>
>> if all or any or all of the mentions of x in the body were
>> changed to y, the meaning of the program would not change.
>> (Also, given the usual simplifying assumptions about renaming,
>> non-shadowing, and alpha equivalence.)
>>
>> If the guarantees your === would provide is weaker than that,
>> what are its guarantees, and why do you believe those to be
>> sufficient?
>>
>
> I have a further thought on this position:
> Your position is stronger than Java's! In fact, Java's reference equality
> == provides pretty much the guarantees that I was proposing, namely
> interchangeability in the intersection / conjunction of the interfaces:
>
> interface Master { void master(); void general(); }
> interface Slave { void slave(); void general(); }
> class Implementation implements Master, Slave { ... }
> class Use {
> void mediate(Master m, Slave s) {
> if (m == s) {
> m.master(); // interface/contract conforming
> use
> s.slave(); // dito
> ((Slave)m).slave(); // m.slave() is a type error
> ((Master)s).master(); // s.master() is a type error
> m.general(); // here m and s are exchangeable
> s.general(); // dito
> }
> }
>
> void invoke(Implementation imp) {
> mediate(imp, imp);
> }
> }
>
> With contracts, we could not fix up the type error `m.slave' using a cast.
> At least, I see a way to do it, but I don't think it should be done with
> contracts.
Because Java has downcast, a Java upcast is only a loss of static
information about the dynamic possibilities. It is not actually a loss of
any of these dynamic possibilities, as your code demonstrates. There is no
sense in which anything in your code above expresses an intersection or
conjunction of dynamic possibilities. Indeed, the combination of the static
type declarations and the dynamic equality test give you static knowledge
that within the if-body you have the same union of possibilities starting
from either parameter variable.
--
Text by me above is hereby placed in the public domain
Cheers,
--MarkM
_______________________________________________
dev-tech-js-engine-internals mailing list
dev-tech-js-engine-internals@lists.mozilla.org
https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
