Querying Relations from the Host Language

Rule bodies and safety left three jobs to ordinary code: computing new values, testing for absence, and aggregating. To do any of them, that code has to ask a query and read its answer. The program below extends the course catalogue from Evaluating relations. requires(c, p) and before(p, c) mean what they meant there. credits(c, n) records that course c is worth n credits, and cost(c, p, n) holds when p, worth n credits, must be taken before c. load takes a list of (course, credits, required courses) tuples and adds the matching credits and requires facts. credits_needed totals the credits that must come before a course:

relation requires : (String, String);
relation credits  : (String, Int);
relation before   : (String, String);
relation cost     : (String, String, Int);

rule before(p, c)  :- requires(c, p);
rule before(p, c)  :- requires(c, q) and before(p, q);
rule cost(c, p, n) :- before(p, c) and credits(p, n);

fn load(catalogue: [(String, Int, [String])]) {
    for entry in catalogue {
        add credits(entry.0, entry.1);
        for p in entry.2 { add requires(entry.0, p); }
    }
}

fn credits_needed(course: String) -> Int =
    fold(solutions cost(course, ?p, ?n), 0, |total, row| total + row.1);

fn main() {
    load([("intro", 4, []),
          ("discrete", 3, []),
          ("data_structures", 4, ["intro"]),
          ("pl", 3, ["data_structures", "discrete"]),
          ("compilers", 3, ["pl"])]);

    println(before("discrete", "compilers"));
    println(solutions before(?p, "compilers"));
    for requires("pl", ?p) { println("pl requires " ++ p); }

    println(credits_needed("compilers"));
    println(solutions cost("compilers", ?, ?n));
    println(fold(solutions cost("compilers", ?, ?n), 0, |total, n| total + n));
}

It prints:

true
["data_structures", "discrete", "intro", "pl"]
pl requires data_structures
pl requires discrete
14
[3, 4]
7

credits_needed and the last two lines of main both ask about the courses before compilers. Their queries differ only in ?p and ?, but the first total is 14 and the second is 7.

The answers raise these questions:

• How does a local value reach a query? A rule cannot see a query’s locals, yet credits_needed uses its parameter course inside a query.
• What type does a query have? before appears once as a Bool and once inside a list of strings, and requires supplies a loop variable. How does the type checker know which is which?
• Why did the total change? What did replacing ?p with ? remove from the answer?
• What if the facts change while a program is using an answer? A for body can add to the relation it walks, and a list from solutions can outlive the facts it was computed from.

Moving answers between a query language and a programming language became a practical problem as soon as relational databases had application programs to serve.

Two languages in one program

A relational query describes a whole set of rows, but the programming languages of the 1970s handled data one record at a time. IBM’s System R project connected the two by letting a PL/I or Cobol program contain SQL statements. A preprocessor took the statements out and compiled them before the host program was compiled. The connection between a statement and its host was the cursor: a program opened a query, then fetched its rows one at a time into host variables, so that a set-valued answer became a loop.

Joachim Schmidt’s Pascal/R (1977) put relations inside the language as a data type. Its selections combined Pascal’s sets with the quantifiers of logic, and this one from a later report by Matthias Jarke and Schmidt reads as a set definition:

enames := [<e.ename> OF EACH e IN employees: (e.estatus = professor) AND …]

The friction between the two kinds of language acquired a name, impedance mismatch, usually credited to a 1984 paper by George Copeland and David Maier. William Cook and Ali Ibrahim’s later survey lists what the term covers, including imperative programs against declarative queries and data structures against relations and indexes. The approaches they compare include queries passed to a database as text at run time, queries embedded in a host program and handled by a preprocessor, and persistent objects. Erik Meijer, Brian Beckman, and Gavin Bierman’s LINQ (2006) gave .NET languages a query syntax that compiles into calls to standard operators, so that the compiler can type-check a query as it does other code.

Bridger’s relations and host code share one parser, one type checker, and one set of values. The mismatch that remains is between a query’s answer, a set that exists all at once, and a program that runs one step at a time.

A query as an expression

A query form evaluates its bound arguments first. Each argument that is not a hole evaluates to a value, left to right, threading the store and $\Delta$ as a call’s arguments do, and those values become constants in the query. The query then reads $M(P,\Delta )$, using the $\Delta$ left by evaluating those arguments.

