Fixpoints

A unique feature of Flix is its built-in support for fixpoint computations on constraint on relations and constraint on lattices.

We assume that the reader is already familiar with Datalog and focus on the Flix specific features.

Using Flix to Solve Constraints on Relations

We can use Flix to solve a fixpoint computation inside a function.

For example, given a set of edges s, a src node, and dst node, compute if there is a path from src to dst. We can elegantly solve this problem as follows:

def isConnected(s: Set[(Int32, Int32)], src: Int32, dst: Int32): Bool =
    let rules = #{
        Path(x, y) :- Edge(x, y).
        Path(x, z) :- Path(x, y), Edge(y, z).
    };
    let edges = inject s into Edge;
    let paths = query edges, rules select true from Path(src, dst);
    not (paths |> Array.isEmpty)

def main(): Unit & Impure =
    let s = Set#{(1, 2), (2, 3), (3, 4), (4, 5)};
    let src = 1;
    let dst = 5;
    if (isConnected(s, src, dst)) {
        println("Found a path between \${src} and \${dst}!")
    } else {
        println("Did not find a path between \${src} and \${dst}!")
    }

The isConnected function behaves like any other function: We can call it with a set of edges (Int32-pairs), an Int32 source node, and an Int32 destination node. What is interesting about isConnected is that its implementation uses a small Datalog program to solve the task at hand.

In the isConnected function, the local variable rules holds a Datalog program fragment that consists of two rules which define the Path relation. Note that the predicate symbols, Edge and Path do not have to be explicitly introduced; they are simply used. The local variable edges holds a collection of edge facts that are obtained by taking all the tuples in the set s and turning them into Edge facts. Next, the local variable paths holds the result of computing the fixpoint of the facts and rules (edges and rules) and selecting the Boolean true if there is a Path(src, dst) fact. Note that here src and dst are the lexically-bound function parameters. Thus, paths is either an empty array (no paths were found) or a one-element array (a path was found), and we simply return this fact.

Flix is strongly typed. Any attempt to use predicate symbol with terms of the wrong type (or with the wrong arity) is caught by the type checker. Note also that Flix supports type inference, hence we did not have to declare the type of Edge nor of Path.

Stratified Negation

Flix supports stratified negation which allow restricted use of negation in rule bodies. For example:

def main(): Unit & Impure =
    let movies = #{
        Movie("The Hateful Eight").
        Movie("Interstellar").
    };
    let actors = #{
        StarringIn("The Hateful Eight", "Samuel L. Jackson").
        StarringIn("The Hateful Eight", "Kurt Russel").
        StarringIn("The Hateful Eight", "Quentin Tarantino").
        StarringIn("Interstellar", "Matthew McConaughey").
        StarringIn("Interstellar", "Anne Hathaway").
    };
    let directors = #{
        DirectedBy("The Hateful Eight", "Quentin Tarantino").
        DirectedBy("Interstellar", "Christopher Nolan").
    };
    let rule = #{
        MovieWithoutDirector(title) :-
            Movie(title),
            DirectedBy(title, name),
            not StarringIn(title, name).
    };
    query movies, actors, directors, rule
        select title from MovieWithoutDirector(title) |> println

The program defines three local variables that contain information about movies, actors, and directors. The local variable rule contains a rule that captures all movies where the director does not star in the movie. Note the use negation in this rule. The query returns an array with the string "Interstellar" because Christopher Nolan did not star in that movie.

Design Note

Flix enforces that programs are stratified, i.e. a program must not have recursive dependencies on which there is use of negation. If there is, the Flix compiler rejects the program.

Programming with First-class Constraints

A unique feature of Flix is its support for first-class constraints. A first-class constraint is a value that can be constructed, passed around, composed with other constraints, and ultimately solved. The solution to a constraint system is another constraint system which can be further composed. For example:

def getParents(): #{ ParentOf(String, String) | r } = #{
    ParentOf("Pompey", "Strabo").
    ParentOf("Gnaeus", "Pompey").
    ParentOf("Pompeia", "Pompey").
    ParentOf("Sextus", "Pompey").
}

def getAdoptions(): #{ AdoptedBy(String, String) | r } = #{
    AdoptedBy("Augustus", "Caesar").
    AdoptedBy("Tiberius", "Augustus").
}

def withAncestors(): #{ ParentOf(String, String),
                        AncestorOf(String, String) | r } = #{
        AncestorOf(x, y) :- ParentOf(x, y).
        AncestorOf(x, z) :- AncestorOf(x, y), AncestorOf(y, z).
}

