arXiv:1404.7078v2 [cs.DB] 2 May 2014

Query shredding: Efficient relational evaluation of queries
over nested multisets (extended version)
James Cheney

Sam Lindley

Philip Wadler

University of Edinburgh

University of Edinburgh

University of Edinburgh

jcheney@inf.ed.ac.uk

Sam.Lindley@ed.ac.uk

wadler@inf.ed.ac.uk

ABSTRACT
Nested relational query languages have been explored extensively,
and underlie industrial language-integrated query systems such as
Microsoft’s LINQ. However, relational databases do not natively
support nested collections in query results. This can lead to major performance problems: if programmers write queries that yield
nested results, then such systems typically either fail or generate
a large number of queries. We present a new approach to query
shredding, which converts a query returning nested data to a fixed
number of SQL queries. Our approach, in contrast to prior work,
handles multiset semantics, and generates an idiomatic SQL:1999
query directly from a normal form for nested queries. We provide
a detailed description of our translation and present experiments
showing that it offers comparable or better performance than a recent alternative approach on a range of examples.

1.

INTRODUCTION

Databases are one of the most important applications of declarative programming techniques. However, relational databases only
support queries against flat tables, while programming languages
typically provide complex data structures that allow arbitrary combinations of types including nesting of collections (e.g. sets of
sets). Motivated by this so-called impedance mismatch, and inspired by insights into language design based on monadic comprehensions [33], database researchers introduced nested relational
query languages [26, 4, 5] as a generalisation of flat relational
queries to allow nesting collection types inside records or other
types. Several recent language designs, such as XQuery [25] and
PigLatin [23], have further extended these ideas, and they have
been particularly influential on language-integrated querying systems such as Kleisli [35], Microsoft’s LINQ in C# and F# [22, 28,
6], Links [8, 20], and Ferry [11].
This paper considers the problem of translating nested queries
over nested data to flat queries over a flat representation of nested
data, or query shredding for short. Our motivation is to support
a free combination of the features of nested relational query languages with those of high-level programming languages, particularly systems such as Links, Ferry, and LINQ. All three of these

This paper is an extended version of a paper to appear at SIGMOD 2014.

systems support queries over nested data structures (e.g. records
containing nested sets, multisets/bags, or lists) in principle; however, only Ferry supports them in practice. Links and LINQ currently either reject such queries at run-time or execute them inefficiently in-memory by loading unnecessarily large amounts of data
or issuing large numbers of queries (sometimes called query storms
or avalanches [12] or the N + 1 query problem). To construct
nested data structures while avoiding this performance penalty, programmers must currently write flat queries (e.g. loading in a superset of the needed source data) and convert the results to nested data
structures. Manually reconstructing nested query results is tricky
and hard to maintain; it may also mask optimisation opportunities.
In the Ferry system, Grust et al. [11, 12] have implemented shredding for nested list queries by adapting an XQuery-to-SQL translation called loop-lifting [15]. Loop-lifting produces queries that
make heavy use of advanced On-Line Analytic Processing (OLAP)
features of SQL:1999, such as ROW_NUMBER and DENSE_RANK,
and to optimise these queries Ferry relies on a SQL:1999 query
optimiser called Pathfinder [14].
Van den Bussche [31] proved expressiveness results showing
that it is possible in principle to evaluate nested queries over
sets via multiple flat queries. To strengthen the result, Van den
Bussche’s simulation eschews value invention mechanisms such as
SQL:1999’s ROW_NUMBER. The downside, however, is that the flat
queries can produce results that are quadratically larger than needed
to represent sets and may not preserve bag semantics. In particular, for bag semantics the size of a union of two nested sets can be
quadratic in the size of the inputs — we give a concrete example in
Appendix A.
Query shredding is related to the well-studied query unnesting
problem [17, 10]. However, most prior work on unnesting only
considers SQL queries that contain subqueries in WHERE clauses,
not queries returning nested results; the main exception is Fegaras
and Maier’s work on query unnesting in a complex object calculus [10].
In this paper, we introduce a new approach to query shredding
for nested multiset queries (a case not handled by prior work).
Our work is formulated in terms of the Links language, but should
be applicable to other language-integrated query systems, such as
Ferry and LINQ, or to other complex-object query languages [10].
Figure 1 illustrates the behaviour of Links, Ferry and our approach.
We decompose the translation from nested to flat queries into
a series of simpler translations. We leverage prior work on normalisation that translates a higher-order query to a normal form in
which higher-order features have been eliminated [34, 7, 10]. Our
algorithm operates on normal forms. We review normalisation in
Section 2, and give a running example of our approach in Section 3.
Sections 4–7 present the remaining phases of our approach, which

(a)

(b)
Ferry

Q
r

Links
normalisation

Q'

RDBMS

r

Q

loop-lifting Pathfinder

r

rebuilding

Figure 1: (a) Default Links behaviour (flat queries)

Q

RDBMS

r1
...
rn

BACKGROUND

We use metavariables x, y, . . . , f, g for variables, and c, d, . . .
for constants and primitive operations. We also use letters t, t0 , . . .
for table names, `, `0 , `i , . . . for record labels and a, b, . . . for tags.
We write M [x := N ] for capture-avoiding substitution of N for
x in M . We write ~x for a vector x1 , . . . , xn . Moreover, we extend
vector notation pointwise to other constructs, writing, for example,
−−−−→
h` = M i for h`1 = M1 , . . . , `n = Mn i.
We write: square brackets [−] for the meta level list constructor;
w :: ~v for adding the element w onto the front of the list ~v ; ~v ++ w
~
for the result of appending the list w
~ onto the end of the list ~v ; and
concat for the function that concatenates a list of lists. We also

normalisation shredding

Q1
...
Qn
r1
...
rn

stitching

r

(b) Ferry (nested list queries)

are new. The shredding phase translates a single, nested query to a
number of flat queries. These queries are organised in a shredded
package, which is essentially a type expression whose collection
type constructors are annotated with queries. The different queries
are linked by indexes, that is, keys and foreign keys. The shredding translation is presented in Section 4. Shredding leverages the
normalisation phase in that we can define translations on types and
terms independently. Section 5 shows how to run shredded queries
and stitch the results back together to form nested values.
The let-insertion phase implements a flat indexing scheme using a let-binding construct and a row-numbering operation. Letinsertion (described in Section 6) is conceptually straightforward,
but provides a vital link to proper SQL by providing an implementation of abstract indexes. The final stage is to translate to SQL
(Section 7) by flattening records, translating let-binding to SQL’s
WITH, and translating row-numbering to SQL’s ROW_NUMBER. This
phase also flattens nested records; the (standard) details are included in Appendix E for completeness.
We have implemented and experimentally evaluated our approach
(Section 8) in comparison with Ulrich’s implementation of looplifting in Links [30]. Our approach typically performs as well or
better than loop-lifting, and can be significantly faster.
Our contribution over prior work can be summarised as follows.
Fegaras and Maier [10] show how to unnest complex object queries
including lists, sets, and bags, but target a nonstandard nested relational algebra, whereas we target standard SQL. Van den Bussche’s simulation [31] translates nested set queries to several relational queries but was used to prove a theoretical result and was not
intended as a practical implementation technique, nor has it been
implemented and evaluated. Ferry [11, 12] translates nested list
queries to several SQL:1999 queries and then tries to simplify the
resulting queries using Pathfinder. Sometimes, however, this produces queries with cross-products inside OLAP operations such as
ROW_NUMBER, which Pathfinder cannot simplify. In contrast, we
delay introducing OLAP operations until the last stage, and our experiments show how this leads to much better performance on some
queries. Finally, we handle nested multisets, not sets or lists.
This report is the extended version of a SIGMOD 2014 paper,
and contains additional details, proofs of correctness, and comparison with related work in appendices.

2.

(c)
Our approach

Q1
...
Qn

RDBMS

(c) Our approach (nested bag queries)

N JxKρ
N Jc(X1 , . . . , Xn )Kρ
N Jλx.M Kρ
N JM N Kρ
N Jh`i = Mi in
i=1 Kρ
N JM.`Kρ

N Jif L then M else N Kρ

N Jreturn M Kρ
N J∅Kρ
N JM ] N Kρ
N Jfor (x ← M ) N Kρ
N Jempty M Kρ
N Jtable tKρ

= ρ(x)
= JcK(N JX1 Kρ , . . . , N JXn Kρ )
= λv.N JM Kρ[x7→v]
= N JM Kρ (N JN Kρ )
= h`i = N JMi Kρ in
i=1
=N
 JM Kρ .`
N JM Kρ , if N JLKρ = true
=
N JN Kρ , if N JLKρ = false
= [N JM Kρ ]
= []
= N JM Kρ ++ N JN Kρ
=
concat[N JN Kρ[x7→v] | v ← N JM Kρ ]
true, if N JM Kρ = [ ]
=
false, if N JM Kρ 6= [ ]
= JtK

Figure 2: Semantics of λNRC
make use of the following functions:
n−1
init [xi ]n
i=1 = [xi ]i=1

last [xi ]n
i=1 = xn

enum([v1 , . . . , vm ]) = [h1, v1 i, . . . hm, vm i]
In the meta language we make extensive use of comprehensions,
primarily list comprehensions. For instance, [v | x ← xs, y ←
ys, p], returns a copy of v for each pair hx, yi of elements of xs
and ys such that the predicate p holds. We write [vi ]n
i=1 as shorthand for [vi | 1 ≤ i ≤ n] and similarly, e.g., h`i = Mi in
i=1 for
h`1 = M1 , . . . , `n = Mn i.

2.1

Nested relational calculus

We take the higher-order, nested relational calculus (evaluated
over bags) as our starting point. We call this λNRC ; this is essentially a core language for the query components of Links, Ferry,
and LINQ. The types of λNRC include base types (integers, strings,
−−→
booleans), record types h` : Ai, bag types Bag A, and function
types A → B.
−−→
Types
A, B ::= O | h` : Ai | Bag A | A → B
Base types
O ::= Int | Bool | String
We say that a type is nested if it contains no function types and flat
if it contains only base and record types.
The terms of λNRC include λ-abstractions, applications, and the
standard terms of nested relational calculus.
~ ) | table t | if M then N else N 0
Terms M, N ::= x | c(M
−−−−→
| λx. M | M N | h` = M i | M.` | empty M
| return M | ∅ | M ] N | for (x ← M ) N
We assume that the constants and primitive functions include
boolean values with negation and conjunction, and integer values
with standard arithmetic operations and equality tests. We assume
special labels #1 , #2 , . . . and encode tuple types hA1 , . . . , An i
as record types h#1 : A1 , . . . , #n : An i, and similarly tuple terms

hM1 , . . . , Mn i as record terms h#1 = M1 , . . . , #n = Mn i. We
assume fixed signatures Σ(t) and Σ(c) for tables and constants. The tables are constrained to have flat relation type
(Bag h`1 : O1 , . . . , `n : On i), and the constants must be of base
type or first order n-ary functions (hO1 , . . . , On i → O).
Most language constructs are standard. The ∅ expression builds
an empty bag, return M constructs a singleton, and M ] N builds
the bag union of two collections. The for (x ← M ) N comprehension construct iterates over a bag obtained by evaluating M , binds
x to each element, evaluates N to another bag for each such binding, and takes the union of the results. The expression empty M
evaluates to true if M evaluates to an empty bag, false otherwise.
λNRC employs a standard type system similar to that presented
in other work [35, 20, 6]. We will also employ several typed intermediate languages and translations mapping λNRC to SQL. All
of these (straightforward) type systems are omitted due to space
limits; they will be available in the full version of this paper.

Semantics. We give a denotational semantics in terms of lists.
Though we wish to preserve bag semantics, we interpret objectlevel bags as meta-level lists. For meta-level values v and v 0 , we
consider v and v 0 equivalent as multisets if they are equal up to
permutation of list elements. We use lists mainly so that we can
talk about order-sensitive operations such as row_number.
We interpret base types as integers, booleans and strings, function types as functions, record types as records, and bag types as
lists. For each table t ∈ dom(Σ), we assume a fixed interpretation
JtK of t as a list of records of type Σ(t). In SQL, tables do not
have a list semantics by default, but we can impose one by choosing a canonical ordering for the rows of the table. We order by
all of the columns arranged in lexicographic order (assuming linear
orderings on field names and base types).
We assume fixed interpretations JcK for the constants and primitive operations. The semantics of nested relational calculus are
shown in Figure 2. The (standard) typing rules are given in Appendix B. We let ρ range over environments mapping variables to
values, writing ε for the empty environment and ρ[x 7→ v] for the
extension of ρ with x bound to v.

2.2

Query normalisation

In Links, query normalisation is an important part of the execution model [7, 20]. Links currently supports only queries mapping
flat tables to flat results, or flat–flat queries. When a subexpression
denoting a query is evaluated, the subexpression is first normalised
and then converted to SQL, which is sent to the database for evaluation; the tuples received in response are then converted into a Links
value and normal execution resumes (see Figure1(a)).
For flat–nested queries that read from flat tables and produce a
nested result value, our normalisation procedure is similar to the
one currently used in Links [20], but we hoist all conditionals into
the nearest enclosing comprehension as where clauses. This is a
minor change; the modified algorithm is given in the full version of
this paper. The resulting normal forms are:
U ~
Query terms
L ::= C
~ where X) return M
Comprehensions
C ::= for (G
Generators
G ::= x ← t
Normalised terms M, N ::= X | R | L
−−−−→
Record terms
R ::= h` = M i
~ | empty L
Base terms
X ::= x.` | c(X)
Any closed flat–nested query can be converted to an equivalent term
in the above normal form.

JdepartmentsK =
(id)
1
2
3
4

name
Product
Quality
Research
Sales

JtasksK =
(id)
1
2
3
4
5
6
7
8
9
10
11
12
13
14

employee
Alex
Bert
Cora
Cora
Cora
Cora
Cora
Drew
Drew
Erik
Erik
Fred
Gina
Gina

JemployeesK =
(id)
1
2
3
4
5
6
7

task
build
build
abstract
build
call
dissemble
enthuse
abstract
enthuse
call
enthuse
call
call
dissemble

dept
Product
Product
Research
Research
Sales
Sales
Sales

JcontactsK =
(id)
1
2
3
4
5
6
7

name
Alex
Bert
Cora
Drew
Erik
Fred
Gina

dept
Product
Product
Research
Research
Sales
Sales
Sales

salary
20000
900
50000
60000
2000000
700
100000

name
Pam
Pat
Rob
Roy
Sam
Sid
Sue

client
false
true
false
false
false
false
true

Figure 3: Sample data
T HEOREM 1. Given a closed flat–nested query ` M : Bag A,
there exists a normalisation function norm Bag A , mapping each M
to an equivalent normal form norm Bag A (M ).
The normalisation algorithm and correctness proof are similar
to those in previous papers [7, 20, 6]. The details are given in
Appendix C. The normal forms above can also be viewed as an
SQL-like language allowing relation-valued attributes (similar to
the complex-object calculus of Fegaras and Maier [10]). Thus, our
results can also be used to support nested query results in an SQLlike query language. In this paper, however, we focus on the functional core language based on comprehensions, as illustrated in the
next section.

3.

RUNNING EXAMPLE

