Hi Sam, I read and followed your message, but I'm now confused about the topic. Are we discussing hypothetical variants of JS in which we are happy to trust user code to uphold system invariants? Or are we discussing what can actually be done in current and future JS? If the former, I agree, but why is this a more interesting question than what we would do if we had even fewer legacy constraints?
Checkable purity in E is based on E's auditors which are haphazardly documented. I'll try to find some relevant pointers soon. Joe-E's auditors are based on E's. Checkable purity in Joe-E is explained at < http://www.cs.berkeley.edu/~daw/papers/pure-ccs08.pdf>. On Wed, Dec 4, 2013 at 11:53 AM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu>wrote: > On Wed, Dec 4, 2013 at 11:54 AM, Mark Miller <erig...@gmail.com> wrote: > > On Wed, Dec 4, 2013 at 6:52 AM, Peter Thiemann > > <thiem...@informatik.uni-freiburg.de> 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 > -- 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
