[TYPES] Types in distributed systems

[David Ryan]

Hi Stan,

First off, let me say that I would know less about the theory of type
systems than you.  However, I've spent many years being interested in the
application of data in distributed systems.  I developed Argot (
www.argot-sdk.org) to address the issues you've raised.

Argot uses a concept analogous to a dictionary.  Each system contains a
dictionary of versioned data types.  When communication begins, first a
small set of core data types are compared to ensure the base dictionary
types are compatible (these are data types used to define other data
types).  Following this, the two systems compare each message to be
communicated.  The peers will then only communicate with the messages that
are commonly defined.

Argot is designed to allow individual systems to change over time, yet
continue to communicate.  Anyone working with XML type systems will know
the difficulty of keeping systems in alignment.

Regards,
David.



On Fri, Aug 29, 2014 at 10:57 PM, Harley Eades III <harley.eades at gmail.com>
wrote:

> [ 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 <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
>
>