def withAdoptions(): #{ AdoptedBy(String, String),
                        AncestorOf(String, String) | r } = #{
    AncestorOf(x, y) :- AdoptedBy(x, y).
}

def main(): Unit & Impure =
    let c = false;
    if (c) {
        query getParents(), getAdoptions(), withAncestors()
            select (x, y) from AncestorOf(x, y) |> println
    } else {
        query getParents(), getAdoptions(), withAncestors(), withAdoptions()
            select (x, y) from AncestorOf(x, y) |> println
    }

The program uses three predicate symbols: ParentOf, AncestorOf, and AdoptedBy. The getParentsfunction returns a collection of facts that represent biological parents, whereas the getAdoptions function returns a collection of facts that represent adoptions. The withAncestors function returns two constraints that populate the AncestorOf relation using the ParentOf relation. The withAdoptions function returns a constraint that populates the ParentOf relation using the AdoptedBy relation.

In the main function the local variable c controls whether we query a Datalog program that only considers biological parents or if we include adoptions.

As can be seen, the types the functions are row-polymorphic. For example, the signature of getParents is def getParents(): #{ ParentOf | r } where r is row polymorphic type variable that represent the rest of the predicates that the result of the function can be composed with.

Design Note

The row polymorphic types are best understood as an over-approximation of the predicates that may occur in a constraint system. For example, if a constraint system has type #{ A(String), B(Int32, Int32) } that does necessarily mean that it will contain facts or rules that use the predicate symbols A or B, but it does guarantee that it will not contain any fact or rule that refer to a predicate symbol C.

Polymorphic First-class Constraints

Another unique feature of Flix is its support for first-class polymorphic constraints. That is, constraints where one or more constraints are polymorphic in their term types. For example:

def edgesWithNumbers(): #{ LabelledEdge(String, Int32 , String) | r } = #{
    LabelledEdge("a", 1, "b").
    LabelledEdge("b", 1, "c").
    LabelledEdge("c", 2, "d").
}

def edgesWithColor(): #{ LabelledEdge(String, String, String) | r } = #{
    LabelledEdge("a", "red", "b").
    LabelledEdge("b", "red", "c").
    LabelledEdge("c", "blu", "d").
}

def closure(): #{ LabelledEdge(String, l, String),
                  LabelledPath(String, l, String) } with Boxable[l] = #{
    LabelledPath(x, l, y) :- LabelledEdge(x, l, y).
    LabelledPath(x, l, z) :- LabelledPath(x, l, y), LabelledPath(y, l, z).
}

def main(): Unit & Impure =
    query edgesWithNumbers(), closure()
        select (x, l, z) from LabelledPath(x, l, z) |> println;
    query edgesWithColor(), closure()
        select (x, l, z) from LabelledPath(x, l, z) |> println

Here we use two predicate symbols: LabelledEdge and LabelledPath. Each predicate has a type parameter named l and is polymorphic in the "label" type associated with the edge/path. Note how edgesWithNumbers returns a collection of edge facts where the labels are integers, whereas edgesWithColor returns a collection of facts where the labels are strings. The closure function is polymorphic and returns two rules that compute the transitive closure of edges that have the same label.

The Flix type system ensures that we cannot accidentally mix edges (or paths) with different types of labels.

Design Note

The Boxable type class constraint simply requires that each label type has Eq, Order, and ToString instances.

Injecting Facts into Datalog

Flix provides a flexible mechanism that allows functional data structures (such as lists, sets, and maps) to be converted into Datalog facts.

For example, given a Flix list of pairs we can convert it to a collection of Datalog facts:

let l = (1, 2) :: (2, 3) :: Nil;
let p = inject l into Edge;

where l has type List[(Int32, Int32)]. The inject expression converts l into a Datalog constraint set p of type #{ Edge(Int32, Int32) | ... }.

The inject expression works with any type that implements the Foldable type class. Consequently, it can be used with lists, sets, maps, and so forth.

The inject expression can operate on multiple collections simultaneously. For example:

let names = "Lucky Luke" :: "Luke Skywalker" :: Nil;
let jedis = "Luke Skywalker" :: Nil;
let p = inject names, jedis into Name, Jedi;

where p has type #{ Name(String), Jedi(String) | ... }.

Pipelines of Fixpoint Computations

The solution (i.e. fixpoint) of a constraint system is another constraint system. We can use this to construct pipelines of fixpoint computations, i.e. to feed the result of one fixpoint computation into another fixpoint computation. For example:

