Typed Datalog

Static type safety is an important feature of many commercial programming languages, as has become apparent in our experience developing LogicBlox—a Datalog-based platform for building enterprise-scale systems for corporate planning. Existing approaches to enhancing Datalog (and Prolog) with type safety are problematic for LogicBlox applications because (1) they do not support inclusion constraints, which are crucial for database reasoning, and (2) their worst-case running times are exponential in the size of the programs. In the LogicBlox environment—where clients interactively add and execute programs and queries—efficient compilation and execution are critical, and so a PTIME type-checking algorithm is preferred. Furthermore, one of the central design goals of LogicBlox is to express the compiler itself in Datalog, which in general excludes exponential-time algorithms. This paper presents a definition of type safety for Datalog which can express inclusion constraints along with an efficient (PTIME) and sound (but not complete) type-checking algorithm, proposes work-arounds for some common limitations of the algorithm, and indicates how the type-checking algorithm itself may be represented in Datalog.