To motivate and illustrate our work, we present an extended example showing how our shredding translation could be used to provide useful functionality to programmers working in LINQ using
F#, Ferry or Links. We first describe the code the programmer
would actually write and the results the system produces. Throughout the rest of the paper, we return to this example to illustrate how
the shredding translation works.
Consider a flat database schema Σ for an organisation:
tasks(employee : String, task : String)
employees(dept : String, name : String, salary : Int)
contacts(dept : String, name : String, client : Bool)
departments(name : String)

Each department has a name, a collection of employees, and a collection of external contacts. Each employee has a name, salary and
a collection of tasks. Some contacts are clients. Figure 3 shows
a small instance of this schema. For convenience, we also assume
every table has an integer-valued key id.
In λNRC , queries of the form for . . . where . . . return . . . are natively supported. These are comprehensions as found in XQuery or
functional programming languages, and they generalise idiomatic

SQL SELECT FROM WHERE queries [4]. Unlike SQL, we can use
(nonrecursive) functions to define queries with parameters, or parts
of queries, and freely combine them. For example, the following
functions define useful query patterns over the above schema:
tasksOfEmp e = for (t ← tasks)
where (t.employee = e.name)
return t.tsk
contactsOfDept d = for (c ← contacts)
where (d.dept = c.dept)
return hname = c.name, client = c.clienti
employeesByTask t =
for (e ← employees, d ← departments)
where (e.name = t.employee ∧ e.dept = d.dept)
return hb = e.employee, c = d.depti

Nested queries allow free mixing of collection (bag) types with
record or base types. For example, the following query
employeesOfDept d = for (e ← employees)
where (d.dept = e.dept)
return hname = e.name, salary = e.salary,
tasks = tasksOfEmp ei

returns a nested result: a collection of employees in a department,
each with an associated collection of tasks. That is, its return type
is Bag hname:String, salary:Int, tasks:Bag Stringi
Consider the following nested schema for organisations:
Task
Employee
Contact
Department

= String
= hname : String, salary : Int, tasks : Bag Task i
= hname : String, client : Booli
= hname : String, employees : Bag Employee,
contacts : Bag Contacti
Organisation = Bag Department

Using some of the above functions we can write a query Qorg that
maps data in the flat schema Σ to the nested type Organisation, as
follows:
Qorg = for (d ← departments)
return (hname = d.name,
employees = employeesOfDept d,
contacts = contactsOfDept di

We can also define and use higher-order functions to build queries,
such as the following:
filter p xs = for (x ← xs) where (p(x)) return x
any xs p = ¬(empty(for (x ← xs) where (p(x)) return hi))
all xs p = ¬(any xs (λx.¬(p(x))))
contains xs u = any xs (λx.x = u)

To illustrate the main technical challenges of shredding, we consider a query with two levels of nesting and a union operation.
Suppose we wish to find for each department a collection of people of interest, both employees and contacts, along with a list of the
tasks they perform. Specifically, we are interested in those employees that earn less than a thousand euros and those who earn more
than a million euros, call them outliers, along with those contacts
who are clients. The following code defines poor, rich, outliers, and
clients:
isPoor x = x.salary < 1000
isRich x = x.salary > 1000000
outliers xs = filter (λx.isRich x ∨ isPoor x) xs
clients xs = filter (λx. x.client) xs

We also introduce a convenient higher-order function that uses its
f parameter to initialise the tasks of its elements:
getTasks xs f = for (x ← xs) return hname = x.name, tasks = f xi

Using the above operations, the query Q returns each department, the outliers and clients associated with that department, and
their tasks. We assign the special task “buy” to clients.
Q(organisation) =
for (x ← organisation)
return (hdepartment = x.name,
people =
getTasks(outliers(x.employees)) (λy. y.tasks)
] getTasks(clients(x.contacts)) (λy. return “buy”)i)

The result type of Q is:
Result = Bag hdepartment : String,
people : Bag hname : String, tasks : Bag Stringii

We can compose Q with Qorg to form a query Q(Qorg ) from the
flat data stored in Σ to the nested Result. The normal form of this
composed query, which we call Qcomp , is as follows:
Qcomp = for (x ← departments)
return (
hdepartment = x.name,
people =
(for (y ← employees) where (x.name = y.dept ∧
(y.salary < 1000 ∨ y.salary > 1000000))
return (hname = y.name,
tasks = for (z ← tasks)
where (z.employee = y.name)
return z.taski))
] (for (y ← contacts)
where (x.name = y.dept ∧ y.client)
return (hname = y.name,
tasks = return “buy”i))i)

The result of running Qcomp on the data in Figure 3 is:
[hdepartment = “Product”,
people = [hname = “Bert”, tasks = [“build”]i,
hname = “Pat”, tasks = [“buy”]i]i]
hdepartment = “Research”, people = ∅i,
hdepartment = “Quality”, people = ∅i,
hdepartment = “Sales”,
people = [hname = “Erik”, tasks = [“call”, “enthuse”]i,
hname = “Fred”, tasks = [“call”]i,
hname = “Sue”, tasks = [“buy”]i]i]

Now, however, we are faced with a problem: SQL databases
do not directly support nested multisets (or sets). Our shredding
translation, like Van den Bussche’s simulation for sets [31] and
Grust et al.’s for lists [12], can translate a normalised query such
as Qcomp : Result that maps flat input Σ to nested output Result
to a fixed number of flat queries q1 : Result 1 , . . . , qn : Result n
whose results can be combined via a stitching operation Qstitch :
Result 1 × · · · × Result n → Result. Thus, we can simulate the
query Qcomp by running q1 , . . . , qn remotely on the database and
stitching the results together using Qstitch . The number of intermediate queries n is the nesting degree of Result, that is, the number
of collection type constructors in the result type. For example, the
nesting degree of Bag hA : Bag Int, B : Bag Stringi is 3. The
nesting degree of the type Result is also 3, which means Q can be
shredded into three flat queries.
The basic idea is straightforward. Whenever a nested bag appears in the output of a query, we generate an index that uniquely
identifies the current context. Then a separate query produces the
contents of the nested bag, where each element is paired up with its
parent index. Each inner level of nesting requires a further query.
We will illustrate by showing the results of the three queries and
how they can be combined to reconstitute the desired nested result.

The outer query q1 contains one entry for each department, with an
index ha, idi in place of each nested collection:
r1 = [hdepartment = “Product”, people = ha, 1ii,
hdepartment = “Quality”, people = ha, 2ii,
hdepartment = “Research”, people = ha, 3ii,
hdepartment = “Sales”,
people = ha, 4ii]

The second query q2 generates the data needed for the people
collections:
r2 = [hha, 1i, hname = “Bert”, tasks = hb, 1, 2iii,
hha, 4i, hname = “Erik”, tasks = hb, 4, 5iii,
hha, 4i, hname = “Fred”, tasks = hb, 4, 6iii,
hha, 1i, hname = “Pat”, tasks = hd, 1, 2iii,
hha, 4i, hname = “Sue”, tasks = hd, 4, 7iii]

The idea is to ensure that we can stitch the results of q1 together
with the results of q2 by joining the inner indexes of q1 (bound to
the people field of each result) with the outer indexes of q2 (bound
to the first component of each result). In both cases the static components of these indexes are the same tag a. Joining the people
field of q1 to the outer index of q2 correctly associates each person
with the appropriate department.
Finally, let us consider the results of the innermost query q3 for
generating the bag bound to the tasks field:

In order to shred nested queries, we introduce an abstract type
Index of indexes for maintaining the correspondence between outer
and inner queries. An index a  d has a static component a and a
dynamic component d. The static component a links the index to
the corresponding returna in the query. The dynamic component
identifies the current bindings of the variables in the comprehension.
Next, we modify types so that bag types have an explicit index
component and we use indexes to replace nested occurrences of
bags within other bags:
Shredded types A, B ::= Bag hIndex , F i
−−→
Flat types
F ::= O | h` : F i | Index
We also adapt the syntax of terms to incorporate indexes. After
shredding, terms will have the following forms:
U ~
Query terms
L, M ::= C
Comprehensions
Generators
Inner terms
Record terms
Base terms
Indexes
Dynamic indexes

r3 = [hhb, 1, 2i, “build”i, hhb, 4, 5i, “call”i, hhb, 4, 5i, “enthuse”i,
hhb, 4, 6i, “call”i, hhd, 1, 2i, “buy”i, hhd, 4, 7i, “buy”i]

Recall that q2 returns further inner indexes for the tasks associated with each person. The two halves of the union have different
static indexes for the tasks b and d, because they arise from different comprehensions in the source term. Furthermore, the dynamic
index now consists of two id fields (x.id and y.id) in each half of
the union. Thus, joining the tasks field of q2 to the outer index of
q3 correctly associates each task with the appropriate outlier.
Note that each of the queries q1 , q2 , q3 produces records that contain other records as fields. This is not strictly allowed by SQL, but
it is straightforward to simulate such nested records by rewriting to
a query with no nested collections in its result type; this is similar to Van den Bussche’s simulation [31]. However, this approach
incurs extra storage and query-processing cost. Later in the paper,
we explore an alternative approach which collapses the indexes at
each level to a pair ha, ii of static index and a single “surrogate”
integer, similarly to Ferry’s approach [12]. For example, using this
approach we could represent the results of q2 and q3 as follows:
r20 = [hha, 1i, hname = “Bert”, tasks = hb, 1iii,
hha, 4i, hname = “Erik”, tasks = hb, 2iii,
hha, 4i, hname = “Fred”, tasks = hb, 3iii,
hha, 1i, hname = “Pat”, tasks = hd, 1iii,
hha, 4i, hname = “Sue”, tasks = hd, 2iii]
r30 = [hhb, 1i, “build”i, hhb, 2i, “call”i, hhb, 2i, “enthuse”i,
hhb, 3i, “call”i, hhd, 1i, “buy”i, hhd, 2i, “buy”i]

The rest of this paper gives the details of the shredding translation, explains how to stitch the results of shredded queries back
together, and shows how to use row_number to avoid the space
overhead of indexes. We will return to the above example throughout the paper, and we will use Qorg , Q and other queries based on
this example in the experimental evaluation.

4.

SHREDDING TRANSLATION

As a pre-processing step, we annotate each comprehension body
in a normalised term with a unique name a — the static component
of an index. We write the annotations as superscripts, for example:
~ where X) returna M
for (G

C ::= returna hI, N i
~ where X) C
| for (G
G ::= x ← t
N ::= X | R | I
−−−→
R ::= h` = N i
~ | empty L
X ::= x.` | c(X)
I, J ::= a  d
d ::= out | in

A comprehension is now constructed from a sequence of genera~ where X) followed by a body of the
tor clauses of the form for (G
form returna hI, N i. Each level of nesting gives rise to such a generator clause. The body always returns a pair hI, N i of an outer
index I, denoting where the result values from the shredded query
should be spliced into the final nested result, and a (flat) inner term
N . Records are restricted to contain inner terms, which are either
base types, records, or indexes, which replace nested multisets. We
assume a distinguished top level static index >, which allows us to
treat all levels uniformly. Each shredded term is associated with an
outer index out and an inner index in. (In fact out only appears in
the left component of a comprehension body, and in only appears
in the right component of a comprehension body. These properties
will become apparent when we specify the shredding transformation on terms.)

4.1

Shredding types and terms

We use paths to point to parts of types.
Paths p ::=  | ↓.p | `.p
The empty path is written . A path p can be extended by traversing
a bag constructor (↓.p) or selecting a label (`.p). We will sometimes
write p.↓ for the path p with ↓ appended at the end and similarly
for p.`; likewise, we will write p.~
` for the path p with all the labels
of ~
` appended. The function paths(A) defines the set of paths to
bag types in a type A:
paths(O) = {}
Sn
paths(h`i : Ai in
i=1 {`i .p | p ← paths(Ai )}
i=1 ) =
paths(Bag A) = {} ∪ {↓.p | p ← paths(A)}

We now define a shredding translation on types. This is defined
in terms of the inner shredding TAU, a flat type that represents the
contents of a bag.
TOU = O
n
Th`i : Ai in
i=1 U = h`i : TAi Uii=1
TBag AU = Index

Un

VLWp =

V i=1 Ci W?a,p
?
Vh`i = Mi in
i=1 Wa,`j .p
b
~
Vfor (G where X) return M W?a,
~ where X) returnb M W?
Vfor (G
a,↓.p

U

(VLW?>,p )

Tx.`Ua = x.`
n
Tc([Xi ]n
i=1 )Ua = c([TXi Ua ]i=1 )
Tempty LUa = empty VLW

= concat([VCi W?a,p ]n
i=1 )
= VMj W?a,p
~ where X) returnb ha  out, TM U i]
= [for (G
b
~ where X) C | C ← VM W? ]
= [for (G

n
Th`i = Mi in
i=1 Ua = h`i = TMi Ua ii=1
TLUa = a  in

b,p

Figure 4: Shredding translation on terms
Given a path p ∈ paths(A), the type VAWp is the outer shredding
of A at p. It corresponds to the bag at path p in A.
VBag AW = Bag hIndex , TAUi
VBag AW↓.p = VAWp
−−→
Vh` : AiW`i .p = VAi Wp

For example, consider the result type Result from Section 3. Its
nesting degree is 3, and its paths are:
paths(Result) = {, ↓.people., ↓.people.↓.tasks.}
We can shred Result in three ways using these three paths, yielding
three shredded types:
A1 = VResultW
A2 = VResultW↓.people.
A3 = VResultW↓.people..↓.tasks.

or equivalently:
A1 = Bag hIndex , hdepartment : String, people : Index ii
A2 = Bag hIndex , hname : String, tasks : Index ii
A3 = Bag hIndex , Stringi

The shredding translation on terms VLWp is given in Figure 4.
This takes a term L and a path p and gives a query VLWp that computes a result of type VAWp , where A is the type of L. The auxiliary translation VM W?a,p returns the shredded comprehensions of
M along path p with outer static index a. The auxiliary translation
TM Ua produces a flat representation of M with inner static index
a. Note that the shredding translation is linear in time and space.
Observe that for emptiness tests we need only the top-level query.
Continuing the example, we can shred Qcomp in three ways,
yielding shredded queries:
q1 = VQcomp W
q2 = VQcomp W↓.people.
q3 = VQcomp W↓.people..↓.tasks.
or equivalently:
q1 = for (x ← departments)
returna h>  1, hdepartment = x.name, people = a  inii
q2 = (for (x ← departments)
for (y ← employees) where (x.name = y.dept ∧
(y.salary < 1000 ∨ y.salary > 1000000))
returnb (ha  out, hname = y.name, tasks = b  inii))
] (for (x ← departments)
for (y ← contacts) where (x.name = y.dept ∧ y.client)
returnd (ha  out, hname = y.name, tasks = d  inii))
q3 = (for (x ← departments)
for (y ← employees) where (x.name = y.dept ∧
(y.salary < 1000 ∨ y.salary > 1000000))
for (z ← tasks) where (z.employee = y.employee)
returnc hb  out, z.taski)
] (for (x ← departments)
for (y ← contacts) where (x.name = y.dept ∧ y.client)
returne hd  out, “buy”i)

As a sanity check, we show that well-formed normalised terms
shred to well-formed shredded terms of the appropriate shredded
types. We discuss other correctness properties of the shredding
translation in Section 5. Typing rules for shredded terms are shown
in Appendix B.
T HEOREM 2. Suppose L is a normalised flat-nested query with
` L : A and p ∈ paths(A), then ` VLWp : VAWp .

