On Tue, Dec 3, 2013 at 2:06 PM, Peter Thiemann < [email protected]> wrote:
> > > On 03.12.2013, at 22:09, Mark Miller <[email protected]> wrote: > > ---------- >> From: *Andreas Schlegel* >> <[email protected]<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[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&[email protected]>>, >> "Mark S. Miller" >> <[email protected]<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[email protected]> >> > >> Cc: Brendan Eich >> <[email protected]<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[email protected]>>, >> [email protected]<https://mail.google.com/mail/?view=cm&fs=1&tf=1&[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. 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? > > For new languages or for subsets of an existing language, such as the > distributed portion of Dr. SES, a weaker equality primitive, join, could be > extended to be in bed with contract-membranes in ways that maintain most of > what is useful about object identity, as explained in the thread with Phil > and Jeremy. Not only is join compatible with contract-membranes, it > enhances them by providing a useful new contract combinator. > > > I didn't have time, yet, to chase up all references that you gave in the > email exchange, but it is not quite clear to me in what situation you want > to apply the join operator. > I have found that for most situations where I thought I needed EQ I can get by with join. In a distributed context, I only finally understood object identity once Norm abstracted out the Grant Matcher puzzle from the Escrow Exchange agent. join is adequate for grant matching. And because of the asynchronous nature of distributed programs, it is ideal for the distributed escrow exchange agent. > It seems it only makes sense to apply it to a pair of objects that > (transitively via a proxy chain) refer to the same target object, but > potentially imposing different constraints / contracts. > Disagree with the "only". join was invented for purposes other than contract-membranes, and it is only a recent insight that it would work well with them. It was invented to test distributed identity in a way adequate for grant matching, and to do so in a way pleasant to use in an asynchronous distributed system, where you won't locally know the "answer" to the "test" for a while. It is so named because it also forms a join in E-Order -- the dual of the fork in E-Order caused by sending distributed messages. > In that case you want to impose both constraints on the joined object, > right? > yes. > So you'd have to check EQ-ness first? Otherwise you get an exception? > In the implementation of join, yes. In E, since EQ is an exposed primitive, join is not primitive. Instead, it is defined as def join(x, y) { return when (x, y) -> { if (x == y) { return x } else { throw "..." } } } What I'm advocating in this thread is that, for new languages, there be no exposed EQ operation and that join instead be primitive. > > An open question is how to arrange for the built-in join to be in bed with > user-extensible contract-membranes in a way that both preserves security > under mutual suspicion and provides the needed functionality. A good test > case is a local and a distributed implementation of Horton assuming > mutually suspicious machines. > > -- Cheers, --MarkM _______________________________________________ dev-tech-js-engine-internals mailing list [email protected] https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
