Good, I think we're converging on what the important sub-problem is: building an abstraction mechanism that enables the open-ended expression of projections, but not the expression of non-projections. My previous statements about join were premised on such a projection-only abstraction. But I mistakenly thought that we could build it by adapting the E and Joe-E auditor logic. Sam is right that we can't. Some of Cormac's work on trace-monitoring temporal contracts might be the answer, or at least a place to start.
Once we have such an open-ended projection-only abstraction, then all these questions about equality become interesting and pressing. On Wed, Dec 4, 2013 at 1:55 PM, Peter Thiemann < thiem...@informatik.uni-freiburg.de> wrote: > 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 >> > > -- 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
