Signature for Interaction, Part 1: binary case

Well I do not find time today --- my plan was there is going to be brief and gentle illustration of signature (or types) for interaction, with many examples, and this will happen, but not now. And after that introduction we shall come back to "Modelling Interaction" in its third installment, at which point we shall be able to articulate the principle augmenting Frankel's thesis with a concrete notation with which we may be able to write what may correspond to "class models" in the present setting (NB: not yet with graphical syntax --- that is for later).

Our narrative can be interrupted by other interesting things which are taking place --- so the narraive may not be a completely continuous business but the basic structure is like that.

By the way a brief report: based on Gary's syntax we are now converging into a rather neat syntax for scribbling ---- I think it is neat. It's curly but not too curly --- but it is at readers' discretion to judge how cosy you find it.

* * *

I cannot spend much time but why not just to give a flavour of what we are going to discuss from tomorrow? A prelude...

Here is a bit of signature for a method:

int foobar(string s, int i)

As we already argued this is a notation for a special (and very tractable) instance of interaction.
Then why not we can write this as (the following is not that syntax Gary and I have arrived at: it is one of the syntaxes we once used as the signature for two-party conversation):

protocol Foobar {
foobar ?(string, int);
!(int)
}

This is a way to abstract how somebody receives (?) two arguments with an operator name "foobar" and returns an integer. But why we are using such marks as "?" and "!" ? Easy, since we are in the symmetric world:

...... This kind of interaction is relevant to both parties. (Frankel)

But request-reply is also relevant to both parties. If we consider the "interaction" signature above from the caller's viewpoint, what we get is:

protocol FoobarUser {
foobar !(string, int);
?(int)
}

where we have exchanged ? and !. We have not done much, but this time this "signature" represents a user/caller's side of the story: the user sends with the method name "foobar" with a string and an integer, and then receives an integer. So this notation is symmetric: it assumes that interaction is "relevant to both parties".

Haven't you never thought that it is strange that we can write a method signature from the viewpoint of a method but not from the viewpoint of its user? Well in functions we do not have to distinguish them (since functions accumulate ...). But now we can --- and need to --- write both sides of the story. Since the world is now symmetric in general.

Of course this notation becomes interesting when we treat more complex interactions, on which we shall discuss next.

Before closing for today I record when this idea of signature happened: it was 1993. And we thought we found types for describing interaction rather neatly, one of the possible candidates for "signature for interaction". Well we never knew at that time how far we had to come from there. This was the beginning, and perhaps even a nice beginning too, but still "signature for interaction" simply it is not: it does not serve our purpose: it serves some class of interactions well, but not their whole.

So the next post will discuss good stories and bad stories about this notation: how this notation nicely sevres as a way to describe, abstractly, many kinds of interactions and validate our programs against such descriptions: and where, to our dismay, it fails disastrously; and why it does so. That observation will lead us to a more general idea of types for interaction whose finding needed many dialogues with our respectable industry and academic colleagues (and which by the way has already been implicit in the notation above, as it turned out --- but without our ever knowing, as is often the case).

And at that point we shall become ready to do real scribbling...