[TYPES] Types in distributed systems

[Philip Wadler]

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" <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
>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.seas.upenn.edu/pipermail/types-list/attachments/20140830/76f65da0/attachment.ksh>