Messaging without time: modeless user-interfaces for programs
Sun 21 Feb 2010 16:31 NZDT
Most thinking about messaging seems to be framed in terms of process languages, like the π-calculus. In the π-calculus, processes evolve according to an internal clock, the ticks of which correspond to communication events between subprocesses. Many real programming languages based around messaging, like Erlang, are based around similar models, meaning that programmers write programs whose notion of time is implicit, rather than explicit. This can make it difficult to write programs which can reason about differing orders of events or cope with contradictory assertions about the state of the outside world.
An alternative way of dealing with messaging is to take an epistemic reasoning approach closely connected with Functional Reactive Programming (FRP): instead of writing programs that wait for the arrival of specific messages, one at a time, write programs that deal with a queryable monotonically increasing collection of all messages that have arrived or departed so far. Metadata about each message—the sender, the recipient, the time of receipt—are reified as queryable fields attached to each datum in the collection. The state of the program’s world is directly derivable from the program itself and the collection of messages that have been exchanged thus far.
By letting programs step back from the low-level detail of the exchange of messages and take a broader overview of the whole conversation thus far, we let programs behave much more flexibly in the face of such common distributed-systems challenges as lost messages, duplicated messages, out-of-order messages, inconsistent data, and timeouts.
I’ve been off-and-on thinking about these timeless ‘epistemic messaging’ systems for a couple of years now, since a customer project let us investigate their potential suitability for a particular style of long-lived database; while I could write more, and hope to in future, I want to record an observation that occurred to me a couple of days ago about a connection between modeless user interfaces and timeless messaging systems.
In the same way that modal user interfaces constrain the interaction between the user and program into a sequential, question-and-answer style, π-calculus-style programs constrain the interaction between programs in a distributed system into a similar one-thing-at-a-time sequential style, which can lead to programs having a sensitive dependence on message arrival order. Modeless user interfaces, by contrast, make possible a more open-ended, non-linear style of interaction with the user, and epistemic messaging does the same thing for program-to-program interaction: because the state of each program (and thereby its next action) is derived from the collection of messages that have been exchanged, the program can more easily be written to cope with messages arriving in an unusual order. Epistemic-messaging programs can even be written to be able to re-plan (and maybe even re-execute) their actions if received messages were to be permitted to be replaced mid-run.
(Aside: I wonder if there’s a connection here to the Curry-Howard isomorphism? A program operating epistemically over a collection of messages feels like a kind of type/formula, where a similar program in a π-calculus-like system feels like a program/proof.)