[TYPES] Types in distributed systems

[Frank Pfenning]

Session types were invented to address well-typed communication
between processes.   I believe Honda's CONCUR 1993 paper "Types for Dyadic
Interaction" started this line of development, with much subsequent
work I will not try to review, alongside other foundational work on
directly assigning typed to versions of Milner's pi-calculus.

More recently, it was discovered that session types arise from a
Curry-Howard interpretation of linear logic, where linear propositions
correspond to session types, sequent proofs correspond to processes,
and cut reduction corresponds to communication.  In this kind of
system, deadlock and race freedom are guaranteed by typing.
See Caires & Pf. (CONCUR 2010) for a pure calculus, and Toninho et al.
(ESOP 2013) for a full functional language with an encapsulation
of session-typed concurrency in a monad-like construct.

There is a natural notion of subtyping that arises in the system if
you have labeled forms of internal and external choice.  This permits
some forms of backward-compatible upgrades of services, but may
not address everything you had in mind.

  - Frank


On Thu, 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
>



-- 
Frank Pfenning, Professor and Head
Department of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3891

http://www.cs.cmu.edu/~fp
+1 412 268-6343
GHC 7019