On 12/03/13 23:32, Mark Miller wrote:
On Tue, Dec 3, 2013 at 2:06 PM, Peter Thiemann
<[email protected]
<mailto:[email protected]>> wrote:
On 03.12.2013, at 22:09, Mark Miller <[email protected]
<mailto:[email protected]>> wrote:
----------
From: *Andreas Schlegel* <[email protected]
<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[email protected]>>
Date: Tue, Dec 3, 2013 at 6:33 AM
To: Tom Van Cutsem <[email protected]
<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[email protected]>>,
"Mark S. Miller" <[email protected]
<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[email protected]>>
Cc: Brendan Eich <[email protected]
<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[email protected]>>,
[email protected]
<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[email protected]>
Hello,
yes you're right, the problem of the contracts researched by
prof. Thiemann was, that the targets behind the proxies could
not be compared by == and ===.
How can I merge contracts of multiple proxies and represent
them by just a single proxy, if I cannot compare them (or get
the target)?
We have discussed first an approach with new operators
spezific to proxy comparism but this is not the way.
If I can include a trap for asking the proxy if he's
transparent or not, it is possible to use the same operators
by asking the proxy.
Yes, for JS or any language where identity is based on an
equality *predicate*, it is too late: The conflict between
contracts and identity can't be fixed. Note that, through my lack
of foresight about this issue, E is among the languages that
can't be fixed.
Actually, I don't think it is too late. We have come up with a
design where the proxy's handler can determine whether equality is
opaque or transparent - this is what Andreas is currently trying
to implement. This way, you may create proxies with different EQ
semantics while still guaranteeing that EQ is an equivalence
relation.
There is much here that I did not understand: What is "transparent" vs
"opaque" equality? How can it be up to the handlers to determine this,
on the one hand, but still guarantee that it is an equivalence
relation, on the other hand? These two seem to be in conflict.
Transparent equality: EQ recursively dereferences proxies to their
ultimate non-proxy targets and compares those.
Opaque equality: EQ directly compares, i.e., the current state of
affairs in JS.
Consider
var p = new Proxy ( target, handler);
The trick is *not* to trap equality, but to let the handler control
whether EQ dereferences p to target before comparing pointers. Notice
that one handler only controls one step of dereferencing. If target is a
proxy, again, then EQ recursively asks that proxy's handler until either
a non-proxy object is reached *or* the handler does not request further
forwarding.
Here is an outline of the proposal:
http://proglang.informatik.uni-freiburg.de/projects/JSProxy/proxy.pdf
With this design each individual proxy can choose to be transparent or
opaque, while guaranteeing that EQ implements a non-trivial equivalence
relation - the latter is straightforward to check.
In any case, weakening EQ so that the only guarantee that remains is
that it is an equivalence relation would break existing uses of EQ in
JS (i.e., "===" aside from NaN). For example, an EQ that always said
true would still be an equivalence relation, so clearly something more
is needed. 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?
Observational equivalence is hard to argue against, but I’ll give it a
try, anyway. I believe such a strong spec is too limiting and excludes
many useful applications. Examples that I am concerned about are
wrappers for transparent monitoring and enforcing contracts. Apparently
and unsurprisingly others are concerned about these examples, too.
Here is an example scenario. Then, I provide some code fragments to
support a proposal for a weaker spec for ===. This leads to a question
about join in the end.
~~~~~~
Consider a function sync(master,slave) that takes two objects and that
wants these two objects to exchange information: the master syncing with
the slave. For efficiency, the function sync first checks if these two
objects are “the same”, in which case no synchronization is needed;
perhaps a flag or timestamp needs to be set to indicate that
synchronization has been achieved. If the objects are different, then
some potentially expensive sequence of method calls may be needed to
exchange the information. (Perhaps involving authentication, passing of
capabilities, etc.)
If we put a contract on sync that imposes a Master interface on master
and a Slave interface on slave and this contract is implemented using
opaque proxies, then the sync function is losing the efficient shortcut.
(Why would an object implement the Master and the Slave interface? Here
are two possible reasons: the master may be elected at run time or there
may be a hierarchical system where level-n masters are slaves on
level-(n+1))
~~~~~~
A proposal for a weaker spec for ===
In the following code fragments, I am using Java interface notation to
indicate a dynamically checked contract for brevity.
Let’s say we have a function that can treat “same” objects more
efficiently, as motivated in the sync example:
function f (x, y) {
...
if (x === y) {
… x.foo(); x.inc(); y.inc(); z = y.bar() …
}
…
}
Using contracts, x and y may be restricted to certain roles.
Let’s say,
interface Role1 {
foo();
inc();
}
interface Role2 {
bar();
inc();
}
var g = … apply contract( (Role1, Role2) -> Any ) to f;
var obj = {
state: 42;
foo: function () { this.state = 0; };
bar: function () { return this.state;};
inc: function () { this.state++; };
}
g (obj, obj);
I want to argue that this call of g should execute the code guarded by
(x === y) in f, because the interposition of the contract may otherwise
change the semantics. In other words, I want to make sure that g(obj,
obj) either raises an error due to a contract violation or it has
exactly the same effect and result as f(obj, obj).
What guarantees can we assume below (x===y)?
If x===y, then uses of x and y *in their common interface* (i.e., in the
intersection of their roles) are interchangeable.
In the example, the common interface is
interface Role1&Role2 {
inc();
}
therefore
if (x === y) { … x.foo(); x.inc(); y.inc(); z = y.bar() … }
must be observationally equivalent to each of the following
if (x === y) { … x.foo(); x.inc(); x.inc(); z = y.bar() … }
if (x === y) { … x.foo(); y.inc(); y.inc(); z = y.bar() … }
if (x === y) { … x.foo(); y.inc(); x.inc(); z = y.bar() … }
That is, sameness of x and y is reduced to the ability to observe the
same state changes through both x and y. Of course, limited to the
common interface.
The extreme case for the above f-example would arise if the interfaces
Role1 and Role2 were disjoint. In this case, no transformation would be
sanctioned from the knowledge that x === y.
~~~~~~
This observation leads me to a question about join:
If only join is provided, but not EQ, then I don’t see how to implement
the function f above. If I successfully obtain z = join(x, y), then it
fulfills interface Role1&Role2, but I cannot use it in lieu of x or y in
the body of the conditional because it does not implement foo() and bar().
If Role1&Role2 were empty, then the successful join would produce a
useless object. For example, in the Master/Slave example above, it is
highly likely that the interfaces are disjoint.
--
Cheers,
--MarkM
-Peter
_______________________________________________
dev-tech-js-engine-internals mailing list
[email protected]
https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
