On Wed, Dec 4, 2013 at 11:54 AM, Mark Miller <[email protected]> wrote: > On Wed, Dec 4, 2013 at 6:52 AM, Peter Thiemann > <[email protected]> wrote: >> >> >> 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. > > > 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 believe that the shadow target technique is in fact required to implement contracts on top of proxies. First, it's only required at all if we need to support higher-order contracts on frozen objects, as your paper discusses. Frozen objects are a minority use case in JS today, and it may be that trading off support for them with other desirable properties of contracts is worth it. Second, many uses of frozen objects can be handled without shadow targets, by simply performing a shallow copy of the object, and proxying all of the fields. This works for any object other than those that have some immutable (ie, nonconfigurable _and_ nonwritable) and some mutable fields. Third, the problem with frozen objects, and the reason that shadow targets are needed at all, is because of precisely the problem that Andreas and Peter raise in this thread. The invariant enforcement design that proxies follow, which is exactly the same design we chose in Racket (see our OOPSLA 2012 paper), is to compare the result of an intercepted operation with the result of the same operation on the target. If the two results are not "equal", then an error is signalled. In Racket, the sense of "equal" chosen is one that traverses proxies, and therefore no shadow targets are needed. Unfortunately, JS provides only one sensible equality operation, which is `===`, and you and Tom wanted to preserve the invariant that: `x.f === x.f` for all immutable data properties on non-host objects. This would reduce expressiveness without shadow targets, which fortunately don't cause problems because we've already given up on any equalities that traverse proxies. But once we're discussing equality predicates that traverse proxies, shadow targets are no longer an issue, because such equality predicates can _fix_ the problem that required shadow targets in the first place. > > 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. > > > 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. "Guarding membranes", in your terminology, are just "contracts" (or "projections" in the terminology of denotational semantics, going back to the 70s). However, there's no reason that they need the special level of language support you describe. (Note: I've had trouble finding any documentation for E's checkably pure functions.) In fact, I don't think that level of support buys you anything. We already have the fact that intercepted operations return a semantically-appropriate value, by the basic semantics. And even with checkably-pure functions, using a proxy invokes potentially arbitrary code which you wouldn't want to do without trusting the code. In Racket, we've used a proxy system which (a) supports an equality operation that traverses proxies, and (b) allows proxy handlers to perform arbitrary operations without any problems that I know of based on these issues. Sam _______________________________________________ dev-tech-js-engine-internals mailing list [email protected] https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
