{'fraction_non_alphanumeric': 0.03635244374605129, 'fraction_numerical': 0.005216348879780978, 'mean_word_length': 4.445003087236483, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Linked visualisations via Galois dependencies

We present new language-based dynamic analysis techniques for linking visualisations and other structured outputs to data in a fine-grained way, allowing a user to interactively explore how data attributes map to visual or other output elements by selecting (focusing on) substructures of interest. This can help both programmers and end-users understand how data sources and complex outputs are related, which can be a challenge even for someone with expert knowledge of the problem domain. Our approach builds on bidirectional program slicing techiques based on Galois connections, which provide desirable round-tripping properties. Unlike the prior work in program slicing, our approach allows selections to be negated. In a setting with negation, the bidirectional analysis has a De Morgan dual, which can be used to link different outputs generated from the same input. This offers a principled language-based foundation for a popular interactive visualisation feature called brushing and linking where selections in one chart automatically select corresponding elements in another related chart. Although such view coordination features are valuable comprehension aids, they tend be to hard-coded into specific applications or libraries, or require programmer effort.


INTRODUCTION
Techniques for dynamic dependency analysis have been fruitful, with applications ranging from information-flow security [29] and optimisation [18] to debugging and program comprehension [32,10]. There are, however, few methods suitable for fine-grained analysis of richly structured outputs, such as data visualisations and multidimensional arrays. Dataflow analyses [26] tend to focus on analysing variables rather than parts of structured values. Where-provenance [7] and related data provenance techniques are fine-grained, but are specific to relational query languages. Taint tracking [21] is also fine-grained, but works forwards from input to output. For many applications, it would be useful to be able to focus on a particular part of a structured output, and have an analysis isolate the input data pertinent only to that substructure. This is a need that increasingly arises outside of traditional programming. Journalists and data scientists use programs to compute charts and other visual summaries from data, charts which must be interpreted by colleagues, policy makers and lay readers alike. Interpreting a chart correctly means understanding what the components of the visualisation actually represent, i.e. the mapping between data and visual elements. But this is a hard task, requiring time and expertise, even with access to the data and source code used to create the visualisation. In practice it is easy for innocent (but devastating) mistakes such as transposing two columns of data to go unnoticed [20]. Since visualisations are simply cases of programs that transform structured inputs (data tables) into structured outputs (charts and other graphics), general-purpose language-based techiques for fine-grained dependency tracking should be able to help with this, by making it possible to reveal these relationships automatically to an interested user.

Linking structured outputs to structured inputs
First, interpreting a chart would be much easier if the user were able to explore the relationship between the various parts of the chart and the underlying data interactively, discovering the relevant relationships on a need-to-know basis. For example, selecting a particular bar in a bar chart could highlight the relevant data in a table, perhaps showing only the relevant rows, as illustrated in Figure 1. We could certainly do more and say something about the nature of the relationship (summation, in this case), but even just revealing the relevant data puts a reader in a much better position to fact-check or confirm their own understanding of what they are looking at. Indeed, visualisation designers sometimes create "data-linked" artefacts like these by hand, such as Nadieh Bremer's award-winning visualisation of population density growth in Asian cities [6], at the cost of significant programming effort. Libraries such as Altair [30] alleviate some of this work, but require data transformations to specified using a limited set of combinators provided (and understood) by the library.
What we would rather do instead is allow a data scientist to author analyses and visualisations using an expressive functional language like the one shown in Figure 1, with data linking provided automatically for the computed artefact, as baked-in transparency feature. At the core of this is a program analysis problem: we want to be able to focus on a particular chart element, and determine the inputs that contribute to it. Given the output selection, this is a matter of performing some kind of backwards analysis to identify the relevant data. As well providing a path to automation, framing data linking as a program analysis problem invites interesting questions that a hand-crafted solution is unlikely to properly address. For example, does the union of two output selections depend on the union of their respective dependencies? Do dependencies "round-trip", in that they identify sufficient resources to reconstruct the selected output? Are they minimal? These questions are important to establishing trust and a language-based approach offers a chance to address them. | type ← ["Bio", "Hydro", "Solar", "Wind"], 10 let plot = zipWith (fun p1 p2 → { x: p1.x, y: p1.y / p2.y }) 11 (series type "USA") (series type "China") 12 ] 13 } Fig. 2. Linking visualisations via common data dependencies

Linking structured outputs to other structured outputs
Second, authors often present distinct but related aspects of data in separate charts. In this situation a reader should be able to focus on (select) a visual element in one chart or other structured output and automatically see elements of a different chart which were computed using related inputs. For example in Figure 2 below, selecting the bar on the left should automatically highlight all the related visual elements on the right. This is a well-recognised use case called brushing and linking [3], which is supported by geospatial applications like GeoDa [2] and charting libraries like Plotly, but tends to be baked into specific views, or require programmer effort and therefore anticipation in advance by the chart designer. Moreover these applications and libraries provide no direct access to the common data which explains why elements are related.
Again, we would like to enable a more automated (and ubiquitous) version of brushing and linking, without imposing a burden on the programmer. They should be able to express visualisations and other data transformations using standard functional programming features such as those shown in Figure 2, and have brushing and linking enabled automatically between computed artefacts which depend on common data. At the core of this requirement is a variant of our original program analysis problem: we want to select a part of the output and perform a backwards analysis to identify the required inputs, as before, but then also to perform a forwards analysis to identify dependent parts of the other output. Moreover, we would also like the brushing and linking feature to be able to provide a concise view of the data that explain why the two selections are linked. Note that the intuition behind the forwards analysis here is not the same as the one we appealed to in the context of round-tripping: there the (hypothetical) question was whether the selected data was sufficient to reconstruct the selected output, whereas to identify related items in another view, we must determine those parts for which the selected data is necessary. As before, a language-based approach offers the prospect of addressing these sorts of question in a robust way.

