Datalog is a declarative logic programming language that has been used in a
variety of applications, including big-data analytics, language processing,
networking and distributed systems, and program analysis.
In this paper, we propose first-class Datalog constraints as a mechanism to
construct, compose, and solve Datalog programs at run time. The benefits are
twofold: We gain the full power of a functional programming language to operate
on Datalog constraints-as-values, while simultaneously we can use Datalog where
it really shines: to declaratively express and solve fixpoint problems.
We present an extension of the lambda calculus with first-class Datalog
constraints, including its semantics and a type system with row polymorphism
based on Hindley-Milner. We prove soundness of the type system and implement it
as an extension of the Flix programming language.