A solution assigns a value to each of the query’s named holes (?x). An assignment is a solution when some choice of values for the anonymous holes (?) puts the complete fact in $M(P,\Delta )$. An anonymous hole therefore requires a value to exist, but the solution does not record which value it was. Writing $\mathrm{sols}(q,S)$ for the set of solutions to $q$ in $S$, and using the catalogue above:

A hole named twice is one variable, so before(?c, ?c) asks for a course that comes before itself. requires(?c, ?) has four matching facts but three solutions, because pl requires two courses and the assignment c = "pl" is counted once.

solutions turns the set into a list in canonical order, and ${\bar{\theta }}_i$ below is the value that solution ${\theta }_i$ contributes to the list, whose shape depends on the number of named holes, as the table below sets out:

$$\frac{\{{\theta }_1,\dots ,{\theta }_k\}=\mathrm{sols}(q,M(P,\Delta ))\text{in canonical order}}{\rho ⊢⟨\text{solutions}q,\sigma ,\Delta ⟩\Downarrow ⟨[{\bar{\theta }}_1,\dots ,{\bar{\theta }}_k],\sigma ,\Delta ⟩}(\text{E-Solutions})$$

A bare query yields whether the set is empty:

$$\frac{\mathrm{sols}(q,M(P,\Delta ))\ne \varnothing }{\rho ⊢⟨q,\sigma ,\Delta ⟩\Downarrow ⟨\text{true},\sigma ,\Delta ⟩}(\text{E-Query-True})\frac{\mathrm{sols}(q,M(P,\Delta ))=\varnothing }{\rho ⊢⟨q,\sigma ,\Delta ⟩\Downarrow ⟨\text{false},\sigma ,\Delta ⟩}(\text{E-Query-False})$$

A relational for reads the set once, from the ${\Delta }_0$ it starts with, then runs its body once per solution with the holes bound. Everything the body does to the store and to $\Delta$ passes on to the next turn:

