Linear Types and RDP?

I’ve been thinking recently about how I might achieve linearity types for RDP. A type is ‘linear’ if it must be consumed at least once… and at most once.

Linear types are very useful. They can be used to enforce protocols, handshakes, that open files are closed when we’re done, that closed files are opened before use. Linear types are often used to prohibit unsafe concurrent access to state, and safely model constraints on computation resources.

For RDP, I don’t really need to enforce ‘closing files’ (since RDP’s ‘Resource Acquisition Is Demand’ idiom achieves that), but I could still benefit from enforcing linear decisions in a protocol, or providing exclusive access for state manipulation. For example, a simple state model for RDP is that state carries a value at every instant, and that a demand may ‘set’ it at every instant, but this does not work well if there might be multiple demands trying to set the value concurrently.

Linear types would also allow me to model response callbacks as dynamic behavior, whereas now they’re a bit special.

I’ve pursued this idea in the past, but kept running up against a problem: how do ‘delay’ and ‘anticipate’ interact with linear types? When switching between choices or ‘dynamic’ behaviors that consume a linear type, how do we ensure there isn’t a brief ‘gap’ or ‘overlap’ in the consumption of said linear type?

I write this article because I’ve finally figured out the answer: linear behaviors in RDP must be consumed *at* a particular logical time (latency, relative to when the behavior was generated). Thus, the only thing you can do with the behavior before that time is ‘delay’, and you cannot delay a linear behavior past its time. This ensures that every path uses the value at the same logical instant, and thus that there are no gaps or overlaps. An interesting consequence of having these temporal-linear types is that they can enforce some real-time constraints.

Ideally, we could use type-inference to determine the time index for each temporal-linear dynamic behavior.

Note: I have no plans to add linear types to my Haskell model of RDP. But they’ll certainly be on the table when I eventually develop the RDP-based language, Awelon.

Advertisements
This entry was posted in Language Design, Reactive Demand Programming, State, Types. Bookmark the permalink.

2 Responses to Linear Types and RDP?

  1. I’ve come up with new concerns since writing this article.

    If there is nothing new in RDP, and demands are spatially idempotent (two identical demands must return identical responses), then from where does uniqueness of linear types originate? What is the base case? If resource capabilities are published to a shared registry – a matchmaker, or linker – then how can they possibly be unique resources?

    What is the story for linear types in RDP? At the moment, I’m thinking they may be incompatible.

    • David Barbour says:

      It seems I’ll need to use an oracle pattern – i.e. a linear type that serves as a uniqueness generator can be provided by the runtime. This can be divided (consuming the parent, but creating two more linear uniqueness generators) or consumed to produce a unique value. A uniqueness generator as a demand on a behavior would allow unique responses.

      The utility of uniqueness is mostly in discovering `unique` demand monitors or state at the edges of the system, which can then be used to provide `global` state or resources on a per-client basis (giving nice qualities of both worlds).

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s