Re: Capabilities interact nicely with Substructural Types and Reactivity

Linear types are very useful for enforcing that protocols complete. E.g. if
you have a trade protocol, you don't want it left hanging in a limbo.
Instead, each 'step' in the protocol can be linear, and enable only the
particular methods for that step. (State machines can be modeled this way,
too.)

A good example of using an affine type is to break up "rights" to a
rendering window: at first you get the whole rectangle as a type, but then
you can break off a piece of that window and delegate it. Conceptually, we
cannot really 'copy' the affine type, just split it. We could also use
relevant types to enforce that every part of the window is actually used,
or at least returned to the pool, rather than dropped and forgotten.

Really, these are very powerful, very simple concepts with a wide variety
of applications - and a good fit for proof-by-construction, for creating
those 'rules' of a valid game. The problem is that capabilities allow
participants to leave the game at any time, which can result in situations
that, while they are perhaps not insecure, are at least painful.


On Thu, Sep 12, 2013 at 5:40 PM, Mark Miller <[email protected]> wrote:

> DavidB, I think the discussion is getting side tracked by a minor point. I
> tried reading your first message on this thread. It sounds cool but I don't
> actually understand it either. If it could be restated in terms more of us
> could understand -- especially non-type-theorists -- I suspect we'd all be
> quite interested.
>
> Concrete example would help tremendously!
>
>
>

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk