Data Migration Functor

definition example theorem

Let $F:\mathcal{C}\to \mathcal{D}$ be a Functor between schemas. Three data migration functors relate instances:

• ${\Delta }_F:\mathcal{D}\text{-}\mathbf{Inst}\to \mathcal{C}\text{-}\mathbf{Inst}$ (pullback / “duplicate or destroy”): ${\Delta }_F(I):=F;I$, precomposition; on morphisms $({\alpha }_F{)}_c:={\alpha }_{F(c)}$ (Definition 3.68). It duplicates or destroys tables and columns.
• ${\Sigma }_F:\mathcal{C}\text{-}\mathbf{Inst}\to \mathcal{D}\text{-}\mathbf{Inst}$, the left adjoint of ${\Delta }_F$ (“sum”: union data), built from colimits in $\mathbf{Set}$.
• ${\Pi }_F:\mathcal{C}\text{-}\mathbf{Inst}\to \mathcal{D}\text{-}\mathbf{Inst}$, the right adjoint (“product”: pair/query data — database programmers say join), built from limits in $\mathbf{Set}$.

$${\Sigma }_F⊣{\Delta }_F⊣{\Pi }_F.$$

Sources: 7 Sketches §3.4 (Definition 3.68, §3.4.3–3.4.4, Eq. 3.77, Exercises 3.67, 3.76, 3.78), Remark 3.100, §3.6 (“All concepts are Kan extensions”); FQL; DaoFP Chapter 19 (${\Sigma }_F,{\Pi }_F$ are the left and right Kan extensions along $F$), Chapter 11 (Dependent Sum/Dependent Product along a map of types); 7 Sketches §1.4.2 (the preorder shadow: Pushforward and Pullback of Partitions); CTfS §5.1.4 (Examples 5.1.4.7, 5.1.4.10, Exercises 5.1.4.5, 5.1.4.8, 5.1.4.11), Application 5.2.1.2

Examples

• $\mathsf{Gr}\to \mathsf{DDS}$: ${\Delta }_F$ turns a Discrete Dynamical System into its graph (§3.4.1).
• Airline seats (Eq. 3.5): $F:\mathcal{A}\to \mathcal{B}$ sends $\mathsf{Economy},\mathsf{FirstClass}\mapsto \mathsf{AirlineSeat}$. ${\Delta }_F$ copies the seat table into both; ${\Sigma }_F(I)(\mathsf{AirlineSeat})=I(\mathsf{Economy})\bigsqcup I(\mathsf{FirstClass})$; ${\Pi }_F(I)(\mathsf{AirlineSeat})$ is the set of pairs $(e,f)$ with the same price and position — presumably empty here, but with “Rewards Program” and “First Class Seats” it finds the first-class seats in the rewards program: a query.
• Single-set summaries ($\mathcal{D}=\underline{1}$, $!:\mathcal{C}\to \underline{1}$, 7S Exercise 3.76): identifying $\underline{1}\text{-}\mathbf{Inst}\simeq \mathbf{Set}$, ${\Sigma }_{!}(I)=\mathrm{colim}I$ and ${\Pi }_{!}(I)=\lim I$. For the email schema $\mathsf{Email}\rightrightarrows \mathsf{Address}$ (Eq. 3.77, $\cong \mathsf{Gr}$, 7S Exercise 3.78), ${\Sigma }_{!}(I)$ is the set of emailing groups (connected components: Bob–Grace–Pat–Emmy, Sue–Doug) — a typical $\Sigma$ quotient; ${\Pi }_{!}(I)$ is the set of self-to-self emails ($Em\_6$) — a typical $\Pi$ selection. See Finite Limits in Set.

A worked example with tables (CTfS §5.1.4, from Spivak’s Functorial data migration). Let $\mathcal{C}$ have two fact tables, $T1$ (SSN, First, Last) and $T2$ (First, Last, Salary), over leaf tables SSN, First, Last, Salary; let $\mathcal{D}$ have one fact table $\mathsf{T}$ with all four columns; $F:\mathcal{C}\to \mathcal{D}$ sends $T1,T2\mapsto \mathsf{T}$.

