work on thesis

thesis/main.tex

@@ -17,6 +17,8 @@
 \usepackage{graphicx}
 \usepackage[style=ieee, sorting=ynt]{biblatex}    %advanced citations
 \usepackage[english=british]{csquotes}           %biblatex recommended to load this
+\usepackage{listings}[language = haskell]
+\usepackage{multicol}
 \addbibresource{bib.bib}
 %\usepackage[right]{showlabels}
 %\usepackage[justific=raggedright,totoc]{idxlayout}

thesis/src/01_preliminaries.tex

@@ -3,6 +3,8 @@ We assume familiarity with basic concepts of category theory that should be taug
 
 In the rest of this section we will look at other categorical notions that are either less well-known, or crucial for this thesis and therefore require special attention.
 
+% TODO add conventions i.e. \C for categories, how do products and coproducts look, etc.
+
 \section{Stable Natural Numbers Object}
 
 \section{Extensive and Distributive Categories}
@@ -22,8 +24,8 @@ Monads are widely known among programmers as a way of modelling effects in pure
 
 For programmers a second equivalent definition is more useful:
 
-\begin{definition}[Kleisli triple~\cite{moggi}]
+\begin{definition}[Kleisli Triple~\cite{moggi}]
-  A kleisli triple on a category $\C$ is a triple $(F, \eta, _*)$, where $F : \vert \C \vert \rightarrow \vert \C \vert$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\vert\C\vert}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting. With the following laws:
+  A kleisli triple on a category $\C$ is a triple $(F, \eta, \_^*)$, where $F : \vert \C \vert \rightarrow \vert \C \vert$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\vert\C\vert}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting. With the following laws:
   \begin{enumerate}
     % TODO add quantifiers
     \item $\eta_X^* = id_{FX}$
@@ -32,6 +34,68 @@ For programmers a second equivalent definition is more useful:
   \end{enumerate}
 \end{definition}
 
+In functional languages like Haskell the Kleisli lifting is usually called \textit{bind} or written infix as \lstinline{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (pointfully) written as \lstinline{f x >>= g} or using Haskell's do-notation:
+\begin{lstlisting}
+  do y <- f x
+     g y
+\end{lstlisting}
+
 % todo change moggi citation to manes, once I got the original
 \begin{theorem}[\cite{moggi}] The notions of Kleisli triple and monad are equivalent.
 \end{theorem}
+\begin{proof}
+The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out and can be looked up in the appendix. % TODO add reference to appendix
+
+
+''$\Rightarrow$'':
+Given a Kleisli triple $(F, (\eta_X)_{X\in \vert C \vert}, \_^*)$, 
+we get a monad $(F, \eta, \mu)$ where $F$ is the object mapping of the Kleisli triple together with the functor action $F(f : X \rightarrow Y) = (\eta_Y \circ f)^*$,
+$\eta$ is the morphism family of the Kleisli triple where naturality is easy to show and $\mu$ is a natural transformation defined as $\mu_X = id_{FX}^*$
+
+
+''$\Leftarrow$'': \\
+Given a monad $(F, \eta, \mu)$,
+we get a Kleisli triple $(F, (\eta_X)_{X\in\vert\C\vert}, \_^*)$ by restricting the functor $F$ on objects, 
+forgetting the naturality of $\eta$ and defining $f^* = \mu_Y \circ Ff$ for any $f : X \rightarrow FY$.
+\end{proof}
+
+For the rest of this thesis we will use both equivalent notions interchangeably to make definitions easier.
+
+\section{Strong and Commutative Monads}
+When modelling partiality with a monad, one would expect the following two programs to be equivalent:
+\begin{multicols}{2}
+  \begin{lstlisting}
+    do x <- p
+       y <- q
+       return (x, y)
+    \end{lstlisting}
+    
+    \begin{lstlisting}
+    do y <- q
+       x <- p
+       return (x, y)
+  \end{lstlisting}
+\end{multicols}
+where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
+
+\begin{definition}[Strong Monad~\cite{moggi}] A monad $M$ on a cartesian category $\C$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times MY \rightarrow M(X \times Y)$, satisfying the following conditions:
+% TODO rethink this... either:
+  % - leave it out
+  % - do commuting diagrams
+  % - keep this style and introduce assoc
+
+  \begin{enumerate}
+  \item $M\pi_2 \circ \tau_{1,X} = \pi_2$
+  \item $M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,MZ}$
+  \item $\tau_{X,Y} \circ (id_X \times \eta_Y) = \eta_{X\times Y}$
+  \item $\tau_{X,Y} \circ (id_X \times \mu_Y) = \mu_{X\times Y} \circ M\tau_{X,Y} \circ \tau_{X,MY}$
+\end{enumerate}
+\end{definition}
+
+Now we can express the above condition:
+\begin{definition}[Commutative Monad~\cite{moggi}]
+  A strong monad $M$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength $\hat{\tau}_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap$, where $swap = \langle \pi_2 , \pi_1 \rangle$. Concretely if the following equation holds:
+  \[
+  \tau_{X,Y}^* \circ \hat{\tau}_{X, MY} = \hat{\tau}_{X,Y}^* \circ \tau_{X, MY}
+  \]
+\end{definition}

thesis/src/A1_contributions.tex

@@ -1,5 +1,10 @@
 \chapter{Open Source Contributions}
 % IDEA: Include formalization of kleisli-triple, distributive category and PNNO in appendix.
+Many basic definitions that were needed for the formalization of this thesis were already included in the agda-categories library, but some had to be added, in this section we'll look at these definitions and explain some design decisions that were made.
+
+% TODO chapter formalizing category theory first 
 \section{Kleisli Triple}
+
+\section{Commutative Monad}
 \section{Distributive Categories}
 \section{Stable Natural Numbers Object}