Communication is a great glue

We have been working on theories of session types, and developing a language for session types. Working on session types and conversations (as in Scribble) is a real fun, since settling its status is not so easy. It is not a "technology" though it is a sort of technology. What is it? Is it for a "programming paradigm", such as "session-oriented programming" or "conversation-oriented programming"? Well I would surely like that kind of idea, and we have been having a lot of discussions, but one interesting thing is that, while these ideas are fascinating and surely worth pursuing, that may not be all.

This is because communication is a great glue. It is already a glue (people are using web's protocols often for that purpose, integrating applications). but its real power has not been fully exploited yet, high-level sessions (soon I will explain) and session types will play a central role when we combine different programming languages, different runtime, different abstraction levels, different applications, different virtual machines. So it cannot be only for a specific programming paradigm. By its very nature, sessions and session types, and in fact communications, are to be located between programming languages, between different runtime systems, between different levels of abstractions, between different operating systems, between different applications.

So sessions exist in and for such "betweens". Yes we can have pure session-oriented languages, this will be beautiful and will teach us quite a lot, but the true nature of sessions and session types lie in its sloppiness, its multiplicity, its power to connect the homogeneous and to connect the heterogeneous.

A high-level session is close to a session as we know in network engineering, a session in TCP, a session in SMTP, a session by cookie (well is that a real session? I know you are doubtful, I am too, but still it shows there is some need...), a session in DCCP, that is it, a session naturally comes about when you need control for your asynchronous messages, and you do need many kinds of control, for example flow control, either flow control of two ends (as embedded from the first in TCP) or more global flow control often centring such notions as TCP-friendliness (which is not a mystical notion at all, it is a notion like United Nations, but more effective).

So that is a session as found in network engineering. A high-level session differs from its network-level counterpart in the following two points:

1. It has a structure: it consists of communications of discrete messages, often typed, and is constructed by combining these communications through several basic primitives such as sequencing, local branching, recursion, loops, exceptions, etc.


2. It is a logical unit of interactions, abstracting underlying transport-level details (such as TCP connections), so that it can in principle survive transport failures, it can span over several TCP connections, or even over different protocols, etc. etc.

Of course we all know about the second point, this is what you find when you are chatting with somebody using say skype. But sessions lift them to a first-class programming concept, the idea being explored and materialised by Ray with Nobuko, backed up by a theory developed by Dimitris, Mariangiola and others. As to the first part, you can experience "structure" when you ever program with session types. This "structure" is where "types" in session types play the key role: types describe and assure structures, the best analog we find in usual programing languages is types in ML (Ocaml), Haskell, and to some extent, Java.

This is sessions and session types, or conversations and conversation types (we call high-level sessions "conversations" when we wish to be a little more friendly).

So we have sessions and session types, and, I repeat, though there can be something like "pure session typed programming", which I find fascinating, we also need a robust and impure concept, impure since it will be embedded in a diversity of programming languages, in a diversity of layers of implementations. And this concept should become so well-digested philosophically and descriptively, so effective in performance and in engineering, so well-understood in theory and systems, and so convenient to scribble with, that it will in the end become something you find mundane and matter-of-fact in programming, such as while-loop, if-then-else, etc. etc. Well the new constructs may need more care than these sequential counterpart in their introduction, but it should be as simple and as mundane, when they get finally used.

The diversity of the contexts where this simple notion can be placed, is staggering. Think of parallel computing. Andi and Ray are studying about sessions in parallel computing, where sessions are used in stateless, convergent, deterministic parallel computing. So this is sessions in the world of stateless computing.

Or sessions for servers, for example a server-side of Gmail, (well its client-side too), this is very stateful, if you save a mail, you want it to be saved, even if it has not been saved before, this is what we call stateful. This state, whose connection to interactions can be best understood using the example of List in Milner's textbook on CCS, where interactions and states are exactly and deeply related in just three pages using a very simple example, this state is what can make computation so rich and hard to control, and sessions are going to control it by articulating it by the program's interactional behaviour, either with outside or with other internal entities say threads. These are generally sessions in the world of stateful computing.

So sessions and session types will play many roles. It has its depth in a simple engineering desire, it has its theoretical basis in a magical formalism called the pi-calculus, as well as its theories of types, which in turn come from the lambda-calculus. And its engineering implications, including infrastructural elements which need to assist them, are deep and broad, of which only a little bit (but hopefully some of the key starting bit) has been explored.

Exploring its engineering and theoretical implications leads us to many thoughts, opening up the notion of computing into a broad universe of interactions, in practice and in theories.

kohei