Abstract

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 two decades, it is becoming evident that type-theoretic mathematics has a lot to teach us about designing the foundations of practical modern technology. Indeed, we are seeing an increasing number of applications of type-theoretic ideas in the design of popular programming languages like Rust. But for databases, type-theoretic thinking has found surprisingly little application so far, at least when it comes to the design of database languages and models themselves. This leaves much room for improvement and modernisation. With new type-theoretic mathematics at our disposal, how would we re-think and re-design the foundations of modern databases from first principles?

In our talk, we aim to give a first comprehensive answer to this question. We discuss a novel synthesis of type-theoretic thinking and classical conceptual data modelling, which results in a highly generalisable “polymorphic data model” and an intuitive query language. This solves several issues regarding the interoperability of existing systems and sets a new standard with regard to system extensibility and consistency guarantees. We implemented this approach in TypeDB: the first “polymorphic database” of its kind. We will describe in detail the motivations and design choices that we made when building TypeDB, together with its query language TypeQL, and discuss a set of interesting future challenges and opportunities that we see lying ahead.

Registration link: https://forms.gle/Kk8LfVZCF3RXR2Wm9

Some catering will be provided.