43 Future work

43.1 Towards a calculus for stream processors

Certainly, the implementation of stream processors used in the Fudget library could serve as a semantic base for formal reasoning about stream processor and fudget programs. But we might want to use a more abstract semantics of stream processors, which would also capture truly parallel-evaluating and indeterministic stream processors. Suppose that we have an implementation for indeterministic stream processors. Would the Fudget library still work? Or are we relying on some subtle ordering of messages that today's sequential implementation gives us, thus avoiding tricky race problems? The answer is probably that most of the library would still work, but at some points, we implicitly rely on implementation details. As one example, consider two identity stream processors in parallel:

p :: SP (Either a b) (Either a b)
p = idSP -+- idSP
When using the implementation from the Fudget library, p is nothing but the identity stream processor for type Either a b. But if we were to use indeterministic stream processors, we cannot be sure that message order would be maintained through p. If we first send Left a immediately followed by Right b to p, why should there be a guarantee that it will output these messages in the same order?

Naturally, the Fudget library does not have a lot of identity stream processors in parallel. Fudgets, on the other side, are abundant in the library, and they very often sit in parallel. One example where implicit assumptions exist about message order output from parallel fudgets is in the radio group fudget radioF. Another, more explicit, assumption was made in the implementation of the Explode game in Section38.1.1. In Explode, it is crucial that the internal communication after a explosion has priority over external communication. This is what the continuation-based implementation of stream processors gives.

In order to reason formally about indeterministic stream processors, we present the stream-processor calculus (SP-calculus).

43.1.1 Basic stream processors

There are seven basic ways of forming a stream processor. We let the letter x denote a variable, and s, t, ... stream processors.
x(Variable)
s!t(Put)
x?s(Get)
s<t(Feed)
s<<t(Serial composition)
s+t(Parallel composition)
ls(Loop)
For the reader who has used stream processors in the Fudget library, these operators should be familiar. The operator ! correspond to putSP, and ? can be seen as a combination of abstraction and getSP: x?s is the same as getSP (\x -> s). The feed operator in s<t feeds the message t to the stream processor s (similar to startupSP, which feeds a list of messages to a stream processor). Serial composition corresponds to -==-, and parallel composition and loop are untagged, corresponding to -*- and loopSP.

43.1.2 Congruence rules

Following the style of [BB90], we define a bunch of congruence rules which can be used freely to find reaction rules to apply.
s+t===t+s(Commutativity of +)
(s+t)+u===s+(t+u)(Associativity of +)
(s<<t)<<u===s<<(t<<u)(Associativity of <<)
s<<(t!u)===(s<t)<<u(Internal communication in <<)
(s+t)<u===(s<u)+(t<u)(Distributivity of < over +)
(s!t)<u===s!(t<u)(Output from <)
(s!t)<<u===s!(t<<u)(Output from <<)
(x?s)<t===s[t/x](Substitution)

43.1.3 Reaction rules

Whereas the congruence rules in the last section can be freely used in any direction without changing the behaviour of a stream processor, the reaction rules are irreversible, and introduce indeterminism. The reason is that by applying a rule, we make a choice of how message streams should be merged. There are two places where merging occur, in the output from a parallel composition, and in the input to a loop.
(s!t)+u-->s!(t+u)((Output from +))
We can derive a symmetric rule by using the commutativity of +, but when it comes to the loop, we need two rules.
l(s!t)-->s!l(t<s)(Internal input to l)
(ls)<t-->l(s<t)(External input to l)
As an example of these rules, consider the stream processor (s!t)+(u!v), which can react to s!(t+(u!v)), but also to u!((s!t)+v), using commutativity. Similarly, the loop (l(s!t))<u can react to both s!l(t<s)<u and l(s!t<u).

43.1.4 The \-calculus embedded

The SP-calculus is more expressive than the \-calculus, and we can define a translation from the \-calculus into the SP-calculus.
[[x]]=x(Variable)
[[\x.M]]=x?[[M]](Abstraction)
[[MN]]=[[M]]<[[N]](Application)
The substitution rule for the SP-calculus correspond to the beta-rule of \-calculus. However the eta-rule, which would correspond to x?(s<x)===s, does not hold in general, something that we will see after having defined equivalence of stream processors.

Having the power of \-calculus, we can define some familiar stream processors, such as the identity stream processor and the null stream processor.

fix=f?(x?f<(x<x))<(x?f<(x<x))
id=fix<(f?x?x!f)
0=fix<(f?x?f)

43.1.5 Equivalent stream processors

We can define an equivalence === as the greatest equivalence relation satisfying:

s1===s2 if and only if:

From this definition, we can see that x?(s<x)===s does not hold if s can output something. The left-hand side is blocked, waiting for input, and could not match the output from s.

43.1.6 Future work

More investigation is needed to turn the SP-calculus into an operational semantics for stream processors:

43.2 Stream processors as Internet agents

The interest in the Internet has resulted in a focus on new features in programming languages. The information exchange over Internet has exploded, and there is a need to exchange not only text, graphics and sound in a smooth way, but programs. For program exchange to be smooth, the receiver of a program must be certain that it does not do nasty things with his computer. This can be achieved by accepting programs in a typed language, where the type should give information about everything that the program can do, including all kinds of side effects and communication. This is a property that stream processors have, they can do nothing but outputting messages in a known type.

There is also an interest in having programs running for a while at one site, then moving on to other sites, while gathering information etc. Such programs are often called mobile agents. As we have seen in Chapter25, the necessary machinery for mobile agent programming is already there in the stream-processor concept. However, we need support in the underlying language implementation so that values that are closures can be exchanged between computers.