Arntzenius & Krishnaswami (2016) -- Datafun: A Functional Datalog

The paper

M. Arntzenius and N. R. Krishnaswami, “Datafun: a functional Datalog,” ICFP’16: ACM SIGPLAN International Conference on Functional Programming, pp. 214–227, 2016.

doi:10.1145/2951913.2951948 · read the paper

A summary of the paper and how gen uses it.

Paper Summary

Datalog is a carefully restricted subset of Prolog that trades Turing-completeness for decidability: all queries terminate. This restriction enables bottom-up (forward-chaining) evaluation, making transitive closure and reachability queries natural to express — unlike Prolog’s depth-first top-down strategy, which struggles with such computations. Datalog has proven remarkably successful in practice: pointer analysis (Whaley & Lam), source code analysis (Semmle/.QL), business analytics (LogicBlox/LogiQL), distributed programming (Bloom), and authorization (Microsoft SecPAL). However, every real deployment extends Datalog in application-specific ways, and each extension requires re-establishing the metatheory from scratch.

Datafun addresses this by identifying the semantic essence of Datalog and embedding it into a higher-order functional language. The central insight is that Datalog’s three restrictions (constructor-freeness, range-restriction, stratified negation) collectively enforce one property: the database transformer defined by a Datalog program is a monotone function on a finite-height semilattice. Datafun makes this explicit by tracking monotonicity in its type system.

The language is a simply-typed lambda calculus extended with: (1) finite set types {A} ordered by inclusion; (2) monotone function types A +-> B distinguished from discrete (unconstrained) function types A -> B; (3) a fixed-point operator fix x is e restricted to finite semilattice eqtypes, ensuring termination; and (4) semilattice types with least element and join, generalizing empty set and union. Two variable contexts — discrete and monotone — track which variables may appear in monotone positions. The typing rules enforce monotonicity structurally: discrete function application clears the monotone context from the argument; monotone case elimination requires branches monotone in the introduced variable; the if+ rule restricts the else-branch to the semilattice bottom.

The paper demonstrates Datafun’s expressiveness through examples that span and exceed Datalog’s reach: relational algebra operations (map, filter, cross product), transitive closure (both bounded and generic), CYK parsing (impossible in Datalog due to compound data as arguments), and dataflow analyses (liveness analysis, reaching definitions). The CYK parser is particularly notable — it takes a grammar as a first-class value, something Datalog’s constructor-freeness prohibits.

The denotational semantics interprets Datafun types through three categories (Set, Poset, SemiLat) connected by two adjunctions. Types denote posets; the discrete context maps through the Disc comonad (discretizing the order), while the monotone context preserves order structure. The key decomposition Set <-> Poset <-> SemiLat via Disc/|-| and F/U is novel: the intermediate Poset category gives access to the comonad that distinguishes monotone from non-monotone computation. Fixed-point denotation uses Lemma 4: any monotone map on a finite-height pointed poset has a least fixed point computable by iterated application from the bottom element.

Formal results:

• Lemma 1-3: Semilattice types denote semilattices; finite eqtypes denote finite posets; any element of a semilattice eqtype induces a finite-height sub-poset below it.
• Lemma 4: Monotone maps on finite-height pointed posets have least fixed points computed by iteration from bottom.
• Theorems 1-3: Weakening, exchange, and both discrete and monotone substitution are admissible, with compositional semantic equations.
• Theorems 4-5: The logical relation a <= b | A is a preordered PER (partial reflexivity + transitivity).
• Theorem 6 (Termination): If a | A (the value is in the logical relation at its type), then a evaluates to a value.
• Theorem 7 (Fundamental theorem): Every well-typed term inhabits the logical relation, yielding total correctness as a corollary.

The operational semantics introduces iter forms that model fixed-point computation as iterative application with convergence checking, along with bounded variants (iter<=) that clamp to an upper bound. The termination proof uses a logical relations argument where semantic types are PERs equipped with a preorder — the syntactic counterpart of the order structure needed in the denotational semantics.

Key Concepts

• Monotonicity tracking via types. Two function types (A -> B discrete, A +-> B monotone) with separate variable contexts. The type system statically guarantees that fixed-point bodies are monotone, ensuring well-definedness and termination.

• Semilattice types as the convergence substrate. Types with a least element and join operator generalize sets. Fixed-point iteration starts from bottom and ascends monotonically through finite-height lattices. The bounded variant (fix x <= e_top is e) extends this to infinite types by clamping. The clamp is silent: on exceeding e⊤ the value is “clamped to the upper bound” and “may not have the value you expect” (§3.4.1).

• Stratified negation as post-fixpoint testing. After a fixed-point computation completes, negative information can be tested (membership negation, absence checks). This corresponds directly to Datalog’s stratified negation — non-monotone operations are permitted only on fully-computed strata.

• Higher-order abstraction over relations. Generic transitive closure (trans), parameterized parsers, and reusable dataflow analysis frameworks become possible because relations are first-class set values and functions over them are first-class.

• Three-category denotational semantics (Set, Poset, SemiLat). The novel decomposition through Poset as an intermediate category provides the Disc comonad that distinguishes monotone from non-monotone computation, enabling the fixed-point semantics.

