Last month I gave a talk at FLOPS about finite functional programming or ‘λFS’, my latest attempt (previously: Datafun) to combine functional programming with relational programming à la Datalog or SQL – and tensor algebra too, because why not?
In λFS, a relation R is treated as a function: we let R(x) = true iff x is in R, false otherwise. This function is finite in that R(x) = true for only finitely many inputs x: these are its support. The paper gives a type system for ensuring functions have finite support. At runtime, we represent a finite boolean function by tabulating its support in a hash table or a balanced tree (like a table in a database).
This generalizes beyond booleans to any codomain with a ‘default’ value. A function’s support are those inputs whose output is non-default; for instance, the booleans with false as default, or the integers with 0 as default. A finite function can then be represented as a key-value table whose keys are the function’s support; any other key implicitly maps to the default value. Non-boolean finite maps arise naturally as the result of aggregations, while tensor algebra is essentially relational algebra over non-boolean (usually real-valued) finite maps.
Nontermination and evaluation order
In the talk, I mentioned that recursion was future work for λFS. Naturally, someone – I think it was Atsushi Igarashi – asked what the difficulty was. The primary difficulty is that recursion allows nontermination. Semantics for nontermination usually use domain theory, which has fallen out of fashion in recent decades, and which consequently I’ve never deeply studied and find a bit intimidating.1
Moreover, as soon as nontermination or any effect is involved, there is a question of evaluation order. Even in the untyped lambda calculus, where evaluation is confluent, call-by-name and call-by-value evaluation terminate on different programs. What’s worse, in relational languages ‘evaluation order’ has a more expansive meaning than in functional languages. Consider this example:
R, S : nat => bool -- finitely supported; tables
test : nat -> bool -- not finitely supported; a procedure
Q : nat => bool -- finitely supported; a table
Q(x) = R(x) and test(x) and S(x)
Here, => denotes a finite function, represented as a table, while -> denotes an arbitrary function, represented by a procedure or closure. Thinking relationally, our query Q is the intersection of the tables R and S, filtered by the black-box predicate test.
The central question is: in what order do we evaluate this query? We could go left-to-right: for each x in R, if test(x) passes, check if x is in S. In Python:
[x for x in R if test(x) if x in S]
Or, noting that test may be expensive but looking up an entry in a table is cheap, we could check if x is in S before calling test:
[x for x in R if x in S if test(x)]
And if we happen to know S is much smaller than R, we can save a lot of time by iterating over S instead of R:
[x for x in S if x in R if test(x)]
The standard relational philosophy regards evaluation order as an implementation detail, decided by the query planner. However, this ordering may affect whether Q terminates, because different orders call test on different arguments. A contrived example:
R = {"hello", "world"}
S = {"hello", "alice"}
test(x) = x == "hello" or loop-forever()
Q(x) = R(x) and test(x) and S(x)
Left-to-right execution calls test("hello"), which succeeds, followed by test("world"), which loops forever. But if we intersect R and S before calling test, we only test "hello" and so terminate.
I have expressed this problem in λFS, but it arises in any SQL or Datalog engine supporting user-defined functions, and exposes a tension between typical DB and PL assumptions:
DB The query engine may choose the execution strategy to optimize performance.
PL We can reason compositionally about program behavior – in particular, about termination or execution time.
λFS tries to bridge DB and PL, and gets stuck in the awkward middle: I must either favor one perspective over another, or find a way to thread the needle’s eye. I do not yet know how best to do this. Instead, here are three directions forward – three sketches of possible semantics for λFS with recursion (or Datalog with nonterminating functions).
1 Left to right evaluation has a simple cost model
The simplest strategy to implement also has the most straightforward semantics: evaluate from left to right. This is the most typical PL approach: it avoids query planning and puts the job squarely in the hands of the programmer. This makes the execution time of a query easy to predict and reason about, as my friend Rob Simmons pointed out to me while working on Finite Choice Logic Programming; this is more or less the cost model of Dusa, an implementation of FCLP.
In this approach, a conjunction of n terms turns into at most n nested loops. For instance, R(x) and S(y) becomes 2 loops:
for x in R:
for y in S:
yield (x,y)
In a query like R(x) and S(x), where the variables of S(x) are already entirely grounded, we generate a test rather than a loop:
for x in R:
if x not in S: continue
yield x
If some but not all variables of a conjunct are grounded, we need an index; for example, to run R(x,y) and S(y,z), we want to index S by y:
for x,y in R:
for z in S_index[y]: -- assuming an appropriate S_index
yield (x,y,z)
If we have these indexes and all our conjuncts are applications of finite maps, the cost model is simple: count the prefix firings. That is, for every prefix of the conjunction, count how many assignments of its free variables satisfy it. So for R(x,y) and S(y,z), we add together:
- The number of
x,ytuples satisfyingR(x,y). - The number of
x,y,ztuples satisfyingR(x,y) and S(y,z).
What about black-box predicates like test(x)? For such a conjunct:
All its arguments must be grounded by the preceding conjuncts, so that when we reach it we have concrete values for them.
We add the cost of evaluating
test(x)for each firing of our preceding conjuncts. This may exceed the number of totalxvalues; for instance,R(x) and S(y) and test(x)will calltest(x)once for eachx,ypair.
This straightforwardly answers our original question about termination: we run predicates on exactly the values which satisfy their preceding conjuncts. By complete coincidence, the left-to-right grounding requirement exactly matches the type system in the finite functional programming paper; I originally regarded this as a weakness of the type system, but with a left-to-right execution strategy it makes perfect sense.
I like the simplicity and predictability of this approach, and appreciate how it ‘bites the bullet’, making the programmer responsible for performance (though this is plainly also a downside).
Unfortunately, for some queries (the cyclic queries) this makes it impossible to achieve acceptable performance – for instance, the triangle query edge(x,y) and edge(y,z) and edge(x,z).2
2 Nondeterministic evaluation order allows declarative optimizations
We’ve seen three plausible evaluation orders for R(x) and test(x) and S(x).
Why commit ourselves unnecessarily?
The typical DB approach is to give the query planner/optimizer as much leeway as possible by leaving the order of evaluation unspecified.
This means we cannot say exactly which values we will call test on, but we can bound this set above and below.
Similarly, program termination goes from a yes/no question to yes/no/maybe.
Returning to our running example, R(x) and test(x) and S(x), we can’t call test without some x value.
The only sources we have are R and S; so any query execution will call test on at most the values in either R or S, and at least the values that are in both.
If test(x) terminates for all x ∈ R ∪ S, our query terminates; if it diverges for some x ∈ R ∩ S, our query diverges; otherwise, it may go either way.
But all terminating executions should give the same result.
Unfortunately, I don’t know how to specify this nondeterminism in a compositional way. There are two typical approaches to semantics: operational and denotational.
Operationally, I’m not sure how to give semantics that correspond to bottom-up logic programming at all, let alone which capture variation in evaluation order. In particular, in λFS, how do finite λs evaluate? Normal procedural λs wait until they’re applied to an argument to reduce, but the entire point of finite functions is that they don’t do that; they’re tabled eagerly like database queries. But it’s not obvious how to capture this behavior in a small-step operational semantics. (Datafun does have an operational semantics, but only because it uses monad comprehensions, which commit to left-to-right evaluation – exactly what I want to get away from!)
Denotationally, the natural way forward would be to augment the denotational semantics outlined in the Finite Functional Programing paper with domain theory and some form of nondeterminism. Unfortunately, I’m not yet familiar enough with the domain theory of nondeterminism (powerdomains) to know how to make this work.
If you think you know an appropriate approach here, or would like to work on this together, please email me (qnrxunery@tznvy.pbz, rot13).
3 ‘Parallel and’ has the most declarative behavior
What if we could have our cake and eat it too? So far I’ve assumed that if we execute test(x) and it diverges, then our query diverges. This is why evaluation order matters: it affects which x we call test on. We can drop this assumption if we allow ourselves to think a little less sequentially.
Let ⊥ represent divergence. The typical implementation of and is sequential, examining its left argument first and short-circuiting if it yields false:
false and x = false -- short circuit; don't evaluate x
true and x = x
⊥ and x = ⊥ -- we never get around to evaluating x.
This is ugly: logical conjunction is symmetric, but this and is left-biased.
Let’s restore symmetry while preserving continuity:
false and x = false -- no need to evaluate x further
true and x = x
x and false = false -- no need to evaluate x further
x and true = x
I call this ‘parallel and’ by analogy with Plotkin’s parallel or.3
Sequential ‘and’ always fully evaluates its left argument, but parallel ‘and’ evaluates both arguments concurrently, terminating when either yields false or both yield true.
This miraculously restores determinism to λFS.
Consider our previous example:
R = {"hello", "world"}
S = {"hello", "alice"}
test x = (x == "hello") or loop-forever()
Q(x) = R(x) and test(x) and S(x)
Left-to-right execution evaluates test("world") and S("world") = ⊥ and false.
With sequential ‘and’ this diverges, but with parallel ‘and’ it is simply false.
No matter whether we iterate over R first, S first, or their intersection, we get the same intuitively correct answer: Q = {"hello"}.
Unfortunately it is not clear how to implement parallel and efficiently.
It is not inconceivable, however: miniKanren’s search strategy, for instance, resembles an implementation of parallel-or, and I have heard from Will Byrd that Andorra Prolog supported a form of conjunction analogous to parallel and. I myself had a paper at miniKanren 2025 about fair conjunction using an iterator interface for the implementation of worst-case optimal joins.
So I suspect this problem is crackable. But is it worth it?4