.gitignore

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

.gitlab-ci.yml

@@ -1,16 +0,0 @@
-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,9 +7,7 @@
         "-synctex=1",
         "-interaction=nonstopmode",
         "-file-line-error",
-        "-shell-escape",
         "-pdf",
-        "-xelatex",
         "-outdir=%OUTDIR%",
         "main.tex"
       ],
@@ -24,4 +22,4 @@
       ]
     }
   ]
-  }
+  }

slides/code-examples/example.hs

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

slides/code-examples/reverse.agda

@@ -13,12 +13,16 @@ 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 [] a = now a
+      reverseAcc = foldl (λ xs x → x ∷ (♯ xs)) -- 'flip _∷_' with extra steps
-      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,7 +36,6 @@
 % - We use serif for math environements
 % - isomath is used for upGreek letters
 % ----------------------------------------------------------------------------------------
-\usepackage{fvextra}
 \usepackage{isomath}
 \usefonttheme[onlymath]{serif}
 \usepackage{exscale}
@@ -50,7 +49,7 @@
 % ========================================================================================
 % Setup for Titlepage
 % ----------------------------------------------------------------------------------------
-\title{Implementing Categorical Notions of Partiality and Delay in Agda}
+\title{Implementing Notions of Partiality and Delay\\ in Agda}
 \subtitle{Subtitle}
 \author[L. Vatthauer]{
 Leon Vatthauer%\inst{1}
@@ -139,20 +138,71 @@ Leon Vatthauer%\inst{1}
 % The main document
 % ------------------------------------------------
 \usepackage{MnSymbol} % for \squaredots
-\usepackage{minted}
+\usepackage{listings}
-\setminted[agda]{
+\lstset{mathescape}
-	linenos=true,
+
-	breaklines=true,
+\usepackage{xcolor}
-	encoding=utf8,
+
-	fontsize=\small,
+\definecolor{codegray}{rgb}{0.5,0.5,0.5}
-	% frame=lines
+\definecolor{string}{HTML}{79731B}
+\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}
+}
 
-\usepackage{noto-mono}
+\lstset{style=mystyle}
-% \usepackage{fontspec}
-% \setmonofont{Noto Sans Mono}
 
 \usepackage{lmodern}
 
@@ -186,8 +236,6 @@ 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,29 +1,27 @@
-\section{Partiality in Type Theory}
 \begin{frame}[t, fragile]{Partiality in Haskell}{}
-  \begin{itemize}
+  \begin{itemize}[<+->]
-    \item<1-> Haskell allows users to define arbitrary partial functions, some can be spotted easily by their definition:
+    \item Haskell allows users to define arbitrary partial functions, some can be spotted easily by their definition:
     \vskip 1cm
-    \begin{minted}{agda}
+    \begin{lstlisting}[language=myhaskell, linewidth=12cm]
 head :: [a] -> a
-head []     = error "empty list"
+head [] = error "empty list"
 head (x:xs) = x
-\end{minted}
+\end{lstlisting}
-      \mycallout<2->{21, 1.5}{
+      \mycallout<3->{21, 1.5}{
         ghci> head []\\
         *** Exception: empty list\\
         CallStack (from HasCallStack):\\
         error, called at example.hs:2:9 in main:Main
       }
-    \item<3->
+    \item
     others might be more subtle:
     \vskip 1cm
-    \begin{minted}{agda}
+    \begin{lstlisting}[language=myhaskell, linewidth=12cm]
-reverse :: [a] -> [a]
+reverse l = rev l []
-reverse l = reverseAcc l []
+where
-  where
+  rev []     a = a
-    reverseAcc []     a = a
+  rev (x:xs) a = rev xs (x:a)
-    reverseAcc (x:xs) a = reverseAcc xs (x:a)
+\end{lstlisting}
-\end{minted}
     
     \mycallout<4->{21, 2}{
     ghci> ones = 1 : ones\\
@@ -32,6 +30,7 @@ reverse l = reverseAcc l []
     }
   \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}
@@ -39,56 +38,59 @@ 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{minted}{agda}
+  \begin{lstlisting}[linewidth=14cm, language=myagda]
 data Maybe (A : Set) : Set where
-  just : A → Maybe A
+  just : A $\rightarrow$ Maybe A
   nothing : Maybe A
-\end{minted}
+\end{lstlisting}
 
   for head we can then do:
 
-  \begin{minted}{agda}
+  \begin{lstlisting}[linewidth=14cm, language=myagda]
-head : ∀ A → List A → Maybe A
+head : $\forall$ A $\rightarrow$ List A $\rightarrow$ Maybe A
-head nil         = nothing
+head nil = nothing
 head (cons x xs) = just x
-\end{minted}
+\end{lstlisting}
 
-  \item What about \mintinline{agda}|reverse|?
+  \item What about \lstinline|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{minted}{agda}
+    \begin{lstlisting}[linewidth=20cm, language=myagda]
 data Delay (A : Set) : Set where
-  now : A → Delay A
+  now : A $\rightarrow$ Delay A
-  later : ∞ (Delay A) → Delay A
+  later : $\infty$ (Delay A) $\rightarrow$ Delay A
-\end{minted}
+\end{lstlisting}
     \item The delay datatype contains a constant for non-termination:
-    \begin{minted}{agda}
+    \begin{lstlisting}[linewidth=20cm, language=myagda]
 never : Delay A
-never = later (♯ never)
+never = later ($\sharp$ never)
-\end{minted}
+\end{lstlisting}
     \item and we can define a function for \textit{running} a computation (for some amount of steps):
 
-    \begin{minted}{agda}
+    \begin{lstlisting}[linewidth=20cm, language=myagda]
-run_for_steps : Delay A → ℕ → Delay A
+run_for_steps : Delay A $\rightarrow$ $\mathbb{N}$ $\rightarrow$ 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 ♭ x for n steps
+run later x for suc n steps = run $\flat$ x for n steps
-\end{minted}
+\end{lstlisting}
   \end{itemize}
 \end{frame}
 
 \begin{frame}[c, fragile]{Partiality in Agda}{Reversing (possibly infinite) lists}
 \centering
-\begin{minted}{agda}
+\begin{lstlisting}[language=myagda]
-reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
+foldl : $\forall$ {A B : Set} $\rightarrow$ (A $\rightarrow$ B $\rightarrow$ A) $\rightarrow$ A $\rightarrow$ Colist B $\rightarrow$ Delay 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 → Colist A → Delay (Colist A)
+    reverseAcc : Colist A $\rightarrow$ Colist A $\rightarrow$ Delay (Colist A)
-    reverseAcc [] a = now a
+    reverseAcc = foldl ($\lambda$ xs x $\rightarrow$ x $\squaredots$ ($\sharp$ xs))
-    reverseAcc (x ∷ xs) a = later (♯ reverseAcc (♭ xs) (x ∷ (♯ a)))
+\end{lstlisting}
-\end{minted}
 \end{frame}

slides/sections/01_abstracting.tex

@@ -1,56 +0,0 @@
-\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

@@ -1,24 +0,0 @@
-\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,9 +90,8 @@
 \newcommand*{\theauthor}{\@author}
 \makeatother
 
-\usepackage{noto-mono}
+\usepackage{fontspec}
-%\usepackage{fontspec}
+\setmonofont{Noto Sans Mono}
-%\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 $\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{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{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}$