Path(x, y), Edge(y, z). The minimal model of the facts and rules is: Edge(1, 2). Edge(2, 3). Edge(3, 4). Path(1, 2). Path(2, 3). Path(3, 4). Path(1, 3). Path(1, 4). Path(2, 4). In Flix, Datalog programs are values. The above program can be embedded in Flix as follows: def main(): #{Edge(Int, Int), Path(Int, Int)} = let f = #{ Edge(1, 2). Edge(2, 3). Edge(3, 4). }; let p = #{ Path(x, y) :- Edge(x, y). Path(x, z) :- Path(x, y), Edge(y, z). }; solve f <+> p The local variable f holds a Datalog program value that consists of the edge facts. Similarly, the local variable p is a Datalog program value that consists of the two rules. The f <+> p expression computes the composition (i.e. union) of the two Datalog programs f and p. The solve expression computes the minimal model of the combined Datalog program, returning the edge and path facts shown above. Since Datalog programs are first-class values, we can refactor the above program into several functions. For example: def edges(): #{Edge(Int, Int), Path(Int, Int)} = #{ Edge(1, 2). Edge(2, 3). Edge(3, 4). } def closure(): #{Edge(Int, Int), Path(Int, Int)} = #{ Path(x, y) :- Edge(x, y). Path(x, z) :- Path(x, y), Edge(y, z). } def main(): #{Edge(Int, Int), Path(Int, Int)} = solve edges() <+> closure() The un-directed closure of the graph can be computed by adding the rule: Path(x, y) :- Path(y, x). We can modify the closure function to take a Boolean argument that determines whether we want to compute the directed or un-directed closure: def closure(directed: Bool): #{Edge(Int, Int), Path(Int, Int)} = let p1 = #{ Path(x, y) :- Edge(x, y). Path(x, z) :- Path(x, y), Edge(y, z). }; let p2 = #{ Path(y, x) :- Path(x, y). }; if (directed) p1 else (p1 <+> p2) Type-safe composition The Flix type system ensures that Datalog program values are well-typed. For example, the following program fragment does not type check: let p1 = Edge(123, 456).; let p2 = Edge("a", "b").; p1 <+> p2; because in p1 the type of the Edge predicate is Edge(Int, Int) whereas in p2 it has type Edge(String, String). The Flix compiler rejects such programs as ill-typed. Stratified negation The Flix compiler ensures that every Datalog program value constructed at run-time is stratified. Stratification is important because it guarantees the existence of a unique minimal model in the presence of negation.