Update .gitlab-ci.yml

.gitignore

@@ -51,3 +51,4 @@ slides/*.pdf
 _region_.tex
 *.xdv
 thesis/_minted-main/
+slides/_minted-main/

.gitlab-ci.yml

@@ -0,0 +1,16 @@
+variables:
+  LATEX_IMAGE: danteev/texlive
+
+build:
+  image: $LATEX_IMAGE
+  script:
+    - cd thesis
+    - latexmk -pdf -xelatex -shell-escape main.tex
+    - cd ../slides
+    - latexmk -pdf -xelatex -shell-escape main.tex
+
+  artifacts:
+    paths:
+      - "thesis/*.pdf"
+      - "slides/*.pdf"
+

slides/.vscode/settings.json

@@ -7,7 +7,9 @@
         "-synctex=1",
         "-interaction=nonstopmode",
         "-file-line-error",
+        "-shell-escape",
         "-pdf",
+        "-xelatex",
         "-outdir=%OUTDIR%",
         "main.tex"
       ],

slides/code-examples/example.hs

@@ -3,10 +3,12 @@ hd [] = error "empty list"
 hd (x : _) = x
 
 main :: IO ()
-main = print (hd []::[String])
+main = do
+  print (Main.reverse ([1,2,3]::[Int]))
+  print (hd []::[String])
 
 reverse :: [a] -> [a]
-reverse l = rev l []
+reverse l = reverseAcc l []
   where
-    rev []     a = a
+    reverseAcc []     a = a
-    rev (x:xs) a = rev xs (x:a)
+    reverseAcc (x:xs) a = reverseAcc xs (x:a)

slides/code-examples/reverse.agda

@@ -13,16 +13,12 @@ module reverse where
     now : A → Delay A
     later : ∞ (Delay A) → Delay A
 
-  foldl : ∀ {A B : Set} → (A → B → A) → A → Colist B → Delay A
-  foldl c n [] = now n
-  foldl c n (x ∷ xs) = later (♯ foldl c (c n x) (♭ xs))
-
-  -- reversing possibly infinite lists
   reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
   reverse {A} = reverseAcc []
     where
       reverseAcc : Colist A → Colist A → Delay (Colist A)
-      reverseAcc = foldl (λ xs x → x ∷ (♯ xs)) -- 'flip _∷_' with extra steps
+      reverseAcc [] a = now a
+      reverseAcc (x ∷ xs) a = later (♯ reverseAcc (♭ xs) (x ∷ (♯ a)))
 
   run_for_steps : ∀ {A : Set} → Delay A → ℕ → Delay A
   run now   x for n     steps = now x

slides/main.tex

@@ -24,8 +24,8 @@
 		   ]{styles/beamerthemefau}
 % ----------------------------------------------------------------------------------------
 % Input and output encoding
-\usepackage[T1]{fontenc}
+% \usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
+% \usepackage[utf8]{inputenc}
 % ----------------------------------------------------------------------------------------
 % Language settings
 \usepackage[english]{babel}
@@ -36,6 +36,7 @@
 % - We use serif for math environements
 % - isomath is used for upGreek letters
 % ----------------------------------------------------------------------------------------
+\usepackage{fvextra}
 \usepackage{isomath}
 \usefonttheme[onlymath]{serif}
 \usepackage{exscale}
@@ -49,7 +50,7 @@
 % ========================================================================================
 % Setup for Titlepage
 % ----------------------------------------------------------------------------------------
-\title{Implementing Notions of Partiality and Delay\\ in Agda}
+\title{Implementing Categorical Notions of Partiality and Delay in Agda}
 \subtitle{Subtitle}
 \author[L. Vatthauer]{
 Leon Vatthauer%\inst{1}
@@ -138,71 +139,20 @@ Leon Vatthauer%\inst{1}
 % The main document
 % ------------------------------------------------
 \usepackage{MnSymbol} % for \squaredots
-\usepackage{listings}
+\usepackage{minted}
-\lstset{mathescape}
+\setminted[agda]{
-
+	linenos=true,
-\usepackage{xcolor}
+	breaklines=true,
-
+	encoding=utf8,
-\definecolor{codegray}{rgb}{0.5,0.5,0.5}
+	fontsize=\small,
-\definecolor{string}{HTML}{79731B}
+	% frame=lines
-\definecolor{keyword}{HTML}{447A59}
-\definecolor{background}{HTML}{E6E6E6}
-\definecolor{error}{HTML}{9B0511}
-\definecolor{agda-name}{HTML}{3b31f9}
-\definecolor{agda-keyword}{HTML}{fc970a}
-\definecolor{agda-constructor}{HTML}{08aa20}
-
-
-\lstdefinestyle{mystyle}{
-    backgroundcolor=\color{background},
-    % commentstyle=\color{codegreen},
-    % keywordstyle=\color{keyword},
-    numberstyle=\tiny\color{codegray},
-    stringstyle=\color{string},
-    basicstyle=\ttfamily\small,
-    breakatwhitespace=false,         
-    breaklines=true,                 
-    captionpos=b,                    
-    keepspaces=true,                 
-    numbers=left,                    
-    numbersep=5pt,                  
-    showspaces=false,                
-    showstringspaces=false,
-    showtabs=false,                  
-    tabsize=2
-}
-\lstdefinelanguage{myhaskell}{
-	keywords=[1]{
-		where
-	},
-	keywordstyle=[1]\color{agda-keyword},
-	keywords=[2]{
-		error
-	},
-	keywordstyle=[2]\color{error},
-	keywords=[3]{
-		head, reverse, rev
-	},
-	keywordstyle=[3]\color{agda-name},
-	morestring=[b]"
 }
+\usepackage{multicol}
 
-\lstdefinelanguage{myagda}{
-	keywords=[1]{
-		data, where
-	},
-	keywordstyle=[1]\color{agda-keyword},
-	keywords=[2]{
-		Delay, Set, foldl, Colist, reverse, reverseAcc, run_for_steps, run, for, steps, fin-colist, inf-colist, never, head, List, Maybe
-	},
-	keywordstyle=[2]\color{agda-name},
-	keywords=[3]{
-		now, later, zero, suc, just, nothing, nil, cons
-	},
-	keywordstyle=[3]\color{agda-constructor}
-}
 
-\lstset{style=mystyle}
+\usepackage{noto-mono}
+% \usepackage{fontspec}
+% \setmonofont{Noto Sans Mono}
 
 \usepackage{lmodern}
 
@@ -236,6 +186,8 @@ at (#3) {#4};
 \end{frame}
 
 \input{sections/00_intro.tex}
+\input{sections/01_abstracting.tex}
+\input{sections/02_goals.tex}
 
 % Stylized outline
 %\begin{frame}[title]{-}

slides/sections/00_intro.tex

@@ -1,27 +1,29 @@
+\section{Partiality in Type Theory}
 \begin{frame}[t, fragile]{Partiality in Haskell}{}
-  \begin{itemize}[<+->]
+  \begin{itemize}
-    \item Haskell allows users to define arbitrary partial functions, some can be spotted easily by their definition:
+    \item<1-> Haskell allows users to define arbitrary partial functions, some can be spotted easily by their definition:
     \vskip 1cm
-    \begin{lstlisting}[language=myhaskell, linewidth=12cm]
+    \begin{minted}{agda}
 head :: [a] -> a
-head [] = error "empty list"
+head []     = error "empty list"
 head (x:xs) = x
-\end{lstlisting}
+\end{minted}
-      \mycallout<3->{21, 1.5}{
+      \mycallout<2->{21, 1.5}{
         ghci> head []\\
         *** Exception: empty list\\
         CallStack (from HasCallStack):\\
         error, called at example.hs:2:9 in main:Main
       }
-    \item
+    \item<3->
     others might be more subtle:
     \vskip 1cm
-    \begin{lstlisting}[language=myhaskell, linewidth=12cm]
+    \begin{minted}{agda}
-reverse l = rev l []
+reverse :: [a] -> [a]
-where
+reverse l = reverseAcc l []
-  rev []     a = a
+  where
-  rev (x:xs) a = rev xs (x:a)
+    reverseAcc []     a = a
-\end{lstlisting}
+    reverseAcc (x:xs) a = reverseAcc xs (x:a)
+\end{minted}
     
     \mycallout<4->{21, 2}{
     ghci> ones = 1 : ones\\
@@ -30,7 +32,6 @@ where
     }
   \end{itemize}
 
-% TODO right of this add error bubble that shows `reverse ones`
 \end{frame}
 
 \begin{frame}[t, fragile]{Partiality in Agda}{The Maybe Monad}
@@ -38,59 +39,56 @@ In Agda every function has to be total and terminating, so how do we model parti
 
 \begin{itemize}[<+->]
   \item Simple errors can be modelled with the maybe monad
-  \begin{lstlisting}[linewidth=14cm, language=myagda]
+  \begin{minted}{agda}
 data Maybe (A : Set) : Set where
-  just : A $\rightarrow$ Maybe A
+  just : A → Maybe A
   nothing : Maybe A
-\end{lstlisting}
+\end{minted}
 
   for head we can then do:
 
-  \begin{lstlisting}[linewidth=14cm, language=myagda]
+  \begin{minted}{agda}
-head : $\forall$ A $\rightarrow$ List A $\rightarrow$ Maybe A
+head : ∀ A → List A → Maybe A
-head nil = nothing
+head nil         = nothing
 head (cons x xs) = just x
-\end{lstlisting}
+\end{minted}
 
-  \item What about \lstinline|reverse|?
+  \item What about \mintinline{agda}|reverse|?
 \end{itemize}
 \end{frame}
 
 \begin{frame}[t, fragile]{Partiality in Agda}{Capretta's Delay Monad}
   \begin{itemize}[<+->]
     \item Capretta's Delay Monad is a \textbf{coinductive} data type whose inhabitants can be viewed as suspended computations. 
-    \begin{lstlisting}[linewidth=20cm, language=myagda]
+    \begin{minted}{agda}
 data Delay (A : Set) : Set where
-  now : A $\rightarrow$ Delay A
+  now : A → Delay A
-  later : $\infty$ (Delay A) $\rightarrow$ Delay A
+  later : ∞ (Delay A) → Delay A
-\end{lstlisting}
+\end{minted}
     \item The delay datatype contains a constant for non-termination:
-    \begin{lstlisting}[linewidth=20cm, language=myagda]
+    \begin{minted}{agda}
 never : Delay A
-never = later ($\sharp$ never)
+never = later (♯ never)
-\end{lstlisting}
+\end{minted}
     \item and we can define a function for \textit{running} a computation (for some amount of steps):
 
-    \begin{lstlisting}[linewidth=20cm, language=myagda]
+    \begin{minted}{agda}
-run_for_steps : Delay A $\rightarrow$ $\mathbb{N}$ $\rightarrow$ Delay A
+run_for_steps : Delay A → ℕ → Delay A
 run now   x for n     steps = now x
 run later x for zero  steps = later x
-run later x for suc n steps = run $\flat$ x for n steps
+run later x for suc n steps = run ♭ x for n steps
-\end{lstlisting}
+\end{minted}
   \end{itemize}
 \end{frame}
 
 \begin{frame}[c, fragile]{Partiality in Agda}{Reversing (possibly infinite) lists}
 \centering
-\begin{lstlisting}[language=myagda]
+\begin{minted}{agda}
-foldl : $\forall$ {A B : Set} $\rightarrow$ (A $\rightarrow$ B $\rightarrow$ A) $\rightarrow$ A $\rightarrow$ Colist B $\rightarrow$ Delay A
+reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
-foldl c n [] = now n
-foldl c n (x $\squaredots$ xs) = later ($\sharp$ foldl c (c n x) ($\flat$ xs))
-
-reverse : $\forall$ {A : Set} $\rightarrow$ Colist A $\rightarrow$ Delay (Colist A)
 reverse {A} = reverseAcc []
   where
-    reverseAcc : Colist A $\rightarrow$ Colist A $\rightarrow$ Delay (Colist A)
+    reverseAcc : Colist A → Colist A → Delay (Colist A)
-    reverseAcc = foldl ($\lambda$ xs x $\rightarrow$ x $\squaredots$ ($\sharp$ xs))
+    reverseAcc [] a = now a
-\end{lstlisting}
+    reverseAcc (x ∷ xs) a = later (♯ reverseAcc (♭ xs) (x ∷ (♯ a)))
+\end{minted}
 \end{frame}

slides/sections/01_abstracting.tex

@@ -0,0 +1,56 @@
+\section{Categorical Notions of Partiality}
+
+% \begin{frame}[t, fragile]{Classifying Partiality Monads}
+% A partiality monad should have the following properties:
+%   \begin{itemize}
+%     \item The following two 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 (partial) computations.
+%   \end{itemize}
+% \end{frame}
+
+\begin{frame}[t, fragile]{Capturing Partiality Categorically}
+\begin{itemize}
+  \item moggi denotational semantics (values A, computations TA)
+
+  \item restriction categories
+
+  \item equational lifting monads
+\end{itemize}
+\end{frame}
+
+\begin{frame}[t, fragile]{The Maybe Monad}
+\begin{itemize}
+  \item Short definition
+  \item is equational lifting monad
+\end{itemize}
+\end{frame}
+
+\begin{frame}[t, fragile]{The Delay Monad}
+\begin{itemize}
+  \item Definition
+  \item Strong-Bisimilarity
+  \item Weak-Bisimilarity (Monad?)
+\end{itemize}
+\end{frame}
+
+\begin{frame}[t, fragile]{Iteration}
+\begin{itemize}
+  \item Elgot-Algebras
+  \item Free Elgot-Algebras yield monad K
+  \item K is equational lifting
+  \item K instantiates to maybe and delay
+\end{itemize}
+\end{frame}

slides/sections/02_goals.tex

@@ -0,0 +1,24 @@
+\section{Implementation in Agda}
+
+\begin{frame}[t, fragile]{Goals}
+  \begin{itemize}
+    \item Formalize delay monad (categorically as terminal coalgebra) + properties
+    \item Formalize K + properties
+    \item Case study on Setoids
+  \end{itemize}
+\end{frame}
+
+\begin{frame}[t, fragile]{Category theory in Agda}
+  agda-categories
+\end{frame}
+
+\begin{frame}[t, fragile]{What I managed to show}
+  TODO
+\end{frame}
+
+\begin{frame}[t, fragile]{Further work}
+\begin{itemize}
+  \item Show that $\tilde{D}$ is monad (under conditions)
+  \item Show that $K \cong \tilde{D}$ (under conditions)
+\end{itemize}
+\end{frame}

thesis/main.tex

@@ -53,7 +53,7 @@
   \chaptermark{#1}%
   \addcontentsline{toc}{chapter}{#1}}
 
-\newcommand\C{\mathcal{C}}
+%\newcommand\C{\mathcal{C}}
 
 \declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition}
 \declaretheorem[name=Example,style=definition,sibling=definition]{example}
@@ -90,8 +90,9 @@
 \newcommand*{\theauthor}{\@author}
 \makeatother
 
-\usepackage{fontspec}
+\usepackage{noto-mono}
-\setmonofont{Noto Sans Mono}
+%\usepackage{fontspec}
+%\setmonofont{Noto Sans Mono}
 
 
 \begin{document}

thesis/src/01_preliminaries.tex

@@ -149,7 +149,7 @@ When modelling partiality with a monad, one would expect the following two progr
 \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:
+\begin{definition}[Strong Monad~\cite{moggi}] A monad $M$ on a cartesian category $\mathcal{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:
   \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}$