Interactive terms and evaluation stores

Here's the final version of my PADL paper. I've hived off all the technical spec to a separate technical report, and devoted the space thereby liberated to a clearer explanation of how it works: interactive terms, lifting and unlifting, value stores, evaluation traces and evaluation stores, reification, memo-reification and synchronisation. The mutually recursive relationship between reification and synchronisation is one of the things I've tried to clarify.

I went to FP lunch at Nottingham on Friday. The main reason for the trip was to hook up with Henrik, but I also gave a talk. For the talk I knocked up some slides that animate the evaluation store for the example programming scenario in the paper, using output generated by my F# implementation. It's much easier to visualise how the system works this way, so I've included them below. I've also include a rather crude hand-crafted animation of the mock-up UI from the paper. As mentioned in the paper, I only allow edits to program constants, which in this setting, means terms built purely out of constructors.

Motivating example

These slides animate the motivating example from the paper. The programmer interactively discovers and fixes two bugs in a simple program which compare two lists. The UI shown is only a mock-up, intended to be representative of what one could build on top of my current system.

In the scenario, the programmer takes her program through 5 editing states. For some states, the slides also show some alternative view configurations. For example, at state 4, the programmer collapses the recursive call to equal, once she realises the problem actually lies with the definition of equal_nat. This isn't an edit to the program, but just to the view. Browsing features like this will be essential to a practical implementation of interactive programming, but are orthogonal to the work presented in the paper.

The following diagram illustrates some of the features of this hypothetical UI; they're not essential to understanding the paper, but are useful for making sense of the mock-ups:

Interactive terms

The second set of slides show how edits are enabled. A transformation called lifting replaces constants in the original program by references to store locations initialised to those constants. (I call this a value store, to distinguish it from an evaluation store, below.) The result of lifting is called an interactive term (shown on the right), whence we can recover a non-interactive term (on the left) by unlifting at a particular store state. Edits are modelled by mutations to the value store, and so an interactive term is associated with a family of unliftings, one for each possible state of the value store. Lifting thus converts a term into a mutable representation, and unlifting does the reverse.

Evaluation stores

Because the unlifting of an interactive term changes as the value store changes, how it executes may also change. It can compute a different value; or it can compute the same value, but "for a different reason". In other words the intensional behaviour of the program can change, even if extensionally it is unchanged. This behaviour is reified into a mutable representation called an evaluation store. These slides show the evaluation store evolving through the 5 states of our scenario. There are two further states which show how fragments of reified evaluation persist and are reused if they arise in subsequent states. The notation used in the slides is explained in the paper.

So what next? The main limitation of the current system is that only data values can be changed. This in turn effectively requires a restriction to a first-order language. The reason is this. In an interactive programming system, functions are not purely extensional beasts. Their intensional behaviour is observable too. We can't therefore allow modification of functional values without permitting arbitary code modification, since the intensional behaviour of a function is given by its definition. This doesn't arise in standard FRP systems, which are higher-order, but where functions behave purely extensionally.

Interestingly, and as Thorsten mentioned, once you permit code changes, you obtain something of a higher-order feel, even in a first-order setting. So code modification is the key thing I want to enable, from which higher-order functions should naturally follow.

The whys and what ifs of programming

I'm submitting this paper to PADL this coming Friday. Conveniently, the organisers extended the deadline by a week, so I have a few days to solicit some comments. It's not as coherent as I would like, but for the first time I've got something approaching an end-to-end story: a problem, a motivating example, a solution (with formal spec), and an implementation. It's still restricted to a first-order, call-by-value setting, allowing me to side-step the issue of code modification. (If values can have function type, and values can change, then there's no side-stepping the issue. Ditto call-by-name, which allows values to have code in them.) I'm planning to tackle code modification next, and with that in place it should be easy enough to accommodate higher-order functions too.

I've narrowed my motivation down to focus on an "interactive" style of programming, where the programmer is engaged in an ongoing dialogue with the development environment, and all programming activities, including writing new code, are framed in terms of the programmer asking questions and the development environment responding. It took me a while to realise that having a narrow motivation is really the only sane methodology. If there are other applications or benefits (as I think there are) they're best treated separately, else the whole thing gets too unwieldy. For now it's nice to have a narrow problem to solve and a reasonably simple story to tell.

There's not much yet in the way of theorems about formal properties of the system. So far, the formalism is really just serving as a dependently-typed programming language, only one I don't happen to have a compiler for. Guess I should probably start using Agda.

There is some source code though. I was planning to host it on GitHub, but unfortunately I'm still running on Windows, and Git on Windows looks a bit sketchy. So I'm using Google Code. (Annoyingly its source browser doesn't like the apostrophes I've used in my identifiers, so I may think again.) The code is now in F# instead of Haskell, which will hopefully make experimenting with UI ideas a bit easier. For now there's no UI, though.

So: what are the biggest problems with this paper? I'm glossing lots of important issues, time and space performance being obvious ones, and how to recover something like normal effectful programming.

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?

Sleepless near Seattle

View Larger Map

I'm off to Vancouver on Sunday to spend five weeks at UBC, thanks to the people at Universitas 21, who were kind enough to part with the required cash. It'll be a chance to immerse myself a bit in Gregor Kiczales' current thinking on fluid AOP. I'm banking on fluid AOP being the "killer app" for interactive programming languages. Every paradigm needs its killer app!

Unfortunately I'm still miles away from useful applications, but I finally have something to report. I even have some software that works, almost 800 lines of entirely uninteractive Haskell.

I'm planning to submit this paper to Onward! at the end of the week. In terms of technical maturity (or lack of) I feel stranded half-way between "applied" conferences like OOPSLA and more formal ones like ICFP, so I'm not sure if this is the right forum. The paper is rather rough in parts, particularly towards the end. I've also gratuitously ignored the topic of bidirectionality, which is essential to practical interactive programming. I would welcome comments on which bits are hardest to make sense of.