The meaning of a program change is a change to the program's meaning

TL;DR

This paper advocates a shift in programming language theory towards understanding program changes as modifications to the program's meaning, emphasizing a change-oriented perspective.

Contribution

It introduces a change-oriented viewpoint that redefines the meaning of program changes as alterations to the program's semantics.

Findings

Highlights the gap in current theory focusing only on program meaning

Proposes a new perspective linking program modifications to semantic changes

Encourages future research on change semantics in programming languages

Abstract

Programming is the activity of modifying a program in order to bring about specific changes in its behaviour. Yet programming language theory almost exclusively focuses on the meaning of programs. We motivate a "change-oriented" viewpoint from which the meaning of a program change is a change to the program's meaning.

Equations

$$e\Rightarrow v{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@cmyk@stroke{0}{0}{0}{0.50}\pgfsys@color@cmyk@fill{0}{0}{0}{0.50}\text{ and }}e,\delta e\mathrel{\Rightarrow_{\delta}}\delta v{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@cmyk@stroke{0}{0}{0}{0.50}\pgfsys@color@cmyk@fill{0}{0}{0}{0.50}\text{ implies }}e\oplus\delta e\Rightarrow v\oplus\delta v$$

Full text

\xpatchcmd\ps@firstpagestyle

Manuscript submitted to ACM Submitted to Incremental Computation 2019

\xpatchcmd\ps@standardpagestyleManuscript submitted to ACM Submitted to Incremental Computation 2019

@ACM@manuscriptfalse

The meaning of a program change is a change to the program’s meaning

Roly Perera

0000-0001-9249-9862

The Alan Turing Institute96 Euston RdNW1 2DBLondonLondon, UK

rperera@turing.ac.uk

††copyright: none

Programming as dialogue

Incremental computations (18, 26, 1, 14, 3) map input changes to output changes, ideally faster than running from scratch on the new input. The program itself is assumed to be fixed. It may be possible to replace functional inputs with other functions, but changes to the program text itself are not usually considered.

Programming is also an incremental endeavour (12, 11). The focus here is on program changes, often in the context of a fixed input such as a test case. Since the entire goal is to bring about specific changes in behaviour, the output changes that arise are of great interest to the programmer. Live programming (25, 10, 13) and test-driven development (2) recognise this, but neither provides a fine-grained notion of change. New outputs appear wholesale, leaving it up to the programmer to figure out what changed and why.

This suggests a research problem: developing an incremental, fine-grained semantics which maps program changes to output changes, interpreting the meaning of program changes as changes to the program’s meaning.

As a toy example, suppose I wish to compute the sum of the squares of a list of integers. I start with a simpler program, say a function which simply copies a list:

As a sanity-check, I run my function at an argument: Perhaps seeking a “tabular” view of the problem, I decide to pair each element with its square, making the following edit (new code is shown in green): I can now re-run the earlier test case, to check that the output has become [(1, 1), (3, 9)]. But what if the programming environment could directly interpret my program change as an output change? These are, after all, the intuitive consequences of editing the program in the specific way that I did: my edit paired each element with its square (on the right). Here, for example, the output delta confirms my intuition that, of the two occurrences of 1 in the revised output, it is the second one which should be considered “new”.

Towards a semantics of program change

Rather than considering in detail how this might this work, we content ourselves with an informal exploration of the problem. Work on program slicing (21, 24) and live programming with holes (17) assigns meaning to incomplete programs and their (partial) completions; this has some of the flavour of what we want, but is a rather monotone notion. To support structural reorganisations like moves and splices, we will suppose a term graph representation of programs (23), perhaps provided by a structure editor (4) able to assign unique addresses to subterms (20):

f[][]f:x:xfxs

:fx:(,)xsqxsf

The graphs on the left graphically represent the two defining clauses of f; we place them side-by-side to establish them as disjoint parts of the same definition. Inputs nodes (patterns) are shown in white, and output nodes (values) in grey. The recursive call to f appears as an application node with no output edge.

The program edit is shown graphically to the right, as a “graph delta” to the cons clause of the definition. The new pair constructor and its child edges, which should be read as pointers, are shown in green. The pointer to the first element of the output is dotted blue, meaning the pointer value has changed; this is necessarily the case here because it refers to a newly-created node.

What we seek, then, is a semantics that allows us to “execute” the edit to the program to obtain a corresponding edit to its execution. Below left is the original execution of the test case, represented as a term graph with a shape resembling a big-step derivation:

f:1:1f:3:3f[][]

:f1:(,)1sq1:f3:(,)3sq9[]f[]

To the right is the modified execution we would like to obtain, with delta-colouring showing new nodes spliced into the computation in a way that accounts for the output delta identified previously. What this illustrates is that a suitable notion of execution delta should (we contend) “operationalise”, or account for, output deltas, generalising the idea from dynamic program slicing that parts of executions account for specific parts of the output (21).

In the other direction, we must seek an appropriate technical sense in which those execution deltas “correspond” to the program deltas that gave rise to them. As an example of a potential property of interest, one might consider whether there exists a map from execution nodes to program nodes preserving the graph structure and delta colouring.

Executing changes via changes in executions

