Datalog

Morel includes support for Datalog, a declarative logic programming language commonly used for program analysis, knowledge representation, and deductive databases.

Overview

Datalog extends Morel with:

• Declarative relations defined by facts and rules
• Recursive queries using stratified negation
• Semi-naive evaluation for efficient fixpoint computation
• Type-safe integration with Morel's type system

Getting Started

Basic Example

val program = ".decl edge(x:int, y:int)
edge(1, 2).
edge(2, 3).
edge(3, 4).
.output edge";

Datalog.execute program;

val it = {edge=[{x=1,y=2},{x=2,y=3},{x=3,y=4}]}
  : {edge:{x:int, y:int} list} variant

Transitive Closure

val tc = ".decl edge(x:int, y:int)
.decl path(x:int, y:int)
edge(1, 2).
edge(2, 3).
edge(3, 4).

(* Base case: direct edges are paths *)
path(X, Y) :- edge(X, Y).

(* Recursive case: paths are transitive *)
path(X, Z) :- path(X, Y), edge(Y, Z).

.output path";

Datalog.execute tc;

val it = {path=[{x=1,y=2},{x=1,y=3},{x=1,y=4},{x=2,y=3},{x=2,y=4},{x=3,y=4}]}
  : {path:{x:int, y:int} list} variant

Syntax

The syntax is based on Souffle with the following differences:

• Souffle's number type is int
• Souffle's symbol type is string
• Souffle's .input directive has one argument; Morel's has an optional second argument for the file name

Declarations

Relations must be declared before use:

.decl relation_name(param1:type1, param2:type2, ...)

Supported types:

• int - integers (mapped to Morel int)
• string - strings (mapped to Morel string)

Examples:

.decl edge(x:int, y:int)
.decl person(name:string, age:int)

Facts

Facts define base data:

edge(1, 2).
person("Alice", 30).
color(red).

Rules

Rules derive new facts from existing ones:

head(Args) :- body1(Args1), body2(Args2), ...

Components:

• Head: Single atom defining what is derived
• Body: Comma-separated atoms (conjunction)
• Variables: Must start with uppercase letter
• Constants: Numbers or quoted strings

Example:

.decl parent(p:string, c:string)
.decl ancestor(a:string, d:string)

parent("Alice", "Bob").
parent("Bob", "Carol").

(* Base case *)
ancestor(P, C) :- parent(P, C).

(* Recursive case *)
ancestor(A, D) :- ancestor(A, X), parent(X, D).

Negation

Use ! to negate atoms (requires stratification):

.decl student(name:string)
.decl graduate(name:string)
.decl undergraduate(name:string)

student("Alice").
student("Bob").
graduate("Alice").

(* Bob is a student but not a graduate *)
undergraduate(X) :- student(X), !graduate(X).

Stratification: Negation cycles are prohibited:

(* INVALID - negation cycle *)
p(X) :- edge(X, Y), !q(X).
q(X) :- edge(X, Y), !p(X).

Comparison Operators

Rules can include comparisons between variables and constants:

.decl num(n:int)
.decl small(n:int)
num(1). num(5). num(10).
small(X) :- num(X), X < 7.       (* less than *)

Supported operators:

• = - equality
• != - not equal
• < - less than
• <= - less than or equal
• > - greater than
• >= - greater than or equal

Examples:

(* Find self-loops in a graph *)
self_loop(X) :- edge(X, Y), X = Y.

(* Distinct pairs only *)
sibling(X, Y) :- parent(P, X), parent(P, Y), X != Y.

(* Ordered pairs to avoid duplicates *)
sibling(X, Y) :- parent(P, X), parent(P, Y), X < Y.

Arithmetic Expressions

Head atoms can contain arithmetic expressions:

.decl fact(n:int, value:int)
fact(0, 1).
fact(N + 1, value * (N + 1)) :- fact(N, value), N < 10.

This computes factorial values: {(0,1), (1,1), (2,2), (3,6), ...}.

Supported operators:

• + - addition
• - - subtraction
• * - multiplication

Variables in arithmetic expressions must be grounded by positive body atoms.

Input Directive

Load facts from CSV files:

.decl dept(deptno:int, dname:string, loc:string)
.input dept "data/scott/depts.csv"
.output dept

The CSV file should have a header row matching the relation's parameter names.

Output Directive

Specify which relations to return:

.output relation_name

Multiple outputs are supported:

.output edge
.output path

Comments

(* This is a block comment *)

// This is a line comment

.decl edge(x:int, y:int)  (* Inline comment *)

API

See the Datalog structure, and functions execute, translate, validate.

Datalog.execute

Executes a Datalog program and returns a variant:

Datalog.execute : string -> 'a variant

Return type:

• Single output: {relation: element_type list} variant
• Multiple outputs: {rel1: type1 list, rel2: type2 list, ...} variant
• No outputs: unit variant

Example:

val result = Datalog.execute ".decl num(n:int)
num(1). num(2). num(3).
.output num";

val result = {num=[1,2,3]} : {num:int list} variant

Datalog.validate

Validates a Datalog program and returns its type:

Datalog.validate : string -> string

