On 12/4/13 5:54 PM, Mark Miller wrote:
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.
Ok good, I see how this provides a meaningful equivalence relation.
But I don't see how it helps your goal.
a) In order to do a membrane of any sort, including a
contract-membrane, you need to use the shadow target technique, where
the system-recognized target for master and slave in your example are
distinct shadow targets. And where the shared real target is not
system recognized, but is only our way of describing what the handlers
are doing; and thus not available to any system enforcement mechanism.
I don't think that all contracts require a membrane, for example, if you
just restrict an object to reading or writing a subset of its
properties, then no recursive wrapping is required.
I don't understand "shadow target technique", but if the master/slave
roles are contracts like Role1 and Role2, then each of them can be
represented by a proxy and the two proxies can share a single target.
You write "If x===y, then uses of x and y *in their common interface*
(i.e., in the intersection of their roles) are interchangeable."
b) But this is untrue in your proposal, even if the same
system-recognized target were somehow used, because the different
handlers can perform different side effects, including differing side
effects on the shared target.
True. I was stuck in the contract world, where the handler implements a
projection.
So I should tune down my proposal to contract wrappers where contracts
are implemented in a suitable DSL that only expresses projections.
Let's distinguish two categories of membrane:
x) A general membrane maintains the basic membrane invariant, that
there is no leakage across the membrane boundary. But invocations that
cross the membrane can have their meaning changed by the handlers in
any way allowed by the JS Proxy invariant enforcement mechanism.
y) A guarding membrane is one which either disallows an operation, or
(identity aside) allows it with the same semantics it would have had
in the absence of the membrane's interposition.
Given checkably-pure functions (which E and Joe-E have but JS
currently does not) one can use the general membrane mechanism to
build a membrane maker to be parameterized by checkably-pure guard
predicates, so that it only makes guarding membranes. What you (and
IIUC Phil and Jeremy) are generally seeking are guarding membranes,
which would answer issue #b. But in JS (as of ES6) these would be
implemented by unprivileged user code, and so not something that the
=== implementation could directly recognize. A new equivalence
operation, whether an EQ-like equivalence predicate or a join, could
be provided as part of the same package and be in bed with this
guarding membrane maker.
Note that the guarding membranes made by this maker would still need
to use the shadow target technique, so objection #a still stands --
testing "the same system-recognized proxy target" will not help you
build these new equivalence operations as part of the guarding
membrane maker package.
My understanding of the above is that given an appropriate way of
restricting a handler to essentially implement a projection, then the
proxy of that handler could safely be transparent while granting an
equivalence restricted to uses in the common interface.
Well, such a handler DSL could be designed and then we could all have
our cake and eat it.
-Peter
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.
Given a synchronous join:
if (join(master, slave)) {
... use master for mastery stuff, use slave for slavy stuff ...
} else {
... do the more expensive thing ...
}
Given the actual async join:
Q(join(master, slave)).then(() => {
... use master for mastery stuff, use slave for slavy stuff ...
}, () => {
... do the more expensive thing ...
});
We're here using join only to test whether it succeeds, not to
actually use its result. Admittedly this is kludgy, but IMO no more
kludgy than the problem statement demands. This would certainly not be
the typical case for using join.
--
Cheers,
--MarkM
-Peter
--
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