• ${\Delta }_F$ (“if I get my information from you, your information becomes my information”): from $\mathsf{T}$ = {XF667: 115-234 Bob Smith $250, XF891: 122-988 Sue Smith $300, XF221: 198-877 Alice Jones $100} it produces $T1$ and $T2$ as two projections of the same rows — duplicating the table and deleting a column from each copy.
• ${\Sigma }_F$ puts the rows of $T1$ = {Bob Smith, Sue Smith, Alice Jones} and $T2$ = {Alice Jones $100, Sam Miller $150, Sue Smith $300, Carl Pratt $200} into one table $\mathsf{T}$ with 7 rows. Missing values are filled with fresh labeled nulls / Skolem variables such as T1-001.Salary and T2-002.SSN: “the universal response: freely add new variables that take the place of missing information”.
• ${\Pi }_F$ keeps only the pairs $(t_1,t_2)$ that agree on First and Last — a join: (Sue Smith, 122-988, $300) and (Alice Jones, 198-877, $100).
• Along $F:\underline{3}\to \underline{2}$, $1\mapsto 1$, $2,3\mapsto 2$: ${\Sigma }_F(I_1,I_2,I_3)=(I_1,I_2\bigsqcup I_3)$ and ${\Pi }_F(I_1,I_2,I_3)=(I_1,I_2\times I_3)$ (CTfS Exercises 5.1.4.8, 5.1.4.11). Along $[1]\to [2]$ skipping the middle object, $\Delta$ composes the two foreign keys “word ↦ part of speech ↦ word class” into one (CTfS Exercise 5.1.4.5).
• Schema evolution (CTfS Application 5.2.1.2): when our understanding of a subject changes through schemas ${\mathcal{C}}_1\to {\mathcal{C}}_2\to \cdots \to {\mathcal{C}}_n$, old data is pushed forward with $\Sigma$ “in the freest possible way” and the epochs are united by a colimit in ${\mathcal{C}}_n\text{-}\mathbf{Set}$.

“Everything follows from the definition of adjoint functors”; complex migrations are built from $\Delta ,\Sigma ,\Pi$ — “in practice essentially all useful migrations”. The word pullback here is not the limit of a cospan, though via the Category of Elements and discrete opfibrations it is a pullback in $\mathbf{Cat}$ (Remark 3.100).

In compilers and databases

With an algebraic type side — attributes in an algebra of a Lawvere Theory, labelled nulls created by ${\Sigma }_F$ — the same three functors are the semantics of the CQL query language (Algebraic Database).

JuliaLeanHaskell

Docs: FinCats · Data migration · ACSets API · Graphs · Theories & presentations

using Catlab
@present SchDDS(FreeSchema) begin State::Ob; next::Hom(State, State) end
@acset_type DDS(SchDDS)
I = @acset DDS begin State = 7; next = [4, 4, 5, 5, 5, 7, 6] end
F = FinFunctor(Dict(:V => :State, :E => :State), Dict(:src => id(SchDDS[:State]), :tgt => :next),
               FinCat(SchGraph), FinCat(SchDDS))
 
Δ = DeltaMigration(F)                    # pullback along F
G = migrate(Graph, I, Δ)                 # a Graph
ΣF = SigmaMigrationFunctor(F, Graph, DDS)   # left adjoint (computed by colimits)
J = ΣF(G)                                   # a DDS again (Σ_F Δ_F I → I is the counit; J ≇ I in general)
# Π-migrations (limits/queries) are expressed with conjunctive queries (`@migration` with `@join`)

-- Δ_F is precomposition; Σ_F and Π_F are left/right Kan extensions along F
#check CategoryTheory.Functor.lan     -- left Kan extension functor (Σ_F)
#check CategoryTheory.Functor.ran     -- right Kan extension functor (Π_F)
#check CategoryTheory.Functor.lanAdjunction   -- lan ⊣ precomposition

-- Δ_F on hand-rolled instances: precompose the object/arrow assignment
-- Σ_F / Π_F are Kan extensions: see the `Lan` and `Ran` types in Data.Functor.Kan (kan-extensions)
-- newtype Lan g h a = forall b. Lan (g b -> a) (h b)      -- Σ (a coend)
-- newtype Ran g h a = Ran (forall b. (a -> g b) -> h b)   -- Π (an end)