Algebraic Data Types for Datalog

Datalog is a popular language for implementing program analyses, providing an elegant formalism for concisely and declaratively specifying least fixpoint-based algorithms, and solving them efficiently. However, plain Datalog can only work with atomic values and offers no first-class support for structured data of any kind. This makes it cumbersome to express algorithms that need even very simple data structures, so non-trivial analyses tend to rely on extra-logical features that allow creating new values to represent compound data on the fly. We propose a more principled solution: we extend QL, a dialect of Datalog, with a notion of algebraic data types, offering the usual combination of products, disjoint unions and recursion, seamlessly integrated with the logical features of QL. These data types can be desugared into applications of a low-level operator for creating fresh values at runtime, which is meta-theoretically well behaved and easy to implement. To demonstrate the practical usefulness of our approach, we discuss case studies tackling problems from the general area of program analysis that were previously difficult or impossible to solve in QL.