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.