[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
See the Acute system by Sewell and others. http://www.cl.cam.ac.uk/~pes20/acute/index.html -- P . \ Philip Wadler, Professor of Theoretical Computer Science . /\ School of Informatics, University of Edinburgh . / \ http://homepages.inf.ed.ac.uk/wadler/ On 29 August 2014 03:24, "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 >
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
