On Wed, Dec 4, 2013 at 6:52 AM, Peter Thiemann < [email protected]> wrote:
> On 12/03/13 23:32, Mark Miller wrote: > >> On Tue, Dec 3, 2013 at 2:06 PM, Peter Thiemann <[email protected] >> freiburg.de <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&to= >>> [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&to=tomvc. >>> [email protected]>>, >>> "Mark S. Miller" <[email protected] >>> <https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=erights@ >>> google.com>> >>> Cc: Brendan Eich <[email protected] >>> <https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=brendan@ >>> mozilla.com>>, >>> [email protected] >>> <https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=dev- >>> [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. 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. 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. 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. > > > >> 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 [email protected] https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
