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.
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
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:
The second set of slides show how edits are enabled. A transformation called
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
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.