Re: [TYPES] Types in distributed systems

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Thank you all for the given pointers. Much more than I had initially 
anticipated. I skimmed over some of the mentioned papers and they all 
look great. This should keep me busy for a little while.


On 30/08/14 14:26, Philip Wadler wrote:
> 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]
> <mailto:[email protected]>> wrote:
>
>     [ The Types Forum,
>     http://lists.seas.upenn.edu/__mailman/listinfo/types-list
>     <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
>     <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.
>


-- 
Ionuț G. Stan  |  http://igstan.ro