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

\section{Categorical Notions of Partiality}

\begin{frame}[t, fragile]{Capturing Partiality Categorically}{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}$, then values are denoted by objects $A$ and computations by $TA$
  \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)
  % , i.e. the following programs should yield equal results:
  %   \begin{multicols}{2}
  %     \begin{minted}{haskell}
  %       do x <- p
  %          y <- q
  %          return (x, y)
  %       \end{minted}
        
  %       \begin{minted}{haskell}
  %       do y <- q
  %          x <- p
  %          return (x, y)
  %     \end{minted}
  %   \end{multicols}
  %   where p and q are programs.  
  \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}

\begin{frame}[t, fragile]{Capturing Partiality Categorically}{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}\]
  \end{itemize}
  
\end{frame}

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

\begin{frame}[t, fragile]{Capturing Partiality Categorically}{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 KY, g : X \rightarrow KZ, h: Y \rightarrow KZ$.
\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 Categorically}{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}

% write on board:
% equational lifting: do x <- p; return (return x, x) = do x <- p; return (p, x)

\begin{frame}[t, fragile]{Capturing Partiality Categorically}{The Maybe Monad}
\begin{itemize}[<+->]
  \item $MX = X + 1$
  \item on a distributive category the maybe monad is strong and commutative:
    \[ \tau_{X,Y} := X \times (Y + 1) \overset{dstr}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+1}{\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["dstr", 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 Categorically}{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 Categorically: $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 (on a cartesian, cocartesian, distributive category)
  \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}

% write on board:
% \eta = now
% given f : X \rightarrow TY, f* is defined by corecursion.



%%%%%%%%
% NOTE:
% quotienting D should be covered later in the agda chapter, not here!

% \begin{frame}[t, fragile]{The quotiented Delay Monad}
%   Following the work in~\cite{quotienting} we quotient $D$ by weak bisimilarity: 
%   \[\mprset{fraction={===}}
%   \inferrule {p \downarrow c \\ q \downarrow c} {p \approx q}\hskip 2cm
%   \inferrule {p \approx q} {later\; p \approx later\; q}\]

% \end{frame}
%%%%%%%

\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras~\cite{elgotalgebras}}
The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}:
\begin{definition}
  A (unguarded) Elgot Algebra 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}}
Recall the following notion:
\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}:
    \item \textbf{Naturality}:
    \item \textbf{Codiagonal}:
    \item \textbf{Uniformity}:
  \end{itemize}
\end{definition}
\begin{block}{Remark}
Strong Elgot Monads are regarded as minimal semantic structures for interpreting effectful while-languages.
\end{block}

\end{frame}


% TODO 
% maybe dont talk about elgot monads at all, give intuition for the initial pre Elgot monad.
\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}
  \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$
    \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}
  ...
\end{frame}


%% TODOs:
% cite stefan
% cite sergey