A Datalog-based compiler

For the past few weeks, I have been exploring the idea of writing parts of a compiler in Datalog. In this article, I’ll share what I’ve learned so far, and my eventual goal of using a Datalog system in Wipple!

What is Datalog?

In traditional procedural programming, you write code that checks conditions and updates values based on those conditions. Datalog is a different kind of programming language: it’s based on the logic paradigm, where you express programs as a series of logical rules.

There are other, more sophisticated logic-oriented languages like Prolog, but Datalog operates purely on a database of facts. A fact is a relationship between two objects. To evaluate a Datalog program, you provide some initial facts, and then run your rules to produce new facts. These facts are added to the database, and the process repeats until no new facts are generated.

Prolog and Datalog are declarative: they don’t let you describe how your program should run, only the rules themselves. These languages let you write rule-based systems extremely concisely, and you can embed them in larger programs, using each paradigm where it makes sense. The main difference between Prolog and Datalog is that in Prolog, you evaluate until a specific goal is satisfied, but in Datalog, you’re building up a database of all possible relationships.

Logic programming also requires a bit of a mindset shift — you’re always working with sets of values, not specific values. Operations in Datalog conceptually happen on all possible candidates at the same time, and there’s no way (at least not in my simple engine) to “check” for specific values. You’re describing general relationships, not conditions.

I think these characteristics of Datalog make it a great potential way to write a new typechecker for Wipple, and I’ve published a simple Datalog engine written in TypeScript on GitHub.

A simple Datalog example

Let’s write a simple system in my Datalog engine that relates the less-than (<) and greater-than (>) operations. Again, we won’t be checking if one number is less than another, we’ll be describing the rules of the system.

In our system, there are two facts and two rules:

• Fact 1: a is less than b, aka. a < b.
• Fact 2: a is greater than b, aka. a > b.
• Rule 1: If a < b and b < c, then a < c, aka. the transitive rule.
• Rule 2: If a < b, then b > a, aka. the inverse rule.

Let’s set up our facts first:

class Num {}
const lessThan = fact`${Num} < ${Num}`;
const greaterThan = fact`${Num} > ${Num}`;

In my engine, Num is purely a marker type and is never instantiated. In our system, we only care about numbers, but in systems with multiple types of objects (eg. expressions and types), this helps prevent creating facts that involve the wrong objects.

The fact`...` syntax uses a tagged template to concisely define a new, unique fact along with its description.

Next, let’s create a list of our rules:

const rules = [
    rule("transitive", (a) => {
        // ...
    }),
    rule("inverse", (a) => {
        // ...
    }),
];

rule takes a function that the engine will call with a set of candidates, represented to us with an opaque Var object. We can write queries in the body of this function to constrain the set of inputs, and eventually produce a new fact. Our transitive rule will look like this:

rule("transitive", (a) => {
    const b = lessThan(a);
    const c = lessThan(b);
    return lessThan(a, c);
}),

In my engine, a fact f is a function that you can call with one or two Vars. If you provide a single Var, a, it’s a query that produces a new Var, b, corresponding to all objects involved in the fact f(a, b). If you provide two Vars, you get back a new fact, which you can return from the rule.

Walking through the transitive rule looks like this:

1. We are given an a.
2. Find a b that is less than the a.
3. Find a c that is less than the b.
4. Declare that the a is less than the c.

When I say “Find an x”, I mean that each query creates a branch that is evaluated multiple times, once per candidate. You could think of rewriting this example as a series of flatMap operations:

const newFacts = (facts, numbers) =>
    numbers.flatMap((a) =>
        numbers
            .filter((b) => facts.contains(lessThan, a, b))
            .flatMap((b) =>
                numbers
                    .filter((c) => facts.contains(lessThan, b, c))
                    .map((c) => createFact(lessThan, a, c)),
            ),
    );

Finally, we can add our rules to a Context, along with some initial facts, and run the program:

const ctx = new Context();

const one = new Val("1");
const two = new Val("2");
const three = new Val("3");
const four = new Val("4");

ctx.add(lessThan(one, two));
ctx.add(lessThan(two, three));
ctx.add(lessThan(three, four));

ctx.run(rules);

run works by evaluating each rule in rules with the current set of facts in the context. If the rules produce at least one new combination of facts for their inputs, then they are run again. This process repeats until the system “settles”.

This “naïve” evaluation approach doesn’t scale very well, and other (but more complex) evaluation models exist. Wipple programs are typically small, but if the compiler’s performance becomes a concern, I will look into more efficient ways to evaluate the rules.

Tracing facts

Writing a concise typechecker actually isn’t my goal for using Datalog in Wipple. The greatest advantage of Datalog for Wipple is that Datalog facts can be automatically traced: you can store all the previous facts and rules used along the way. For example, if we print the context in the above example, we get output like this:

ctx.print(greaterThan(four, one));

4 > 1 (inverse)
  1 < 4 (transitive)
    1 < 2
    2 < 4 (transitive)
      2 < 3
      3 < 4

I plan to use these traces as part of a redesign of Wipple’s diagnostics, where error messages are presented as logical arguments. I think there is a lot of potential here!

I’ve written a few more examples of Datalog systems in the Wipple Datalog Engine repository. One of them is a simple typechecker — here is the output…

f num :: Int (type of function call <- type of function's output)
  f num contains function f : x -> x
  f : x -> x declares output x
  x :: Int (type of function parameter <- type of input)
    f num contains parameter num
    f num contains function f : x -> x
    num :: Int
    f : x -> x declares parameter x