Type Theory as a Unifying Paradigm for Modern Databases

Over the past decades, data modeling has become a highly diversified discipline with many competing paradigms emerging across various application domains. We argue that higher levels of abstraction including, in particular, the integration of high-level programming and reasoning techniques, will pave the way forward for future knowledge management systems. As a programmatic foundation for this endeavor, we will discuss a novel type theoretical modeling and reasoning paradigm, which aims to strike a powerful balance between what can be naturally semantically modeled and what can be practically implemented. TypeQL is a multi-purpose database language rooted in these foundations: it is designed around the expressivity of natural language and backed by type theoretical principles. This rigorous high-level approach to database language reduces development and maintenance loads, preventing hard to spot data integrity and logic errors through its underlying type system, while also providing a unifying toolset for a large class of domain-specific applications ranging from querying connected data in knowledge graphs for drug discovery to reasoning and adaptive decision making in cognitive robotics.