def main(): Unit & Impure =
    let f1 = #{
        ColorEdge(1, "blue", 2).
        ColorEdge(2, "blue", 3).
        ColorEdge(3, "red", 4).
    };
    let r1 = #{
        ColorPath(x, c, y) :- ColorEdge(x, c, y).
        ColorPath(x, c, z) :- ColorPath(x, c, y), ColorEdge(y, c, z).
    };
    let r2 = #{
        ColorlessPath(x, y) :- ColorPath(x, _, y).
    };
    let m = solve f1, r1 inject ColorPath;
    query m, r2 select (x, y) from ColorlessPath(x, y) |> println

The program uses three predicates: ColorEdge, ColorPath, and ColorlessPath. Our goal is to compute the transitive closure of the colored edges and then afterwards construct a graph where the edges have no color.

The program first computes the fixpoint of f1 and r1 and injects out the ColorPath fact. The result is stored in m. Next, the program queries m and r2, and selects all ColorlessPath facts.

Using Flix to Solve Constraints on Lattices

Flix supports not only constraints on relations, but also constraints on lattices. To create such constraints, we must first define the lattice operations (the partial order, the least upper bound, and so on) as functions, associate them with a type, and then declare the predicate symbols that have lattice semantics.

We begin with the definition of the Sign data type:

enum Sign {
              case Top,

    case Neg, case Zer, case Pos,

              case Bot
}

We need to define the usual Eq, Order, and ToString instances for this new type. Note that the order instance is unrelated to the partial order instance we will later define, and is simply used to sort elements for pretty printing etc.

instance Boxable[Sign]

instance Eq[Sign] {
    pub def eq(x: Sign, y: Sign): Bool = match (x, y) {
        case (Bot, Bot) => true
        case (Neg, Neg) => true
        case (Zer, Zer) => true
        case (Pos, Pos) => true
        case (Top, Top) => true
        case _          => false
    }
}

instance Order[Sign] {
    pub def compare(x: Sign, y: Sign): Comparison =
        let num = w -> match w {
            case Bot => 0
            case Neg => 1
            case Zer => 2
            case Pos => 3
            case Top => 4
        };
        num(x) <=> num(y)
}

instance ToString[Sign] {
    pub def toString(x: Sign): String = match x {
        case Bot => "Bot"
        case Neg => "Neg"
        case Zer => "Zer"
        case Pos => "Pos"
        case Top => "Top"
    }
}

With these type class instances in place, we can now define the lattice operations on Sign.

We define the bottom element and the partial order:

instance LowerBound[Sign] {
    pub def minValue(): Sign = Bot
}

instance PartialOrder[Sign] {
    pub def lessEqual(x: Sign, y: Sign): Bool =
        match (x, y) {
            case (Bot, _)   => true
            case (Neg, Neg) => true
            case (Zer, Zer) => true
            case (Pos, Pos) => true
            case (_, Top)   => true
            case _          => false
        }
}

Next, we define the least upper bound and greatest lower bound:

instance JoinLattice[Sign] {
    pub def leastUpperBound(x: Sign, y: Sign): Sign =
        match (x, y) {
            case (Bot, _)   => y
            case (_, Bot)   => x
            case (Neg, Neg) => Neg
            case (Zer, Zer) => Zer
            case (Pos, Pos) => Pos
            case _          => Top
        }
}

instance MeetLattice[Sign] {
    pub def greatestLowerBound(x: Sign, y: Sign): Sign =
        match (x, y) {
            case (Top, _)   => y
            case (_, Top)   => x
            case (Neg, Neg) => Neg
            case (Zer, Zer) => Zer
            case (Pos, Pos) => Pos
            case _          => Bot
        }
}

With all of these definitions we are ready to write Datalog constraints with lattice semantics. But before we proceed, let us also write a single monotone function:

def sum(x: Sign, y: Sign): Sign = match (x, y) {
    case (Bot, _)   => Bot
    case (_, Bot)   => Bot
    case (Neg, Zer) => Neg
    case (Zer, Neg) => Neg
    case (Zer, Zer) => Zer
    case (Zer, Pos) => Pos
    case (Pos, Zer) => Pos
    case (Pos, Pos) => Pos
    case _          => Top
}

We can now finally put everything to use:

pub def main(): Unit & Impure =
    let p = #{
        LocalVar("x"; Pos).
        LocalVar("y"; Zer).
        LocalVar("z"; Neg).
        AddStm("r1", "x", "y").
        AddStm("r2", "x", "y").
        AddStm("r2", "y", "z").
        LocalVar(r; sum(v1, v2)) :-
            AddStm(r, x, y), LocalVar(x; v1), LocalVar(y; v2).
    };
    query p select (r, v) from LocalVar(r; v) |> println

Warning

Note the careful use of ; to designate lattice semantics.