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.


  1. Ankur says:

    Just want to draw your attention to this visual programming language here