Contributions
To make progress towards these challenges, we present a bidirectional analysis which tracks finegrained data dependencies between input and output selections, with round-tripping properties characterised by Galois connections. Selections have a complement, which we use to adapt the analysis to compute fine-grained dependencies between two outputs which depend on common inputs. Recent program slicing techniques [22,23,27] allow the user to focus on the output by "erasing" parts deemed to be irrelevant; the erased parts, called holes, are propagated backwards by a backwards analysis which identifies parts of the program and input which are no longer needed. Although these approaches also enjoy useful round-tripping properties characterised by Galois connections, they only allow focusing on prefixes of a structured output, rather than arbitrary substructures, a notion which is not closed under complement. Our specific contributions are as follows: -a new bidirectional dynamic dependency analysis which operates on selections of arbitrary parts of data values, for a core calculus with lists, records and mutual recursion, and a proof that the analysis is a Galois connection ( § 3); -a second bidirectional dependency analysis, derived from the first by De Morgan duality, which is also a Galois connection and which can be composed with the first analysis to link outputs to outputs, with an extended example based on matrix convolution ( § 4); -a richer surface language called Fluid, implemented in PureScript, with familiar functional programming features such as piecewise definitions and list comprehensions, and a further Galois connection linking selections between the core and surface languages ( § 5). First we introduce the core calculus which provides the setting for the rest of the paper, and which will serve as the desugaring target for the surface syntax presented in § 5.

CORE LANGUAGE
The core calculus is a mostly standard call-by-value functional language with datatypes and records. The main distinguishing feature is the use of eliminators, a trie-like pattern-matching construct that more familiar pattern-matching features like case expressions and piecewise function definitions easily desugar into. (A single core construct allows us to define the semantics of pattern-matching once and defer syntactic considerations to the surface language.) We give a big-step environmentbased semantics, which is easier for the backward and forward dependency analyses in § 3, and introduce a compact (term-like) representation of derivation trees in the operational semantics, called traces, which we will use to define the analyses over a fixed execution. Mutual recursion requires some care for the backwards analysis so we also treat that as a core language feature.

