tl;dr
We present a (novel?) method for iterative recomputation of a pure function. The method introduces no extraneous state.
Background n Motivation
A significant portion of software developed today follows what we will refer to as the isolated state paradigm, which recommends that in a software application all the state should be conglomerated and managed in exactly one location, and all other aspects of the program should be expressed as a pure function of the state.
Perhaps the most notable example of this is the Elm language and frontend framework, which popularized a style of front-end development (namely, the Elm architecture, or TEA) abiding by the isolated state paradigm. More generally, any model/view/contoller framework places all application state into the model and therefore abides by isolated state. Event-log-based frameworks also abide by isolated state, as they dictate that all application state should be derivable from the event log.
One issue that isolated-state frameworks inevitably run into is performance. Since almost all aspects of the application are expressed as pure functions of the application state, this means that any update to the application state entails a recomputation of all other aspects of the application. In small applications this is an implementation detail, but in large applications this can be a crippling punch to performance.
There are a number of existing solutions to this problem, but all of them are some combination of only being a partial solution, introducing new overhead, or requiring departure from the isolated state paradigm.
React and Vue avoid full-application recomputation by splitting an application into small parts called ‘components’ each essentially a miniature application embedded in its parent component. Each component manages only a small part of the application, and when the state of a single component changes, only the computations relevant to that component are performed again; other components may recompute but won’t necessarily.
As such, we avoid full-app recomputations on state changes. However, the state controlled by a React or Vue component is genuinely owned by it; that is, this strategy fragments state: instead of state being stored in one single location, each component owns a bit of it. The isolated state paradigm is no longer being followed.
The Elm frontend framework offers a kind of laziness to improve performance. This is nothing more than veiled memoization of pure functions1 and (presumably) comes with the same flaw with memoization as always: in memoization of a function , when computing and then we may successfully avoid actually recomputing (if ) but we also gain the need to test if first. Hence, we only manage at best to reduce the algorithm to , which in the case of an isolated-state application is .
Elm has another trick up its sleeve, which is diffing. The output of an Elm application is a description of a web UI. When the UI is rendered to the screen, instead of starting from scratch Elm will mutatively modify whatever happens to be on the screen already. In most cases this means that only a small update needs to be made.
This sounds good. Actually, it is, except for the following. In order for Elm to perform this, it still has to compute the entirety of the output of the Elm application, which it then diffs with the output from the previous render in order to figure out what on the screen needs to be modified. In other words, while it’s good that we avoid re-painting the entire application from scratch each time, we’ve still only reduced the runtime to .
Not to mention microoptimizations. For instance, the Shpadoinkle framework writes its core datatypes Chruch-encoded in the name of performance.
To make matters worse, I believe it is the case that UI description computation is upward-closed even in the presence of memoization: if you have to recompute some part of the decsription, you also have to recompute everything above it (in the UI tree). This means that if a change is small but deep, it still may entail a large amount of work being re-performed.
Which is—in principle—so silly! We know what part of the state is changing: a single TODO item is going from ‘incomplete’ to ‘complete’. And we know how our state relates to our UI, meaning that we should be able to tell ahead-of-time what part of the UI needs to be recomputed and what part doesn’t. We ought to be able to directly respond to the TODO item being checked of as follows: make a small change to the state, and then jump directly to its related UI element and re-render, without going through intermediate processes.
And we do have a way to do that already (see React components), but—as far as I know—no solution to this is known that preserves the isolated state paradigm.
This is what we present here: a way to respond to small state changes with equally-small computations while retaining the ability to lie in an isolated stte paradigm. Our solution is highly general and may actually be better phrases as followed. It gives a way to respond to small changes in a function input with small changes in the function output. (When applied to isolated-state applications we recover the description from before). Our solution is not perfect—if applied to the web we’d maybe still have to perform DOM diffing—but is still quite good.
So... let’s see it.
Delta Types
Let be a type and be a type equipped with a monoid structure as well as a surjective monoid homomorphism
into the group of all bijections over . Then we call a delta type for .
A delta type gives a way of modelling bijections over , which we can think of as ‘changes’ to values of type . (For instance, the bijection over gives a ‘change’ to any value )
We require that the homomorphism be surjective so that all bijections over can be represented by .
For any delta type for and we define
to be the application of the symmetry represented by to the value . (The operator is pronounced “nudge”)
Derivatives
Let be types and be delta types for . Also let
be a function. Then a function
is called a derivative of if and only
for all .
This condition states in essence that if we make a small change to , the image gives exactly what change will be induced in the output under .
Note that derivatives are not necessarily unique, as the behaviour of is not restricted if ; that is, the derivative need not give attention to the parts of that will never attain. (This fact is not particularly consquential)
Interlude
Hence we have summoned forth a notion of ‘changes’ (delta types) and of ‘making changes’ (function derivatives).
The point of all this is as follows. Say we have a function which is expensive to compute. However, say we know that we will be frequently computing on only slightly different values of . This could happen, for instance, if is the state type for an isolated-state application and computes the rest of the application from the state.
It is in our interest to avoid full recomputations of the output of . To that end, we may find some delta types and alongside a derivative for . If our chosen delta types allow for efficient computation of in the cases that our application actually observes, then we can respond to state changes by computing
by the derivative law we know that this is equal to . Hence we have an efficient way to compute compute the output for the new input without having to actually recompute all of .
Canonical Delta Types
Here we present canonical delta types for , , products, and sums (function types will be addressed later). Such a collection of types (including function types) is good enough to model all computation, and in fact is all you get in some languages such as Haskell. The delta types we present here should give reasonably-efficient computation in most applications. (If better peformance is required one can always choose their own delta types)
Products
—
Sums
For any sum type let and be the canonical injections.
Let be types with respective delta types . We construct a canonical delta type for as follows.
Let be the monoid direct product. Let homomorph into via
Then let the canonical delta type be with and with the rest of the delta type structure inherited from and then extended in the obvious way.
A standing question is that of extensibility. Say we give delta types language support. It seems like it would be mistaken to fix for each type a static delta type, as what delta type is appropriate may change by context. For instance, say we fix for the type
List the following delta type. If is the delta type for , then we define to be
Here an “indexed modification” delta consists of an index and a delta and acts on by applying the -delta to the index of a given list. A “splicing” delta consists of an index and a length and a sequence ; it acts on by taking a list and replacing its through elements with the list .
The details of this delta type are not really significant; the point is that we are choosing some operations to bless as having representations as deltas (any non-blessed operation will be represented as a plain ). The operations we choose to bless here are identity, indexed modification, and splicing. This choice is reasonable because a large number of list operations can be expressed as a composition of these primitives. As just one example, append and prepend are special cases of splicing.
Now when writing derivatives for functions out of , we are able to treat indexed modification, splicing, and compositions thereof specially. This means, for instance, that for a render function where each TODO item is rendered to exactly one web component, the derivative can be extremeley efficient in the case that a TODO item gets marked as ‘complete’. Such an action would produce an “indexed modification” delta, which the derivative could recognize and update the result incrementally.
Fantastic! But maybe not future proof.
One thing we might want to do is sort a TODO list, perhaps by date, or perhaps by some notion of priority. To add this feature to our app we could will into existence a type and then change our render function to have type
That is, we could add to our model. But for the sake of example let’s say we decided to do sorting by keeping the model as just a but choosing to order that list by the desired display order.
The trouble with this is that sorting cannot be efficiently represented by our current delta type for . A sort is not expressible as a composition of indexed modifications and splices, meaning that any time the application user performs a sort, the model update will be passed along as a plain ; this in turn means that the view derivative recieves no information about the incoming update and is forced to recompute the view from scratch. Which is doing extra work, because a sort in the model should ideally become an in-place sort in the view.
The obvious solution here is to add a variant to the delta type ; ie, redefine
(For clarity, a “sorting” delta is to be interpreted as a finite permutation over the indices of the list. Care will have to be taken regarding the case where the incoming does not well-represent a permutation.)
With this new variant, we can now express a user “sort” action as a “sorting” delta-type, and we can modify our derivative to handle the “sorting” delta type nicely. And then we’re done!
From a high-level viewpoint, this solution looks like the following:
That operation is not efficiently represented by the current delta type, so the application slows down
Solution: modify the delta type and view derivative
Poor code locality — The fact that sorting has no good representation as a is an issue that is relevant only to the callsite which actually performs the sorting, and should not be made a problem for the module in which is defined. (Imagine a large app with hundreds of callsites each of which need their own extensions to . We don’t want to force the module containing to have knowledge of all those hundreds of callsites!)
As a framework user, I don’t have to have to manually define my derivatives. It should be automatic or at least semi-automatic.
delta; doing so will add an appropriate variant to the delta type definition on the appropriate type. For instance, if we have
[delta]
remove :: forall a. Int -> List a -> List a
remove = {- implementation -}
then a constructor Remove :: Int -> Delta (List a) will be added to the definition of Delta (List a) and its interpretation will be given by remove. This allows the delta type for List a to be extended in a callsite-local way!
The big issue I see with this is how to work it into derivatives. Alongside the [delta] tag we’d need some kind of "remove derivative” or something which would be used when performing automatic derivative generation in order to actually make use of the new delta type variant. Just not sure how to do this at the moment.