$$\frac{\begin{array}{c}\{{\theta }_1,\dots ,{\theta }_k\}=\mathrm{sols}(q,M(P,{\Delta }_0))\text{in canonical order}\\ \rho \cup {\theta }_i⊢⟨e_b,{\sigma }_{i-1},{\Delta }_{i-1}⟩\Downarrow ⟨v_i,{\sigma }_i,{\Delta }_i⟩(1\le i\le k)\end{array}}{\rho ⊢⟨\text{for}q{e}_b,{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨(),{\sigma }_k,{\Delta }_k⟩}(\text{E-For-Query})$$

A return in the body abandons the remaining solutions, by the same convention as a for over a list.

The form of a query fixes its type, and the relation’s declaration supplies the rest. A bound argument is checked against its column, and a hole takes its column’s type. T-Solutions and T-For-Query take T-Query as a premise, so all three look up the relation and check bound arguments the same way:

$$\frac{q=R(a_1,\dots ,a_n)R:(\vec{\tau })\Gamma ⊢a_i:{\tau }_i\text{for each bound }{a}_i}{\Gamma ⊢q:\text{Bool}}(\text{T-Query})$$

$$\frac{\Gamma ⊢q:\text{Bool}q\text{holes }?x_{j_1},\dots ,?x_{j_k}\text{at types }{\tau }_{j_1},\dots ,{\tau }_{j_k}}{\Gamma ⊢\text{solutions}q:[({\tau }_{j_1},\dots ,{\tau }_{j_k})]}(\text{T-Solutions})$$

$$\frac{\Gamma ⊢q:\text{Bool}q\text{holes }?x_{j_1},\dots ,?x_{j_k}\text{at types }{\tau }_{j_1},\dots ,{\tau }_{j_k}\Gamma ,x_{j_1}:{\tau }_{j_1},\dots ,x_{j_k}:{\tau }_{j_k}⊢e_b:()}{\Gamma ⊢\text{for}q{e}_b:()}(\text{T-For-Query})$$

In these rules, $?x_{j_1},\dots ,?x_{j_k}$ are the query’s distinct named holes, in order of first appearance. solutions before(?c, ?c) has one named hole, so its type is [String]. A hole named twice takes the type of both columns, so they must agree: r(?x, ?x) on a relation of (Int, String) is a type error.

The number of named holes fixes the shape of each element in E-Solutions and T-Solutions:

solutions cost(course, ?p, ?n) therefore has type [(String, Int)], which is why the lambda in credits_needed can read row.1 as an Int. Only T-For-Query extends the context. In the other two forms a hole’s name goes nowhere.

Bridger’s query forms

From the host into a query

An argument is the route from a local into a query. cost(course, ?p, ?n) evaluates course where the query is asked and looks for facts with that value in the first column. A rule sees only top-level names, because its meaning has to be the same at every query site. The argument is evaluated before $M(P,\Delta )$ is read, and that value is the only thing the query takes from its surroundings, so one rule set can answer credits_needed for any course.

A for evaluates its arguments once, however many solutions follow. In this program, next prints a line and returns one more than it did the last time, starting from 1:

relation e : (Int);

ref calls = 0;

fn next() -> Int {
    calls := deref calls + 1;
    println("next");
    deref calls
}

fn main() {
    add e(1);
    add e(2);
    add e(3);
    for e(?x) { if x == next() { println(x); } }
    for e(next()) { println("hit"); }
}

The first loop calls next once per turn. next returns 1, 2, and 3, each matching x, so the program prints next and the value three times. The second loop calls next once, printing next a fourth time. Its query is e(4), which has no solution, so its body never runs.

A hole always introduces a new name. In the following code, the second argument is the local c and the first is a new variable of the same name:

let c = "pl";
println(solutions before(?c, c));
for before(?c, c) { println(c); }
println(c);

This prints the three courses before pl as a list, then the same three on separate lines, then pl. Inside the body, the hole’s c shadows the local, and after the body the local is visible again.

A hole-free query looks exactly like a function call, and the parser treats it as one. It becomes a query when its callee evaluates to a relation, which adds a case to E-App. Name resolution works as it does for any other name. If a local shadows a relation, as let before = |a: Int, b: Int| a + b; does, then before(1, 2) is an ordinary call inside that scope, and solutions before(?x, 2) is rejected because before no longer names a relation. A relation’s name is not otherwise a value, so let r = before; is rejected.

Holes bind only in a for

A bare query answers yes or no, and its holes bind nothing, so this program is rejected at println(c), where c is an unbound variable:

if before(?c, ?c) { println(c); }

A query can have any number of solutions, so a binding here would have to pick one, and nothing in the else branch or under a not could use it. A program that wants one of the solutions asks for the list. The first in canonical order is head(solutions before(?c, ?c)), an Option that unwrap_or opens for now and pattern matching opens in Part VIII.

Walking a fixed set

E-For-Query computes the solutions once, before the first turn, and the body’s changes to $\Delta$ do not alter that list. Queries inside the body read the current $\Delta$, however. friend below starts with two facts, and the body adds each one’s reverse:

relation friend : (Int, Int);

fn main() {
    add friend(1, 2);
    add friend(2, 3);
    for friend(?a, ?b) {
        add friend(b, a);
        println(len(solutions friend(?x, ?y)));
    }
    println(solutions friend(?a, ?b));
}

This prints 3, 4, and then [(1, 2), (2, 1), (2, 3), (3, 2)]. The walk made two turns, for the two facts it started with. The reversed facts it added were visible to the inner query but did not join the walk. A clear in the body behaves the same way: with e holding 1, 2, and 3, for e(?x) { clear e; println(x); } prints all three values and leaves e empty.

Here add cannot make a loop run longer. With n declared as relation n : (Int);, this loop adds a larger number for each fact, a step a rule may not take, and it ends after two turns, printing [1, 2, 11, 12]:

add n(1);
add n(2);
for n(?x) { add n(x + 10); }
println(solutions n(?x));

The value of solutions is an ordinary list, so it holds the answer from the moment of the query. In let found = solutions e(?x); add e(4);, found keeps its old contents, and a new query sees the new fact.

From a query into the host

The answer to solutions can be handed to any function that takes a list, so a count is len, a sum is fold, and a largest value is maximum. Asking about each course in turn gives the effect of a SQL GROUP BY:

map(solutions credits(?c, ?), |c| (c, credits_needed(c)))

which is

[("compilers", 14), ("data_structures", 4), ("discrete", 0),
 ("intro", 0), ("pl", 11)]

The two totals in the opening program come from what the holes keep. cost("compilers", ?p, ?n) has four solutions, since each assignment names a course:

[("data_structures", 4), ("discrete", 3), ("intro", 4), ("pl", 3)]

cost("compilers", ?, ?n) names only n, and there are only two distinct assignments to it, 3 and 4. Dropping ?p removed the values that made the four rows different, so the fold over [3, 4] computes 7. Both programs type-check, and both run without error.

Working across the boundary

A degree plan needs a value no rule can compute. A course’s earliest semester is 1 when it requires nothing, and otherwise one more than the latest semester among the courses it requires. semester(c, n) holds the result, ready(c) is true when c has no semester yet and all that it requires have one, and each pass of schedule’s while assigns one semester’s courses:

relation semester : (String, Int);

fn ready(c: String) -> Bool =
    not semester(c, ?)
        and filter(solutions requires(c, ?p), |p| not semester(p, ?)) == [];

fn schedule() {
    clear semester;
    ref n = 1;
    while len(solutions semester(?c, ?)) < len(solutions credits(?c, ?)) {
        for c in filter(solutions credits(?c, ?), ready) {
            add semester(c, deref n);
        }
        n := deref n + 1;
    }
}

fn main() {
    load([("intro", 4, []),
          ("discrete", 3, []),
          ("data_structures", 4, ["intro"]),
          ("pl", 3, ["data_structures", "discrete"]),
          ("compilers", 3, ["pl"])]);

    if before(?c, ?c) {
        println("the catalogue has a cycle");
    } else {
        schedule();
        println(solutions semester(?c, ?t));
    }
}

It prints:

[("compilers", 4), ("data_structures", 2), ("discrete", 1), ("intro", 1), ("pl", 3)]

Rules compute before to any depth and always stop, even over a cycle. not tests for absence, which a rule may not do, and deref n puts a computed integer into a fact, which a rule may not do either. schedule is also a loop to a fixpoint, like the rounds of Evaluating relations, but written by hand, and none of the guarantees about rules apply to it. Without the check in main, add requires("intro", "compilers") would leave compilers, data_structures, intro, and pl never ready. The while would run forever, while before(?c, ?c) still answers at once.

ready asks queries, so it is impure, and a rule’s filter could not call it, but host code can. The facts in semester are a snapshot as well: an add requires(…) after schedule() leaves semester as it was, until schedule() runs again.

Building it

The remaining cases of eval_expr rest on the solutions method from Evaluating relations. The arms call it and read the substitutions it returns, and it evaluates a query’s arguments itself, so an arm must not evaluate them as well.

The Rel::Query case of the Relation arm implements E-Query-True and E-Query-False. The Solutions case implements E-Solutions. It works out the query’s named holes, each distinct name once, in order of first appearance, then builds one value per substitution: () for no named holes, the bound value for one, and a tuple in hole order for more. The substitutions are already in canonical order.

The ForQuery arm is the second walk promised in Conditionals and loops, over this node from the AST:

Expr::ForQuery(Query, Box<Expr>, Span)

It takes the list of substitutions once. For each one, it extends the environment at the for with the substitution’s bindings, using Subst::iter, and runs the body, discarding the value. A Control::Return from the body passes straight out. The arm yields Value::Unit.

The Call arm from Evaluating function calls gains the case that section promised. Evaluate the callee first, as before. If the result is a Value::Relation, wrap the unevaluated arguments as QArg::Exprs and treat the call as a hole-free query with that name.

The type checker needs the matching arms, in types/check.rs. T-Query, T-Solutions, and T-For-Query look up the relation’s column types, check each bound argument against its column, and give each hole its column’s type. The language reference lists the stuck states.

The design space

How a query reaches the database

A call-level interface such as Java’s JDBC passes a query as a string:

String sql = "SELECT anc FROM ancestor WHERE des = '" + name + "'";
ResultSet rows = statement.executeQuery(sql);
while (rows.next()) { System.out.println(rows.getString("anc")); }

The Java compiler sees two strings and a variable. A misspelled column surfaces when the line runs, and getString picks a result by a name and a type that nothing has checked. Because name is pasted into the query’s text, a name containing a quote can change what the query says, which is the mechanism of SQL injection. Parameterized queries address that by passing values separately from the text, as Bridger’s arguments do.

A program can also build a string while it runs. A search form with optional criteria can add a WHERE clause for each box the user filled in. Bridger’s query has its shape fixed in the source: which relation it reads and which columns are holes cannot depend on a value, so a program with several shapes writes each one. Cook and Ibrahim conjecture that the lack of such dynamic queries is the main reason most forms of embedded SQL were abandoned. LINQ’s query operators are ordinary method calls, so a program can decide at run time whether to apply one, and the result is still type-checked.

Relations as values

let r = before; is an error in Bridger, and every query reads the one global $\Delta$. A function taking no parameters can therefore return a different answer after an add, as it could after a write to a global ref. Two families at once need an extra column saying which family a fact belongs to, and clear resets a relation for every part of the program that uses it.

Flix makes Datalog programs values. Madsen and Lhoták’s paper shows a function returning sets of facts and rules, which the program combines with <+>, passes to solve, and then narrows with project:

let facts = getParents() <+> getAdoptions();
let model = solve(facts <+> heritage(withAdoptions));
project AncestorOf model

A program can hold two sets of facts at once, and it can choose its rules at run time, as heritage does here with a Bool. The price is in the type system, which uses row polymorphism to describe a fragment of a program that mentions only some relations. Combining fragments at run time can also produce recursion through negation, which their design has to detect at compile time. Bridger’s rules are fixed when the program is written, which lets the checks on rule bodies run once before main, and leaves one closure to reuse between changes to $\Delta$.

Changing facts during a walk

In the 1995 reunion of the System R team, Pat Selinger and Don Chamberlin recalled a bug from 1976 or 1977. An update meant to give a raise to low-paid employees was scanning those employees through an index on salary. Each raise moved a row further along the index, where the scan met it again. By Chamberlin’s account, a ten percent raise for everyone under 25,000 dollars finished without error with everyone earning 25,000. The team discussed it at a meeting that happened to fall on Halloween, and it has been the Halloween problem ever since. Database systems now keep an update’s rows apart from the scan that finds them, which is the effect E-For-Query specifies.

Other languages decide this differently. Python detects the change and stops: adding a key while iterating over a dictionary raises RuntimeError with dictionary changed size during iteration. Prolog systems settled on what Lindholm and O’Keefe called the logical view of a changing database, in which a goal already running keeps seeing the clauses that existed when it started, which is close to Bridger’s rule. If a Bridger walk included new facts, for n(?x) { add n(x + 10); } would never end. A program that wants a fixpoint in host code writes a while, as schedule does, and the while is where the program can fail to stop.

Computing all of it

A Bridger query computes its whole answer. before("discrete", "compilers") could stop at its first derivation, and first_big below could stop at the first large value. Instead, each computes the closure and sorts the full list before the first turn or the first true:

fn first_big(limit: Int) -> Int {
    for e(?x) { if x > limit { return x; } }
    -1
}

A SQL cursor can deliver rows as the engine finds them, without waiting for the rest of the answer. Prolog finds one solution at a time and looks for the next on backtracking, and once stops after the first. Both make an early exit cheaper, though SQL’s rows have no guaranteed order without ORDER BY, and Prolog’s solutions come in the order of its search. A sorted list that does not depend on evaluation strategy has to exist in full before the first element is known. Cost semantics counts what that costs.

Sets or bags

Relations in Codd’s model are sets, but SQL tables and query results can hold duplicate rows. The same four credit values in a SQLite table give different answers depending on what the query asks for: SELECT SUM(x) gives 14, and SELECT SUM(DISTINCT x) gives 7. SQL’s default keeps a row per match, so a sum needs no key column, and a query that lists values can repeat them until DISTINCT removes them. Prolog offers both: findall keeps one answer per proof, and setof sorts its answers and removes duplicates.

Bridger’s answers are always sets. The meaning of a query stays a set of facts, and a list of solutions never reflects how many derivations a fact had or the order they were found. The cost appears in the opening program: a sum across the four courses has to keep the course among its named holes, or courses with the same credits collapse into one solution.

Further reading

The mismatch: Cook and Ibrahim’s “Integrating Programming Languages & Databases: What’s the Problem?” sets out criteria for a solution and evaluates persistent languages, object-relational mappers, call-level interfaces, and embedded queries against them.

System R: Chamberlin and colleagues’ “A History and Evaluation of System R” (1981) covers its phases, including the interface to host languages. The 1995 reunion transcript is the team’s own conversation about the project, the Halloween problem among much else.

Queries inside a language: Jarke and Schmidt’s working paper (1982) describes Pascal/R’s selections and how to evaluate them efficiently. Meijer, Beckman, and Bierman’s “LINQ” (2006) is a short summary of the .NET design.

Datalog as a value: Madsen and Lhoták’s “Fixpoints for the Masses” (2020) gives a lambda calculus with first-class Datalog constraints, its type system, and a soundness proof. A copy is on the author’s page.

Concept checks