Example:

Datalog.validate ".decl edge(x:int, y:int)
edge(1, 2).
.output edge";

val it = "{edge:{x:int, y:int} list}" : string

Return values:

• Success: Type representation like "{edge:{x:int, y:int} list}"
• Parse error: "Parse error: ..."
• Semantic error: "Compilation error: ..." (safety, stratification)

Datalog.translate

Translates a Datalog program to Morel source code:

Datalog.translate : string -> string option

Example:

Datalog.translate ".decl edge(x:int, y:int)
.decl path(x:int, y:int)
edge(1,2). edge(2,3).
path(X,Y) :- edge(X,Y).
path(X,Z) :- path(X,Y), edge(Y,Z).
.output path";

val it = SOME "let
  val edge = [(1, 2), (2, 3)]
  val path =
    Relational.iterate edge
      (fn (allPath, newPath) =>
        from (x, y) in newPath, (v0, z) in edge
          where y = v0 yield (x, z))
in
  {path = from (x, y) in path}
end" : string option

Datalog in Native Morel

Morel's core language can express Datalog-style deductive queries directly, without using the Datalog structure. This is possible because of two key features:

• Unbounded variables: Variables in from expressions that are not bound to a collection iterate over all values of their type
• Predicate inversion: Morel can invert predicates to generate values efficiently, rather than testing all possible values

This means Datalog-style logic programming can be intermixed with functional programming and SQL-style queries in the same program.

Correspondence

A Datalog program translates naturally to Morel:

Datalog	Morel
Relation declaration	Function returning bool
Fact r(1, 2).	(1, 2) elem facts in function body
Rule body , (and)	andalso
Multiple rules (or)	orelse
Variable	Unbounded variable in from
Existential (body variable not in head)	exists expression
Query	from with where calling predicate

Example: Transitive Closure

The Datalog transitive closure program:

.decl edge(x:int, y:int)
.decl path(x:int, y:int)
edge(1, 2).
edge(2, 3).
path(X, Y) :- edge(X, Y).
path(X, Z) :- path(X, Y), edge(Y, Z).
.output path

Corresponds to this native Morel:

let
  val edges = [(1, 2), (2, 3)]
  fun edge (x, y) = (x, y) elem edges
  fun path (x, y) =
    edge (x, y) orelse
    (exists z where path (x, z) andalso edge (z, y))
in
  from x, y where path (x, y)
end;

val it = [(1,2),(2,3),(1,3)] : (int * int) list

The key points:

• edge is a predicate function: given (x, y), returns whether that edge exists
• path is a recursive predicate combining the base case (edge) and recursive case using orelse
• The body variable z (which appears in the rule body but not the head) becomes an exists expression
• The query from x, y where path (x, y) uses unbounded variables x and y, which Morel resolves via predicate inversion

Example: Self-Loops

Find vertices with self-loops:

.decl edge(x:int, y:int)
.decl self_loop(x:int)
edge(1, 1). edge(2, 3). edge(4, 4).
self_loop(X) :- edge(X, Y), X = Y.
.output self_loop

In native Morel:

let
  val edges = [(1, 1), (2, 3), (4, 4)]
  fun edge (x, y) = (x, y) elem edges
  fun self_loop x =
    exists y where edge (x, y) andalso x = y
in
  from x where self_loop x
end;

val it = [1, 4] : int list

Mixing Paradigms

Because Datalog-style predicates are just Morel functions, you can freely mix deductive, functional, and relational code:

let
  (* Datalog-style: define reachability as a predicate *)
  val edges = [(1, 2), (2, 3), (3, 4)]
  fun edge (x, y) = (x, y) elem edges
  fun reachable (x, y) =
    edge (x, y) orelse
    (exists z where reachable (x, z) andalso edge (z, y))

  (* Functional: transform the result *)
  fun formatPair (x, y) =
    Int.toString x ^ " -> " ^ Int.toString y

  (* SQL-style: query with aggregation *)
  val summary =
    from x, y where reachable (x, y)
      group x compute c = count
in
  (* Combine all three styles *)
  from x, y where reachable (x, y)
    yield formatPair (x, y)
end;

val it = ["1 -> 2","1 -> 3","1 -> 4","2 -> 3","2 -> 4","3 -> 4"]
  : string list

When to Use Each Style

Use the Datalog structure (Datalog.execute) when:

• You have a standalone Datalog program as a string
• You want automatic semi-naive evaluation optimization
• You're working with Datalog syntax from external sources

Use native Morel predicates when:

• You want to mix deductive logic with other Morel code
• You need fine-grained control over evaluation
• You're building predicates programmatically

Both approaches use the same underlying mechanism: predicate inversion converts unbounded variable queries into efficient iteration.

Evaluation

Morel uses semi-naive evaluation for efficient fixpoint computation:

1. Initialize: Start with facts
2. Iterate: Apply rules to derive new tuples using only newly derived tuples from the previous iteration
3. Fixpoint: Stop when no new tuples are derived
4. Output: Return results for output relations

Safety Rules

All Datalog programs must be safe and stratified.

Safety

