[ 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
