\[ \definecolor{ink}{RGB}{26,26,26} \definecolor{tight}{RGB}{0,120,174} \definecolor{loose}{RGB}{224,112,26} \definecolor{accent}{RGB}{224,112,26} \definecolor{muted}{RGB}{91,93,97} \newcommand{\tight}[1]{{\color{tight}{#1}}} \newcommand{\loose}[1]{{\color{loose}{#1}}} \newcommand{\larr}{\mathrel{\color{loose}{\rightsquigarrow}}} \newcommand{\tarr}{\mathrel{\color{tight}{\to}}} \newcommand{\set}{\mathcal{S}\mathrm{et}} \newcommand{\rel}{\mathbb{R}\mathrm{el}} \]
Programs compose. Specifications compose.
Double categories let them compose together.
An ordinary category has one kind of arrow. A double category has two:
- tight arrows are programs: things you run;
- loose arrows are specifications: things you check;
- squares are evidence that the programs respect the specs.
if \(x \mathrel{\loose{R}} y\) then \(\tight{f}(x) \mathrel{\loose{R'}} \tight{g}(y)\)
Take two different sorting algorithms, and the spec perm, relating two lists that are rearrangements of each other.
insertionSort on [3,1,2] and mergeSort on [2,3,1] both give [1,2,3]. That holds for every pair of permutations, so the square exists. The algorithms agree however the input may be arranged.
A double category is a pseudo category object in \(\mathbf{Cat}\); loose composition is associative and unital only up to coherent isomorphism (Grandis and Paré 1999).
Objects are types, tight arrows are functions, loose arrows are relations. A square means the functions preserve the relation.
The relation \(\loose{\mathsf{els}} : \mathsf{List\ Nat} \larr \mathsf{Set\ Nat}\) relates a list to the set of its elements.
If els relates xs to s, it relates cons x xs to insert x s, hence cons implements insert.
Non-example. els relates [1,1] to {1}, but length gives 2 and size gives 1. No square!
A square says this implementation respects that abstraction.
This is data refinement; \(\rel\) is an equipment, where each function also gives a loose arrow, its graph (Shulman 2008).
Squares glue like floor tiles, in two directions.
Top to bottom, programs compose: run one, then the next.
\((\tight{g} \circ \tight{f})(x) = \tight{g}(\tight{f}(x))\)
Left to right, specs compose: chain relations through a middle point.
\(x \mathrel{(\loose{R} ; \loose{S})} z \iff \exists y.\ x \mathrel{\loose{R}} y \wedge y \mathrel{\loose{S}} z\)
sort . nub: dedupe, then sort. xs has elements s then s has size n: xs has n distinct elements.
Rows first or columns first gives the same big square (the interchange law): the whole program meets the whole spec.
Squares with identity tight sides form a bicategory of loose arrows; when every function also has a loose companion, the double category is an equipment (Shulman 2008).
For a relation \(\loose{r} : a \larr b\), the relation \(\loose{\mathsf{List}\ r} : \mathsf{List}\ a \larr \mathsf{List}\ b\) relates two lists of the same length whose elements are related pairwise.
reverse :: List a -> List a works for every type a, so it can’t look at the elements, only rearrange them. So it maps related lists to related lists: the square always exists.
Take \(\loose{r}\) to be the graph of a function h, and out falls, for free: map h . reverse = reverse . map h
Reynolds’ relational parametricity interprets types as relations and polymorphic terms as families of squares in \(\rel\) (Reynolds 1983; Wadler 1989).
A double category is a category of programs and a category of specifications, glued together by squares that say “this program meets this spec”.
More about double categories