TypeDB Lectures
Type Theory as the Unifying Foundation for Modern Databases
If the term “type theory” sounds exciting to you, chances are you are either a theoretical computer scientist or a mathematician. But with several high-profile successes of the field over the last decade or two, it is becoming evident that type theoretical mathematics has a lot to teach us about the design of the foundations of practical modern technology.
Indeed, in modern programming languages, we are seeing an increasing number of applications of powerful type-theoretic ideas (including, for example, the ‘affine substructural type system’ that governs borrowing in Rust, or pattern-matching mechanisms used to destructure algebraic data). Transferring these fundamental ideas from mathematics to real-life systems can yield substantial benefits in terms of expressivity, performance, and safety of our applications.
But what about database languages? As a matter of fact, type-theoretic thinking has found little to no application in database design so far — at least when it comes to the design of database models. Indeed, the field of databases has been historically slow in the adoption of new ideas, partially due to its highly commercialized nature. This leaves much room for improvement and modernization: with new type-theoretic mathematics at our disposal, how would we re-think and re-design the foundations of modern databases in the best possible way?
The question has, in fact, recently started to draw more and more interest from both academia and industry. In this lecture, we will give a first comprehensive answer, and take you on a whirlwind tour of how to synthesize type-theoretic thinking with conceptual data models, and the repercussions that this synthesis has. In more detail, we will:
- Describe the mathematical origins of the most prominent database paradigms.
- Learn how contemporary mathematics re-thinks these foundations with type theory.
- Give a crash in type theory, tailored to non-mathematicians.
- Explain how conceptual modeling theory enables ‘highly generalizable data models’.
And finally, we will combine the above to synthesize conceptual data models and type theory to create a new ‘unified’ foundation for the modern database.
Before joining Vaticle, Christoph has led cutting-edge research in Theoretical Computer Science and Mathematics at the University of Oxford, where he also completed his PhD in Computer Science in 2019. He worked in the areas of Higher-Dimensional Category Theory and Computable Geometry, and co-wrote a book on the mathematical foundations for a synthesis of these two subjects. Christoph has been closely following the movement of type-theoretic databases over the past several years, and shares our vision at Vaticle to bring theory and practice together in order to built the next generation framework for modern databases applications.
