Algebraic Database

definition theorem example program

An algebraic database (Schultz, Spivak, Vasilakopoulou & Wisnesky) is the categorical model of a relational database with data in it: not only tables and foreign keys, but typed values — integers, strings — on which functions such as $+$ or comparison act, and equations that mix the two. Its ingredients:

• a type side $\mathsf{Type}$: a multi-sorted algebraic theory, i.e. a Lawvere Theory — a cartesian strict monoidal category whose objects are freely generated by base sorts (Definition 3.1) — e.g. sorts Int, String and operations +, length;
• a schema $\mathcal{S}=(S_e,S_o)$ (Definition 5.2): an entity category $S_e$ (tables and foreign keys, a finitely presented category as for C-sets) and an observables profunctor $S_o:S_e\nrightarrow \mathsf{Type}$ saying which values can be observed from a row — attributes, and terms built from them such as salary(manager(e)) + 1;
• an instance (Definition 6.2): a functor $I$ on the collage of $S_e$ and $\mathsf{Type}$ whose restriction to $\mathsf{Type}$ preserves finite products — a set of rows per table and a $\mathsf{Type}$-algebra of values, possibly containing labelled nulls (unknown values that are still subject to equations).

Sources: Schultz, Spivak, Vasilakopoulou & Wisnesky, Algebraic Databases, Theory Appl. Categ. 32 (2017), arXiv:1602.03501 (notes) Definitions 3.1, 5.2, 6.2, 7.1, 9.2, Propositions 7.3, 7.4, 7.12, Theorem 8.10; Schultz & Wisnesky, Algebraic Data Integration, J. Funct. Programming 27 (2017), arXiv:1503.03571 (notes) (the CQL language and its implementation); Spivak, Functorial data migration, Inform. and Comput. 217 (2012); CTfS §§3.5, 4.4 and Data Migration Functor.

Migration functors

A schema mapping $F:\mathcal{S}\to \mathcal{T}$ — a functor on entities compatible with observables — induces three functors between categories of instances, exactly as for C-sets:

$${\Sigma }_F⊣{\Delta }_F⊣{\Pi }_F,{\Delta }_F(I)=I\circ F(\text{Definition 7.1}).$$

${\Delta }_F$ restricts (“project to the old schema”), its right adjoint ${\Pi }_F$ (Proposition 7.3, a right Kan Extension) joins, and its left adjoint ${\Sigma }_F$ (Proposition 7.4, a coend) unions and merges — and is where labelled nulls are created: pushing data forward into a table that needs a value nobody supplied produces a fresh null, constrained by equations. The type side makes one subtlety visible: ${\Sigma }_F$ preserves the property “values form a $\mathsf{Type}$-algebra” only when the observables part of $F$ is cartesian (Proposition 7.12).

Queries are bimodules

A query (Definition 9.2) has for clauses (variables ranging over tables), where clauses (equations), and return clauses (observables) — the uber-query form of select–from–where. Queries from $\mathcal{R}$ to $\mathcal{S}$ are the same as bimodules (profunctors between collages, Theorem 8.10), and everything — schemas, mappings, instances, queries — lives in one Double Category $\mathbb{D}\mathrm{ata}$, a proarrow equipment: functors are the tight arrows, profunctors the loose ones. Composition of queries is composition of profunctors, which is why it is a Coend.

What the algebraic type side buys

plain C-sets	algebraic databases
attributes are arbitrary functions into fixed sets	attributes land in an algebra of a theory; equations can mention arithmetic
no unknown values	labelled nulls, constrained by equations, created by $\Sigma$
a query is a diagram of tables	a query can compute (return salary + bonus)
equality of instances is equality of tables	equality is decided in the theory — a word problem (Congruence)

The last row is the cost: deciding whether two observables are equal requires deciding equality in the type side, which for an arbitrary equational theory is undecidable. CQL handles it with completion procedures and congruence closure.

Sophia

Sophia’s store is a database whose “type side” is large: hashes, payload encodings, effect rows and machine primitives with overflow and rounding semantics. Two prim nodes that differ only in overflow discipline are different — equality is decided in the type side, and Sophia’s design puts these attributes into the hash for exactly that reason. Hash-schema migration (MIGRATES_TO) is a schema mapping applied by re-elaboration rather than by ${\Sigma }_F$. See Graph Schema and Hashing and Identity.

JuliaLean

Docs: Data migration · FinCats · Wiring diagrams · ACSets API

using Catlab
@present SchTermGraph(FreeSchema) begin
    (Term, Child)::Ob
    parent::Hom(Child, Term); child::Hom(Child, Term)
    Label::AttrType
    tag::Attr(Term, Label)
end
@acset_type TermGraph(SchTermGraph, index = [:parent, :child])
t = @acset TermGraph{Symbol} begin
    Term = 4; tag = [:add, :x, :mul, :lit2]
    Child = 4; parent = [1, 1, 3, 3]; child = [2, 3, 2, 4]
end
# Δ along a schema mapping F : SchGraph → SchTermGraph: restrict an instance to a smaller schema.
F = FinFunctor(Dict(:V => :Term, :E => :Child), Dict(:src => :parent, :tgt => :child),
               FinCat(SchGraph), FinCat(SchTermGraph))
g = migrate(Graph, t, DeltaMigration(F))
(nv(g), ne(g))                                       # (4, 4): the call graph, labels forgotten
# Observables combine structure and the type side: tag(parent(c)) and tag(child(c)) for each edge c.
pairs = query(t, @relation (p = p, c = c) begin
    Child(parent = x, child = y)
    Term(_id = x, tag = p)
    Term(_id = y, tag = c)
end)
sort(collect(zip(pairs.p, pairs.c)))                 # [(:add, :mul), (:add, :x), (:mul, :lit2), (:mul, :x)]

import Mathlib
open CategoryTheory
-- Δ_F is precomposition with F: an instance I on D becomes the instance F ⋙ I on C.
-- Its adjoints Σ_F ⊣ Δ_F ⊣ Π_F are Mathlib's left and right Kan extensions along F.
#check @Functor.lan       -- left Kan extension along F (Σ_F)
#check @Functor.ran       -- right Kan extension along F (Π_F)
example {C D : Type} [SmallCategory C] [SmallCategory D] (F : C ⥤ D) (I : D ⥤ Type) (c : C) :
    (F ⋙ I).obj c = I.obj (F.obj c) := rfl