DependentOptics.tex

\documentclass[11pt]{amsart}          
\usepackage{amsfonts}
\usepackage{amssymb}  
\usepackage{amsthm} 
\usepackage{amsmath} 
\usepackage{tikz-cd}
\usepackage{float}
\usepackage[]{hyperref}
\usepackage{minted}
\hypersetup{
  colorlinks,
  linkcolor=blue,
  citecolor=blue,
  urlcolor=blue}
\newcommand{\hask}[1]{\mintinline{Haskell}{#1}}
\newenvironment{haskell}
  {\VerbatimEnvironment
  	\begin{minted}[escapeinside=??, mathescape=true,frame=single, framesep=5pt, tabsize=1]{Haskell}}
  {\end{minted}}

\author{Bartosz Milewski}
\title{Dependent Optics}
\begin{document}
\maketitle{}

\section{Dependent types}

Dependent types, in programming, are families of types indexed by elements of an indexing type. For instance, counted vectors are families of tuples indexed by natural numbers---the lengths of the vectors.

In category theory we model dependent types as fibrations. We start with the total space $E$, the base space $B$, and a projection, or a display map, $p \colon E \to B$. The fibers of $p$ correspond to members of the type family. For instance, the total space, or the bundle, of counted vectors is the list type $\mathit{List} (A)$ (a free monoid generated by $A$) with the projection $\mathit{len} \colon \mathit{List} (A) \to \mathbb{N}$ that returns the length of a list.

Another way of looking at dependent types is as objects in the slice category $\mathcal{C}/B$. Counted vectors, for instance, are represented as objects in $\mathcal{C}/\mathbb{N}$ given by pairs $\langle \mathit{List} (A), \mathit{len} \rangle$.   Morphisms in the slice category correspond to fibre-wise mappings between bundles.

We often require that $\mathcal{C}$ be a locally cartesian closed category, that is a category whose slice categories are cartesian closed. In such categories, the base-change functor $f^*$ has both the left adjoint, the dependent sum $\Sigma_f$; and the right adjoint, the dependent product $\Pi_f$. The base-change functor is defined as a pullback:
\[
 \begin{tikzcd}
f^* E
\arrow[dr, phantom,  , very near start, "\lrcorner"]
 \arrow[d, "f^*p"']
 \arrow[r, "g"]
 & E
 \arrow[d, "p"]
 \\
 B'
 \arrow[r, "f"]
 &B
  \end{tikzcd}
\]
This pullback defines a \emph{cartesian product} in the slice category $\mathcal{C}/B$ between two objects: $\langle B', f \rangle$ and $\langle E, p \rangle$. In a locally cartesian closed category, this product has the right adjoint, the internal hom in $\mathcal{C}/B$.

\section{Dependent optics}
The most general optic is given by two monoidal actions $L_m$ and $R_m$ in two categories  $\mathcal{C}$ and $ \mathcal{D}$. It can be written as the following coend of the product of two hom-sets:

\[ O(A, A'; S, S') =  \int^{m \colon \mathcal{M}} \mathcal{C}( S, L_m A) \times \mathcal{D}(R_m A', S') \]
Monoidal actions are parameterized by objects in a monoidal category $(\mathcal{M}, \otimes, 1)$.

Dependent optics are a special case of general optics, where one or both categories in question are slice categories. When the monoidal action is defined in the slice category, the transformations must respect fibrations. For instance, the action in the bundle $\langle E, p \rangle$ over $B$ must commute with the projection:
\[p \circ L_m = p \]
This is reminiscent of gauge transformations in physics, which act on fibers in bundles over spacetime. The action must respect the monoidal structure of $\mathcal{M}$ so, for instance,
\[L_{m \otimes n} \cong L_m \circ L_n \]
\[ L_1 \cong \mathit{Id} \]

We can define a dependent (mixed) optic as:

\[ \int^{m : \mathcal{M}} (\mathcal{C}/B)( S, L_m A) \times (\mathcal{D}/B')(R_m A', S') \]

Just like regular optics, dependent optics can be represented using Tambara modules, which are profunctors with the additional structure given by transformations:
\[ \alpha_{m, \langle A, A' \rangle} \colon P \langle A, A' \rangle \to P\langle L_m A, R_m A' \rangle \]
where $A$ and $A'$ are objects in the appropriate slice categories.
The optic is then given by the following end in the Tambara category:
\[ O(A, A'; S, S') =  \int_{p : \mathbf{Tam}} \mathbf{Set}(P \langle A, A' \rangle, P \langle S, S' \rangle) \]


\section{Dependent lens}

The primordial optic, the lens, is defined by the monoidal action of a product. By analogy, we define a dependent lens by the action of the product in a slice category. The action parameterized by an object $\langle C, q \rangle$ on another object $ \langle A, p \rangle$ is given by the pullback:
\[ M_C A = C \times_B A \]
Since a pullback is the product in the slice category $\mathcal{C}/B$, it is automatically associative and unital, so it can be used to define a dependent lens:
\[ \mathit{DLens}(A, A'; S, S') = \int^{\langle C, p \rangle : \mathcal{C}/B} (\mathcal{C}/B)( S, C \times_B A) \times (\mathcal{C}/B)(C \times_B A', S')\]


Since $\mathcal{C}$ is locally cartesian closed, there is an adjunction between the product and the exponential. We can use it to get:
\[ \cong \int^{\langle C, p \rangle : \mathcal{C}/B} (\mathcal{C}/B)( S, C \times_B A) \times (\mathcal{C}/B)(C , [A', S']_B) \]
We can then apply the Yoneda lemma to get the setter/getter form:
\[  (\mathcal{C}/B)( S, [A', S']_B \times_B A) \]

The internal hom $[A', S']_B$ in a locally cartesian closed category can be expressed using a dependent product:
\[ \left [\left \langle A' \atop p \right \rangle, \left \langle S' \atop q \right \rangle \right ] \cong \Pi_p \left(p^* \left \langle S' \atop q \right \rangle \right)\]
where $p \colon A' \to B$ is the fibration of $A'$, $\Pi_p$ is the right adjoint to the base change functor, and $p^*$ is the base-change functor along $p$.

The dependent lens can be written as:
\[ (\mathcal{C} / B) \left( \left \langle S \atop r \right \rangle, \Pi_p \left(p^* \left \langle S' \atop q \right \rangle \right) \times \left \langle A \atop r' \right \rangle \right) \]
In particular, if $B$ is $\mathbb{N}$, this is equal to an infinite tuple of functions:
\[O(A, B; S, T) \cong \prod_n \left( s_n \to \left((b_n \to t_n) \times a_n \right) \right) \]
or fiber-wise pairs of setter/getter $\langle s_n \to b_n \to t_n, s_n \to a_n \rangle$ indexed by $n$.

\section{Traversals}

Traversals are optics whose monoidal action is generated by polynomial functors of the form:
\[ M_{c} a = \sum_{n \colon \mathbb{N}} c_n \times a^n \]
The coefficients $c_n$ can be expressed as a fibration $ \langle C, p \colon C \to \mathbb{N} \rangle$, with $C = \sum_n c_n$, the sum of the fibers. The set of powers of $a$ can be similarly written as $\langle L(a), \mathit{len} \rangle$, with $L(a)$ the type of list of $a$ (a free monoid generated by $a$), and $\mathit{len}$ the function that assigns the length to a list. The monoidal action can then be written using a product (pullback) in the slice category $\mathbf{Set}/\mathbb{N}$:
\[ \left \langle {C \atop p} \right \rangle \times \left \langle {L(a) \atop \mathit{len}} \right \rangle \]

There is an obvious forgetful functor $U \colon \mathbf{Set}/\mathbb{N} \to \mathbf{Set}$, which can be used to express the polynomial action:
\[ M_c a = U\left( 
  \left \langle {C \atop p} \right \rangle \times \left \langle {L(a) \atop \mathit{len}} \right \rangle \right) \]
The traversal is the optic:
\[ \int^{\langle C, p \rangle : \mathbf{Set}/\mathbb{N}} \mathbf{Set} 
\left(s, M_c a \right)  
  \times \mathbf{Set}(M_c b, t) \]
Eqivalently, the second factor can be rewritten as:
\[  \mathbf{Set}\left( \sum_{n \colon \mathbb{N}} c_n \times b^n, t\right) \cong \prod_{n \colon  \mathbb{N}}  \mathbf{Set}(c_n \times b^n, t)\]
This, in turn, is equivalent to a single hom-set in the slice category:
\[ 
 \cong  
(\mathbf{Set}/\mathbb{N})\left(\left \langle {C \atop p} \right \rangle \times \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right) \]
where $\pi_1$ is the projection from the cartesian product.

The traversal is therefore a mixed optic:
\[ \int^{\langle C, p \rangle : \mathbf{Set}/\mathbb{N}} \mathbf{Set} 
\left(s,  M_c a \right)  
  \times (\mathbf{Set}/\mathbb{N})\left( \left \langle {C \atop p} \right \rangle 
  \times \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right) \]

The second factor can be transformed using the internal hom adjunction:
\[ 
(\mathbf{Set}/\mathbb{N})\left(\left \langle {C \atop p} \right \rangle, \left[ \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right] \right) \]
We can then use the ninja Yoneda lemma on the optic to ``integrate'' over $\langle C, p \rangle$ and get:
\[ O(a, b; s, t) \cong \mathbf{Set} \left(  s, U\left( 
  \left[ \left \langle {L(b) \atop \mathit{len}} \right \rangle, \left \langle {\mathbb{N} \times t \atop \pi_1} \right \rangle \right] \times \left \langle {L(a) \atop \mathit{len}} \right \rangle \right) \right) \]
which, in components, reads:
\[ s \to \sum_n \left( (b^n \to t) \times a^n \right) \]
 


\end{document}