bsc-leon-vatthauer/slides/sections/01_abstracting.tex

\section{Categorical Notions of Partiality}

\begin{frame}[t, fragile]{Preliminaries}
  We work in category $\mathcal{C}$ that
  \begin{itemize}[<+->]
    \item has finite products
    \item has finite coproducts
    \item is distributive, i.e. the following is an iso:
    % https://q.uiver.app/#q=WzAsMixbMCwwLCIoWCBcXHRpbWVzIFkpICsgKFggXFx0aW1lcyBaKSJdLFs0LDAsIlggXFx0aW1lcyAoWSArIFopIl0sWzAsMSwiZHN0bF57LTF9ICA6PSBbIFxcbGFuZ2xlIGlkICwgaW5sIFxccmFuZ2xlICwgXFxsYW5nbGUgaWQgLCBpbnIgXFxyYW5nbGVdIl1d
    \[\begin{tikzcd}
      {(X \times Y) + (X \times Z)} &&&& {X \times (Y + Z)}
      \arrow["{dstl^{-1}  := [ \langle id , inl \rangle , \langle id , inr \rangle]}", from=1-1, to=1-5]
    \end{tikzcd}\]
    % https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgKFkgKyBaKSJdLFs0LDAsIihYIFxcdGltZXMgWSkgKyAoWCBcXHRpbWVzIFopIl0sWzAsMSwiZHN0bCJdXQ==
    \[\begin{tikzcd}
      {X \times (Y + Z)} &&&& {(X \times Y) + (X \times Z)}
      \arrow["dstl", from=1-1, to=1-5]
    \end{tikzcd}\]
    \item has a natural numbers object $\mathbb{N}$ (which is stable)
  \end{itemize}
  
\end{frame}

