Deconstructing Datalog This thesis deconstructs Datalog from a categorical and type theoretic perspective to determine what makes it tick. Datalog’s semantic guarantees are provided by brute syntactic restrictions, such as stratification and the absence of function symbols. In place of these, we find compositional semantic properties such as monotonicity, which we capture using types. We show that this permits integrating Datalog’s features with those of typed functional languages, such as algebraic data types and higher order functions.

"We have not attempted to embed Datafun into an existing language, as this would greatly complicate the context-management operations needed to ensure monotonicity." 😿

This is extremely well written, which I can say, because despite not having a strong background, I understood all of the introductory material. The idea of dividing between monotone and non-monotone expressions is challenging, from a usability perspective. It feels like a leaky abstraction problem made explicit, complicating the language?