Syntax and typing
Although our implementation in untyped, types help describe the structure of the core language. Figure 3 introduces the types A, B which include Bool, Int and function types A → B, but also lists List A and records Rec ( # " x: A) which exemplify the two kinds of structured data of which are of interest: recursive datatypes with varying structure, and tabular data with a fixed shape. As usual the notation x: A denotes the binding of x to A (understood formally as a pair); # " x: A denotes the sequence of bindings that results from zipping same-length sequences #" x and #" A . In a record type Rec (

# "
x: A) the field names in #" x are required to be unique.
x: recursive functions The terms of the language are defined in Figure 3. These include Boolean constants true and false, integers n, variables x, and applications e e ′ . Primitives are not first-class; the expression ( #" e ) is the fully saturated application of to a sequence of arguments. (First-class and infix primitives are provided by desugarings in § 5). We also provide list constructors [] and e : e ′ , record construction ( # " x: e) and record projection e.x. The final two term forms, anonymous functions λ and recursive let-bindings let h in e where h is of the form # " x: , are explained below after we introduce the pattern-matching construct (eliminator). The typing rules for terms are given in Figure 4, and are intended only to help a reader understand the language; therefore the rules are simple and do not include features such as polymorphism. The main typing rules of interest are the ones which involve eliminators.

Eliminators
Eliminators , are also defined in Figure 3, and are inspired by Connelly and Morris's notion of generalised trie [9], elaborated further by Hinze [16]. Eliminators specify how to match against a partial value of some type and select a continuation for further execution, where is either a term e or another eliminator . The Boolean eliminator {true: , false: ′ } selects either or ′ depending on whether a Boolean value is true or false. The record eliminator {( #" x ): } matches a record with fields #" x and then returns with the variables #" x bound to the components of the record. The list eliminator {[]: , (:): } maps the empty list to and a non-empty list to another eliminator which specifies how the head and tail of the list are to be matched. The variable eliminator x: extends the usual notion of trie, matching any value, binding it to x, and then returning . Eliminators resemble the "case trees" commonly used as an intermediate form when compiling languages with pattern-matching [13], and can serve as an elaboration target for more advanced features such as the piecewise definitions described in § 5.
The use of nested eliminators to match sub-values will become clearer if we consider the typing judgement Γ ⊢ : A → B for eliminators given in Figure 4. (Eliminators always have function type, so this should be read as a four-place relation, with → part of the notation.) The typing rule for variable eliminators reveals the connection between eliminators and functions: it converts a continuation which can be assigned type B under the assumption that x is of type A into an eliminator of type A → B. The typing rule for Boolean eliminators says that to make an eliminator of type Bool → A, we simply need two continuations and ′ of type A. The rule for the empty record states that to make an eliminator of type Rec () → A, we simply need a continuation of type A. The rule for non-empty records allows us to treat an eliminator of type Rec ( # " x: A) → A ′ → B as an eliminator of type Rec ( # " x: A · y: A ′ ) → B, representing the isomorphism between A → B → C and A × B → C but at the level of record types [16]. (Formalising eliminators precisely requires Bird and Meertens-style nested datatypes [4] and polymorphic recursion, but these details need not concern us here.) The typing rule for list eliminators {[]: , (:): } combines some of the flavour of record and Boolean eliminators. To make an eliminator of type List A → B, we need a continuation of type B for the empty case, and in the non-empty case, an eliminator of type A → List A → B which can be treated as an eliminator of type A × List A → B in order to process the head and tail.

Eliminators as functions.
We can now revisit the term forms λ and let h in e. If is an eliminator of type A → B, then λ is an anonymous function of the same type. If h is of the form # " x: , then let h in e introduces a sequence of mutually recursive functions which are in scope in e. The typing rule for let h in e uses an auxiliary typing judgement Γ ⊢ h : Δ which assigns to every x in Δ a function type A → B as long as the to which x is bound in h has that type.

Values.
Values v, u, and environments are also defined in Figure 3, and are standard for call-by-value. (Environments are more convenient than substitution for tracking variable usage.) To support mutual recursion, the closure form cl( , h, ) captures the (possibly empty) sequence h of functions with which the function was mutually defined, in addition to the ambient environment . For the typing judgements ⊢ : Γ and ⊢ v : A for environments and values ( Figure 4), only the closure case is worth noting, which delegates to the typing rules for recursive definitions and eliminators. Figure 6 gives the operational semantics of the core language. In § 3 we will define forward and backward analyses over a single execution; in anticipation of that use case, we treat the operational semantics as an inductive data type, following the "proved transitions" approach of Boudol and Castellani for reversible CCS [5]. The inhabitants of this data type are derivation trees explaining how a result was computed, and the analyses will be defined by structural recursion over these trees. Expressed in terms of inference rules, these trees can become quite cumbersome, so we introduce an equivalent but more term-like syntax for them, called a trace ( Figure 5), similar to the approach taken by Perera et al. for -calculus [24]. The judgement T :: , e ⇒ v defined at the top of Figure 6 states that term e under environment evaluates to value v, and that T is a proof term that witness that fact. (In the figure the traces appear in grey, to reinforce the idea that they are not part of the definition of ⇒ but rather a notation for its inhabitants.) The rules for Booleans, integers and lists are standard and have unsurprising trace forms. For variables, we give an explicit inductive definition of the environment lookup relation ∈ at the bottom of the figure, again so that later we can perform analysis over a proof that an environment contains a binding. The lambda rule is standard except that we specify for the sequence of definitions being simultaneously defined, since a lambda is not recursive. For record construction, the trace form contains a subtrace T i for each field, and for record projection, which T :: , e ⇒ v T witnesses that e evaluates to v in  also uses the lookup relation ∈, the trace form T # " x: v .y records both the record # "

Evaluation.
x: v and the field name y that was selected.
The rule for (mutually) recursive functions let h in e, where h is a sequence # " x: of function definitions, makes use of the auxiliary relation , h ↠ ′ at the bottom of Figure 6 which turns h into an environment ′ binding each function name x i to a closure cl( , h, i ) capturing and a copy of h. For primitive applications, the trace records the values of the arguments which were passed to the operation . The rule for application e e ′ is slightly non-standard, because it must deal with both mutual recursion and pattern-matching. First we unpack the recursive definitions h from the closure cl( 1 , h, ) computed by e, and again use the auxiliary relation ↠ to promote this into an environment 2 of closures. We then use the relation ⇝ explained below to match v against the eliminator , obtaining the branch e ′′ of the function to be executed and parameter bindings 3 . In addition to subtraces T and U for the function and argument, the application trace T U ▶ w: T ′ also has subtraces w for the pattern-match and T ′ for the selected branch.
2.2.4 Pattern matching. The judgement w :: v, ⇝ , also defined in Figure 6 states that eliminator can match v and produce environment and continuation , with containing the variable bindings that arose during the match. Matches w are a compact notation for proof terms for the ⇝ relation, analogous to traces for the ⇒ relation, and again appear in grey in the figure.
Variable eliminators x: match any value, returning the singleton environment x: v and continuation . Boolean eliminators match any Boolean value, returning the appropriate branch and empty environment . List eliminators {[]: , (:): } match any list. The nil case is analogous to the handling of Booleans; the cons case depends on the fact that the nested eliminator for the cons branch has the curried type A → List A → B. First, we recursively match the head v of type A using , obtaining bindings and eliminator : List A → B as the continuation. Then the tail v ′ is matched using to yield additional bindings ′ and final continuation ′ . Record matching is similar: the empty record case resembles the nil case, and the non-empty case relies on the nested eliminator having curried type Rec ( # " x: A) → A ′ → B. The initial part # " x: v of the record is matched using , returning another eliminator ′ of type A ′ → B. Then the last field y: u is matched using ′ to yield final continuation .

A BIDIRECTIONAL DYNAMIC DEPENDENCY ANALYSIS
We now extend the core language from § 2 with a bidirectional mechanism for tracking data dependencies. § 3.1 establishes a way of selecting (parts of) values, such as the height of a bar in a bar chart. § 3.2 defines a forward analysis function ⇒ T which specifies how selections on programs and environments (collectively: input selections) becomes selection on outputs; selections represent availability, with the computed output selection indicating the data available to the downstream computation. § 3.3 defines a backward dependency function ⇒ T specifying how output selections are mapped back to inputs; then selections represent demands, with the computed input selection identifying the data needed from the upstream computation. Both functions are monotonic; this will become important in § 3.4, where show that ⇒ T and ⇒ T form a Galois connection, establishing the round-tripping properties sketched intuitively in § 1.1 which are important for trusting the results of the analyses.

Lattices of selections
Our approach to representing selections is shown in Figure 7. The basic idea is to parameterise the type Val of values by a (bounded) lattice A of selection states . We add selection states to Booleans, integers, records and lists. For our present purposes, we are only interested in dependencies between first-order data, so closures are not (directly) selectable, although they have selectable parts; closures also capture the ambient availability (explained in § 3.2.2 below), which is also a selection state . We parameterise the type Term of terms in the same way, but only add selection states to the term constructors corresponding to selectable values, allowing us to trace data dependencies back to expressions that appear in the source code. We return to this in § 5.

Fig. 8. Partial order on values
Selectable term e ∈ Term A ::= ... The fact that A is a bounded lattice means it has top and bottom elements ⊤ and ⊥ representing fully selected/unselected, plus meet and join operations ⊓ and ⊔ for combining selection information, with ⊤ and ⊥ as their respective units. Recall the data field of the bar chart computed in Figure 1, which contained a list of records; the record corresponding to China was (x: "China" · y: 295.3). The two-point lattice 2 def = ⟨2, tt, ff, ∧, ∨⟩ can represent the selection of the field y as (x: "China" ff · y: 295.3 tt ) ff , indicating that the number 295.3 is selected, but neither the string "China", nor the record itself is selected. Because lattices are closed under component-wise products, we often write ( , ) ⊑ ( ′ , ′ ) to mean that ⊑ ′ and ⊑ ′ . This also suggests more interesting lattices of selections, such as vectors of Booleans to represent multiple selections simultaneously, which might be visualised using different colours (as in Figure 1).

Selections of a value.
The analyses which follow will be defined with respect to a fixed computation, and so we will often need to talk about the selections of a given value. To make this notion precise, consider that the raw (unselectable) syntax described in § 2 can be recovered from a selectable term via an erasure operation ⌊v⌋ : Val A → Val 1 which forgets the selection information, where 1 is the trivial one-point lattice. We refer to ⌊v⌋ as the shape of v. Allowing u, v from now on to range over raw values, and reserving u, v for selectable values, we can then define: i.e. that erase to v.
Since its elements have a fixed shape, Sel v is a "representable" functor: it is isomorphic to a function space whose domain is the set of selection positions in v. In particular, the pointwise comparison of any v, v ′ in Sel v A using the partial order ⊑ of A is well defined, as is the pointwise application (zip) of a binary operation [12]. It should be clear that if A is a lattice, then Sel v A is also a lattice, with ⊤ v , ⊥ v , ⊓ v , and ⊔ v defined pointwise. For example, if u and u ′ have the same shape and v and v ′ have the same shape, the join of the lists (u : v) and (u ′ : ′ v ′ ) is defined and equal to (u ⊔ u ′ ) : ⊔ ′ (v ⊔ v ′ ). Similarly, the top element of Sel v A is the selection of v which has ⊤ at every selection position. (We omit the v indices from the lattice operations if it is clear which lattice is being referred to.) The notion of the "selections" of v extends to the other syntactic forms.
3.1.2 Environment selections and hole equivalence. The notion of a "selection" of v also extends pointwise to environments, so that Sel A means the set of selectable environments ′ of shape , where the variables in ′ are bound to selections of the corresponding variables in . One challenge arises from the pointwise use of ⊔ to combine environment selections. Since environments contain other environments recursively through closures, environment join is a very expensive operation if treated naively. One implementation option is to employ an efficient representation of values which are fully unselected, which is the case for the majority of bindings in an environment.
We therefore enrich the set of selectable values Val A with a distinguished element hole, written □, which is an alternative notation for ⊥ v for any v, i.e. the selectable value of shape v which has ⊥ at every selection position. The equivalence of □ to any such bottom element is established explicitly by the partial order defined in Figure 8: the first rule always allows □ on the left-hand side of ⊑, and other rules allow □ on the right-hand side of ⊑ as long as all the selections that appear on the left-hand side are ⊥. (The rules for recursive definitions h, eliminators and terms e are analogous and are omitted.) If we write for the equivalence relation induced by ⊑ on selectable values, which we call hole-equivalence, it should be clear that □ ⊔ v v and □ ⊓ v □. This means the join of two selections v, v ′ of v can be implemented efficiently, whenever one selection is □, by simply discarding □ and returning the other selection without further processing. Because □ is equivalent to ⊥ v for any v, all such bottom elements are hole-equivalent. For example, the selectable value □ : ⊤ □ is hole-equivalent to 5 ⊥ : ⊤ □, but also to 6 ⊥ : ⊤ [] ⊥ , and so the last two selections, even though they have different shapes, are hole-equivalent by transitivity. In practice we only use the hole ordering to compare selections with the same shape.

Forward data dependency
We now define the core bidirectional data dependency analyses for a fixed computation T :: , e ⇒ v, where T is a trace. In practise one would first evaluate a program to obtain its trace T , and then run multiple forward or backward analyses over T with appropriate lattices. We start with the forward dependency function ⇒ T which "replays" evaluation, turing input availability into output availability, with T guiding the analysis whenever holes in the input selection would mean the analysis would otherwise get stuck. ⇒ T uses the auxiliary function ⇝ w for forward-analysing a pattern-match, which introduces the key idea of a selection as the data available to a downstream computation.
3.2.1 Forward match. Figure 9 defines a family of forward-match functions ⇝ w of type Sel v, A → Sel , A×A for any w :: v, ⇝ , . (The definition is presented in a relational style for readability, but should be understood as a total function defined by structural recursion on w, which appears in grey to emphasise the connection to Figure 6.) Forward-match replays the match witnessed by w, transferring the selections on the relevant parts of v ∈ Sel v A to the output environment ∈ Sel A, and from the relevant part of ∈ Sel A to the chosen continuation ∈ Sel A. ⇝ w also returns the meet of the selection states associated with the part of v consumed by , which we call the availability of v (in the context of ), since it represents the extent to which the demand implied by was met. A variable match consumes nothing of v and so the availability is v, ⇝ w , , v and forward-match along w to and , with ambient availability x: w ·y: simply ⊤, the unit for meet. A Boolean match consumes either true or false , with availability ; empty list and record matches are similar. When we match a cons, we return the meet of the on the cons node itself with the availabilities and ′ computed for v and v ′ . Non-empty records are similar, but to process the initial part of the record, we supply the neutral selection state ⊤ on the subrecord in order to use the definition recursively. (Subrecords are not first-class, but exist only as intermediate artefacts of the interpreter.) One might imagine dispensing with the need for w by simply defining ⇝ w by case analysis on v and . However, it is then unclear how to proceed in the event that v is a hole. It would be legitimate to produce □ as the output continuation and ⊥ as the output selection state, but for the output environment to be well-typed, it must provide variable bindings corresponding to those introduced in the baseline computation where v was matched against . If ⇝ is defined with respect to a known w, this can be achieved via an additional rule ⇝ -hole-1 that defines the behaviour at hole to be the same as the behaviour at any -equivalent value in Sel v A. The ⇝ -hole-2 rule makes a similar provision for , which may also be a hole. Operationally, these rules can be interpreted as "expanding" enough of the holes in v or to make another rule of the definition match. There will be exactly one non-hole rule that matches, corresponding to the execution path originally taken, and although there may be multiple such expansions, the following property implies that the result of ⇝ w will be unique up to . Figure 9 also defines a family of forward-evaluation functions ⇒ T of type Sel ,e A × A → Sel v A for any T :: , e ⇒ v. Like forward-match, forward-evaluation is presented in a relational style, but should be understood as a total function defined by structural recursion on T . Forward evaluation replays T , using the input selection ( , e) ∈ Sel ,e A to determine an output selection v ∈ Sel v A. The rules mirror those of the evaluation relation ⇒, although there is an additional selection state input called the ambient availability. We explain this with reference to the application rule, which is the only point where a new ambient availability is assigned.

Forward evaluation.
Function application. The rule assumes the application e e ′ already has an ambient availability ; at the outermost level this will usually be ⊤. The rule passes down when recursively forwardevaluating e and e ′ , but computes a new selection state ⊓ ′ when transferring control to the function, combining ambient availability captured by the closure and ′ obtained by forwardmatching the argument v with the eliminator of the closure, representing the availability of those parts of v demanded by the function. The ambient availability is used to upper-bound the availability of any selectable values constructed in the dynamic context of that function, establishing a dependency between the resources consumed by functions and resources they produce. The auxiliary function ↠ ,h : Sel ,h A × A → Sel ′ A for any , h ↠ ′ is given at the bottom of Figure 9 and follows ↠, but captures the ambient availability into each closure.
Primitive application. Primitive operations are the other source of input-output dependencies beyond user-defined functions. Since a primitive operation is opaque, these dependencies cannot be derived from its execution, but must be specified by the primitive operation directly. More specifically, ∈ Int i → Int is required to provide a forward-dependency function #" n * : A i → A for every #" n ∈ Int i which specifies how to turn an input selection #" ∈ A i for #" n into an output selection ′ on ( #" n ). There is one such function per possible input #" n , since the dynamic dependencies for a primitive operation with an annihilator, such as multiplication, depend on the values passed to the operation. Primitives are free to implement forward-dependency however they want, except that § 3.3.2 will also require to provide a backward-dependency function for any input #" n , and § 3.4 will require these to be related in a certain way for the consistency of the whole system to be guaranteed.
Other rules. All other rules pass the ambient availability into any subcomputations unchanged. Variable lookup disregards the ambient , simply preserving the selection on the returned value. The lambda rule captures it in the closure, along with the environment; the letrec rule passes it on to ↠ so it is captured by recursive closures as well. Record projection is more interesting, disregarding not only the ambient but also the availability of the record itself. Containers are considered to be independent of the values they contain: here, v i has its own internal availability which is preserved by projection, but there is no implied dependency of the field on the record from which it was projected. Record construction also reflects this principle, preserving the field selections into the resulting record selection unchanged. But it also sets the availability of the record value to be the meet of and ′ , reflecting the dependency of the container on the constructing expression and also on any resources consumed by the ambient function. The rules for nil, cons and integers are similar.
Hole case. A hole rule is also needed, because if e is □, forward evaluation must continue; in particular, subsequent steps may extract non-□ values from and result in non-□ outputs. The rule is similar to the rules for ⇝ w and again can be understood operationally as using the information in T to expand □ sufficiently for another rule to apply, with a result which is unique up to . Environments have no special □ form. However, application and record projection must accommodate the case where the selection on the closure or record being eliminated is represented by □. In these rules ⇒ T is used to denote the relational composition of ⇒ T and .

Backward data dependency
The backward dependency function ⇒ T "rewinds" evaluation, turning output demand into input demand, with T guiding the analysis backward. We start with the auxiliary function ⇝ w which is used for backward-analysing a pattern-match. Figure 10 defines a family of backward-match functions ⇝ w of type Sel , A × A → Sel v, A for any w :: v, ⇝ , . Backward-match rewinds the match witnessed by w, turning demand on the environment and continuation into demand on the value and eliminator that were originally matched. The additional input represents the downstream demand placed on any resources that were constructed in the context of this match; ⇝ w transfers this to the matched portion of v, establishing a backwards link between resources produced and resources consumed in a given function context.

Backward match.
In the variable case, no proper part of v was matched, so is disregarded. The rule need only ensure that the demand v in the singleton environment x: v is propagated backward. If a Boolean constant was matched, becomes the demand on that constant, and , capturing the demand on the continuation, is used to construct the demand on the original eliminator, with □ used to represent the absence of demand on the non-taken branch. (Using □ for this means matches w need only retain information about taken branches.) The nil case is similar.
For a cons match w : w ′ , we split the environment into and ′ (there is a unique well-typed decomposition) and then backward-match w and w ′ recursively to obtain v and v ′ , representing the demand on the head and tail of the list. These are combined into the demand on the entire list, using as the demand on the cons node itself. represents the demand on the interim eliminator used to match the tail, and the demand on the eliminator used to match the head, which are , , ⇝ w v, and , with ambient demand , backward-match along w to v and v backward-evaluates along T to and e, with ambient demand then combined into a demand on the eliminator used to match the whole list, with □ again used to represent the absence of demand on the nil branch. Records are similar, except there is only a single branch, and the selection state computed for the initial part of the record is an artefact of processing records recursively, and is disregarded. Figure 10 also defines a family of backward-evaluation functions ⇒ T of type Sel v A → Sel ,e A × A for any T :: , e ⇒ v. Backward evaluation rewinds T , using the output selection v ∈ Sel v A to determine an input selection ( , e) ∈ Sel ,e A. The rules resemble those of the evaluation relation ⇒ with inputs and outputs flipped, and with an additional output called the ambient demand. The general pattern is that each backward rule takes the join of the demand attached to any partial values constructed at that step, and the ambient demand associated with any subcomputations, and passes it upwards as the new ambient demand. The output environment is constructed similarly, by joining the demand flowing back through the environment copies used to evaluate subcomputations. Demand is also attached to the source expression when it is the expression form responsible for the construction of a demanded value.
Function application. The application rule is where the ambient demand is used and the function context changes, so we start here. The rule essentially runs the forward evaluation rule in reverse, using the trace T ′ to backward-evaluate the function body. The ambient demand associated with T ′ is the join of the demand on any resources constructed directly by that function invocation, and is transferred to the matched part of the function argument by the backward-match function ⇝ w . The ambient demand passed upwards into the enclosing function context is ⊔ ′ , representing the resources needed along T and U. The auxiliary function ↠ ,h : Sel ′ A → Sel ,h A × A for any , h ↠ ′ defined at the bottom of Figure 10 is used to turn 2 , capturing the demand flowing back through any recursive uses of the function and any others with which it was mutually defined, into information that can be merged back into the demand on the closure. The function ↠ ,h is also used in the letrec rule, which otherwise follows the generic pattern described above.
Primitive application. Each primitive operation : Int i → Int must provide a backwarddependency function #" n * : A → A i for every #" n ∈ Int i which specifies how to turn the output selection ′ on ( #" n ) into an input selection #" a ∈ A i on #" n . The rule for primitive application uses this information to pair each argument n i with its demand i and then backwards-evaluate the argument. The ambient demand passed upward is the join of those arising from these subcomputations, and is unrelated to the execution of the primitive itself, similar to a function application. Here #" means the fold of ⊔ (with unit ⊥) over the sequence of selection states 1 · .. · ′ | #" x | . Environment demands #" = 1 · .. · | #" n | are joined (pointwise) in a similar fashion.
Other rules. In the variable case, no partial values were constructed during evaluation and there are no subcomputations, so the ambient demand is ⊥, the unit for ⊔. The returned environment selection demands v for the variable x and □ for all other variables, using the family of backwards lookup functions − ∋ x: − of type Sel v A → Sel A for any x: v ∈ also defined in Figure 10. (The output of the function is on the left in the relational notation.) For atomic values such as integers and nil, the ambient demand is simply the demand associated with the constructed value, which is also attached to the corresponding expression, and the environment demand has □ for every variable in the original environment , written □ .
For closures, the ambient demand is unpacked along with the other components, preserving any internal selections on and . Composite values such as records and cons cells follow the general pattern; thus for records, the ambient demands ′ i for the subcomputations are joined with the on the record itself to produce the ambient demand passed upward. Record projection never demands the record constructor itself, but simply promotes the field demand into a record demand, using using ∋ # " x: v to demand fields other that y with □. Hole rule. The hole rule, as elsewhere, ensures that the function is defined when v is □, and it is easy to show that ⇒ T preserves ⊑, and thus . Lemma 3.6 (Monotonicity of

Round-tripping properties of
We now establish more formally the round-tripping properties, alluded at the beginning of the section, that relate For the analyses to be coherent, we expect to produce an input selection ( ′ , e ′ ) ⊑ ( , e). Pairs of (monotonic) functions f : X → Y and g : Y → X that are related in this way are called Galois connections. Galois connections generalise isomorphisms: f and g are not quite mutual inverses, but are the nearest to an inverse each can get to the other. We will present a visual example of some of these round-tripping properties in § 4.2; here we establish the relevant theorems.
Definition 3.7 (Galois connection). Suppose X and Y are sets equipped with partial orders ≤ X and ≤ Y . Then monotonic functions f : Galois connections are also adjoint functors between poset categories, with right and left adjoints f and g usually called the upper and lower adjoints, because f approximates an inverse of g from above, and g an inverse of f from below. Galois connections compose component-wise, so it is useful to think of them as having a type X → Y , with the direction (by convention) given by the lower adjoint. If f : X → Y is a Galois connection, we will write f * and f * for the lower and upper adjoints respectively; an important property we will return to is that f * preserves joins and f * preserves meets. We now show that ⇒ T and ⇒ T form a Galois connection ⇒ T for any A (Theorem 3.11) by first establishing that the relevant auxiliary functions also form Galois connections. Theorem 3.8 (Galois connection for pattern-matching). Suppose w :: v, ⇝ , . Then We assume (rather than prove) that the forward and backwards dependency functions #" n = ( #" n * , #" n * ) provided for every primitive operation : Int i → Int form a Galois connection of type A → A i . Under this assumption the following holds.
Theorem 3.11 (Galois connection for evaluation). Suppose T : is an adjoint pair might seem rather weak as a correctess property: it merely ensures that the two analyses are related in a sensible way, not that they actually capture any useful information. This is a familiar problem from other approximate analyses like type systems and model checking, where properties like soundness or completeness are essential but do not by themselves guarantee utility. One could certainly define versions of ⇒ T and ⇒ T that are too coarse grained to be useful yet still satisfy Theorem 3.11. However Galois connections do at least require that every tightening or tweak to the forward analysis is paired with a corresponding adjustment to the backward analysis, and vice-versa. In § 6 we consider how other ideas from provenance and program slicing might be adapted to provide additional correctness criteria.

DE MORGAN DEPENDENCIES FOR BRUSHING AND LINKING § 3 addresses the first kind of question we motivated in the introduction ( § 1.1). In particular ⇒
T can answer questions like: "what data is needed to compute this bar in a bar chart?", and indeed we were able to use our implementation to generate Figure 1. The second problem we set ourselves was how to link selections between cognate outputs, i.e. outputs computed from the same data ( § 1.2). This is called "brushing and linking" [3] in data visualisation, and has been extensive studied as an interaction paradigm, but with little emphasis on techniques for automation. Intuitively, the problem has a bidirectional flavour: one must consider how dependencies flow backward from a selection in one output to a selection v in the common data, and then forward from the selected data v to a corresponding selection in the other output. A natural question then is whether the analysis established in § 3 can supply the information required to support an automated solution.
An immediate problem is that the flavour of the forward dependency required here differs from that provided by the forward analysis ⇒ T defined in § 3.2. That was able to answer the question: what can we compute given only the data selected in v? But to identify the related data in another output, we must determine not what the input selection v is sufficient for, but what it is necessary for: those parts of the other output that depend on v. In fact the question can be formulated as a kind of dual: what would we not be able to compute if the data selected in v were unavailable?

De Morgan duality
Why ⇒ T is unsuitable as a forward dependency relation for linking cognate outputs can also be understood in terms of compositionality. Suppose V 1 and V 2 are the lattices of selections for two views computed from a shared input source, and D is the lattice of selections for the shared input. Using the procedure given in § 3, we can obtain two Galois connections f : V 1 → D and g : V 2 → D as shown in Figure 11a below; we ask the reader to ignore Figure 11b for the moment.
Unfortunately, f and g are not composable, as their types makes clear. While the upper adjoint g * : D → V 2 has the correct type to compose with the lower adjoint f * : V 1 → D, the result is not a Galois connection: g * preserves meets, whereas f * preserves joins. However, it turns out that if selections are closed under complement, we can derive an analysis of what is necessary for a given input selection from an analysis of what it is sufficient for. The effect is to invert g, yielding a Galois connection g • with a type that allows it to compose with f . Then the composite g • • f is a Galois connection linking V 1 to V 2 via D, as shown in Figure 11b, offering a general mechanism for brushing and linking, with nice round-tripping properties. We now unpack this in more detail.

Example: matrix convolution
We now illustrate the ⇒ T • Galois connection, contrasting it with ⇒ T , using an example which computes the convolution of a 5 × 5 matrix with a 3 × 3 kernel. Convolution has an intuitive dependency structure and the values involved have an easy visual presentation, making it useful for conveying the flavour of the four distinct (but connected) dependency relations that arise in the framework. The source code for the example is given in Figure 12, and shows the convolve function, plus zero, wrap and extend which provide different methods for handling the boundaries of the input matrix. The angle-bracket notation is used to construct matrices, which were omitted from § 2. (The formal treatment is similar to records.) Fluid was used to generate the diagrams in Figure 13, which show the four dependency relations and two of their four possible round-trips. Figure 13a shows the ⇒ T Galois connection defined in § 3.4. In the upper figure, the user selects (in green) the output cell at position (2, 2) (counting rows downwards from 1). This induces a demand (via the lower adjoint ⇒ T ) on the input matrix image and the kernel filter, revealing (in yellow) that the entire kernel was needed to compute the value 1, but only some of the input matrix. In particular the elements at (1, 3) and (3, 1) in image were not needed, because of zeros present in filter. If we then "round-trip" that input selection, computing the corresponding availability on the output using the upper adjoint ⇒ T , the green selection grows: it turns out that the data needed to make (2, 2) available are sufficient to make (1, 1) available as well. Figure 13b shows the De Morgan dual ⇒ T • . In the upper part of the figure, the user selects (green) kernel cell (1, 2) to see the output cells that depend on it. This is computed using the De Morgan dual of ⇒ T . First we negate the input selection, marking (1, 2) as unavailable, and all other inputs as available. Then we forward-analyse with ⇒ T to determine that with this data selection, we can only compute the top row of the output. (If it seems odd that we can compute even the top row, notice that the example uses the method zero for dealing with boundaries; wrap or extend would give a different behaviour.) Then we negate that top row selection to produce the (yellow) output selection shown in the figure. These are exactly the output cells which depend on kernel cell (1,2) in the sense that they cannot be computed if that input is unavailable.
We can then round-trip this output selection using the De Morgan dual of ⇒ T . We first negate the yellow output selection (selecting the top row of the output again), and then use ⇒ T to determine the needed inputs, which turn out to be the top two rows of image, and the top row of filter. Negating again produces the green output selection shown in the lower figure. Thus the backwards De Morgan dual computes the inputs that would not be needed if the selected outputs were not needed: more economically, the inputs that are only needed for the selected output. Here the round-trip reveals that if kernel cell (1, 2) is unavailable, then the entire top row of the kernel might as well have been unavailable too, and similarly for the bottom 3 rows of the input.

Relationship to Galois slicing
The De Morgan dual puts us in a better position to consider the relationship between the present system and earlier work on Galois slicing, a program slicing technique that has been explored for pure functional programs [22], functional programs with effects [27], and -calculus [24]. We consider other related work in § 6.1.
Galois slicing operates on lattices of slices, which are programs (or values) where parts deemed irrelevant are replaced by a hole □. (If we think of the notion of selection defined in § 3.1.1 as picking out a subset of the paths in a term, then slices resembles selections which are prefix-closed, meaning that if a given path in a term is selected, then so are all of its prefixes.) For a fixed computation, a meet-preserving forward-slicing function is defined which takes input slices to output slices, discarding parts which cannot be computed because the needed input is not present, plus a joinpreserving backward-slicing function taking output slices to input slices, retaining the parts needed for the output slice. For example Figure 14a shows a computation with output (0.4, 0.6), and Figure 14b gives the backward slice for output slice (0.4, □). Forward and backward slicing, for a given computation, form a Galois connection, giving the analyses the nice round-tripping properties we motivated in § 3.4.
Unfortunately, the notion of slice does not lend itself to computing dependencies where the needed input or output is a proper part of a value, such as a component of a tuple. Differential slicing [22] improves on this by using Galois slicing to compute a pair of input slices (e, e ′ ) for a pair of output slices (v, v ′ ) where v ⊑ v ′ . By monotonicity, e ⊑ e ′ . This can be used to compute a (differential) slice for an arbitrary subtree, by setting v to be the "spine" of the original output up to the location of the subtree, and v ′ to be v with the subtree of interest plugged back in. Here we could focus on the value 0.4 in the output by computing the backward slice for (□, □) ( Figure 14c) and then comparing it with the backward slice for (0.4, □), generating a differential slice where the parts that are different are highlighted (Figure 14d). But although it supports a notion of selection which is closer to what we need, the differential slice highlights only the program parts that are needed exclusively by the selected output. Here, 2 and 3 are needed to compute the spine as well (in order to decide which conditional branch to execute), so they are excluded from the differential slice. In fact differential slicing is similar to the dual of ⇒ T , and as such underapproximates the dependency information needed for data linking.

GALOIS CONNECTIONS FOR DESUGARING
Elaborating a richer surface language into a simpler core is a common pattern with well known benefits. It can, however, make it harder to express certain information to the programmer in terms of the surface language. We face this problem with the analysis in § 3, which links outputs not only to inputs, but also to expressions responsible for introducing data. We could use this information in an IDE to link structured outputs to relevant code fragments, but only if we are able to map term selections back to the surface program. We now sketch a bidirectional desugaring procedure which addresses this, and which composes with the Galois dependency analysis defined in § 3.

Surface language syntax
The surface language Fluid extends the core syntax with list notation [s,…,s ′ ], Haskell 98-style list comprehensions [17], list enumerations, first-class primitives and piecewise function definitions and pattern-matching, as shown in Figure 15. Typing rules are given in Appendix A, Figures 18  and 19. We attach selection states to (selectable) surface terms s, t that desugar to selectable core terms, and let s, t range over "raw" surface terms, which are isomorphic to the selectable terms where the type of selection states is the unit lattice 1. Figure 16 shows how the end-to-end mapping would appear to a user. (For illustrative purposes the library function map and some raw data are included in the same source file.) On the left, the user selects a cons cell (green) in the output; by backwards evaluating and then backwards desugaring, we are able to highlight the list comprehension, the cons in the second clause of map, and both occurrences of the constant "Hydro". These last two are highlighted because the selected cons cell was constructed by eliminating a Boolean that was in turn constructed by the primitive == operator, which consumed the two strings. The user might then conjecture that the two occurrences of "Geo" were somehow responsible for the inclusion of the third cons cell in the output; they can confirm this by making the green selection on the right. (Highlighting == too would clearly be helpful here; we discuss this possibility in § 6.1.) The grey selection is included to contrast the cons highlighting with the data demanded by the list elements themselves, which is quite different.

Forward desugaring
To define the forward evaluation function ⇒ T in § 3.2, we performed a regular evaluation using ⇒ to obtain a trace T , and then defined ⇒ T by recursion over T , with T guiding the analysis in the presence of □. There are no holes in the surface language, so we can take a simpler approach, defining a single forward desugaring relation ↠ , and then showing that for every raw surface term t ↠ e, there is a monotonic function ↠ t : Sel t A → Sel e A, which is simply ↠ domain-restricted to Sel t A. The full definition of ↠ is given in Appendix A ; Figure 17 gives a representative selection of the rules.
The definition follows a similar pattern to ⇒ T . At each step, we take the meet of the availability on any parts of s being consumed at that step, and use that as the availability of any parts of e being generated at that step. Thus the rules for list notation simply transfer the selection state on the opening and closing brackets [ and ] to the corresponding cons and nil of the resulting list, and those on intervening delimiters , to the corresponding cons. List comprehensions [ s | #" q ] have a rule for each kind of qualifier q at the head of #" q , plus a rule for when #" q is . The general pattern is to push the on the comprehension itself through recursively, so it ends up on all core terms generated during its elaboration: in particular the false branch when q is a guard, and the singleton list when #" q is empty. Auxiliary relations ⇀ and ↗ p (defined in Appendix A, Figures 22  and 23) transfer availability on guards and generators onto the eliminators they elaborate into.

Backward desugaring
The backwards analysis is then defined as a family of backward desugaring functions ↠ t : Sel e A → Sel t A for any t ↠ e, with the raw surface term t guiding the analysis backwards. (The role of t in disambiguating the backwards rules should be clear if you consider that e typically matches multiple rules but only one for a given t.) Figure 17 gives some representative rules; the full definition is given in Appendix A To reverse a desugaring step, we take the join of the demand on any parts of e which were constructed at this step, and use that as the demand on the parts of s which were consumed at this step, turning demand on the core term into (minimal) demand on the surface term. Thus the effect of the list comprehension rules and auxiliary judgements is to set the demand on the comprehension itself to be the join of the demand of all the syntax generated during the elaboration of the comprehension, using auxiliary judgments ↘ p and r ↠ e r forward-desugars to e

Round-tripping properties and compositionality
It is easy to verify that ↠ t and ↠ t are monotonic. Moreover they form an adjoint pair.
The ↠ t Galois connection readily composes with ⇒ T to produce surface-language selections like the ones shown in Figure 16. This is useful, although somewhat monolithic. In future work we will investigate techniques for backwards desugaring at arbitrary steps in the computation (perhaps by interleaving desugaring with execution), and presenting selections on intermediate values (such as lists) in the surface language, even though they were not obtained via desugaring.

CONCLUSION
Our research was motived by the goal of making computational outputs which are automatically able to reveal how they relate to data in a fine-grained way. A casual reader who wants to understand or fact-check a chart, or a scientist evaluating another's work, should be able to do so by interacting directly with an output. Recent work by Walny et al. suggests that developers would also benefit from such a feature while implementing visualisations, for example to check whether a quantity is represented by diameter or area in a bubble chart [31]. Galois connections provide an appealing setting for this problem because of their elegant roundtripping properties. However, existing dynamic analysis techniques based on Galois connections do not lend themselves to richly structured outputs like visualisations and matrices. We presented an approach that allows focusing on arbitrary substructures, which also means data selections can be inverted. This enables linking not just of outputs to data, but of outputs to other outputs, providing a mathematical basis for a widely used (but so far ad hoc) feature in data visualisation. We implemented our approach in Fluid, a realistic high-level functional programming language. Our implementation can be found at https://github.com/explorable-viz/fluid.

Other related work and future directions
We close by considering some limitations and opportunities in the context of other related work. Galois slicing [22,27,24] was considered in § 4.3.
Executable slicing. Executable slices [14] are programs with some parts removed, but which are still executable. Our approach computes data selections, not executable slices, but such a notion has obvious relevance in data science, since "explaining" a part of a result should (arguably) entail being able to recompute it. Expression provenance [1] explains how primitive values are computed using only primitive operations; however, this still omits crucial information, and does not obviously generalise to structured outputs. Work on executable slicing in term rewriting [11] could perhaps be adapted to structured values in our setting.
Dynamic program analysis. Dynamic analysis techniques like dataflow analysis [8,26] and taint tracking [26] tend to focus on variables, rather than parts of structured values, and lack roundtripping properties; Galois dependencies have a clear advantage here. A limitation of dynamic techniques which is shared by our approach is that they can usually only reveal that certain dependencies arise, not why, which requires analysing path conditions [15]. In a data science setting this would clearly be valuable too, and it would be interesting to see if the benefits of the Galois framework can be extended to techniques for computing dynamic path conditions.
Brushing and linking. Brushing and linking has been extensive studied in the data visualisation community [19,3], but although Roberts and Wright [28] argued it should be ubiquitous, no automated method of implementation has been proposed to date. Geospatial applications like GeoDa [2] hard-code view coordination features into specific views, and libraries like d3.js and Plotly support ad hoc linking mechanisms, with varying degrees of programmer effort required. No existing approach provides automation or round-tripping guarantees, or is able to provide data selections explaining why visual selections are linked.