4.2

Shredded packages

To maintain the relationship between shredded terms and the
structure of the nested result they are meant to construct, we use
shredded packages. A shredded package Â is a nested type with
annotations, denoted (−)α , attached to each bag constructor.
−−→
Â ::= O | h` : Âi | (Bag Â)α
For a given package, the annotations are drawn from the same
set. We write Â(S) to denote a shredded package with annotations drawn from the set S. We sometimes omit the type parameter
when it is clear from context. for shredded packages are shown in
Appendix B.
Given a shredded package Â, we can erase its annotations to
obtain its underlying type.
erase(O) = O
n
erase(h`i : Âi in
i=1 ) = h`i : erase(Âi )ii=1
erase((Bag Â)α ) = Bag (erase(Â))

Given a type A and a shredding function f : paths(A) → S, we
can construct a shredded package Â(S).
package f (A) = package f, (A)
package f,p (O) = O
n
package f,p (h`i : Ai in
i=1 ) = h`i : package f,p.`i (Ai )ii=1
package f,p (Bag A) = (Bag (package f,p.↓ (A)))f (p)

Using package, we lift the type- and term-level shredding functions V−W− to produce shredded packages, where each annotation
contains the shredded version of the input type or query along the
path to the associated bag constructor.
shred B (A) = package (VBW ) (A)
−
shred L (A) = package (VLW ) (A)
−

For example, the shredded package for the Result type from
Section 3 is:
Shred Result (Result) =
Bag hdepartment : String,
people : Bag hname : String,
tasks : (Bag String)A3 iA2 iA1

where A1 , A2 , and A3 are as shown in Section 4.1. Shredding
the normalised query Q0 gives the same package, except the type
annotations A1 , A2 , A3 become queries q1 , q2 , q3 .
Again, as a sanity check we show that erasure is the left inverse
of type shredding and that term-level shredding operations preserve
types.

T HEOREM 3. For any type A, we have erase(shred A (A)) =
A. Furthermore, if L is a closed, normalised, flat–nested query
such that ` L : A then ` shred L (A) : shred A (A).

5.

5.2

A shredded value package can be stitched back together into a
nested value, preserving annotations, as follows:
stitch(Â) = stitch >  1 (Â)

QUERY EVALUATION AND STITCHING

Having shredded a normalised nested query, we can then run
all of the resulting shredded queries separately. If we stitch the
shredded results together to form a nested result, then we obtain the
same nested result as we would obtain by running the nested query
directly. In this section we describe how to run shredded queries
and stitch their results back together to form a nested result.

5.1

Evaluating shredded queries

The semantics of shredded queries SJ−K is given in Figure 5.
Apart from the handling of indexes, it is much like the semantics
for nested queries given in Figure 2. To allow different implementations of indexes, we first define a canonical notion of index, and
then parameterise the semantics by the concrete type of indexes X
and a function index : Index → X mapping each canonical index to a distinct concrete index. A canonical index a  ι comprises
static index a and dynamic index ι, where the latter is a list of positive natural numbers. For now we take concrete indexes simply
to be canonical indexes, and index to be the identity function. We
consider other definitions of index in Section 6.
The current dynamic index ι is threaded through the semantics
in tandem with the environment ρ. The former encodes the position
of each of the generators in the current comprehension and allows
us to invoke index to construct a concrete index. The outer index
at dynamic index ι.i is ι; the inner index is ι.i. In order for a
comprehension to generate dynamic indexes we use the function
enum (introduced in Section 2) that takes a list of elements and
returns the same list with the element number paired up with each
source element.
Running a shredded query yields a list of pairs of indexes and
shredded values.
Results
s ::= [hI1 , w1 i, . . . , hIm , wm i]
Flat values w ::= c | h`1 = w1 , . . . , `n = wn i | I
Given a shredded package Â(S) and a function f : S → T , we
can map f over the annotations to obtain a new shredded package
Â0 (T ) such that erase(Â) = erase(Â0 ).
pmap f (O) = O
n
pmap f (h`i : Âi in
i=1 ) = h`i : pmap f (Âi )ii=1
pmap f ((Bag Â)α ) = ((Bag pmap f (Â)))f (α)

The semantics of a shredded query package is a shredded
value package containing indexed results for each shredded query.
For each type A we define HJAK = shred A (A) and for each
flat–nested, closed ` L : A we define HJLKA : HJAK as
pmap SJ−K (shred L (A)). In other words, we first construct the
shredded query package shred L (A), then apply the shredded semantics SJqK to each query q in the package.
For example, here is the shredded package that we obtain after
running the normalised query Qcomp from Section 2.2:
HJQcomp KA = Bag hdepartment : String,
people : Bag hname : String,
tasks : (Bag String)r3 ir2 ir1

where r1 , r2 , and r3 are as in Section 3 except that indexes are of
the form a  1.2.3 instead of ha, 1, 2, 3i.

Stitching shredded query results together

stitch c (O) = c
n
stitch r (h`i : Âi in
i=1 ) = h`i = stitch r.`i (Âi )ii=1
stitch I ((Bag Â)s ) = [(stitch w (Â)) | hI, wi ← s]

The flat value parameter w to the auxiliary function stitch w (−)
specifies which values to stitch along the current path.
Resuming our running example, once the results r1 : A1 , r2 :
A2 , r3 : A3 have been evaluated on the database, they are shipped
back to the host system where we can run the following code inmemory to stitch the three tables together into a single value: the
result of the original nested query. The code for this query Qstitch
follows the same idea as the query Qorg that constructs the nested
organisation from Σ.
for (x ← r1 )
return (hdepartment = x.name,
people = for (hi, yi ← r2 )
where (x.people = i))
return (hname = y.name,
tasks = for (hj, zi ← r3 )
where (y.tasks = j)
return zi)i)

We can now state our key correctness property: evaluating shredded queries and stitching the results back together yields the same
results as evaluating the original nested query directly.
T HEOREM 4. If ` L : Bag A then:
stitch(HJLKBag A ) = N JLK

P ROOF S KETCH . We omit the full proof due to space limits; it
is available in the full version of this paper. The proof introduces
several intermediate definitions. Specifically, we consider an annotated semantics for nested queries in which each collection element
is tagged with an index, and we show that this semantics is consistent with the ordinary semantics if the annotations are erased. We
then prove the correctness of shredding and stitching with respect
to the annotated semantics, and the desired result follows.

6.

INDEXING SCHEMES

So far, we have worked with canonical indexes of the form
a  1.2.3. These could be represented in SQL by using multiple columns (padding with NULLs if necessary) since for a given
query the length of the dynamic part is bounded by the number of
for-comprehensions in the query. This imposes space and running
time overhead due to constructing and maintaining the indexes. Instead, in this section we consider alternative, more compact indexing schemes.
We can define alternative indexing schemes by varying the index
parameter of the shredded semantics (see Section 5.1). Not all possible instantiations are valid. To identify those that are, we first
define a function for computing the canonical indexes of a nested
query result.
IJLK = IJLKε,1
U
n
IJ n
C
i Kρ,ι = concat([IJCi Kρ,ι ]i=1 )
i=1
n
IJh`i = Mi in
i=1 Kρ,ι = concat([IJMi Kρ,ι ]i=1 )
IJXKρ,ι = [ ]
a
IJfor ([xi ← ti ]n
i=1 where X) return M Kρ,ι =
concat([a  ι.j :: IJM Kρ[xi 7→ri ]n ,ι.j
i=1
| hj, ~
ri ← enum([~
r | [ri ← Jti K]n
i=1 , N JXKρ[xi 7→ri ]n ])])
i=1

SJLK = SJLKε,1

n
SJh` = N in
i=1 Kρ,ι = h`i = SJNi Kρ,ι ii=1
SJXKρ,ι = N JXKρ

U
n
SJ n
i=1 Ci Kρ,ι = concat([SJCi Kρ,ι ]i=1 )
SJfor ([xi ← ti ]n
where
X)
CK
=
concat([SJCKρ[xi 7→ri ]n
ρ,ι
i=1

i=1 ,ι.j

SJa  outKρ,ι.i = index (a  ι)
SJa  inKρ,ι.i = index (a  ι.i)

SJreturna N Kρ,ι = [SJN Kρ,ι ]
| hj, ~
ri ← enum([~
r | [ri ← Jti K]n
i=1 , N JXKρ[xi 7→ri ]n ])])
i=1

Figure 5: Semantics of shredded queries
An indexing function index : Index → X is valid with respect
to the closed nested query L if it is injective and defined on every canonical index in IJLK. The only requirement on indexes in
the proof of Theorem 4 is that index is valid. We consider two
alternative valid indexing schemes: natural and flat indexes.

6.1

Natural indexes

Natural indexes are synthesised from row data. In order to generate a natural index for a query every table must have a key, that is,
a collection of fields guaranteed to be unique for every row in the
table. For sets, this is always possible by using all of the field values as a key; this idea is used in Van den Bussche’s simulation for
sets [31]. However, for bags this is not always possible, so using
natural indexes may require adding extra key fields.
Given a table t, let key t be the function that given a row r of t
returns the key fields of r. We now define a function to compute
the list of natural indexes for a query L.
I \ JLK = I \ JLKε
U
\
n
I\J n
i=1 Ci Kρ = concat([I JCi Kρ ]i=1 )
\ JM K ]n )
I \ Jh`i = Mi in
K
=
concat([I
ρ
ρ
i
i=1
i=1
I \ JXKρ = [ ]

a
I \ Jfor ([xi ← ti ]n
i=1 where X) return M Kρ =
\ JM K
concat([a  hkey ti (ri )in
::
I
ρ[xi 7→ri ]n
i=1
i=1
| [ri ← Jti K]n
i=1 , N JXKρ[xi 7→ri ]n ])
i=1

If a  ι is the i-th element of IJLK, then index \L (a  ι) is defined as
the i-th element of I \ JLK. The natural indexing scheme is defined
by setting index = index \L .
An advantage of natural indexes is that they can be implemented
in plain SQL, so for a given comprehension all where clauses can
be amalgamated (using the ∧ operator) and no auxiliary subqueries
are needed. The downside is that the type of a dynamic index
may still vary across the component comprehensions of a shredded query, complicating implementation of the query (due to the
need to pad some subqueries with null columns) and potentially
decreasing performance due to increased data movement. We now
consider an alternative, in which row_number is used to generate
dynamic indexes.

6.2

Flat indexes and let-insertion

The idea of flat indexes is to enumerate all of the canonical dynamic indexes associated with each static index and use the enumeration as the dynamic index.
Let ι be the i-th element of the list [ι0 | a  ι0 ← IJLK], then
index [L (a  ι) = ha, ii. The flat indexing scheme is defined by
setting index = index [L . Let I [ JLK = [index [L (I) | I ← IJLK]
and let S [ JLK be SJLK where index = index [L .
In this section, we give a translation called let-insertion that uses
let-binding and an index primitive to manage flat indexes. In the
next section, we take the final step from this language to SQL.
Our semantics for shredded queries uses canonical indexes. We
now specify a target language providing flat indexes. In order to do
so, we introduce let-bound sub-queries, and translate each compre-

hension into the following form:
−−→
let q = for (Gout where Xout ) return Nout in
−→
for (Gin where Xin ) return Nin
The special index expression is available in each loop body, and is
bound to the current index value.
Following let-insertion, the types are as before, except indexes
are represented as pairs of integers ha, di where a is the static component and d is the dynamic component.
Types
A, B ::= Bag hhInt, Inti, F i
−−→
Flat types
F ::= O | h` : F i | hInt, Inti
The syntax of terms is adapted as follows:
U ~
Query terms
L, M ::= C
Comprehensions
Subqueries
Data sources
Generators
Inner terms
Record terms
Base terms

