Re: [TYPES] Types in distributed systems

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

On 02/09/14 11:55, Peter Sewell wrote:
>> 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?
>
> As you can see from the earlier responses, there's been a lot of work
> addressing different aspects of this problem.   To quickly (and
> partially!) summarise, we have:
>
> - typing to ensure message-passing endpoints conform to some protocols
> (session types etc.), as several people have mentioned
>
> - partially typed systems, in which type-checking part of the system
> ensures that its interactions with some other untrusted (and hence not
> necessarily type-correct) part will not be disastrous.   Andrew
> mentioned James Riely and Matthew Hennessy's work on this, Jan Vitek
> and I dabbled in this direction
> (http://www.cl.cam.ac.uk/~pes20/wrapall.ps), and there's a lot of more
> recent work, especially in non-distributed PL contexts (eg Richards et
> al.'s OOPSLA 13 paper, like types, etc.).
>
> - typing that ensures safety properties in the face of version change
> of some of the endpoints.   Phil mentioned our Acute language, and
> there's also the HashCaml follow-up
> (http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html).   These explore
> how one can preserve type abstraction boundaries using only runtime
> checking of channel-name identity - basically implicitly versioned
> communication channels.
>
> - typing to ensure that dynamic updates of endpoints will work, as
> explored by Mike Hicks and others.

Thank you. This is a very useful summary to have by when studying this 
stuff.

It looks to me that the 3rd point is a subset of the 2nd one? By virtue 
of seeing different versions of a type as different types altogether?


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