• Convergence by finite height. Datalog guarantees termination by restricting term structure. Datafun guarantees it by restricting the type of the iterated value to have finite ascending chains. The bounded fixed-point operator extends this to infinite base types.

• Iteration-based operational semantics. Fixed points are computed by literal iteration from bottom, with convergence detected by equality testing. The iter forms make the computation state explicit.

How gen uses this

Datafun’s contribution is tracking monotonicity with types (abstract; contributions list). Nix has no type system to carry that, so gen takes Datafun’s semantic results: iteration from bottom over a finite-height semilattice converges (Lemma 4), and relational algebra plus fixed points is a query language (S3). Stratification appears in the paper as Datalog’s route to the same effect, which Datafun positions as the alternative to type tracking (S2; S3.5; S7). gen’s stratification is Datalog’s, and the Apt, Blair and Walker page covers it.

gen-graph

Monotone fixpoint iteration (S2, Lemma 4). fixpoint iterates a step function over edge maps from a seed until the edges stop changing. The semilattice is edge maps ordered by inclusion of (from, to) pairs and joined by unionEdges, which is the poset Lemma 4 takes its ascending chain over. The termination guard tests that order: a step whose output does not contain its input fails with an error naming the dropped edge. maxIter (default 1000) caps the number of rounds, and reaching it is an error. Datafun’s bounded fixed point fix x <= e_top is e bounds the value instead and clamps it silently (S3.4.1).

seededFixpoint is the semi-naive variant, which feeds each round only the new edges. The name comes from the Datalog literature. Datafun mentions semi-naive evaluation once, about Flix, in S9.

Transitive closure (S3.4). transitiveClosure iterates relational composition to a fixed point, the shape of Datafun’s trans E = fix X is E | (X . X). compose is relational composition (.) (S3.3) and unionEdges is the join |.

gen-memo

restabilize re-solves a cyclic stratum after a change by iterating each strongly connected component from bottom. For a lattice with a genuine join (union, powerset, or any finite-height bounded semilattice) Lemma 4 gives convergence at the least fixed point, detected when an iteration returns its input. gen-memo does not check that the step is monotone or that the lattice has finite height. Both are obligations on the caller, and a violation shows up as non-termination.

gen-inspect

gen-inspect compiles SQL-like queries over a graph. Datafun frames Datalog as relational algebra plus fixed points. gen-inspect follows that split: a recursive reaches relation is computed as a Horn rule program solved by gen-scope through gen-program, and WHERE, JOIN, projection, ORDER BY and LIMIT run over the resulting table.

gen-dispatch

A gen-dispatch rule can declare its stratum (group) and the kinds it produces (produces) as data, read by groupOf and producesOf without firing the rule. In Datalog a rule’s stratum is a static property of the predicates it derives, and this vocabulary makes it one.

Appendix: Follow-up Work

Unexploited Ideas

Monotone function types (S2, S4). Datafun’s distinction between A -> B and A +-> B has no analogue in gen. gen-schema’s refinement types could approximate it with a refinement that checks a function preserves an ordering on sampled inputs.

Higher-order relations as first-class values (S3.3-3.5). Datafun abstracts over relations: generic transitive closure, parameterised parsers. gen-graph’s fixpoint works on edge maps. A combinator that takes relation transformers as arguments, paralleling Datafun’s trans : {finA x finA} +-> {finA x finA}, would let users define closure operations without writing the iteration loop.

Semilattice aggregation beyond sets (S9). Datafun’s W operator generalises set union to any semilattice join. gen-scope’s folds and gen-memo’s restabilize each take a combining operation from the caller. A shared semilattice-parameterised aggregation vocabulary would unify them.

Loop reordering (S9). Datafun notes that W(x in e1) W(y in e2) e = W(y in e2) W(x in e1) e when the variables are independent. Reordering rule evaluation by independence analysis could speed convergence.

Potential New Libraries or Features

A semilattice algebra. mkSemilattice { bottom; join; eq; } with checks that join is commutative, associative and idempotent would replace ad hoc join and equality pairs across gen-graph, gen-scope and gen-memo with one algebraic structure.

Bounded fixed points are rejected. Datafun’s fix x <= e_top is e clamps a result that exceeds e_top to e_top with no error (S3.4.1: the value “may not have the value you expect”). The clamp is part of the denotational semantics (Fig. 10) and the operational semantics (Fig. 11), so no conforming implementation can make it loud. A clamped result has the same type as a correct one. gen does not build it. gen-graph’s maxIter bounds rounds instead and fails with an error when reached. Datafun’s unbounded fix has no clamp and terminates because its carrier is a structurally finite semilattice (Lemma 2, Lemma 4).

Research Directions

Incremental fixpoints. Nix’s lazy evaluation already skips unforced thunks. Explicit delta tracking across evaluations, as in Mokhov 2018’s build systems, could reduce work further for large rule sets.

Linear Datafun for retraction (S9). Removing a fact is a non-monotone operation. A linear model where certain effects consume facts could bring removal inside the convergence framework.

Static termination checks. Datafun guarantees termination statically, and gen enforces it dynamically with iteration caps and ascent guards. Static analysis of a rule dependency graph could prove termination before evaluation. gen-graph’s cycle detection applied to that graph is a starting point.