C ::= let q = S in S 0
~ where X) return N
S ::= for (G
u ::= t | q
G ::= x ← u
N ::= X | R | index
−−−→
R ::= h` = N i
~ | empty L
X ::= x.~
` | c(X)

The semantics of let-inserted queries is given in Figure 6. Rather
than maintaining a canonical index, it generates a flat index for each
subquery.
We first give the translation on shredded types as follows:
L(O) = O
−−−−−→
−−→
L(h` : F i) = h` : L(F )i
L(Index ) = hInt, Inti
L(Bag hIndex , F i) = Bag hhInt, Inti, L(F )i

For example:
L(A2 ) = Bag hhInt, Inti, hname : String, tasks : hInt, Intiii
Without loss of generality we rename all the bound variables in
our source query to ensure that all bound variables have distinct
names, and that none coincides with the distinguished name z used
for let-bindings. The let-insertion translation L is defined in Figure 7, where we use the following auxiliary functions:
expand(x, t) = h`i = x.`i in
i=1
−−→
where Σ(t) = Bag h` : Ai
~ where X) C) = G
~ :: gens C
gens (for (G
gens (returna N ) = [ ]
~ where X) C) = X :: conds C
conds (for (G
conds (returna N ) = [ ]
~ where X) C) = body C
body (for (G
body (returna N ) = N

Each comprehension is rearranged into two sub-queries. The first
generates the outer indexes. The second computes the results. The
translation sometimes produces n-ary projections in order to refer
to values bound by the first subquery inside the second.

LJLK = LJLKε
U
m
LJ m
j=1 Cj Kρ = concat([LJCj Kρ ]j=1 )

m
LJh`j = Nj im
j=1 Kρ,i = h`j = LJNj Kρ,i ij=1
LJXKρ,i = N JXKρ

LJtKρ = JtK
LJqKρ = ρ(q)

LJindexKρ,i = i

LJlet q = Sout in Sin Kρ = LJSin Kρ[q7→LJSout Kρ ]
LJfor ([xj ← uj ]m
ri ← enum([~
r | [rj ← LJuj Kρ ]m
j=1 where X) return N Kρ = [LJN Kρ[xj 7→rj ]m ,i | hi, ~
j=1 , N JXKρ[xj 7→rj ]m ])]
j=1

j=1

Figure 6: Semantics of let-inserted shredded queries
U
Un
L( n
i=1 Ci ) =
i=1 L(Ci )
−−→
−→
L(C) = let q = (for (Gout where Xout ) return hRout , indexi) in for (z ← q, Gin where Ly~ (Xin )) return Ly~ (N )
−−→
−→
−−−→ −−→
N = body C
where Gout = concat
(init (gens C))
y = t = Gout
Gin = last (gens C)
V
−−→
Xout = init (conds C)
Rout = hexpand(yi , ti )in
X
n = length Gout
in = last (conds C)
i=1

Ly~ (empty
L) = empty
(Ly~ (L))
U
U
x.`,
if x ∈
/ {y1 , . . . , yn }
Ly~ ( n
Ci ) = n
Ly~ (Ci )
Ly~ (x.`) =
i=1
i=1
z.1.i.`, if x = yi
~ where X) returna ha, N i) = for (G
~ where Ly~ (X))
Ly~ (for (G
Ly~ (c(X1 , . . . , Xm )) = c(Ly~ (X1 ), . . . , Ly~ (Xm ))
return ha, Ly~ (N )i
m
Ly~ (h`j = Xj im
~ (Xj )ij=1
j=1 ) = h`j = Ly
Ly~ (a  d) = ha, L(d)i

L(out) = z.2
L(in) = index

Figure 7: The let-insertion translation
For example, applying L to q1 from Section 4.2 yields:
for (x ← departments)
return hh>, 1i, hdept = x.name, people = indexii

and q2 becomes:
(let q = for (x ← departments) return hhdept = x.namei, indexi in
for (z ← q, y ← employees) where (z.1.1.name = y.dept ∧
(y.salary < 1000 ∨ y.salary > 1000000))
return (hha, z.2i, hname = y.name, tasks = hb, indexiii))
]
(let q = for (x ← departments) return hhdept = x.namei, indexi in
for (z ← q, y ← contacts) where (z.1.1.name = y.dept ∧ y.client)
return (hha, z.2i, hname = y.name, tasks = hd, indexiii))

As a sanity check, we show that the translation is type-preserving:
T HEOREM 5. Given shredded query ` M : Bag hIndex , F i,
then ` L(M ) : L(Bag hIndex , F i).
To prove the correctness of let-insertion, we need to show that
the shredded semantics and let-inserted semantics agree. In the
statement of the correctness theorem, recall that S [ JLK refers to
the version of SJLK using index = index [L .
T HEOREM 6. Suppose ` L : A and VLWp = M . Then
S [ JM K = LJL(M )K.
P ROOF SKETCH . The high-level idea is to separate results into
data and indexes and compare each separately. It is straightforward,
albeit tedious, to show that the different definitions are equal if we
replace all dynamic indexes by a dummy value. It then remains
to show that the dynamic indexes agree. The pertinent case is the
translation of a comprehension:
b
~ i ← Xi )]n
~
[for (G
i=1 for (Gin ← Xin ) return ha  out, N i

which becomes let q = Sout in Sin for suitable Sout and Sin . The
dynamic indexes computed by Sout coincide exactly with those of
I [ JLK at static index a, and the dynamic indexes computed by Sin ,
if there are any, coincide exactly with those of I [ JLK.

7.

CONVERSION TO SQL

Earlier translation stages have employed nested records for convenience, but SQL does not support nested records. At this stage,

we eliminate nested records from queries. For example, we can represent a nested record ha = hb = 1, c = 2i, d = 3i as a flat record
ha b = 1, a c = 2, d = 3i. The (standard) details are presented in
Appendix E.
In order to interpret shredded, flattened, let-inserted terms as
SQL, we interpret index generators using SQL’s OLAP facilities.
~
Query terms
L ::= (union all) C
Comprehensions C ::= with q as (S) C | S 0
~ where X
Subqueries
S ::= select R from G
Data sources
u ::= t | q
Generators
G ::= u as x
~
Inner terms
N ::= X | row_number() over (order by X)
−−−→
Record terms
R ::= N as `
~ | empty L
Base terms
X ::= x.` | c(X)
Continuing our example, L(q1 ) and L(q2 ) translate to q10 and q20
where:
q10 = select x.name as i1_name,
row_number() over (order by x.name) as i1_people
from departments as x
0
q2 = (with q as (select x.name as i1_name,
row_number() over (order by x.name) as i2
from departments as x)
select a as i1_1, z.i2 as i1_2, y.name as i2_name, b as i2_tasks_1,
row_number() over (order by z.i1_name, z.i2,
y.dept, y.employee, y.salary) as i2_tasks_2
from employees as y, q as z
where (z.i1_name = y.dept ∧
(y.salary < 1000 ∨ y.salary > 1000000)))
union all
(with q as (select x.name as i1_name,
row_number() over (order by x.name) as i2
from departments as x)
select a as i1_1, z.i2 as i1_2, y.name as i2_name, d as i2_tasks_1,
row_number() over (order by z.i1_name, z.i2,
y.dept, y.name, y.client) as i2_tasks_2
from contacts as y, q as z
where (z.i1_name = y.dept ∧ y.client))

Modulo record flattening, the above fragment of SQL is almost
isomorphic to the image of the let-insertion translation. The only
significant difference is the use of row_number in place of index.
Each instance of index in the body R of a subquery of the form

QF1: SELECT e.emp FROM employees e
WHERE e.salary > 10000
QF2: SELECT e.emp, t.tsk
FROM employees e, tasks t
WHERE e.emp = t.emp
QF3: SELECT e1.emp, e2.emp
FROM employees e1, employees e2
WHERE e1.dpt = e2.dpt
AND e1.salary = e2.salary
AND e1.emp <> e2.emp
QF4: (SELECT t.emp FROM tasks t
WHERE t.tsk = ’abstract’)
UNION ALL (SELECT e.emp FROM employees
WHERE e.salary > 50000)
QF5: (SELECT t.emp FROM tasks t
WHERE t.tsk = ’abstract’)
MINUS
(SELECT e.emp FROM employees e
WHERE e.salary > 50000)
QF6: ((SELECT t.emp FROM tasks t
WHERE t.tsk = ’abstract’)
UNION ALL (SELECT e.emp FROM employees e
WHERE e.salary > 50000))
MINUS
((SELECT t.emp FROM tasks t
WHERE t.tsk = ’enthuse’)
UNION ALL (SELECT e.emp FROM employees e
WHERE e.salary > 10000))

Figure 8: SQL versions of flat queries used in experiments
−−−→
for (x ← t where X) return R is simulated by a term of the form
−
→
row_number() over (order by x.`), where:
xi : h`i,1 : Ai,1 , . . . , `i,mi : Ai,mi i
−
→
x.` = x1 .`1,1 , . . . , x1 .`1,m1 , . . . , xn .`n,1 , . . . , xn .`n,mn

A possible concern is that row_number is non-deterministic. It
computes row numbers ordered by the supplied columns, but if
there is a tie, then it is free to order the equivalent rows in any
order. However, we always order by all columns of all tables referenced from the current subquery, so our use of row_number is
always deterministic. (An alternative could be to use nonstandard
features such as PostgreSQL’s OID or MySQL’s ROWNUM, but
sorting would still be necessary to ensure consistency across inner
and outer queries.)

8.

EXPERIMENTAL EVALUATION

Ferry’s loop-lifting translation has been implemented in Links
previously by Ulrich, a member of the Ferry team [30], following
the approach described by Grust et al. [12] to generate SQL:1999
algebra plans, then calling Pathfinder [14] to optimise and evaluating the resulting SQL on a PostgreSQL database. We have also implemented query shredding in Links, running against PostgreSQL;
our implementation1 does not use Pathfinder. We performed initial experiments with a larger ad hoc query benchmark, and developed some optimisations, including inlining certain WITH clauses
to unblock rewrites, using keys for row numbering, and implementing stitching in one pass to avoid construction of intermediate inmemory data structures that are only used once and then discarded.
We report on shredding with all of these optimisations enabled.

Benchmark queries. There is no standard benchmark for
queries returning nested results. In particular, the popular TPC1

http://github.com/slindley/links/tree/shredding

Q1 : for (d ← departments)
return (hname = d.name,
employees = employeesOfDept d,
contacts = contactsOfDept di
Q2 : for (d ← Q1)
where (all d.employees (λx.contains x.tasks “abstract”))
return hdept = d.depti
Q3 : for (e ← employees)
return hname = e.name, task = tasksOfEmp(e)i
Q4 : for (d ← departments)
return hdept = d.dept, employees = for (e ← employees)
where (d.dept = e.dept)
return e.employeei
Q5 : for (t ← tasks) return ha = t.task, b = employeesByTask ti
Q6 : for (d ← Q1)
return (hdepartment = d.name,
people =
getTasks(outliers(d.employees)) (λy. y.tasks)
] getTasks(clients(d.contacts)) (λy. return “buy”)i)

Figure 9: Nested queries used in experiments

H benchmark is not suitable for comparing shredding and looplifting: the TPC-H queries do not return nested results, and can be
run directly on any SQL-compliant RDBMS, so neither approach
needs to do any work to produce an SQL query.
We selected twelve queries over the organisation schema described in Section 3 to use as a benchmark. The first six queries,
named QF1–QF6, return flat results and can be translated to SQL
using existing techniques, without requiring either shredding or
loop-lifting. We considered these queries as a sanity check and
in order to measure the overhead introduced by loop-lifting and
shredding. Figure 8 shows the SQL versions of these queries.
We also selected six queries Q1–Q6 that do involve nesting, either within query results or in intermediate stages. They are shown
in Figure 9; they use the auxiliary functions defined in Section 3.
Q1 is the query Qorg that builds the nested organisation view from
Section 3. Q2 is a flat query that computes a flat result from Q1 consisting of all departments in which all employees can do the “abstract” task; it is a typical example of a query that employs higherorder functions. Q3 returns records containing each employee and
the list of tasks they can perform. Q4 returns records containing
departments and the set of employees in each department. Q5 returns a record of tasks paired up with sets of employees and their
departments. Q6 is the outliers query Q introduced in Section 3.

Experimental results. We measured the query execution time
for all queries on randomly generated data, where we vary the number of departments in the organisation from 4 to 4096 (by powers of
2). Each department has on average 100 employees and each employee has 0–2 tasks, and the largest (4096 department) database
was approximately 500MB. Although the test datasets are moderate in size, they suffice to illustrate the asymptotic trends in the
comparative performance of the different techniques. All tests were
performed using PostgreSQL 9.2 running on a MacBook Pro with
4-core 2.6GHz CPU, 8GB RAM and 500GB SSD storage, with
the database server running on the same machine (hence, negligible network latency). We measure total time to translate a nested
query to SQL, evaluate the resulting SQL queries, and stitch the
results together to form a nested value, measured from Links.
We evaluated each query using query shredding and loop-lifting,
and for the flat queries we also measured the time for Links’ default

37.5
4

8

16

32

64

128

#departments

0

QF1

1E+00

4

16

64

256 1024 4096

1E+03
1E+02
1E+01
1E+00

4

16

64

256 1024 4096

1E+02
1E+01
1E+00

4

16

64

4

16

64

256 1024 4096

#departments

1E+03

1E+05
1E+04
1E+03
1E+02
1E+01
1E+00

1E+01
1E+00

4

16

64

loop-lifting implementation for Links) supports grouping and aggregation features that are not handled by our translation. We focused on queries that both systems can handle, but Ferry has a clear
advantage for grouping and aggregation queries or when ordering
is important (e.g. sorting or top-k queries). Ferry is based on list semantics, while our approach handles multiset semantics. So, some
performance differences may be due to our exploitation of multisetbased optimisations that Ferry (by design) does not exploit.
The results for flat queries show that shredding has low per-query
overhead in most cases compared to Links’ default flat query evaluation, but the queries it generates are slightly slower. Loop-lifting,
on the other hand, has a noticeable per-query overhead, likely due
to its invocation of Pathfinder and associated serialisation costs. In
some cases, such as QF4 and QF5, loop-lifting is noticeably slower
asymptotically; this appears to be due to additional sorting needed
to maintain list semantics. We encountered a bug that prevented
loop-lifting from running on query QF6; however, shredding had
negligible overhead for this query. In any case, the overhead of either shredding or loop-lifting for flat queries is irrelevant: we can
simply evaluate such queries using Links’ default flat query evaluator. Nevertheless, these results show that the overhead of shredding
for such queries is not large, suggesting that the queries it generates
are similar to those currently generated by Links. (Manual inspection of the generated queries confirms this.)
The results for nested queries are more mixed. In most cases,
the overhead of loop-lifting is dominant on small data sizes, which
again suggests that shredding may be preferable for OLTP or Web
workloads involving rapid, small queries. Loop-lifting scales poorly

0

256

0

4

shredding
loop-lifting
16

64

256 1024 4096

1E+02
1E+01
1E+00

4

16

64

Q4

1E+03

1E+03

1E+02

shredding
loop-lifting
4

16

64

1E+05
1E+04
1E+03
1E+02
1E+01
1E+00

256 1024 4096

shredding
loop-lifting

1E+02
1E+01
1E+00

4

16

64

16

64

Q6

256 1024 4096

#departments

256 1024 4096

#departments

shredding
loop-lifting

4

256 1024 4096

#departments
1E+04

1E+01

16

Q2
1E+03

4

8

shredding
loop-lifting

1E+04

Q5

256 1024 4096

Discussion. We should re-emphasise that Ferry (and Ulrich’s

128

#departments

#departments

QF1: SELECT e.emp FROM employees e WHERE e.salary > 10000
Experimental
results (flat
QF2:Figure
SELECT10:
e.emp,
t.tsk FROM employees
e, queries)
tasks t
WHERE e.emp = t.emp
QF3: SELECT e1.emp, e2.emp FROM employees e1, employees e2
WHERE e1.dpt = e2.dpt AND e1.salary = e2.salary
(flat) query evaluation.
experimental results for the flat queries
AND e1.emp The
<> e2.emp
QF4: (SELECT
t.emp
tasks
WHERE t.tsk
= ‘abstract’)
are shown
in Figure
10 FROM
and for
thet nested
queries
in Figure 11.
UNIONaxes
(SELECT
e.emp FROM employees
Note that both
are logarithmic.
All times are in milliseconds;
WHERE e.salary > 50000)
the times
are medians of 5 runs. The times for small data sizes
QF5: (SELECT t.emp FROM tasks t WHERE t.tsk = ‘abstract’)
provide a comparison
ofe.emp
the overhead
associated
with shredding,
MINUS (SELECT
FROM employees
e
WHERE
e.salary
> 50000)
loop-lifting or Links’
default
query
normalisation algorithm.

64

1E+04

1E+00

256 1024 4096

1E+02

32

Q3

msec

msec

msec

1E+00

16

#departments

shredding
loop-lifting
default

1E+04

1E+01

8

QF6

QF5

1E+02

4

#departments

shredding
loop-lifting
default

1E+03

256 1024 4096

msec

msec

1E+03

#departments

1E+04

256
0

Q1

shredding
loop-lifting
default

1E+04
msec

64

128
0

QF4

QF3

16

64

#departments

shredding
loop-lifting
default

4

32

QF2

#departments

1E+05
1E+04
1E+03
1E+02
1E+01
1E+00

16

msec

1E+01

8

shredding
loop-lifting
default

1E+04
msec

msec

1E+02

4

#departments

shredding
loop-lifting
default

1E+03

7500

200

msec

0

0

msec

0

msec

37.5

1E+05
1E+04
1E+03
1E+02
1E+01
1E+00

shredding
loop-lifting
4

16

64

256 1024 4096

#departments

Figure 11: Experimental results (nested queries)
on two queries (Q1 and Q6), and did not finish within 1 minute even
for small data sizes. Both Q1 and Q6 involve 3 levels of nesting and
in the innermost query, loop-lifting generates queries with Cartesian products inside OLAP operators such as DENSE_RANK or
ROW_NUMBER that Pathfinder was not able to remove. The queries
generated by shredding in these cases avoid this pathological behaviour. For other queries, such as Q2 and Q4, loop-lifting performs better but is still slower than shredding as data size increases.
Comparison of the queries generated by loop-lifting and shredding
reveals that loop-lifting encountered similar problems with hardto-optimise OLAP operations. Finally, for Q3 and Q5, shredding
is initially faster (due to the overhead of loop-lifting and calling
Pathfinder) but as data size increases, loop-lifting wins out. Inspection of these generated queries reveals that the queries themselves
are similar, but the shredded queries involve more data movement.
Also, loop-lifting returns sorted results, so it avoids in-memory
hashing or sorting while constructing the nested result. It should
be possible to incorporate similar optimisations into shredding to
obtain comparable performance.
Our experiments show that shredding performs similarly or better than loop-lifting on our (synthetic) benchmark queries on moderate (up to 500MB) databases. Further work may need to be done
to investigate scalability to larger databases or consider more realistic query benchmarks.

9.

RELATED AND FUTURE WORK

We have discussed related work on nested queries, Links, Ferry
and LINQ in the introduction. Besides Cooper [7], several authors
have recently considered higher-order query languages. Benedikt
et al. [2, 32] study higher-order queries over flat relations. The
Links approach was adapted to LINQ in F# by Cheney et al. [6].
Higher-order features are also being added to XQuery 3.0 [25].
Research on shredding XML data into relations and evaluating
XML queries over such representations [18] is superficially similar to our work in using various indexing or numbering schemes
to handle nested data. Grust et al.’s work on translating XQuery

32

64

128

to SQL via Pathfinder [14] is a mature solution to this problem,
and Grust et al. [13] discuss optimisations in the presence of unordered data processing in XQuery. However, XQuery’s ordered
data model and treatment of node identity would block transformations in our algorithm that assume unordered, pure operations.
We can now give a more detailed comparison of our approach
with the indexing strategies in Van den Bussche’s work and in
Ferry. Van den Bussche’s approach uses natural indexes (that is,
n-tuples of ids), but does not preserve multiset semantics. Our approach preserves multiplicity and can use natural indexes, we also
propose a flat indexing scheme based on row_number. In Ferry’s
indexing scheme, the surrogate indexes only link adjacent nesting
levels, whereas our indexes take information at all higher levels
into account. Our flat indexing scheme relies on this property,
and Ferry’s approach does not seem to be an instance of ours (or
vice versa). Ferry can generate multiple SQL:1999 operations and
Pathfinder tries to merge them but cannot always do so. Our approach generates row_number operations only at the end, and does
not rely on Pathfinder. Finally, our approach uses normalisation
and tags parts of the query to disambiguate branches of unions.
Loop-lifting has been implemented in Links by Ulrich [30], and
Grust and Ulrich [16] recently presented techniques for supporting higher-order functions as query results. By using Ferry’s looplifting translation and Pathfinder, Ulrich’s system also supports list
semantics and aggregation and grouping operations; to our knowledge, it is an open problem to either prove their correctness or adapt
these techniques to fit our approach. Ferry’s approach supports
a list-based semantics for queries, while we assume a bag-based
semantics (matching SQL’s default behaviour). Either approach
can accommodate set-based semantics simply by eliminating duplicates in the final result. In fact, however, we believe the core
query shredding translation (Sections 4–6) works just as well for a
list semantics. The only parts that rely on unordered semantics are
normalisation (Section 2.2) and conversion to SQL (Section 7). We
leave these extensions to future work.
Our work is also partly inspired by work on unnesting for nested
data parallelism. Blelloch and Sabot [3] give a compilation scheme
for NESL, a data-parallel language with nested lists; Suciu and Tannen [27] give an alternative scheme for a nested list calculus. This
work may provide an alternative (and parallelisable) implementation strategy for Ferry’s list-based semantics [12].

10.

CONCLUSION

Combining efficient database access with high-level programming abstractions is challenging in part because of the limitations
of flat database queries. Currently, programmers must write flat
queries and manually convert the results to a nested form. This
damages declarativity and maintainability. Query shredding can
help to bridge this gap. Although it is known from prior work that
query shredding is possible in principle, and some implementations
(such as Ferry) support this, getting the details right is tricky, and
can lead to queries that are not optimised well by the relational engine. Our contribution is an alternative shredding translation that
handles queries over bags and delays use of OLAP operations until
the final stage. Our translation compares favourably to loop-lifting
in performance, and should be straightforward to extend and to incorporate into other language-integrated query systems.

Acknowledgements. We thank Ezra Cooper, Torsten Grust, and
Jan Van den Bussche for comments. We are very grateful to Alex
Ulrich for sharing his implementation of Ferry in Links and for extensive discussions. This work was supported by EPSRC grants
EP/J014591/1 and EP/K034413/1 and a Google Research Award.

11.

REFERENCES

[1] A. Beckmann. Exact bounds for lengths of reductions in typed
λ-calculus. Journal of Symbolic Logic, 66:1277–1285, 2001.
[2] M. Benedikt, G. Puppis, and H. Vu. Positive higher-order queries. In
PODS, pages 27–38, 2010.
[3] G. E. Blelloch and G. W. Sabot. Compiling collection-oriented
languages onto massively parallel computers. J. Parallel Distrib.
Comput., 8:119–134, February 1990.
[4] P. Buneman, L. Libkin, D. Suciu, V. Tannen, and L. Wong.
Comprehension syntax. SIGMOD Record, 23, 1994.
[5] P. Buneman, S. A. Naqvi, V. Tannen, and L. Wong. Principles of
programming with complex objects and collection types. Theor.
Comput. Sci., 149(1):3–48, 1995.
[6] J. Cheney, S. Lindley, and P. Wadler. A practical theory of
language-integrated query. In ICFP, pages 403–416. ACM, 2013.
[7] E. Cooper. The script-writer’s dream: How to write great SQL in
your own language, and be sure it will succeed. In DBPL, pages
36–51, 2009.
[8] E. Cooper, S. Lindley, P. Wadler, and J. Yallop. Links: web
programming without tiers. In FMCO, volume 4709 of LNCS, 2007.
[9] P. de Groote. On the strong normalisation of intuitionistic natural
deduction with permutation-conversions. Inf. Comput.,
178(2):441–464, 2002.
[10] L. Fegaras and D. Maier. Optimizing object queries using an effective
calculus. ACM Trans. Database Syst., 25:457–516, December 2000.
[11] T. Grust, M. Mayr, J. Rittinger, and T. Schreiber. Ferry:
Database-supported program execution. In SIGMOD, June 2009.
[12] T. Grust, J. Rittinger, and T. Schreiber. Avalanche-safe LINQ
compilation. PVLDB, 3(1), 2010.
[13] T. Grust, J. Rittinger, and J. Teubner. eXrQuy: Order indifference in
XQuery. In ICDE, pages 226–235, 2007.
[14] T. Grust, J. Rittinger, and J. Teubner. Pathfinder: XQuery off the
relational shelf. IEEE Data Eng. Bull., 31(4):7–14, 2008.
[15] T. Grust, S. Sakr, and J. Teubner. XQuery on SQL hosts. In VLDB,
pages 252–263, 2004.
[16] T. Grust and A. Ulrich. First-class functions for first-order database
engines. In DBPL, 2013.
[17] W. Kim. On optimizing an SQL-like nested query. ACM Trans.
Database Syst., 7(3):443–469, Sept. 1982.
[18] R. Krishnamurthy, R. Kaushik, and J. F. Naughton. XML-SQL query
translation literature: The state of the art and open problems. In
Xsym, pages 1–18, 2003.
[19] S. Lindley. Extensional rewriting with sums. In TLCA, 2007.
[20] S. Lindley and J. Cheney. Row-based effect types for database
integration. In TLDI, 2012.
[21] S. Lindley and I. Stark. Reducibility and >>-lifting for computation
types. In TLCA, 2005.
[22] E. Meijer, B. Beckman, and G. M. Bierman. LINQ: reconciling
object, relations and XML in the .NET framework. In SIGMOD,
2006.
[23] C. Olston, B. Reed, U. Srivastava, R. Kumar, and A. Tomkins. Pig
latin: a not-so-foreign language for data processing. In SIGMOD,
pages 1099–1110, 2008.
[24] B. Pierce. Types and Programming Languages. MIT Press, 2002.
[25] J. Robie, D. Chamberlin, M. Dyck, and J. Snelson. XQuery 3.0: An
XML query language. W3C Proposed Recommendation, October
2013. http://www.w3.org/TR/xquery-30/.
[26] H. J. Schek and M. H. Scholl. The relational model with
relation-valued attributes. Inf. Syst., 11:137–147, April 1986.
[27] D. Suciu and V. Tannen. Efficient compilation of high-level data
parallel algorithms. In SPAA, pages 57–66. ACM, 1994.
[28] D. Syme, A. Granicz, and A. Cisternino. Expert F# 3.0. Apress,
2012.
[29] W. W. Tait. Intensional interpretations of functionals of finite type I.
Journal of Symbolic Logic, 32(2):198–212, June 1967.
[30] A. Ulrich. A Ferry-based query backend for the Links programming
language. Master’s thesis, University of Tübingen, 2011. Code
supplement:
http://github.com/slindley/links/tree/sand.
[31] J. Van den Bussche. Simulation of the nested relational algebra by

[32]
[33]
[34]

[35]

the flat relational algebra, with an application to the complexity of
evaluating powerset algebra expressions. Theor. Comput. Sci.,
254(1-2), 2001.
H. Vu and M. Benedikt. Complexity of higher-order queries. In
ICDT, pages 208–219. ACM, 2011.
P. Wadler. Comprehending monads. Math. Struct. in Comp. Sci.,
2(4), 1992.
L. Wong. Normal forms and conservative extension properties for
query languages over collection types. J. Comput. Syst. Sci., 52(3),
1996.
L. Wong. Kleisli, a functional query system. J. Funct. Programming,
10(1), 2000.

APPENDIX
A.

BEHAVIOUR OF VAN DEN BUSSCHE’S
SIMULATION ON MULTISETS

As noted in the Introduction, Van den Bussche’s simulation of
nested queries via flat queries does not work properly over multisets. To illustrate the problem, consider a simple query R ∪ S,
where R and S have the same schema Bag hA : Int, B : Bag Inti.
Suppose R and S have the following values:
A
R= 1
2

B
{1}
{2}

A
S= 1
2

B
{3, 4}
{2}

then their multiset union is:
A
B
1
{1}
R ∪ S = 1 {3, 4}
2
{2}
2
{2}
Van den Bussche’s simulation (like ours) represents these nested
values by queries over flat tables, such as the following:
A
R1 = 1
2

id
a
b

id
R2 = a
b

B
1
2

A
S1 = 1
2

id
a
b

id
a
S2 =
a
b

B
3
4
2

where a, b are arbitrary distinct ids. Note however that R and S
have overlapping ids, so if we simply take the union of R1 and S1 ,
and of R2 and S2 respectively, we will get:
A
1
Wrong 1 = 2
1
2

id
a
b
a
b

id
a
b
Wrong 2 =
a
a
b

B
1
2
3
4
2

corresponding to nested value:
A
B
1 {1, 3, 4}
Wrong = 1 {1, 3, 4}
2
{2, 2}
2
{2, 2}
Instead, both Van den Bussche’s simulation and our approach avoid
clashes among ids when taking unions. Van den Bussche’s simulation does this by adding two new id fields to represent the result of
a union, say id1 and id2 . The tuples originating from R will have
equal id1 and id2 values, while those originating from S will have
different id1 and id2 values. In order to do this, the simulation defines two queries, one for each result table. The first query is of the
form:
T1

=

(R1 × (id1 : x, id2 : x) | x ∈ adom)

∪

(S1 × (id1 : x, id2 : x0 ) | x 6= x0 ∈ adom)

and similarly
T2

=

(R2 × (id1 : x, id2 : x) | x ∈ adom)

∪

(S2 × (id1 : x, id2 : x0 ) | x 6= x0 ∈ adom)

where adom is the active domain of the database (in this case,
adom = {1, 2, 3, 4, a, b}) — this is of course also definable as
a query. Thus, in this example, the result is of the form
A
1
T1 = 2
1
2

id
a
b
a
b

id1
x
y
z
v

id2
x
y
z0
v0

id
a
b
T1 =
a
a
b

id1
x
y
z
w
v

id2
x
y
z0
w0
v0

B
1
2
3
4
2

where x, y are any elements of adom (rows mentioning x and y
stand for 6 instances) and z 6= z 0 , w 6= w0 and v 6= v 0 are any
pairs of distinct elements of adom (rows mentioning these variables stand for 30 instances of distinct pairs from adom). This
leads to an O(|adom| ∗ |R| + |adom|2 ∗ |S|) blowup in the number of tuples. Specifically, for our example, |T1 | = 72, whereas
the actual number of tuples in a natural representation of R ∪ S is
only 9. In a set semantics, the set value simulated by these tables
is correct even with all of the extra tuples; however, for a multiset semantics, this quadratic blowup is not correct — even for our
example, with |adom| = 6, the result of evaluating R ∪ S yields
a different number of tuples from the result of evaluating S ∪ R,
and neither represents the correct multiset in an obvious way. It
may be possible (given knowledge of the query and active domain,
but not the source database) to “decode” the flat query results and
obtain the correct nested result, but doing so appears no easier than
developing an alternative, direct algorithm.

B.

TYPING RULES

The (standard) typing rules for λNRC queries are shown in Figure 12. The typing rules for shredded terms, packages, and values
are shown in Figures 13, 14, 16 and 18.

C.

QUERY NORMALISATION

Following previous work [20], we separate query normalisation
into a rewriting phase and a type-directed structurally recursive
function. Where we diverge from this previous work is that we
extend the rewrite relation to hoist all conditionals up to the nearest comprehension (in order to simplify the rest of the development), and the structurally recursive function is generalised to handle nested data. Thus normalisation can be divided into three stages.
• The first stage performs symbolic evaluation, that is, β-reduction
and commuting conversions, flattening unnecessary nesting
and eliminating higher-order functions.
• The second stage hoists all conditionals up to the nearest enclosing comprehension in order to allow them to be converted
to where clauses.
• The third and final stage hoists all unions up to the top-level,
η-expands tables and variables, and turns all conditionals into
where clauses.

If M is r-SN, then we write max r (M ) for the maximum length of
a reduction sequence starting from M .
A rewrite relation ;r is weakly-normalising, or WN, if all terms
M are weakly-normalising with respect to ;r . Similarly, a rewrite
relation ;r is strongly-normalising, or SN, if all terms M are
strongly-normalising with respect to ;r .
For any ;r we can define a partial function nf r such that nf r (M )
is a normal form of M , if one exists, otherwise nf r (M ) is undefined. Note that there may be more than one normal form for a
given M ; nf r chooses a particular normal form for each M that
has one. If ;r is weakly normalising, then nf r is a total function.
We now describe each normalisation stage in turn.

C.1

Symbolic evaluation

The β-rules perform symbolic evaluation, including substituting
argument values for function parameters, record field projection,
conditionals where the test is known to be true or false, or iteration
over singleton bags.
(λx. N ) M
−−−−→
h` = M i.`i
if true then M else N
if false then M else N
for (x ← return M ) N

M ; M1 ; . . . ; Mn 6;
A term M is strongly normalising with respect to a rewrite relation
;r , or r-SN, if every reduction sequence starting from M is finite.

N [x := M ]
Mi
M
N
N [x := M ]

Fundamentally, β-rules always follow the same pattern. Each is
associated with a particular type constructor T , and the left-hand
side always consists of an introduction form for T inside an elimination form for T . For instance, in the case of functions (the first
β-rule above), the introduction form is a lambda and the elimination form is an application. Applying a β-rule eliminates T in the
sense that the introduction form from the left-hand side either no
longer appears or has been replaced by a term of a simpler type on
the right-hand side.
Each instance of a β-rule is associated with an elimination frame.
An elimination frame is simply the elimination form with a designated hole [ ] that can be plugged with another expression. For
instance, elimination frames for the function β-rule are of the form
E[ ] = [ ] M . If we plug an introduction form λx.N into E[ ],
written E[λx.N ], then we obtain the left-hand side of the associated β-rule (λx.N ) M .
(This notion of an expression with a hole that can be filled by
another expression is commonly used in rewriting and operational
semantics for programming languages [24, ch. 19]; here, it is not
essential but helps cut down the number of explicit rules, and helps
highlight commonality between rules.) The elimination frames of
λNRC are as follows.
E[ ] ::= [ ] M | [ ].` | if [ ] then M else N | for (x ← [ ]) N
The following rules express that comprehensions, conditionals, empty
bag constructors, and unions can always be hoisted out of the above
elimination frames. In the literature such rules are often called commuting conversions. They are necessary in order to expose all possible β-reductions. For instance,

Weak normalisation and strong normalisation. Given a

term M and a rewrite relation ;, we write M 6; if M is irreducible, that is no rewrite rules in ; apply to M . The term M is
said to be in normal form.
A term M is weakly normalising with respect to a rewrite relation ;r , or r-WN, if there exists a finite reduction sequence

;c
;c
;c
;c
;c

(if M then h` = N i else N 0 ).`
cannot β-reduce, but if M then h` = N i.` else N 0 .` can.
E[for (x ← M ) N ] ;c
E[if L then M else N ] ;c
E[∅] ;c
E[M1 ] M2 ] ;c

for (x ← M ) E[N ]
if L then E[M ] else E[N ]
∅
E[M1 ] ] E[M2 ]

For example:
(if L then M1 else M2 ) M ;c if L then M1 M else M2 M

C ONSTANT

VAR

L AM

Σ(c) = hO1 , . . . , On i → O0
[Γ ` Mi : Oi ]n
i=1
Γ ` c(M1 , . . . , Mn ) : O0

Γ, x : A ` x : A

Γ, x : A ` M : B
Γ ` λx. M : A → B

R ECORD

A PP

P ROJECT

[Γ ` Mi : Ai ]n
i=1
n
Γ ` h`i = Mi in
:
h`
i = Ai ii=1
i=1

Γ`M :A→B
Γ`N :A
Γ`MN :B
IF

Γ ` M : Bool
Γ`N :A
Γ ` N0 : A
Γ ` if M then N else N 0 : A

E MPTY

Γ ` ∅ : Bag A

Γ ` M : h`i : Ai in
i=1
Γ ` M.`j : Aj

S INGLETON

U NION

Γ`M :A
Γ ` return M : Bag A

Γ ` M : Bag A
Γ ` N : Bag A
Γ ` M ] N : Bag A
TABLE

F OR

I S E MPTY

Γ ` M : Bag A
Γ, x : A ` N : Bag B
Γ ` for (x ← M ) N : Bag B

Γ ` M : Bag A
Γ ` empty M : Bool

−−→
Σ(t) = Bag h` : Oi
−−→
Γ ` table t : Bag h` : Oi

Figure 12: Typing rules for higher-order nested queries
C ONSTANT

VAR

Σ(c) = hO1 , . . . , On i → O0
[Γ ` Xi : Oi ]n
i=1
Γ ` c(X1 , . . . , Xn ) : O0

−−→
−−→
Γ, x : h` : F i ` x : h` : F i
P ROJECT

Γ ` x : h`i : Ai in
i=1
Γ ` x.`j : Aj
F OR

[Σ(ti ) = Bag Ai ]n
i=1

R ECORD

[Γ ` Ni : Ai ]n
i=1
n
Γ ` h`i = Ni in
:
h`
i = Ai ii=1
i=1

S INGLETON

I NDEX

Γ ` a  d : Index

U NION

[Γ ` Ci : Bag hIndex , F i]n
i=1
]
~
Γ`
C : Bag hIndex , F i

Γ ` I : Index
Γ`N :F
Γ ` returna hI, N i : Bag hIndex , F i

I S E MPTY

Γ, [xi : Ai ]n
Γ, [xi : Ai ]n
i=1 ` X : Bool
i=1 ` C : Bag hIndex , F i
n
Γ ` for ([xi ← ti ]i=1 where X) C : Bag hIndex , F i

Γ ` L : Bag hIndex , F i
Γ ` empty L : Bool

Figure 13: Typing rules for shredded terms
BASE

` O(ΛS ) : O(TS )

R ECORD

BAG

[` Âi (ΛS ) : Â0i (TS )]n
i=1
` h`i :

Âi (ΛS )in
i=1

: h`i :

` Â(ΛS ) : Â0 (TS )

Â0i (TS )in
i=1

`L:A

erase(Â(ΛS )) = A

` (Bag Â(ΛS )) : (Bag Â0 (TS ))A

We write ΛS for the set of shredded terms, and TS for the set of shredded types.
Figure 14: Typing rules for shredded packages

L

Note that some combinations of elimination frames and
rewrite rule are impossible in a well-typed term, such as
if ∅ then M else N . For the purposes of reduction we treat empty
like an uninterpreted constant, that is, we do reduce inside emptiness tests, but they do not in any other way interact with the reduction rules.
Next we prove that ;c is strongly normalising. The proof is
based on a previous proof of strong normalisation for simply-typed
λ-calculus with sums [19], which generalises the >>-lifting approach [21], which in turn extends Tait’s proof of strong normalisation for simply-typed λ- calculus [29].

(→) If S[M [x : = N ]] and N are c-SN then S[(λx.M ) N ] is cSN.
−−−→
~ , are c-SN then S[h−
(hi) If M
` = M i.`i ] is c-SN.
(Bag −) If S[N [x : = M ]] and M are c-SN then
S[for (x ← return M ) N ] is c-SN.
(Bool ) If S[N ] and S[N 0 ] are c-SN then
S[if true then N else N 0 ] is c-SN and
S[if false then N else N 0 ] is c-SN.
P ROOF.
(→): By induction on maxc (S) + maxc (M ) + maxc (N ).
(hi): By induction on

Frame stacks.
S ::= Id | S ◦ E

(frame stacks)

|Id | = 0
|S ◦ E| = |S| + 1

(stack length)
(plugging)

Id [M ] = M
(S ◦ E)[M ] = S[(E[M ])]

Following previous work [19] we assume variables are annotated
with types. We assume variables are annotated with types. We
write A ( B for the type of frame stack S, if S[M ] : B for all
terms M : A.

Frame stack reduction.
S ;c S 0

def

⇐⇒
⇐⇒

max S + (
c

Frame stacks are closed under reduction. A frame stack S is cstrongly normalising, or c-SN, if all reduction sequences starting
from S are finite.
L EMMA 7. If S ;c S 0 , for frame stacks S, S 0 , then |S 0 | ≤ |S|.
P ROOF. Induction on the structure of S.

Reducibility. We define reducibility as follows:
• Id is reducible.
• S ◦ ([ ] N ) : (A → B) ( C is reducible if S and N are
reducible. −−→
• S ◦ ([ ].`) : (` : A) ( C is reducible if S is reducible.
• S : Bag A ( C is reducible if S[return M ] is c-SN for all
reducible M : A.
• S : Bool ( C is reducible if S[true] is c-SN and S[false] is
c-SN.
• M : A is reducible if S[M ] is c-SN for all reducible S : A (
C.
L EMMA 8. If M : A is reducible then M is c-SN.
P ROOF. Follows immediately from reducibility of Id and the
definition of reducibility on terms.
L EMMA 9. x : A is reducible.
P ROOF. By induction on A using Lemma 7 and Lemma 8.
C OROLLARY 10. If S : A ( C is reducible then S is c-SN.

i=1

n
X
max(Mi )) + max(N ) + (
max(Mi0 )).
c

c

i=1

c

(Bag ): By induction on
|S| + max(S[N [x : = M ]]) + max(M ).
c

c

(Bool ): By induction on |S| + maxc (S[N ]) + maxc (S[N 0 ]).
This completes the proof.
Now we obtain reducibility-closure properties for each type constructor.
L EMMA 12

∀M.S[M ] ;c S 0 [M ]
S[x] ;c S 0 [x]

n
X

( REDUCIBILITY- CLOSURE ).

(→) If M [x : = N ] is reducible for all reducible N , then λx.M is
reducible.
−−−→
~ are reducible, then h−
(hi) If M
` = M i is reducible.
(Bag ) If M is reducible, N [x: =M 0 ] is reducible for all reducible
M 0 , then for (x ← M ) N is reducible.
(Bool ) If M, N, N 0 are reducible then if M then N else, N 0 is reducible.
P ROOF. Each property follows from the corresponding part of
Lemma 11 using Lemma 8 and Corollary 10.
We also require additional closure properties for the empty bag and
union constructs.
L EMMA 13

( REDUCIBILITY- CLOSURE II).

(∅) The empty bag ∅ is reducible.
(]) If M, N are reducible, then M ] N is reducible.
P ROOF.
(∅): Suppose S : Bag A ( C is reducible. We need to prove that
S[∅] is c-SN. The proof is by induction on |S| + maxc (S).
The only interesting case is hoisting the empty bag out of a
bag elimination frame, which simply decreases the size of the
frame stack by 1.
(]): Suppose M, N : Bag A, and S : Bag A ( C are reducible.
We need to show that S[M ] N ] is c-SN. The proof is by
induction on |S| + maxc (S[M ]) + maxc (S[N ]). The only
interesting case is hoisting the union out of a bag elimination
frame, which again decreases the size of the frame stack by 1,
whilst leaving the other components of the induction measure
unchanged.
This completes the proof.

Each type constructor has an associated β-rule. Each β-rule
gives rise to an SN-closure property.
L EMMA 11

(SN- CLOSURE ).

T HEOREM 14. Let M be any term. Suppose x1 : A1 , . . . , xn :
An includes all the free variables of M . If N1 : A1 , . . . , Nn : An
~ ] is reducible.
are reducible then M [~
x:=N

P ROOF. By induction on the structure of terms using Lemma 12
and Lemma 13.

C.3

The query normalisation function

The following definition of the function norm generalises the
normalisation algorithm from previous work [20].

T HEOREM 15 ( STRONG NORMALISATION ). The relation ;c
is strongly normalising.

norm A (M ) = Lnf h (nf c (M ))MA

P ROOF. Let M be a term with free variables ~
x. By Lemma 9, ~
x
are reducible. Hence, by Theorem 14, M is c-SN.

where:
Lc([Xi : Oi ]n
i=1 )MO
Lx.`MO
Lempty (M : Bag A)MBool
LM Mh`i :Ai in
i=1
LM MBag A

It is well known that β-reduction in simply-typed λ-calculus has
non-elementary complexity in the worst case [1]. The relation ;c
includes β-reduction, so it must be at least as bad (we conjecture
that it has the same asymptotic complexity, as ;c can be reduced
to β-reduction on simply-typed λ-calculus via a CPS translation
following de Groote [9]). However, we believe that the asymptotic
complexity is unlikely to pose a problem in practice, as the kind
of higher-order code that exhibits worst-case behaviour is rare. It
has been our experience with Links that query normalisation time
is almost always dominated by SQL execution time.

C.2

~ where L) return LM MA ]
BLreturn M M? ~ = [for (G
A,G,L
BLfor (x ← t) M M? ~ = BLM M? ~
A,G,L

BLtable tM?

~
A,G,L

The if-hoisting rule says that if an expression contains an if-hoisting
frame around a conditional, then we can lift the conditional up and
push the frame into both branches:
F [if L then M else N ] ;h if L then F [M ] else F [N ]

We write size(M ) for the size of M , as in the total number of
syntax constructors in M .
L EMMA 16.
1. If M, N, N 0 are h-SN then if M then N else N 0 is h-SN.
2. If M, N are h-SN then M ] N is h-SN.
~ are h-SN then c(M
~ ) is h-SN.
3. If M
−−−−→
~
4. If M are h-SN then h` = M i is h-SN.
P ROOF.
1: By induction on hmax h (M ),
max h (N 0 ), size(N ) + size(N 0 )i.

size(M ),

max h (N ) +

2: By induction on hmax h (M ) + max h (N ), size h (M ) +
size h (N )i using (1).
3 and 4: By induction on
h

n
X

max h (Mi ),

i=1

n
X

size(Mi )i

i=1

using (1).
This concludes the proof.
P ROPOSITION 17. The relation ;h is strongly normalising.
P ROOF. By induction on the structure of terms using Lemma 16.

~ +[x←t],L
A,G+

BL∅M? ~ = [ ]
A,G,L
BLM ] N M? ~ = BLM M? ~ ++ BLN M? ~
A,G,L
A,G,L
A,G,L
BLif L0 M N M? ~ = BLM M? ~
A,G,L
A,G,L∧L0
++ BLN M? ~
0
A,G,L∧¬L

To hoist conditionals (if-expressions) out of constant applications, records, unions, and singleton bag constructors, we define
if-hoisting frames as follows:

| [ ] ] N | M ] [ ] | return [ ]

A,G++[x←t],L

= BLreturn xM?
(x fresh)

If hoisting

−−−−→
−−−−→
~ , [ ], N
~ ) | h`0 = M , ` = [ ], `00 = N i
F [ ] ::= c(M

= c([LXi MOi ]n
i=1 )
= x.`
= empty (LM MBag A )
= h`i = F LM MAi ,`i in
i=1
U
= (BLM M?A,[ ],true )

F LxMA,`i = Lx.`i MA
F Lh`i = Mi in
i=1 MA,`i = LMi MA

Strictly speaking, in order for the above definition of norm A to
make sense we need the two rewrite relations to be confluent. It is
easily verified that the relation ;c is locally confluent, and hence
by strong normalisation and Newman’s Lemma it is confluent. The
relation ;h is not confluent as the ordering of hoisting determines
the final order in which booleans are eliminated. However, it is easily seen to be confluent modulo reordering of conditionals, which in
turn means that norm A is well-defined if we identify terms modulo
commutativity of conjunction, which is perfectly reasonable given
that conjunction is indeed commutative.
T HEOREM 18. The function norm A terminates.
P ROOF. The result follows immediately from strong normalisation of ;c and ;h , and the fact that the functions L−M, BL−M? , and
FL−M are structurally recursive (modulo expanding out the righthand-side of the definition of BLtable tM?A,G,L
~ .

D.

PROOF OF CORRECTNESS OF SHREDDING

The main correctness result is that if we shred an annotated normalised nested query, run all the resulting shredded queries, and
stitch the shredded results back together, then that is the same as
running the nested query directly.
Intuitively, the idea is as follows:
1. define shredding on nested values;
2. show that shredding commutes with query execution; and
3. show that stitching is a left-inverse to shredding of values.
Unfortunately, this strategy is a little too naive to work, because
nested values do not contain enough information about the structure
of the source query in order to generate the same indexes that are
generated by shredded queries.
To fix the problem, we will give an annotated semantics AJ−K
that is defined only on queries that have first been converted to normal form and annotated with static indexes as described in Section 4. We will ensure that N Jerase(L)K = erase(AJLK), where
we overload the erase function to erase annotations on terms and
values. The structure of the resulting proof is depicted in the diagram in Figure 15, where we view a query as a function from the in-

R ESULT

[` vi : Ai ]n
[` J : Index ]n
i=1
i=1
` [vi @Ji ]n
i=1 : Bag A

R ECORD

[` vi : Ai ]n
i=1
n
` h`i = vi in
i=1 : h`i = Ai ii=1

C ONSTANT

Σ(c) = O
`c:O

Figure 16: Typing rules for nested annotated values
SJLK = SJLKε,1

n
SJh` = N in
i=1 Kρ,ι = h`i = SJNi Kρ,ι ii=1
SJXKρ,ι = N JXKρ

SJa  outKρ,ι.i = index (a  ι)
SJa  inKρ,ι.i = index (a  ι.i)

U
n
SJreturna N Kρ,ι = [SJN Kρ,ι @index (a  ι)]
SJ n
i=1 Ci Kρ,ι = concat([SJCi Kρ,ι ]i=1 )
n
SJfor ([xi ← ti ]i=1 where X) CKρ,ι = concat([SJCKρ[xi 7→ri ]ni=1 ,ι.j | hj, ~ri ← enum([~r | [ri ← Jti K]n
])])
i=1 , N JXKρ[xi 7→ri ]n
i=1
Figure 17: Semantics of shredded queries, with annotations
on annotated values is defined as follows:
JΣK

N Jerase(L)K

AJLK

HJLKA
shred (−) (A)

N JAK

erase

AJAK

HJAK

AJLK = AJLKε,1
U
n
AJ n
i=1 Ci Kρ,ι = concat([AJCi Kρ,ι ]i=1 )
n
AJh`i = Mi in
i=1 Kρ,ι = h`i = AJMi Kρ,ι ii=1
AJXKρ,ι = N JXKρ
a
AJfor ([xi ← ti ]n
i=1 where X) return M Kρ,ι =
[AJM Kρ[xi 7→ri ]n ,ι.j @index (a  ι.j)
i=1
| hj, ~
ri ← enum([~
r | [ri ← Jti K]n
i=1 , N JXKρ[xi 7→ri ]n ])]
i=1

stitch

Figure 15: Correctness of shredding and stitching

terpretation of the input schema Σ to the interpretation of its result
type. To prove correctness is to prove that this diagram commutes.

As well as an environment, the current dynamic index is threaded
through the semantics. Note that we use the ordinary semantics to
evaluate values that cannot have any annotations (such as boolean
tests in the last case).
It is straightforward to show by induction that the annotated semantics erases to the standard semantics:
T HEOREM 19. For any L we have erase(AJLK) = N Jerase(L)K.

D.2
D.1

Annotated semantics of nested queries

We annotate bag elements with distinct indexes as follows:

Results
s ::= [w1 @I1 , . . . , wm @Im ]
Inner values
w ::= c | r | s
Rows
r ::= h`1 = w1 , . . . , `n = wn i
Indexes
I, J

Typing rules for these values are in Figure 16. The index annotations @I on collection elements are needed solely for our correctness proof, and do not need to be present at run time.
The canonical choice for representing indexes is to take I =
a  ι. We also allow for alternative indexing schemes in by parameterising the semantics over an indexing function index mapping
each canonical index a  ι.j to a concrete representation. In the
simplest case, we take index to be the identity function (where
static indexes are viewed as distinct integers). We will later consider other definitions of index that depend on the particular query
being shredded. Informally, the only constraints on index are that
it is defined on every canonical index a  ι that we might need in
order to shred a query, and it is injective on all canonical indexes.
We will formalise these constraints later, but for now, index can be
assumed to be the identity function.
Given an indexing function index , the semantics of nested queries

Shredding and stitching annotated values

To define the semantics of shredded queries and packages, we
use annotated values in which collections are annotated pairs of
indexes and annotated values. Again, we allow annotations @J on
elements of collections to facilitate the proof of correctness. Typing
rules for these values are shown in Figure 18.
Results
s ::= [hI1 , w1 i@J1 , . . . , hIm , wm i@Jm ]
Shredded values
w ::= c | r | I
Rows
r ::= h`1 = w1 , . . . , `n = wn i
Indexes
I, J
Having defined suitably annotated versions of nested and shredded values, we now extend the shredding function to operate on
nested values.
VsWp
?
V[vi @Ji ]n
i=1 WI,
?
V[vi @Ji ]n
W
i=1 I,↓.p
?
Vh`i = vi in
i=1 WI,`i .p

= VsW?>  1,p

= [hI, Tvi UJi i@Ji ]n
i=1
= concat([Vvi W?Ji ,p ]n
i=1 )
= Vvi W?I,p

TcUI = c
n
Th`i = vi in
i=1 UI = h`i = Tvi UI ii=1
TsUI = I

Note that in the cases for bags, the index annotation J is passed as
an argument to the recursive call: this is where we need the ghost
indexes, to relate the semantics of nested and shredded queries.
We lift the nested result shredding function to build an (annotated) shredded value package in the same way that we did for

R ESULT

C ONSTANT

[` Ii : Index ]n
[` wi : F ]n
[` Ji : Index ]n
i=1
i=1
i=1
` hI1 , w1 @J1 i, . . . , hIn , wn @Jn i : Bag hIndex , F i

Σ(c) = O
`c:O

R ECORD

[` ni : Fi ]n
i=1
n
` h`i = wi in
i=1 : h`i = Fi ii=1

Figure 18: Typing rules for shredded values
nested types and nested queries.
shred s (Bag A) = package (VsW ) (Bag A)
−
shred s,p (Bag A) = package (VsW ),p (Bag A)

Not all possible indexing schemes satisfy Lemma 21. To identify
those that do, we recall the function for computing the canonical
indexes of a nested query.

−

We adjust the stitching function slightly to maintain annotations;
the adjustment is consistent with its behaviour on unannotated values.
stitch(Â) = stitch >  1 (Â)
stitch c (O) = c
n
stitch r (h`i : Âi in
i=1 ) = h`i = stitch r.cli (Âi )ii=1
stitch I ((Bag Â)s ) = [(stitch w (Â))@J | hI, wi@J ← s]

IJLK = IJLKε,1
U
IJ n
C
= concat([IJCi Kρ,ι ]n
i Kρ,ι
i=1
i=1 )
IJh`i = Mi in
K
=
concat([IJMi Kρ,ι ]n
ρ,ι
i=1
i=1 )
IJXKρ,ι = [ ]
a
IJfor ([xi ← ti ]n
i=1 where X) return M Kρ,ι =
concat([a  ι.j :: IJM Kρ[xi 7→ri ]n ,ι.j
i=1
| hj, ~
ri ← enum([~
r | [ri ← Jti K]n
i=1 , N JXKρ[xi 7→ri ]n ])])
i=1

Note that IJ−K resembles AJ−K, but instead of the nested value v it
computes all indexes of v. An indexing function index : Index →
A is valid with respect to the closed nested query L if it is injective
and defined on every canonical index in IJLK.

The inner value parameter w to the auxiliary function stitch w (−)
specifies which values to stitch along the current path.
We now show how to interpret shredded queries and query packages over shredded values. The semantics of shredded queries (including annotations) is given in Figure 17. The semantics of a
shredded query package is a shredded value package containing
indexed results for each shredded query. For each type A we define
HJAK = shred A (A) and for each flat–nested, closed ` L : A we
define HJLKA : HJAK as pmap SJ−K (shred L (A)).

The only requirement on indexes in the proof of Theorem 4 is that
nested values be well-indexed, hence the proof extends to any valid
indexing scheme. The concrete, natural, and flat indexing schemes
are all valid.

D.3

D.4

Main results

There are three key theorems. The first states that shredding
commutes with the annotated semantics.
T HEOREM 20. If ` L : Bag A then:
HJLKBag A = shred AJLK (Bag A)
In order to allow shredded results to be correctly stitched together, we need the indexes at the end of each path to a bag through
a nested value to be unique. We define indexes p (v), the indexes of
nested value v along path p as follows.
n
indexes  ([vi @Ji ]n
i=1 ) = [Ji ]i=1
n
indexes ↓.p ([vi @Ji ]n
i=1 ) = concat([indexes p (vi )]i=1 )
indexes `i .p (h`i = vi in
i=1 ) = indexes p (vi )

We say that a nested value v is well-indexed (at type A) provided ` v : A, and for every path p in paths(A), the elements of
indexes p (v) are distinct.

L EMMA 24. If index is valid for L then AJLK is well-indexed.

L EMMA 25. SJTM Ua Kρ,ι = TAJM Kρ,ι Ua  ι
P ROOF. By induction on the structure of M .
Case x.`:
=

T HEOREM 22. If ` s : Bag A and s is well-indexed at type
Bag A then stitch(shred s (Bag A)) = s.
Combining Theorem 20, Lemma 21 and Theorem 22 we obtain the
main correctness result (see Figure 15).
T HEOREM 23. If ` L : Bag A then: stitch(HJLKBag A ) =
AJLK, and in particular: erase(stitch(HJLKBag A )) = N JLK.

SJTx.`Ua Kρ,ι
SJx.`Kρ,ι

=
AJx.`Kρ,ι
=
TAJx.`Kρ,ι Ua  ι
Case c([Xi ]n
i=1 ):

L EMMA 21. If ` L : A, then AJLK is well-indexed at A.
Our next theorem states that for well-indexed values, stitching is
a left-inverse of shredding.

Detailed proofs

We first show that the inner shredding function T−U commutes
with the annotated semantics.

=

SJTc([Xi ]n
i=1 )Ua Kρ,ι

=

SJc([TXi Ua ]n
i=1 )Kρ,ι

=

AJc([TXi Ua ]n
i=1 )Kρ,ι

=

JcK([AJTXi Ua Kρ,ι ]n
i=1 )
TAJc([Xi ]n
i=1 )Kρ,ι Ua  ι

Case empty M :

=

SJTempty M Ua Kρ,ι

=

SJempty VM W Kρ,ι

=

AJempty VM W Kρ,ι
TAJempty M Kρ,ι Ua  ι

=
=

SJh`i = TMi Ua in
i=1 Kρ,ι

h`i = SJTMi Ua Kρ,ι in
i=1
=
(Induction hypothesis)
h`i = TAJMi Kρ,ι Ua  ι in
i=1
=
Th`i = AJMi Kρ,ι in
i=1 Ua  ι
=
TAJh`i = Mi in
i=1 Kρ,ι Ua  ι

=

?
Vconcat([AJCi Kρ,ι ]n
i=1 )Wa  ι,p

=

~ ?
Vconcat([AJCKρ,ι | C ← C])W
a  ι,p
~ s ← AJCKρ,ι ]))
concat(concat([VsW?a  ι,p | C ← C,

=

−−−−→
Case h` = M i:
SJTh`i = Mi in
i=1 Ua Kρ,ι

=

U
?
VAJ n
i=1 Ci Kρ,ι Wa  ι,p

=

~
concat([VAJCKρ,ι W?a  ι,p | C ← C])
concat([VAJCi Kρ,ι W?a  ι,p ]n
i=1 )

This completes the proof.

We are now in a position to prove that the outer shredding function V−W commutes with the semantics.

Case L:
=

SJTLUa Kρ,ι
SJa  inKρ,ι

=
aι
=
TAJLKρ,ι Ua  ι
This completes the proof.
The first part of the following lemma allows us to run a shredded
query by concatenating the results of running the shreddings of its
component comprehensions. Similarly, the second part allows us
to shred the results of running a nested query by concatenating the
shreddings of the results of running its component comprehensions.

L EMMA 27. SJVLWp Kρ,1 = VAJLKρ,1 Wp
P ROOF. We prove the following:
1. SJVLWp Kρ,1 = VAJLKρ,1 Wp
U
2. SJ VCW?a,p Kρ,ι = VAJCKρ,ι W?a  ι,p
3. SJVM W?a,p Kρ,ι = VAJM Kρ,ι W?a  ι,p
The first equation is the result we require. Observe that it follows
from (2) and Lemma 26. We now proceed to prove equations (2)
and (3) by mutual induction on the structure of p.
There are only two cases for (2), as the `i .p case cannot apply.

Case :
L EMMA
U 26.
U
1. SJ V n
Ci W?a,p Kρ,ι = concat([SJVCi W?a,p Kρ,ι ]n
i=1 )
Un i=1
2. VAJ i=1 Ci Kρ,ι W?a  ι,p = concat([VAJCi Kρ,ι W?a  ι,p ]n
i=1 )
P ROOF.
1.
=

U U
?
SJ V n
i=1 Ci Wa,p Kρ,ι

=

U
SJ concat([VCi W?a,p ]n
i=1 )Kρ,ι
U
~ ρ,ι
SJ concat([VCW?a,p | C ← C])K

=
=

=

=

=
=

~ C 0 ← VCW? ]))
concat(concat([SJC 0 Kρ,ι | C ← C,
a,p

=

U
~
concat([SJ VCW?a,p Kρ,ι | C ← C])

=

U
−−−→
SJ Vfor (x ← t where X) returnb M W?a, Kρ,ι
(Definition of SJ−K)
−−−→
SJfor (x ← t where X) returnb ha  ι, TM Ub iKρ,ι
(Definition of SJ−K)
−
→
[ha  ι, SJTM Ub Kρ[−
x7−
→
v],ι.i i@b  ι.i
−
−−−−
→
−
→
| hi, ~v i ← enum([~v | v ← JtK, SJXKρ[−
x7−
→
v] ])]
(Lemma 25)
−
→
[ha  ι, TAJM Kρ[x7−−→
v],ι.i Ub  ι.i i@b  ι.i
−
−−−−
→
−
→
| hi, ~v i ← enum([~v | v ← JtK, SJXKρ[−
x7−
→
v] ])]
(Definition of V−W? )
−
→
V[AJM Kρ[−
x7−
→
v],ι.i @b  ι.i
−
−−−−
→
?
−
→
| hi, ~v i ← enum([~v | v ← JtK, SJXKρ[−
x7−
→
v] ])]Wa  ι,
(Definition of AJ−K)
−−−→
VAJfor (x ← t where X) returnb M Kρ,ι W?a  ι,

U
concat([SJ VCi W?a,p Kρ,ι ]n
i=1 )
2.

Case ↓.:

=
=

=

=

=

U
−−−→
SJ Vfor (x ← t where X) returnb M W?a,↓.p Kρ,ι
(Definition of V−W? )
U
−−−→
SJ [for (x ← t where X) C | C ← VM W?b,p ]Kρ,ι
(Definition of SJ−K)
concat([concat
−
→
([SJCKρ[x7−−→
v],ι.i
−
−−−−
→
−
→
| hi, ~v i ← enum([~v | v ← JtK, SJXKρ[−
x7−
→
v] ])])
| C ← VM W?b,p ])
(Definition of SJ−K)
concat
−
→
([SJVM W?b,p Kρ[x7−−→
v],ι.i
−
−−−−
→
−
→
| hi, ~v i ← enum([~v | v ← JtK, SJXKρ[−
x7−
→
v] ])])
(Induction hypothesis (3))
concat
?
−
→
([VAJM Kρ[−
x7−
→
v],ι.i Wb,p
−
−−−−
→
−
→
| hi, ~v i ← enum([~v | v ← JtK, SJXKρ[−
x7−
→
v] ])])
(Definitions of AJ−K and V−W? )
−−−→
VAJfor (x ← t where X) returnb M Kρ,ι W?a  ι,↓.p

There are three cases for (3).

We can now formulate the following crucial technical lemma,
which states that given the descendants of a result v at path p.↓ and
the shredded values of v at path p we can stitch them together to
form the descendants at path p.
L EMMA 28
Bag A, then
v

[ v

HJLKA = shred AJLK (Bag A)
This is straightforward by induction on A, using Lemma 27.
We have proved that shredding commutes with the semantics.
It remains to show that stitching after shredding is the identity on
index-annotated nested results. We need two auxiliary notions: the
descendant of a value at a path, and the indexes at the end of a path
(which must be unique in order for stitching to work).
We define v p,w , the descendant of a value v at path p with
respect to inner value w as follows.

J,p,h`i =wi in
i=1

s J,,I
n
[vi @Ji ]i=1 J,↓.p,I
h`i = vi in
i=1 J,`i .p,I

| hIout , wi@Iin ← VvW?J 0 ,p.~`, Iout = I]
= [v 0 .~
`@Iin | v 0 @Iin ← v J 0 ,p,I ]

Subcase : If J 0 6= I then both sides are empty lists. Suppose that
J 0 = I.
J 0 ,↓.~
`,c @Iin
| hIout , ci@Iin ← VsW?J 0 ,~`, Iout = I]
=
(Definition of − )
[c@Iin | hIout , ci@Iin ← VsW?J 0 ,~`, Iout = I]
=
(J 0 = I)
s
=
(Definition of − )
[v 0 .~
`@Iin | v 0 @Iin ← s J 0 ,,I ]

Subcase `i .p:
−−−→
[( h` = vi

=

v

J 0 ,p.↓.~
`,w @Iin

Case O:

=

p,w

| hIout , wi@Iin ← VvW?J,p , Iout = I]

The proof now proceeds by induction on the structure of A and
side-induction on the structure of p.

We now lift Lemma 27 to shredded packages.
P ROOF OF T HEOREM 20. We need to show that if ` L : Bag A
then

J,p,c

J,p.↓,w @Iin

P ROOF. First we strengthen the induction hypothesis to account
for records. The generalised induction hypothesis is as follows.
If v is well-indexed and ` v J 0 ,p.~`,I : Bag A, then

This completes the proof.

v

=[ v

J,p,I

[( s

Cases  and ↓.: follow from (2) by applying the two parts of Lemma 26
to the left and right-hand side respectively.
Case `i .:
−−−−→
SJVh` = M iW?a,`i .p Kρ,ι
=
(Definition of V−W? )
SJVMi W?a,p Kρ,ι
=
(Induction hypothesis (3))
VAJMi Kρ,ι W?a  ι,p
=
(Definition of AJ−K)
−−−−→
VAJh` = M iKρ,ι W?a  ι,`i .p

v

J,p,I

( KEY LEMMA ). If v is well-indexed and ` v

= v

>  1,p,w

=c
= h`i = v J,p.`i ,wi in
i=1

s,
if J = I
=
[ ],
if J 6= I
= concat([ vi Ji ,p,I ]n
i=1 )
= vi J,p,I

Essentially, this extracts the part of v that corresponds to w. The
inner value w allows us to specify a particular descendant as an index, or nested record of indexes; for uniformity it may also contain
constants.

=
=
=

J 0 ,`i .p.↓.~
`,c @Iin

−−−→
| hIout , c@Iin i ← Vh` = viW?J 0 ,`i .p.~`, Iout = I]
(Definition of − )
−−−→
[c@Iin | hIout , c@Iin i ← Vh` = viW?J 0 ,`i .p.~`, Iout = I]
(Definition of V−W? )
[c@Iin | hIout , c@Iin i ← Vvi W?J 0 ,p.~`, Iout = I]
(Definition of − )
[( vi J 0 ,p.↓.~`,c @Iin | hIout , ci@Iin ← Vvi W?J 0 ,p.~`, Iout = I]
(Induction hypothesis)
[v 0 .~
`@Iin | v 0 @Iin ← vi J 0 ,p,I ]
(Definition of V−W? )
−−−→
0 ~
[v .`@Iin | v 0 @Iin ← h` = vi J 0 ,`i .p,I ]

Subcase ↓.p:
[( [vi @Ji ]n
i=1 J 0 ,↓.p.↓.~
`,c )@Iin
?
| hIout , ci@Iin ← V[vi @Ji ]n
, I = I]
i=1 WJ 0 ,↓.p.~
` out
?
=
(Definitions of − and V−W )
concat([c@Iin | hIout , c@Iin i ← Vvi W?Ji ,p.~`, Iout = I]n
i=1 )
=
(Induction hypothesis)
concat([v 0 .~
`@Iin | v 0 @Iin ← vi Ji ,p ]n
i=1 )
=
(Definition of − )
[v 0 .~
`@Iin | v 0 @Iin ← [v@J]n
i=1 J 0 ,p ]
Case hi: The proof is the same as for base types with the constant
c replaced by hi.

:

−−→
Case h` : Ai where |~
`| ≥ q: We rely on the functions zip ~`, for transforming a record of lists of equal length to a list of records, and
unzip ~`, for transforming a list of records to a record of lists of
equal length. In fact we require special versions of zip and unzip
that handle annotations, such that zip takes a record of lists of equal
length whose annotations must be in sync, and unzip returns such
a record.
zip ~` h`i = [ ]in
i=1 = [ ]
n
h` = si in
zip ~` h`i = vi @J :: si in
i=1
i=1 = h`i = vi ii=1 @J :: zip ~
` i
unzip ~`(s) = h`i = [v.`i @J | v@J ← s]in
i=1

If ~
` is a non-empty list of column labels then zip ~` is the inverse of
unzip ~`.
zip ~`(unzip ~`(s)) = s,

Subcase `i .p:
[ h`i = vi in
i=1 J 0 ,`i .p.↓.`~0 ,Iin @Iin
?
| hIout , Iin i@Iin ← Vh`i = vi in
i=1 WJ 0 ,` .p.`~0 , Iout = I]
i
?
=
(Definitions of − and V−W )
[ vi J 0 ,p.↓.`~0 ,Iin @Iin
| hIout , Iin i@Iin ← Vvi W?J 0 ,p.`~0 , Iout = I]
=
(Induction hypothesis)
[v 0 .`~0 @Iin | v 0 @Iin ← vi J 0 ,p,I ]
=
(Definition of − )
[v 0 .`~0 @Iin | v 0 @Iin ← h`i = vi in
i=1 J 0 ,`i .p,I ]
Subcase ↓.p:

if |~
`| ≥ 1
=

[ v

=

=

=
=

@Iin
| hIout , wi@Iin ← VvW?J 0 ,p.`~0 , Iout = I]
(Definition of − )
[h`i = v J 0 ,p.↓.`~0 .`i ,w in
i=1 @Iin
| hIout , w@Iin i ← VvW?J 0 ,p.`~0 .` , Iout = I]
(Definition of zip)
zip ~` h`i = [v`i ,w @Iin | hIout , w@Iin i ← VvW?J 0 ,p.`~0 .` ,
i
Iout = I]in
i=1
where v`,w stands for v J 0 ,p.↓.`~0 .`,w
(Induction hypothesis)
zip ~` h`i = [v 0 .`~0 .`i @Iin | v 0 @Iin ← v J 0 ,p,I ]in
i=1
(Definition of zip)
[v 0 .`~0 @Iin | v 0 @Iin ← v J 0 ,p,I ]
J 0 ,p.↓.`~0 ,w

=

=

=

=
~ Subcase : If J 0 6= I then both sides of the equation
Case Bag A:
are equivalent to the empty bag. Suppose J 0 = I.

=

=
=
=

=

=

=
=

[ [vi @Ji ]n
i=1 J 0 ,↓.~
`,Iin @Iin
?
, I = I]
| hIout , Iin i@Iin ← V[vi @Ji ]n
i=1 WJ 0 ,~
` out
(Definition of − )
[concat([ vi Ji ,~`,Iin ]n
i=1 )@Iin
?
| hIout , Iin i@Iin ← V[vi @Ji ]n
, I = I]
i=1 WJ 0 ,~
` out
?
n
0
(V[vi @Ji ]i=1 WJ 0 ,~` = hJ , J1 i@J1 , . . . , hJ 0 , Jn i@Jn )
~ 0
[concat([ vi Ji ,~`,Iin ]n
i=1 )@Iin | Iin ← J, J = I]
0
(J = I)
~
[concat([ vi Ji ,~`,Iin ]n
i=1 )@Iin | Iin ← J]
(Definition of − )
[concat([ vi Ji ,~`,Iin
~
| vi @Ji ← [vi @Ji ]n
i=1 ])@Iin | Iin ← J]
(Definition of − )
[concat([ vi .~
` Ji ,,Iin | vi @Ji ← [vi @Ji ]n
i=1 ])@Iin
~
| Iin ← J]
(Definition of − )
[concat([vi .~
`
~
| vi @Ji ← [vi @Ji ]n
i=1 , Ji = Iin ])@Iin | Iin ← J]
(v is well-indexed)
[vi .~
`@Iin | vi @Iin ← [vi @Ji ]n
i=1 ]
(Definition of − and J 0 = I)
[vi .~
`@Iin | vi @Iin ← [vi @Ji ]n
i=1 J 0 ,,I ]

=

[ [vi @Ji ]n
i=1 J 0 ,↓.p.↓.~
`,Iin @Iin
?
| hIout , Iin i@Iin ← V[vi @Ji ]n
, I = I]
i=1 WIout ,↓.p.~
` out
?
(Definitions of − and V−W )
[(concat([ vi Ji ,p.↓.~`,Iin ]))@Iin
| hIout , Iin i@Iin ← concat([Vvi W?Ji ,p.~`]n
i=1 ), Iout = I]
(Expanding concat([V−W? ]n
i=1 ))
[(concat([ vi Ji ,p.↓.~`,Iin ]))@Iin
| vi @Ji ← [vi @Ji ]n
i=1 ,
hIout , Iin i@Iin ← Vvi W?Ji ,p.~`, Iout = I]
(v is well-indexed)
[ vi Ji ,p.↓.~`,Iin @Iin
| vi @Ji ← [vi @Ji ]n
i=1 ,
hIout , Iin i@Iin ← Vvi W?Ji ,p.~`, Iout = I]
(Comprehension → concatenation)
concat
([ vi Ji ,p.↓.~`,Iin @Iin
| hIout , Iin i@Iin ← Vvi W?Ji ,p.~`, Iout = I]n
i=1 )
(Induction hypothesis)
concat([v 0 .~
`@Iin | v 0 @Iin ← vi Ji ,↓.p,I ]n
i=1 )
(Concatenation → comprehension)
[v 0 .~
`@Iin | v 0 @Iin ← [vi @Ji ]n
i=1 J 0 ,↓.p,I ]

This completes the proof.
The proof of this lemma is the only part of the formalisation that
makes use of values being well-indexed. Stitching shredded results
together does not depend on any other property of indexes, thus any
representation of indexes that yields unique indexes suffices.
T HEOREM 29. If s is well-indexed and `
stitch w (shred s,p (A)) = s p,w .
P ROOF. By induction on the structure of A.
Case O:
stitch c (shred s,p (O))
=
c
=
s

p,c

−−−→
Case h` = Ai:

s

p,w

: A then

stitch h`i =wi ini=1 (shred s,p (h`i : Ain
i=1 ))

E.

RECORD FLATTENING

=
h`i = stitch wi (shred s,p.l (A))in
i=1
=
(Induction hypothesis)
h`i = s p.l,wi in
i=1
=
s p,h`i =wi in
i=1

Case Bag A:
stitch I (shred s,p (Bag A))
=

Flat types. For simplicity we extend base types to include the
unit type hi. This allows us to define an entirely syntax-directed
unflattening translation from flat record values to nested record values.
−−→
Types
A, B ::= Bag h` : Oi
Base types
O ::= Int | Bool | String | hi
The Links implementation diverges slightly from the presentation
here. Rather than treating the unit type as a base type, it relies on
type information to construct units when unflattening values.

stitch I (((shred s,p.↓ (A))VsWp ))

Flat terms.

=
[(stitch n (shred s,p.↓ (A))@Iin )
| hIout , wi@Iin ← VsW?p , Iout = I]
=
(Induction hypothesis)
[ s p.↓,w @Iin | hIout , wi@Iin ← VsW?p , Iout = I]
=
(Lemma 28)
s p,I
This completes the proof.

U ~
Query terms
L, M ::= C
Comprehensions
C ::= let q = S in S 0
~ where X) return R
Subqueries
S ::= for (G
Data sources
u ::= t | q
Generators
G ::= x ← u
Inner terms
N ::= X | index
−−−→
Record terms
R ::= h` = N i
~ | empty L
Base terms
X ::= x.` | c(X)

P ROOF OF T HEOREM 22. By Theorem 29, setting p =  and
w = >  1.

Flattening types. The record flattening function (−) flattens
We now obtain the main result.
P ROOF OF T HEOREM 4. Recall the statement of Theorem 4: we
need to show that ` L : Bag A then:
stitch(HJLKBag A ) = stitch(shred AJLK (Bag A)) = AJLK
The first equation follows immediately from Theorem 20, and the
second from Lemma 21 and Theorem 22.
Furthermore, applying erase to both sides we have:
erase(stitch(HJLKBag A )) = erase(AJLK) = N JLK

where the second step follows by Theorem 19.

record types.
(Bag A) = Bag (A )
O = h• : Oi
hi = h• : hii
−−→ 
h` : F i = h[(`i _`0 ) : O | i ← dom(~
`), (`0 : O) ← Fi  ]i

Labels in nested records are concatenated with the labels of their
ancestors. Base and unit types are lifted to 1-ary records (with
a special • field) for uniformity and to aid with reconstruction of
nested values from flattened values.

Flattening terms. The record flattening function (−) is defined on terms as well as types.
U
Un


( n
i=1 Ci ) =
i=1 (Ci )
(let q = Sout in Sin ) = let q = Sout  in Sin 

~
~ where X † ) return N 
(for (G where X) return N ) = for (G
X  = h• = X † i
hi = h• = hii
(m,ni )

0
(h`i = Ni im
i=1 ) = h`i _`j = Xj i(i=1,j=1) ,
ni

where Ni = h`0j = Xj ij=1
(x.`1 . · · · .`n )† = x.`1 . . . `n •
c(X1 , . . . , Xn )† = c((X1 )† , . . . , (Xn )† )
(empty L)† = empty L

The auxiliary (−)† function flattens n-ary projections.

Type soundness.
`L:A

⇒

` L : A

Unflattening record values.
[r1 , . . . , rn ]≺ = [(r1 )≺ , . . . , (rn )≺ ]
h• = ci≺ = c
h• = hii≺ = hi
(m,n )

≺

i
(h`i _`0j = cj i(i=1,j=1)
)

n

≺

i
= h`i = (h`0j = cj ij=1
) im
i=1

Type soundness.
`L:A

⇒

` L≺ : A≺

Correctness
P ROPOSITION 30. If L is a let-inserted query and ` L : Bag A,
then
≺
LJL K = LJLK