Here is a rough sketch of the idea more formally. Suppose we already have a baseline big-step evaluation relation $\displaystyle\Rightarrow_{0}$ for our language. We start by defining a relation $\displaystyle e\Rightarrow v$ for programs represented as term graphs, consistent with the baseline semantics in that $\displaystyle e\Rightarrow v$ implies $\displaystyle|e|\Rightarrow_{0}|v|$ where $\displaystyle|e|$ is the “tree-unravelling” (5) of $\displaystyle e$. Then the idea would be to derive an incremental evaluation relation $\displaystyle\mathrel{\Rightarrow_{\delta}}$ satisfying:

[TABLE]

where $\displaystyle\oplus$ applies a delta to a term graph. Note that this is quite different from the static differentiation problem (3, 6), since $\displaystyle\delta e$ describes an arbitrary change to $\displaystyle e$.

Now, in our setting, it is always possible to compute the difference \displaystyle v\ominus\smash{v^{\raise-0.60275pt\hbox{\scalebox{0.8}{\displaystyle\scriptstyle\prime}}}} between two outputs $\displaystyle v$ and \displaystyle\smash{v^{\raise-0.60275pt\hbox{\scalebox{0.8}{\displaystyle\scriptstyle\prime}}}}, or more generally the difference \displaystyle D\ominus\smash{D^{\raise-0.60275pt\hbox{\scalebox{0.8}{\displaystyle\scriptstyle\prime}}}} between two executions $\displaystyle D:e\Rightarrow v$ and \displaystyle\smash{D^{\raise-0.60275pt\hbox{\scalebox{0.8}{\displaystyle\scriptstyle\prime}}}}:\smash{e^{\raise-0.60275pt\hbox{\scalebox{0.8}{\displaystyle\scriptstyle\prime}}}}\Rightarrow\smash{v^{\raise-0.60275pt\hbox{\scalebox{0.8}{\displaystyle\scriptstyle\prime}}}}, simply by comparing the term-graph representations (20). So in fact we can always trivially exhibit a relation satisfying property (1) by defining \displaystyle e,\delta e\Rightarrow_{\delta}\smash{v^{\raise-0.60275pt\hbox{\scalebox{0.8}{\displaystyle\scriptstyle\prime}}}}\ominus v where $\displaystyle e\Rightarrow v$ and $\displaystyle e\oplus\delta e\Rightarrow v^{\prime}$, supposing that $\displaystyle\ominus$ satisfies $\displaystyle v\oplus(v^{\prime}\ominus v)=v^{\prime}$ (3).

We are left with at least two significant challenges, however. First, we must take care to balance precision with the integrity constraints of the term graph. We must define $\displaystyle e\Rightarrow v$ so that distinct nodes are always used to represent distinct terms (so $\displaystyle v$ remains a well-formed term graph), but also so that nodes are reused systematically in order to obtain precise deltas.

As an example of how nodes can be safely reused, suppose we extracted the expression (x, sq x) in the definition of f into a new function g, replacing free occurrences of x by uses of the argument y of the new function (7):

Such refactorings are common programming “micro-steps” (19). They clearly have no effect on the output $\displaystyle v$ considered as its tree-unravelling $\displaystyle|v|$. But we might also observe that although the expression responsible for constructing the pairs is now inside g, the values used to close that expression are the same as before. Moreover g simply delegates to that expression. So it should be safe to use the same nodes for the pairs in the new execution as we did in the previous one, and view the change simply as a “rewiring” of the computation:

:f1:g(,)1sq1:f3:g(,)3sq9[]f[]

On the other hand, given that f has now simplified to map g, suppose we adjusted our test case as follows: This is also a refactoring, and so again the output unravels to the same tree as before. But now a different expression (one found in the body of map) is responsible for constructing the list nodes in the output. It would therefore be unsafe to use the same nodes as we did previously to construct the list, at least not without additional global knowledge (for example that f is not called anywhere). This explains the new lists nodes that were highlighted in the output delta above:

:map g1:g(,)1sq1:map g3:g(,)3sq9[]map g[]

A second challenge is to efficiently implement $\displaystyle\Rightarrow_{\delta}$ so that memoised (15) parts of a previous evaluation $\displaystyle D:e\Rightarrow v$ can be reused to produce $\displaystyle D^{\prime}:e\oplus\delta e\Rightarrow v^{\prime}$. This leads naturally to the question of whether existing approaches to incremental computation, in particular self-adjusting computation and related work (1, 8, 9), can be be brought to bear on this problem, by using a general-purpose incremental language as a metalanguage to derive an interpreter able to respond to program changes. While Hammer et al. (9) show that such an approach is possible, this technique does not in itself give rise to a direct program-change semantics for the object language, but rather one which is implicit in the (complex) incremental behaviour of the metalanguage.

From programs to programming

Programming is the activity of modifying a program in order to bring about specific changes in its behaviour. Yet programming language theory almost exclusively focuses on the meaning of programs (22). We outlined a “change-oriented” viewpoint from which the meaning of a program change is a change to the program’s meaning. In so doing we skipped over many difficult questions.

We raise one question now with a view to future discussion. Can we extend the change-oriented perspective to the static meaning of a program, such as its type? For example, Omar et al. (16) define a type system which incrementally maintains a proof that a program being edited is well-typed. Viewing such a system as generating a higher-order witness (explaining how specific edits induce specific changes to the type of the program) suggests a static version of our principle: the type of a program change is a change in the program’s type. Equipping changes with types may improve our ability to produce useful error messages, especially if we can extend type deltas to structural reorganisations like the ones considered here.