I've been really negative about checked downcast in my mind, without quite putting my finger on why. It finally occurred to me that downcast is an operation that amplifies rights. Assuming the check passes, you get back an object that has a bigger API (therefore more authority) than the original. If you look at that from the capabilities perspective, that raises some real concerns.
The seal/unseal pattern suggests a possible resolution. What I'm about to describe definitely needs to be refined, but I want to get a first reaction. We're looking at an expression "X as Y". The question is: under what conditions can this be performed? Two sensible answers are: 1. Whenever X is a subtype of Y, because the operation is strictly reducing authority. 2. Whenever X implements a method "as() -> Y" Now the second one is kind of interesting, because it seems like the right place to implement the unseal pattern. Suppose we replace it with: 2. Whenever X implements a method "as(guard: T) -> Y" and make the requirement be that the caller must present proof of authority to unseal in the form of an value of type T. If T is some global type (e.g. bool or unit), then anybody can fabricate a guard value, and the "as" operator can then be called by anyone. But if T is an *opaque* type it cannot be instantiated by anyone, and we can think about programs in which the possession of a suitable guard value serves as proof of authority. And incidentally, a dependent type system makes this more powerful than it looks, because T can be a dependent type that is conditioned on a particular *instance* of an interface... Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