Rule: Every variable in the head must appear in a positive body atom (not inside an arithmetic expression or negated atom).

Valid:

path(X, Y) :- edge(X, Y).
path(X, Z) :- path(X, Y), edge(Y, Z).

Invalid:

(* Y appears in head but not in any positive atom *)
bad(X, Y) :- edge(X, Z).

Rationale: Unsafe rules can produce infinite results.

Stratification

Rule: No relation can depend on its own negation (directly or indirectly).

Invalid:

(* p depends on !q, q depends on !p - negation cycle *)
p(X) :- edge(X, Y), !q(X).
q(X) :- edge(X, Y), !p(X).

Rationale: Negation cycles have no well-defined semantics.

Type Checking

Datalog performs type checking on facts and rules:

Type Mismatches in Facts

Datalog.validate ".decl edge(x:int, y:int)
edge(\"hello\", 2).";

val it = "Compilation error: Type mismatch in fact edge(...):
  expected int, got string for parameter x" : string

Arity Mismatches

Datalog.validate ".decl edge(x:int, y:int)
edge(1, 2, 3).";

val it = "Compilation error: Atom edge/3 does not match
  declaration edge/2" : string

Undeclared Relations

Datalog.validate ".decl edge(x:int, y:int)
path(1, 2).";

val it = "Compilation error: Relation 'path' used in fact
  but not declared" : string

Examples

Factorial

Datalog.execute ".decl fact(n:int, value:int)
fact(0, 1).
fact(N + 1, value * (N + 1)) :- fact(N, value), N < 10.
.output fact";

val it = {fact=[{n=0,value=1},{n=1,value=1},{n=2,value=2},
  {n=3,value=6},{n=4,value=24},...]}
  : {fact:{n:int, value:int} list} variant

Ancestors

val family = ".decl parent(p:string, c:string)
.decl ancestor(a:string, d:string)
.decl descendant(p:string, d:string)

parent(\"Alice\", \"Bob\").
parent(\"Bob\", \"Carol\").
parent(\"Carol\", \"Dan\").

ancestor(P, C) :- parent(P, C).
ancestor(A, D) :- ancestor(A, X), parent(X, D).
descendant(P, D) :- ancestor(D, P).

.output ancestor
.output descendant";

Datalog.execute family;

val it = {ancestor=[...], descendant=[...]}
  : {ancestor:{a:string, d:string} list,
     descendant:{d:string, p:string} list} variant

Siblings

val siblings = ".decl parent(p:string, c:string)
.decl sibling(x:string, y:string)

parent(\"Alice\", \"Bob\").
parent(\"Alice\", \"Carol\").

(* Distinct pairs only *)
sibling(X, Y) :- parent(P, X), parent(P, Y), X != Y.

.output sibling";

Datalog.execute siblings;

val it = {sibling=[{x="Bob",y="Carol"},{x="Carol",y="Bob"}]}
  : {sibling:{x:string, y:string} list} variant

Set Difference with Negation

val diff = ".decl all(x:int)
.decl excluded(x:int)
.decl result(x:int)

all(1). all(2). all(3). all(4).
excluded(2). excluded(4).
result(X) :- all(X), !excluded(X).

.output result";

Datalog.execute diff;

val it = {result=[1,3]} : {result:int list} variant

Loading External Data

Datalog.execute ".decl adj(state:string, adjacent:string)
.decl result(state:string)
.input adj \"data/map/adjacent-states.csv\"
result(state) :- adj(state, \"FL\"), adj(state, \"TN\").
.output result";

val it = {result=["GA"]} : {result:string list} variant

Odd Cycle Detection

Datalog.execute ".decl edge(x:string, y:string)
.decl odd_path(x:string, y:string)
.decl exists_odd_cycle()

edge(\"a\", \"b\").
edge(\"b\", \"c\").
edge(\"c\", \"a\").

odd_path(X, Y) :- edge(X, Y).
odd_path(X, Y) :- odd_path(X, Z), edge(Z, U), edge(U, Y).
exists_odd_cycle() :- odd_path(X, X).

.output exists_odd_cycle";

val it = {exists_odd_cycle=[()]} : {exists_odd_cycle:unit list} variant

Best Practices

Naming Conventions

• Relations: lowercase with underscores (edge, parent_of)
• Variables: uppercase letters (X, Y, Person)
• Constants: numbers or quoted strings

Writing Efficient Rules

1. Put selective atoms first: More restrictive conditions early
2. Avoid Cartesian products: Ensure variables connect atoms
3. Use appropriate base cases: Initialize recursive rules properly

Debugging

Use Datalog.validate to check for errors before execution:

val prog = "...";
val typeResult = Datalog.validate prog;

val typeResult = "{...}" : string

Check if typeResult starts with "Error:" or "Parse error:".

Use Datalog.translate to see the generated Morel code.

References

• Datalog (Wikipedia)
• What You Always Wanted to Know About Datalog (And Never Dared to Ask)
• Foundations of Databases (Abiteboul, Hull, Vianu)

See Also

• Morel Language Reference
• Query expressions in Morel
• Unbounded variables via predicate inversion (GitHub commit with detailed explanation)