\begin{frame}[t, fragile]{Capturing Partiality}{Moggi's categorical semantics~\cite{moggi}}
Goal: interpret an effectul programming language in a category $\mathcal{C}$

\begin{itemize}
  \item<2-> Take a Monad $T$ on $\mathcal{C}$, we view objects $A$ as types of values and objects $TA$ as types of computations.
  \item<3-> Programs form a category $\mathcal{C}_T$ with $\mathcal{C}_T(X,Y) := \mathcal{C}(X, TY)$
\end{itemize}

\onslide<4->
What properties should a monad $T$ for modelling partiality have?

\begin{enumerate}
  \item<5-> Commutativity (also entails strength)
  \item<6-> Morphisms in $\mathcal{C}_T$ should be partial maps
  \item<7-> There should be no other effect besides partiality
\end{enumerate}

\end{frame}

\newcommand{\tdom}{\text{dom}\;}

\begin{frame}[t, fragile]{Capturing Partiality}{Restriction Categories~\cite{restriction}}
\begin{definition}<1->
  A restriction structure on $\mathcal{C}$ is a mapping $\tdom : \mathcal{C}(X,Y) \rightarrow \mathcal{C}(X,X)$ with the following properties:
  \begin{alignat}{1}
    f \circ (\tdom f) &= f\\
    (\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\\
    \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\\
    (\tdom h) \circ f &= f \circ \tdom (h \circ f)
  \end{alignat}
  for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
\end{definition}

\onslide<2->
Intuitively $\tdom f$ captures the domain of definedness of $f$.

\begin{block}{Remark}<3->
  Every category has a trivial restriction structure $\tdom f = id$, we call categories with a non-trivial restriction structure \textit{restriction categories}.
\end{block}
\end{frame}

\begin{frame}[t, fragile]{Capturing Partiality}{Equational Lifting Monads~\cite{eqlm}}
  The following criterion guarantees that some form of partiality is the only possible side-effect:
  \pause
  \begin{definition}
    A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:

    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ==
    \[\begin{tikzcd}
      TX && {TX \times TX} \\
      \\
      && {T(TX \times X)}
      \arrow["\Delta", from=1-1, to=1-3]
      \arrow["\tau", from=1-3, to=3-3]
      \arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
    \end{tikzcd}\]
  \end{definition}
  \pause
  \begin{theorem}
    The Kleisli category of an equational lifting monad is a restriction category.
  \end{theorem}
\end{frame}

\begin{frame}[t, fragile]{Capturing Partiality}{The Maybe Monad}
\begin{itemize}[<+->]
  \item $MX = X + 1$
  \item The maybe monad is strong and commutative:
    \[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1 \]
  \item and the following diagram commutes (i.e. it is an equational lifting monad):
    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0ciJdLFsyLDMsImlkKyEiXSxbMCwzLCJcXGxhbmdsZSBpbmwsaWRcXHJhbmdsZSArICEiLDJdXQ==
    \[\begin{tikzcd}
      {X+1} &&& {(X+1)\times(X+1)} \\
      \\
      &&& {((X+1)\times X) +((X+1)\times 1)} \\
      \\
      &&& {((X+1)\times X)+1}
      \arrow["\Delta", from=1-1, to=1-4]
      \arrow["dstl", from=1-4, to=3-4]
      \arrow["{id+!}", from=3-4, to=5-4]
      \arrow["{\langle inl,id\rangle + !}"', from=1-1, to=5-4]
    \end{tikzcd}\]
  
\end{itemize}
\end{frame}

\begin{frame}[t, fragile]{Capturing Partiality}{Capretta's Delay Monad~\cite{delay}}
\begin{itemize}[<+->]
  \item Recall the delay codatatype:
    
    \[\mprset{fraction={===}}
    \inferrule {x : X} {now\; x : DX}\hskip 2cm
    \inferrule {c : DX} {later\; c : DX}\]

  \item $DX = \nu A. X + A$
  \item By Lambek we get $DX \cong X + DX$ which yields:
  \begin{alignat*}{2}
    &out &&: DX \rightarrow X + DX\\
    &out^{-1} &&: X + DX \rightarrow DX = [ now , later ]
  \end{alignat*}
  \item $D$ (if it exists) is a strong and commutative monad
  \item $D$ is not an equational lifting monad, because besides modelling partiality, it also counts steps \\(e.g. $now\; c \not= later\; (now\; c)$)
\end{itemize}
\end{frame}

\begin{frame}[t, fragile]{Capturing Partiality}{Quotienting the Delay Monad~\cite{quotienting}}
  Following the work by Chapman, Uustalu and Veltri we can quotient $D$ by the 'correct' kind of equality:
  \[\mprset{fraction={===}}
  \inferrule {p \downarrow c \\ q \downarrow c} {p \approx q}\hskip 2cm
  \inferrule {p \approx q} {later\; p \approx later\; q}\]
  \pause
  where
  \[
  \inferrule {\;} {now\;c \downarrow c}\hskip 2cm
  \inferrule {x \downarrow c} {later\; x \downarrow c}\]
  \pause
  we can model this as the coequalizer:
  % https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFhcXHRpbWVzIFxcbWF0aGJie059KSJdLFsyLDAsIkRYIl0sWzQsMCwiRF9cXGFwcHJveCJdLFswLDEsIlxcaW90YV4qIiwwLHsib2Zmc2V0IjotMn1dLFswLDEsIkQgZnN0IiwyLHsib2Zmc2V0IjoyfV0sWzEsMiwiXFxyaG9fWCJdXQ==
  \[\begin{tikzcd}
    {D(X\times \mathbb{N})} && DX && {D_\approx X}
    \arrow["{\iota^*}", shift left=2, from=1-1, to=1-3]
    \arrow["{D fst}"', shift right=2, from=1-1, to=1-3]
    \arrow["{\rho_X}", from=1-3, to=1-5]
  \end{tikzcd}\]
  \pause
  \textbf{Problem}: Defining $\mu_X : D_\approx^2 X \rightarrow D_\approx X$ requires countable choice.
\end{frame}

\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras}
The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}~\cite{elgotalgebras}:
\begin{definition}
  A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
  \begin{itemize}
    \item An object X
    \item for every $f : S \rightarrow X + S$ the iteration $f^\# : S \rightarrow X$, satisfying:
    \begin{itemize}
      \item \textbf{Fixpoint}: $f^\# = [ id , f ^\# ] \circ f$
      \item \textbf{Uniformity}: $(id + h) \circ f = g \circ h \Rightarrow f ^\# = g^\# \circ h$
      \\ for $f : S \rightarrow X + S,\; g : R \rightarrow A + R,\; h : S \rightarrow R$
      \item \textbf{Folding}: $((f^\# + id) \circ h)^\# = [ (id + inl) \circ f , inr \circ h ] ^\#$
      \\ for $f : S \rightarrow A + S,\; h : R \rightarrow S + R$
    \end{itemize}
  \end{itemize}
\end{definition}
\pause
\begin{block}{Remark}
  Every Elgot algebra $(A, (-)^\#)$ comes with a divergence constant $\bot = (inr : 1 \rightarrow A + 1)^\# : 1 \rightarrow A$
\end{block}
\end{frame}

\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Monads~\cite{elgotmonad}}
\begin{definition}
  A monad $\mathbf{T}$ is an Elgot monad if it has an iteration operator $(f : X \rightarrow T(Y + X))^\dagger : X \rightarrow TY$ satisfying:
  \begin{itemize}
    \item \textbf{Fixpoint}: $f^\dagger = [ \eta , f^\dagger ]^* \circ f$
    \\for $f : X \rightarrow T(Y + X)$
    \item \textbf{Uniformity}: $f \circ h = T(id + h) \circ g \Rightarrow f^\dagger \circ h = g^\dagger$
    \\for $f : X \rightarrow T(Y + X) , g : Z \rightarrow T(Y + Z), h : Z \rightarrow X$
    \item \textbf{Naturality}: $g^* \circ f^\dagger = ([ (T inl) \circ g , \eta \circ inr ]^* \circ f )^\dagger$
    \\for $f : X \rightarrow T(Y + X), g : Y \rightarrow TZ$
    \item \textbf{Codiagonal}: $f^{\dagger\dagger} = (T[id , inr ] \circ f)^\dagger$
    \\for $f : X \rightarrow T((Y + X) + X)$
  \end{itemize}
\end{definition}
\pause
\begin{block}{Remark}
Strong Elgot Monads are regarded as minimal semantic structures for interpreting effectful while-languages.
\end{block}

\end{frame}

\begin{frame}[t, fragile]{Partiality from Iteration}{pre-Elgot Monads~\cite{uniformelgot}}
  Relaxing the requirements for Elgot monads we get the following weaker concept:
  \begin{definition}
    A monad $\mathbf{T}$ is called pre-Elgot if every $TX$ extends to an Elgot algebra such that Kleisli lifting is iteration preversing, i.e.
    \[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; f : Z \rightarrow TX + Z, h : X \rightarrow TY\]
  \end{definition}
  \pause
  \begin{theorem}
    Every Elgot monad is pre-Elgot
  \end{theorem}
\end{frame}

\begin{frame}[t, fragile]{Partiality from iteration}{The initial pre-Elgot Monad~\cite{uniformelgot}}
  \begin{itemize}[<+->]
    \item By defining $KX$ as the free Elgot algebra over $X$ we get a monad $K$ (that we assume is stable)
    \item $K$ is strong and commutative
    \item $K$ is an equational lifting monad
    \item $K$ is the initial pre-Elgot monad
  \end{itemize}
\end{frame}

\begin{frame}[t, fragile]{Partiality from iteration}{Closing the gap~\cite{uniformelgot}}
  Let's look at $\mathbf{K}$ under various assumptions:
  \begin{itemize}[<+->]
    \item \textbf{Assuming excluded middle:}
    
    \begin{itemize}[<+->]
      \item The initial pre-Elgot monad and the initial Elgot monad coincide
      \item $DX \cong X \times \mathbb{N} + 1$
      \item $D_\approx X \cong X + 1$
      \item $X + 1$ is the initial (pre-)Elgot monad ($\Rightarrow K \cong (-)+1 \cong D_\approx$)
    \end{itemize}
    
    \item \textbf{Assuming countable choice:}
    \begin{itemize}[<+->]
      \item The initial pre-Elgot monad and the initial Elgot monad coincide
      \item $D_\approx$ is the initial (pre-)Elgot Monad ($\Rightarrow K \cong D_\approx$).
    \end{itemize}
    
  \end{itemize}
\end{frame}