[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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
