<! --- LETTERS --->
$$ \newcommand{\lR}{\mathbb{R}} $$
$$ \newcommand{\lZ}{\mathbb{Z}} $$
$$ \newcommand{\lN}{\mathbb{N}} $$
$$ \newcommand{\lI}{\mathbb{I}} $$
$$ \newcommand{\II}{\mathbb{I}} $$
$$ \newcommand{\bI}{\mathbf{I}} $$
$$ \newcommand{\bC}{\mathbf{C}} $$
$$ \newcommand{\bD}{\mathbf{D}} $$
$$ \newcommand{\bE}{\mathbf{E}} $$
$$ \newcommand{\bF}{\mathbf{F}} $$
$$ \newcommand{\iI}{\mathsf{I}} $$
$$ \newcommand{\iA}{\mathsf{A}} $$
$$ \newcommand{\iB}{\mathsf{B}} $$
$$ \newcommand{\iC}{\mathsf{C}} $$
$$ \newcommand{\iD}{\mathsf{D}} $$
$$ \newcommand{\iE}{\mathsf{E}} $$
$$ \newcommand{\iF}{\mathsf{F}} $$
$$ \newcommand{\iM}{\mathsf{M}} $$
<! --- SYMBOLS --->
$$ \newcommand{\eps}{\epsilon} $$
$$ \newcommand{\SetCat}{\mathrm{Set}} $$
$$ \newcommand{\Bool}{\mathrm{Bool}} $$
$$ \newcommand{\Pos}{\mathrm{Pos}} $$
$$ \newcommand{\lbl}{\mathsf{lbl}} $$
$$ \newcommand{\subdiv}{\mathsf{sd}} $$
$$ \newcommand{\Hom}{\mathrm{Hom}} $$
$$ \newcommand{\Fun}{\mathrm{Fun}} $$
$$ \newcommand{\Psh}{\mathrm{PSh}} $$
<! --- OPERATORS --->
$$ \newcommand{\dim}{\mathrm{dim}} $$
$$ \newcommand{\id}{\mathrm{id}} $$
$$ \newcommand{\src}{\partial^-} $$
$$ \newcommand{\tgt}{\partial^+} $$
$$ \newcommand{\und}[1]{\underline{#1}} $$
$$ \newcommand{\abs}[1]{\left|{#1}\right|} $$
$$ \newcommand{\op}{^{\mathrm{op}}} $$
$$ \newcommand{\inv}{^{-1}} $$
<! --- CATEGORIES, FUNCTORS AND CONSTRUCTIONS --->
$$ \newcommand{\ttr}[1]{\mathfrak{T}^{#1}} $$
$$ \newcommand{\lttr}[2]{\mathfrak{T}^{#1}{(#2)}} $$
$$ \newcommand{\truss}[1]{\mathsf{T}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\sctruss}[1]{\bar{\mathsf{T}}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\rotruss}[1]{\mathring{\mathsf{T}}\!\mathsf{rs}_{#1}} $$
$$\newcommand{\trussbun}[1]{\mathsf{TrsBun}_{#1}} $$
$$ \newcommand{\trusslbl}[1]{\mathsf{Lbl}\mathsf{T}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\blcat}[1]{\mathsf{B}\mathsf{lk}_{#1}} $$
$$ \newcommand{\blset}[1]{\mathsf{Blk}\mathsf{Set}_{#1}} $$
$$ \newcommand{\fcl}[2]{\chi^{#1}_{#2}} $$
$$ \newcommand{\Entr}{\mathsf{Entr}} $$
$$ \newcommand{\Exit}{\mathsf{Exit}} $$
<! --- ARROWS AND RELATIONS --->
$$ \newcommand{\fleq}{\preceq} $$
$$ \newcommand{\fles}{\prec} $$
$$ \newcommand{\xto}[1]{\xrightarrow{#1}} $$
$$ \newcommand{\xot}[1]{\xleftarrow{#1}} $$
$$ \newcommand{\ot}{\leftarrow} $$
$$ \newcommand{\toot}{\leftrightarrow} $$
$$ \newcommand{\imp}{\Rightarrow} $$
$$ \newcommand{\iff}{\Leftrightarrow} $$
$$ \newcommand{\iso}{\cong} $$
$$ \newcommand{\into}{\hookrightarrow} $$
$$ \newcommand{\proto}{\longrightarrow\mkern{-2.8ex}{\raisebox{.3ex}{$\tiny\vert$}}\mkern{2.5ex}} $$
<! --- DIAGRAM ARROWS --->
<! ---... should replace \rlap by \mathrlap, see KaTeX doc --->
$$ \newcommand{\ra}[1]{\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$
$$ \newcommand{\la}[1]{\xleftarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$
$$ \newcommand{\da}[1]{\downarrow\raisebox{.5ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\dra}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}}\kern-.5ex\searrow}} $$
$$ \newcommand{\dla}[1]{\swarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\ua}[1]{\uparrow\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\ura}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}\kern-.5ex\nearrow}} $$
$$ \newcommand{\ula}[1]{\nwarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
Abstract. After a year of hard work, we released the very first version of TypeDB 3, which lays solid foundations for our vision of creating a modern declarative database programming framework.
Context
In 2024 we hunkered down with the team at TypeDB to design, starting from very much at the drawing board from first principle, a lean and modern query language that will be ready for a future of high-level declarative programming.
Key mathematical idea
The key mathematical idea is to bring the Curry-Howard correspondence to databases (as outlined already in our PODS’24 paper). This means clean and rigorous data modeline through type dependencies which, as of TypeDB 3.0, are finally brought to full fruition. A key innovation along the way, is to fully fuse natural language and type theoretic thinking in our language design.
The release
It was incredible fun to work many gifted colleagues on this project (and I hope to write more about our process at some point as well). While this first release does not include all features on our roadmap yet, it lays a very solid foundation for TypeDB in 2025.
Find out more at typedb.com
