Type theoretical databases
Henrik Forssell, H{\aa}kon Robbestad Gylterud, David I. Spivak
TL;DR
This paper introduces a dependent type theory that models databases as a mathematical structure, enabling schema specification, manipulation, and querying within a formal logical framework.
Contribution
It establishes a soundness theorem connecting dependent type theory with an indexed category of simplicial complexes, modeling databases mathematically.
Findings
Category models database schemas and instances
Type theory supports schema specification and manipulation
Enables formal querying within the type-theoretic framework
Abstract
We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. The point of interest for computer science is that this category can be seen to represent tables in a natural way. Thus the category is a model for databases, a single mathematical structure in which all database schemas and instances (of a suitable, but sufficiently general form) are represented. The type theory then allows for the specification of database schemas and instances, the manipulation of the same with the usual type-theoretic operations, and the posing of queries.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.