Constructing Functors via Profunctors
Finally I want to briefly talk about why I am interested in this \(\bigcirc \) thing.
My motivation comes from this ongoing project of interpreting
sophisticated data structures in various monoidal categories such as \((\mathbf {F}, \otimes , I)\)
and \((\mathbf {P}, \mathbin {\circ }, H)\).
I am especially interested in interpreting sequence-like data structures
(lists, queues, finger trees, ...) in \((\mathbf {F}, \otimes , I)\), because their
interpretation in this monoidal category would become data structures for
abstract syntax trees, with potentially good time-complexities for
operations such as variable substitution and pattern matching.
However, a significant difficulty with \((\mathbf {F}, \otimes , I)\) is that the substitution
tensor \(\otimes \) is in general only distributive on one side:
\[
(F + G) \otimes H \cong (F \otimes H) + (G \otimes H)
\]
but in general,
\[
H \otimes (F + G) \not \cong (H \otimes F) + (H \otimes G).
\]
This means that the substructural internal language of \((\mathbf {F}, \otimes , I)\) (where the
variables in a context are combined using \(\otimes \)) allows pattern matching
of a variable \(x : F + G\) only when it is the first variable in a context.
If \(\Gamma \) is non-empty, under the context \(\Gamma , x : F + G\), we cannot in general pattern match \(x\) because we do not have an isomorphism
\[
\llbracket \Gamma \rrbracket \otimes (\llbracket F\rrbracket + \llbracket G\rrbracket )
\cong
\llbracket \Gamma \rrbracket \otimes \llbracket F\rrbracket + \llbracket \Gamma \rrbracket \otimes \llbracket G\rrbracket .
\]
This is a big restriction for programming in \((\mathbf {F}, \otimes , I)\) because many efficient data structures, such as finger trees and self-balancing binary trees, need to pattern match a variable before the variables preceding it are fully consumed.
On the other hand, the monoidal category \((\mathbf {P}, \mathbin {\circ }, H)\) does not have this problem: the tensor \(\mathbin {\circ }\) distributes over coproducts from both directions.
Consequently, in the substructural internal language, we can pattern match coproducts as usual, and many familiar functional data structures (such as finger trees) can be implemented without any problem.
The interpretation of sequence data structures in \((\mathbf {P}, \mathbin {\circ }, H)\) is
exactly van der Ploeg and Kiselyov's type-aligned
sequences.
Now, with the modality \(\bigcirc \), we can construct things for \(\mathbf {F}\) while working in the nicer category \(\mathbf {P}\).
There should be some general theory for this, which I am still working on.
For this post, I will just show you a concrete example.
Fix an object \(A \in \mathbf {F}\) and suppose that we want to construct a representation of the free \(\otimes \)-monoid over \(A\) such that the associated operations are efficient.
In particular, we want to find some \(X \in \mathbf {F}\) with operations:
\[
v : I \to X,\ s : X \otimes X \to X,\ i : A \to X
\]
and co-operations:
\[
p : X \to I + A \otimes X.
\]
One obvious solution for \(X\) is the list object \(\mu X.\; I + A \otimes X\) in \(\mathbf {F}\), but we would like a solution with better time-complexity for \(s : X \otimes X \to X\).
Now we rephrase this problem in the nicer world \((\mathbf {P}, \mathbin {\circ }, H)\). Our goal is to construct a modal object \(Y \in \mathbf {P}\) equipped with the following maps in \(\mathbf {P}\):
\[
\begin {gathered}
v : H \to Y,\ s : Y \mathbin {\circ } Y \to Y,\ i : KA \to Y, \\
p : Y \to \bigcirc (H + KA \mathbin {\circ } Y).
\end {gathered}
\]
Note the \(\bigcirc \) in the codomain of \(p\), because coproducts in \(\mathbf {P}\) need to be reflected to become coproducts in \(\mathbf {F}\).
Without loss of generality, we can assume \(Y\) takes the form of \(\bigcirc Z\) for some (not necessarily modal) object \(Z \in \mathbf {P}\), equipped with maps:
\[
\begin {gathered}
v : H \to \bigcirc Z,\ s : \bigcirc Z \mathbin {\circ } \bigcirc Z \to \bigcirc Z, i : KA \to \bigcirc Z, \\
p : \bigcirc Z \to \bigcirc (H + KA \mathbin {\circ } \bigcirc Z).
\end {gathered}
\]
By composing with the unit map \(Z \to \bigcirc Z\), to obtain \(v\) and \(i\), it is sufficient if we have
\[
v' : H \to Z \quad \text {and}\quad i' : KA \to Z.
\]
Also, by using the functor action of \(\bigcirc \), for \(p\) it is sufficient if we have
\[
p' : Z \to H + KA \mathbin {\circ } \bigcirc Z.
\]
To simplify \(s : \bigcirc Z \mathbin {\circ } \bigcirc Z \to \bigcirc Z\), we need the following result:
Because \(\bigcirc Z\) is modal, by this theorem we have
\[
\bigcirc Z \mathbin {\circ } \bigcirc Z \cong \bigcirc Z \mathbin {\circ } \bigcirc (\bigcirc Z) \cong \bigcirc (Z \mathbin {\circ } \bigcirc Z).
\]
Consequently, to have a map \(s : \bigcirc Z \mathbin {\circ } \bigcirc Z \to \bigcirc Z\), it is sufficient to have
\[
s' : Z \mathbin {\circ } \bigcirc Z \to Z.
\]
Now if we look at the types of the maps \(v', i', p'\), and \(s'\), we can see that \(Z\) is like a list object in \(\mathbf {P}\) except that the second argument of \(s'\) is protected by the modality \(\bigcirc \).
A simple solution for this \(Z\) is
\[
\mu Z.\; H + KA \mathbin {\circ } \bigcirc Z.
\]
But for better complexity, we can adapt Okasaki's catenable list from Chapter 10 of his famous book to work with \(\bigcirc \) too:
\[
\mu Z.\; H + KA \mathbin {\circ } Q (\bigcirc Z),
\]
where \(Q : \mathbf {P} \to \mathbf {P}\) is any efficient implementation of queues on \(\mathbf {P}\) that supports:
\[
\begin {gathered}
H \to Q(\bigcirc Z)
\\
Q(\bigcirc Z) \mathbin {\circ } \bigcirc Z \to Q(\bigcirc Z)
\\
Q(\bigcirc Z) \to H + \bigcirc Z \mathbin {\circ } Q(\bigcirc Z).
\end {gathered}
\]
As I mentioned in the last section, the crucial advantage of \(\mathbf {P}\) is that many efficient data structures can be used to implement queues in \(\mathbf {P}\), such as finger trees.
This would then give us an efficient representation of \(Z\) where all four operations \(v', i', p', s'\) run in constant time.
The original \(X \in \mathbf {F}\) is then
\[
X = RZ = R(\mu Z.\; H + KA \mathbin {\circ } Q (\bigcirc Z)),
\]
whose Kleisli embedding is \(KX = \bigcirc Z\).
This is how we obtain a construction for \(\mathbf {F}\) by making a detour to the nicer world of \(\mathbf {P}\).