Full vs. partial reification

My research project is called interactive programming. The central concepts are (1) reification, where a big-step semantics is taken to characterise a data type, and evaluation to produce instances of this data type; (2) reactivity, the interpretation of a program as a transition system whose states are such instances; and (3) persistence, a means for sharing state across transitions so that common substructure is not duplicated. Since none of these ideas is particularly novel, I need to be careful in my treatment of related work.

Reified evaluation arises, in a restricted form, in Umut Acar's self-adjusting computation, as well as in debuggers that record execution traces or similar structures. Reactivity is central to visual programming, spreadsheet languages, functional reactive programming (FRP), and again, self-adjusting computation. Persistence also arises in self-adjusting computation, as a form of memoisation. Self-adjusting computation is therefore of special importance: it is the only prior work which combines all three concepts. What I want to do here is compare Acar's (mature, well-worked out) system with what I'm hoping to do.

Before I start, I should point the reader to this interim technical report. My report has a number of problems, which I won't attempt to enumerate, and unfortunately it doesn't use the term "reification". (That was Tom Harke's idea.) It should shed some light on what I mean by a persistent evaluation graph, which is essentially Acar's notion of a "trace". My notation is intentionally similar to Acar's.

Self-adjusting computation

Self-adjusting computation is a language and runtime system for incremental computation. After an initial evaluation, the inputs of a program can be repeatedly modified, and the resulting changes to the output observed. During the initial evaluation, the runtime records a trace identifying how parts of the computation depend on other parts. When an input is modified, the output is re-calculated by a change propagation algorithm, which exploits the information in the trace to perform the update efficiently.

Early formulations required the programmer to deal explicitly with much of the technical machinery involved in making a computation self-adjusting. Although the resulting programs were still much easier to write than hand-coded dynamic algorithms, the approach was difficult and error-prone.

The most recent version, a self-adjusting extension of Standard ML called ΔML, provides more direct language support. This brings it closer in concept to interactive programming. Nevertheless it differs in several important respects, thanks to its focus on incremental performance. The following discussion is organised around the common features of reification, reactivity and persistence. The figure show some typical ΔML code.

structure ModList =
struct
  datatype 'a cell = NIL | CONS of 'a * 'a modlist
  withtype 'a modlist = 'a cell box
  type 'a t = 'a modlist

  afun lengthLessThan (l: 'a modlist) : bool box =
  let putM = mkPut $ ()
      afun len (i,l) =
        if i >= n then false
        else case get $ l of
               NIL => true
             | CONS(h,t) => len $ (i+1,t)
  in putM $ (NONE, len $ (0,l)) end

  afun map (f: 'a -> 'b) (l: 'a modlist) : 'b modlist =
  let val putM = mkPut $ ()
      mfun m l =
        case get $ l of
          NIL => NIL
        | CONS(h,t) => CONS (f h, putM $ (SOME h, m t))
  in putM $ (NONE, m l) end
end

Reification

In both systems, the initial evaluation is reified into a data structure capturing the dependencies between parts of the computation.

The key difference seems to be in whether the reification is "full", or only "partial". In self-adjusting computing, the trace only captures the aspects of evaluation relevant to efficient incremental update. In interactive programming, the entire evaluation is reified.

Self-adjusting computation	Interactive programming
The programmer must explicitly identify the adaptive aspects of the computation. The type constructor box distinguishes changable data, which may change after the initial evaluation, from stable data, which cannot. Keywords afun and mfun identify adaptive functions, which produce and consume changeable data.	All data is 'changeable'; all functions are 'adaptive'.
Computations are partly reified into traces. Traces are data structures which record the dependencies between adaptive parts of the computation, and the code fragments associated with them.	Computations are fully reified into evaluations. Evaluations are data structures "all the way down", recording individual steps of the big-step semantics.
No direct requirement that traces reflect in any way the derivation tree given by the original semantics, but only that the final computed values are consistent.	Evaluation graph can at any state be unravelled into the derivation tree given by the original semantics.
Runtime interface exports operations for querying and updating changeable data, but not for observing traces. But trace information could in principle be exported.	Runtime interface exports evaluation graphs as well.

Reactivity

In both systems, data can be modified after the initial evaluation, causing the output to be updated. Synchronisation updates the trace as well as the output, producing a result consistent with an initial evaluation, and leaving the system ready to respond to another input change. Both implementations are imperative, to allow state to be reused across transitions.

The differences seem to follow from the different treatment of traces: partial reification means that self-adjusting computation has an (efficient, but potentially problematic) hybrid execution model.

Self-adjusting computation	Interactive programming
Partial reification means that change propagation must re-execute, rather than merely synchronise, adaptive computations when the modifiables they read have changed.	Full reification of evaluation means no notion of "re-execution". Synchronisation is the reactive mutation of structure, "all the way down".
Re-execution interacts poorly with imperative features such as I/O (effects may be duplicated) and memory allocation (effects may differ). The occurrences of the mkPut primitive in the figure above are a symptom of the latter problem.	Full reification implies a purely functional treatment of effects: the evaluation can include descriptions of effects, and these descriptions can be updated by synchronisation. Invites the question of how interactive programming accommodates "traditional" I/O, such as launching missiles or writing snapshots of execution to a file.
Modification to data values only. Since ΔML is higher-order, these values may be of function type. However, functional values are opaque, rather than represented as changable data structures.	Intention is to permit modification to code as well as data, as a separate consideration from higher-order vs. first-order. Requires programs to have a similar representation to user-defined data types: in Acar's terms, modifiable code, as well as modifiable data.
Functional specification; mutable traces not part of observable behaviour.	Imperative specification; mutable evaluation nodes essential part of observable behaviour.
Imperative, bottom-up implementation, based on priority queue. No proof that algorithm conforms to functional specification.	Top-down implementation, corresponding closely to imperative specification.
Implementation shown to be optimally efficient for programs which are monotone with respect to a particular class of input changes.	Inefficient. No performance guarantees.

Persistence

In both systems, sub-computations are shared across states by a generalised memoisation facility which stores not just computed values but associated traces.

Here, the differences arise because interactive programming makes the identities of evaluation nodes part of the observable structure. This shifts memoisation from a performance trick, to playing an essential role in the treatment of evaluation graphs as purely functional data structures.

Self-adjusting computation	Interactive programming
Traces are not exported by runtime interface, so memoisation can only be observed indirectly, as incremental performance.	Evaluations are exported by runtime interface, so memoisation can be observed as an evaluation subgraph shared by adjacent states.
Only adaptive functions can be memoised, not arbitrary terms. Programmer specifies when adaptive functions are memoised, via keyword mfun.	Evaluation of every term is memoised, effectively by memoising the eval function of the interpreter. Common substructure is therefore always shared by adjacent states; evaluation graph is a purely functional data structure.
Memoisation only occurs across evaluations, not within a single evaluation.	Memoisation occurs within evaluations too, meaning that common sub-computations are shared.
Essential role of memoisation in performance restricts language to CBV. Unclear what kind of incremental performance is possible under CBN.	Not limited to CBV, because performance is disregarded. Intention is to support CBN.

The $64,000 question is: can full reification ever be done efficiently?

FInCo 2007

Here is the draft of a FInCo 2007 paper which elaborates (although still entirely informally) the programming model called declarative interaction which I mentioned in my first posting. FInCo is one of the satellite workshops of ETAPS 2007.

The review comments were useful, and reasonably positive. I'm looking forward to some interesting discussions. I conspicuously failed to give even a passing nod to agent-oriented programming; given the likely focus at the workshop, this is something I need to learn about.

Programming languages for interactive computing

Almost all software systems today are interactive, in that they maintain ongoing interactions with their environments, rather than simply producing a result on termination [GSW06]. Indeed, a consistent trend since the beginning of the digital era has been towards increasingly interactive systems. The trend has progressed on at least two fronts: enhancements to end-user interactivity, and increasingly integrated systems. The trend began with the first teletype and textual interfaces and continued through early GUIs and LAN-based operating systems. It continues with today's 3D virtual worlds and applications deployed over the wide-area network.

With the Internet emerging as the "global operating system", the pressure on our software to be interactive is greater than ever before. Consider how the following requirements can be understood in terms of enhanced interactivity:

• Ability to reconfigure or repair applications without taking them offline → interaction with code as well as data
  
• Long-running, continously-available applications → interaction must be robust
  
• Sessions resumable from wherever we happen to be located → persistence of interactions
  
• Transparent recovery from latency problems and intermittent connectivity → interaction should not be semantically sensitive to the network
  
• Mobile code whose behaviour depends on execution context → dynamically scoped interactions
  

A variety of process algebras and other formalisms have been developed for modelling and reasoning about interactive systems. Yet despite the trend towards greater interactivity, we continue to lack a simple and coherent paradigm for building robust interactive systems. The main bugbear that has faced us has been what we might characterise as an "impedance mismatch" between traditional algorithmic programming languages and the way interactive systems abstractly work. Whereas an algorithmic language treats a program as a black box which produces a final value on termination, an interactive system allows other systems to observe and influence its behaviour as it executes, and must adjust its internal state in response to each interaction to maintain the consistency of the computation.

In current desktop systems, the mismatch is usually resolved by representing the state of the system as a set of mutable stores and then employing a notification scheme to maintain the consistency of the state. Rather than the host language being used to execute a single sequential program to termination, it is employed to execute fragments of imperative code as interactions occur. Each executed fragment must produce exactly the side-effects required to synchronise the state of the system correctly.

Unfortunately this near-universal reliance on the imperative to support interaction has come at an enormous cost in complexity. It will be useful here to recall Brooks' distinction between essential and accidental (or inessential) complexity [Bro87]. Complexity inherent in the problem itself (from a user's perspective), or which can be attributed to human factors, is essential; what remains is accidental or inessential. Interactive systems as currently implemented are dominated by inessential complexity, the main culprits being this ad hoc management of state, explicit concern with flow of control, and unnecessary use of non-deterministic concurrency. Imperative languages (ab)used in this way are the "Turing tar-pit in which everything is possible but nothing of interest is easy" [Per82]. Web applications only complicate things further, by adding a variety of ill-defined staging policies and interaction models into the mix.

Ironically, what unifies much of this inessential imperative complexity is that it exists in the service of essentially declarative ends. Indeed, I suggest that the reason the current paradigm works at all is that systems implemented in this way approximate a much simpler, declarative model of interactive computation. Experienced software designers rely tacitly on something like this declarative model in order to make decisions about what counts as reasonable behaviour. Rather than being ill-suited to interaction, as is sometimes assumed, perhaps because of the somewhat arcane feel of techniques such as monads [JW93][Wad99] for modelling effectful computation, the declarative paradigm - with a simple orthogonal extension to support interactivity - fits the abstract behaviour of interactive, stateful systems surprisingly well. But today, because this declarative behaviour is achieved only indirectly, interactive systems are significantly less reliable and understandable than they need to be, despite the widespread use of design patterns such as Observer [GHJV95] to manage some of the inessential complexity. State-related dysfunctions in particular, such as the gradual degradation of a system over time, spurious sensitivities to the order in which two operations take place, deadlocks and race conditions, are common. I propose that the best way to address the impedance mismatch between algorithmic languages and interactive systems is not to wallow in the tar-pit of imperative languages, but to lift declarative languages into a computational model which supports interaction directly.

The aim of this blog is to explore the conceptual foundations of such a programming model, which I shall refer to as the declarative interaction model. Developing a formal semantics will be a topic for later treatment. Like some other declarative approaches to interaction, the declarative interaction model maintains a clean separation of (stateless, deterministic) declarative computation and (stateful, non-deterministic) reactive computation. The model is distinguished by its modal construal of interaction, whereby an interactive system is taken to be a space of canonically represented "possible worlds", each expressing a purely declarative computation, along with an index into that space indicating the "actual world", which represents the system's current state. To interact with such a system is to select a new actual state from this space of possible states. Interactions (effectful operations) are lifted to meta-programs that manipulate values of modal type; crucially, they are unable to interfere with the purely declarative semantics of each possible state, and in any case are only required when they are essential to application logic. Non-determinism arises from concurrent interactions, which are handled transactionally.

The declarative interaction model relates to many active research areas, including modal type systems, incremental computation, meta-programming, declarative concurrency, transactional concurrency, dataflow computing, interactive computing, and wide-area computing. As we shall see, four closely related concepts in particular are central to the model: modality, incrementality , concurrency, and persistence. A key validation of the model will be the development of an interactive programming language which supports the model directly.