[TYPES] Types in distributed systems

[Harley Eades III]

Hi, Stan.

Just a quick response.  A busy Friday for me.

This reminds me of this tech. report:

http://www.dcs.gla.ac.uk/~simon/publications/TR-2003-131.pdf

I know that linear types as session types are also very promosing.  Take 
a look at some of the papers here:
   http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html
   http://www.cs.cmu.edu/~fp/publications.html

You might also be interested in looking at the pi-calculus and its type
systems.  A quick google using “pi-calculus type system” will bring up
a bunch of options including papers related to session types.

I hope this helps.

.\ Harley Eades

On Aug 28, 2014, at 10:24 PM, Ionuț G. Stan <ionut.g.stan at gmail.com> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hello,
> 
> First, let me acknowledge upfront that I'm a complete dilettante when it comes to type theory (I'm still working through the first chapters of TaPL). That means that what I'm about to ask will be either stupid or extremely inexact. Nevertheless, I'm curious.
> 
> Now, onto my question...
> 
> The TL;DR version is: how does one specify types in a distributed programming model, like actors? And how much can we trust these types?
> 
> I was debating today, on Twitter [1], how to type the sets of messages two actors can exchange; a producer (P) and a consumer (C).
> 
> Let's say that the possible set of messages produced by P is M. We would like, by means of a type system, to know that C can handle: 1) just messages of type M and 2) all possible messages of type M.
> 
> M could be represented by a sum type. Let's consider this particular one:
> 
> M1 = A | B | C
> 
> In a closed world this makes complete sense (to me, at least) and it's easy to verify statically. But in an open world setting, like a distributed system, where P and C are on different machines that may be upgraded separately, things look harder to me. You may guarantee statically that the two properties are met, but at runtime there may appear race conditions that violate the second property.
> 
> For example, we deploy P1 and C1, both agreeing on M1. Next, we add a new variant to M1:
> 
> M2 = A | B | C | D
> 
> P1 and C1 are updated accordingly and we get P2 and C2, which we try to deploy, but a race condition appears and P2 send message D to C1. Obviously, C1 does not understand it. Even though the type system told us that C1 can handle all variants of M, it can't actually.
> 
> A similar scenario appears when removing one of the variants of M1.
> 
> Is there any typing approach to this kind of problem?
> 
> It looks to me that types would have to include a version as well and all runtime communication between different versions should be prohibited by having versioned communication channels.
> 
> Does anyone have any insights or pointers to articles, papers or books that discuss this sort of problem?
> 
> Thank you for reading this!
> 
> 
> [1]: https://twitter.com/shajra/status/504568858967953408
> 
> -- 
> Ionuț G. Stan  |  http://igstan.ro