On Tue, Jul 1, 2014 at 4:55 PM, Matt Oliveri <[email protected]> wrote:
> > But interfaces ARE wrappers! That's the point! > > Ah. I forgot you're using some fancier version of interfaces than Java. > I don't really think so. The two differences, in my mind, are (1) you can't necessarily downcast back to the object [up to the dev], and (2) the interface object construction syntax will be different, because interfaces in BitC can't be tied to a non-existent class hierarchy. But otherwise they are very much like Java interfaces. > But even so, they're not regular wrappers since they share the object > id of the thing they wrap, or so I thought. I don't recall saying that, but it's certainly not my intention. An interface and the object it wraps are logically distinct objects. Downcast should be thought of as an existential "open" operation on the encapsulated thing. > So it still seems > like under your proposal, capabilities effectively become (static > type, object) pairs. Maybe that's the right way to do it with a strong > type system, but maybe not. > That's what capabilities have always been. The classic formulation is that a capability combines the authority to perform operations with a designator to the state on which those operations act. When translated into PL terms, "authority" is essentially "the list of methods". > ...in dynamically checked > languages like E, you don't even have/get to downcast, so there's no > option of attenuating authority just by changing the type. Yes and no. Yes that you can't do it this way. No that we aren't just changing the type, because the "open" operation I'm contemplating gets you a completely different object. The notion of interface that I'm thinking about really *is* wrappers. > Many people > think of static types as convenience and performance improvements for > a dynamic language. Java is compatible with that (limiting) point of > view. If BitC is not, it could be perceived as too theoretical, unless > you put a lot of effort into reeducating regular programmers about > what strong typing is really about, and convince them it has enough > escape hatches to not be crippled. > I think that's a little strong. Most programmers don't view things that way at all, which is good, because that view is completely wrong. Static types restrict which names can be bound to which things. It's true that, under the theory of type erasure, all statically typed programs can be executed as dynamically typed programs. The reverse is not true. Of all the things that will make BitC seem theoretical, this one has to be pretty close to the bottom of the list. The "guarded cast" mechanism that I'm contemplating actually can't be done with type erasure, because the guard check I'm proposing is "present an object with the required type" as opposed to "pass an object to a dev-supplied guard routine". The only reason my version is possible is that we are now contemplating dependent type. This means that the dev-supplied guard routine can now (hypothetically) be encoded in the type. Which is mostly a mis-feature, except that when *simple* things are encoded in the type they can be compiled out where guard procedures often cannot. So yes. You're making a very interesting observation here, which is that the type erasure story ceases to hold when the type system can do substantial computation. I think the re-education load here is going to have a lot to do with idioms. We may end up *having* an unusual type system. The question is how we will *use* it. Programmers coming to BitC will set their perceptions and expectations based on how the early folks write our code. If we go hog-wild embedding proofs in dependent types, we're probably screwed. But if we use dependent array bounds that's something whose value is easily seen. > > What I'm saying is that downcast is a de-encapsulating operation, and > > de-encapsulating operations shouldn't be forced on the designer of the > > object. > > That point of view would make type theorists very happy, but again, I > don't think it's the point of view of most programmers. Changing the > type isn't actually changing the thing, conceptually, so downcast is > just a workaround for missing static information. That is, and always has been, a wrong understanding. I'm certainly not going to hold BitC to backwards compatibility with a foundational security flaw. > I don't yet see what the > additional complexity of your proposal provides for the programmer. I think that's because you haven't had an opportunity to program in capability systems that have a secure de-encapsulation mechanism. But setting that aside, one simple way to say it is that we're getting a mechanism for existentials in a way that lets us use the *same* mechanism for downcast. In a system that doesn't have a class hierarchy, you'll sometimes need a way to get from an interface reference back to the underlying object. At other times the interface acts as a modularity or protection boundary, and you want to be able to do that too. Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
