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.
-Peter
_______________________________________________
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
