diff --git a/.gitignore b/.gitignore index 10f2896..564842d 100644 --- a/.gitignore +++ b/.gitignore @@ -49,3 +49,5 @@ slides/*.pdf *.auxlock .auctex-auto/ _region_.tex +*.xdv +thesis/_minted-main/ diff --git a/thesis/.vscode/settings.json b/thesis/.vscode/settings.json index 08f0ce6..0acc1f6 100644 --- a/thesis/.vscode/settings.json +++ b/thesis/.vscode/settings.json @@ -7,7 +7,9 @@ "-synctex=1", "-interaction=nonstopmode", "-file-line-error", + "-shell-escape", "-pdf", + "-xelatex", "-outdir=%OUTDIR%", "main.tex" ], diff --git a/thesis/Makefile b/thesis/Makefile index b934397..461584d 100644 --- a/thesis/Makefile +++ b/thesis/Makefile @@ -7,7 +7,7 @@ imgpdf = $(wildcard img/*.pdf) all: $(pdf) $(imgpdf) %.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib) $(imgpdf) - latexmk -file-line-error -synctex=1 -halt-on-error -pdf $< + latexmk -file-line-error -synctex=1 -halt-on-error -shell-escape -pdf $< fast: # enforce tex execution diff --git a/thesis/main.tex b/thesis/main.tex index f170940..b76f688 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -1,7 +1,7 @@ \documentclass[a4paper,11pt,numbers=noenddot]{scrbook} \usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry} -\usepackage[utf8]{inputenc} +% \usepackage[utf8]{inputenc} \usepackage[ngerman,english]{babel} \babeltags{german=ngerman} \usepackage{amssymb} @@ -15,22 +15,33 @@ \usepackage{hyperref} \usepackage{makeidx} \usepackage{graphicx} +\usepackage{fvextra} \usepackage[style=ieee, sorting=ynt]{biblatex} %advanced citations \usepackage[english=british]{csquotes} %biblatex recommended to load this -\usepackage{listings} - [ - language=agda, - extendedchars=true, - inputencoding=utf8, - ] +\usepackage{minted} +\setminted[agda]{ + linenos=true, + breaklines=true, + encoding=utf8, + fontsize=\small, + frame=lines +} +\usepackage{etoolbox,xpatch} + +\makeatletter +\AtBeginEnvironment{minted}{\dontdofcolorbox} +\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}} +\xpatchcmd{\inputminted}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{} +\xpatchcmd{\mintinline}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{} % see https://tex.stackexchange.com/a/401250/ +\makeatother +\usepackage{scrhack} + \usepackage{multicol} \addbibresource{bib.bib} %\usepackage[right]{showlabels} %\usepackage[justific=raggedright,totoc]{idxlayout} \usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense} -\lstset{mathescape} - \addto\extrasenglish{% \renewcommand{\chapterautorefname}{Section} \renewcommand{\sectionautorefname}{Section} @@ -79,6 +90,10 @@ \newcommand*{\theauthor}{\@author} \makeatother +\usepackage{fontspec} +\setmonofont{Noto Sans Mono} + + \begin{document} \pagestyle{plain} \input{src/titlepage}% @@ -95,6 +110,8 @@ Erlangen, \today{} \rule{7cm}{1pt}\\ \chapter*{Licensing} \doclicenseThis{} \tableofcontents + + % \include{src/examples} \include{src/00_introduction} diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index 7a008a8..d931b3d 100644 --- a/thesis/src/01_preliminaries.tex +++ b/thesis/src/01_preliminaries.tex @@ -2,7 +2,7 @@ There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits are clear, having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely. Also ideally such a development will bring researchers together and enable them to work in a unified setting. -In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development. +In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development. This also serves as a quick introduction to the library. \section{Setoid Enriched Categories} The usual textbook definition of category hides some design decisions that have to be made when implementing it in type theory. One would usually see something like this: @@ -17,43 +17,97 @@ A category consists of where the composition is associative and the identity morphisms are identities with respect to the composition. \end{definition} -Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, avoiding Russel's Paradox). Agda's type theory does not have these size problems, so one can use Agda's built-in infinite \lstinline|Set| hierarchy for the collections. One question that is still open is how to express equality between morphisms. A tempting possibility is the built-in propositional equality \lstinline|_$\equiv$_| ... but bla bla use setoid, give category definition in agda. +Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, preventing Russel's Paradox), it is not instantly clear how to translate this to a proof assistant. Furthermore in mathematical textbooks equality between morphisms is usually taken for granted, i.e. there is some global notion of equality that is clear to everyone. In Agda we need to be more thorough, there is no global notion of equality that 'just works', e.g. the standard notion of propositional equality has trouble dealing with functions and needs extra axioms like functional extensionality. +The definition of category that we will work with can be seen in listing~\ref{lst:category} (unnecessary information has been stripped). The key differences to the definition above are firstly that instead of talking about collections, Agda's infinite \mintinline{agda}|Set| hierarchy is utilized to prevent size issues, i.e. the whole category is parametrized by 3 universe levels, one for objects, one for morphisms and one for equalities. The consequence is that the category does not contain a set of all morphisms, instead it contains a set of morphisms for any pair of objects. Furthermore the sets of morphisms are equipped with an equivalence relation \mintinline{agda}|_≈_|, making them setoids. This solves the aforementioned issue of how to implement equality between morphisms, it is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}. +Because of this proofs like \mintinline{agda}|∘-resp-≈| are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. Lastly, the authors also add symmetric proofs like \mintinline{agda}|sym-assoc| to definitions, in this case to guarantee that the opposite category of the opposite category is equal to the original category, and a similar reason for requiring \mintinline{agda}|identity²|, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis. -% TODO move -We assume familiarity with basic concepts of category theory that should be taught in any introductory course, or can be looked up in~\cite{Lane1971}. In particular we will need the notions of category, functor, functor algebra, natural transformation, product and coproduct. +For the rest of this thesis we will assume familiarity with basic concepts of category theory (like functors and natural transformations)~\cite{Lane1971}. We will not explain how they are implemented in order to look at more interesting concepts, for that one should seek out the agda-categories library (\href{https://github.com/agda/agda-categories}{Github}) or consult \cite{agda-categories}. We will however introduce further categorical notions using only their agda representation, it goes without saying that every time we say category, we actually mean setoid-enriched category as defined above. + +\begin{listing}[H] + \begin{minted}{agda} +record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where + field + Obj : Set o + _⇒_ : Obj → Obj → Set ℓ + _≈_ : ∀ {A B : Obj } → (A ⇒ B) → (A ⇒ B) → Set e + + id : ∀ {A : Obj} → (A ⇒ A) + _∘_ : ∀ {A B C : Obj} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C) + + assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} + → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) + sym-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} + → h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f + identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f + identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f + identity² : ∀ {A} → id ∘ id {A} ≈ id {A} + equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B}) + ∘-resp-≈ : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} + → f ≈ h + → g ≈ i + → f ∘ g ≈ h ∘ i + \end{minted} + \caption{Definition of Category~\cite{agda-categories}} + \label{lst:category} +\end{listing} \section{Monads} -% TODO do in Agda -Monads are widely known among programmers as a way of modelling effects in pure languages. Categorically a Monad is a monoid in the category of endofunctors of a category, or in more accessible terms: +Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis, so we will introduce them now. Categorically a Monad is a triple consisting of an endofunctor and two natural transformations called unit and multiplication satisfying some identity and associativity laws (also called the monad laws), the definition can be seen in listing~\ref{lst:monad}. -\begin{definition}[Monad~\cite{Lane1971}] - A monad on a category $\C$ is a triple $(F, \eta, \mu)$, where $F : \C \rightarrow \C$ is an endofunctor and $\eta : Id \rightarrow F, \mu : F^2 \rightarrow F$ are natural transformations, satisfying the following laws: - \begin{enumerate} - % TODO add quantifiers - \item $\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X$ - \item $\mu_X \circ \eta_{FX} = id_{FX}$ - \item $\mu_X \circ F\eta_X = id_{FX}$ - \end{enumerate} -\end{definition} +\begin{listing}[H] + \begin{minted}{agda} +record Monad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where +field + F : Endofunctor C + η : NaturalTransformation idF F + μ : NaturalTransformation (F ∘F F) F -For programmers a second equivalent definition is more useful: + open Category C + module F = Functor F + module η = NaturalTransformation η + module μ = NaturalTransformation μ -\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: - \begin{enumerate} - % TODO add quantifiers - \item $\eta_X^* = id_{FX}$ - \item $\eta_X \circ f^* = f$ - \item $f^* \circ g* = (f \circ g^*)^*$ - \end{enumerate} -\end{definition} + assoc : ∀ {X : Obj} → μ.η X ∘ F.₁ (μ.η X) ≈ μ.η X ∘ μ.η (F.₀ X) + sym-assoc : ∀ {X : Obj} → μ.η X ∘ μ.η (F.₀ X) ≈ μ.η X ∘ F.₁ (μ.η X) + identityˡ : ∀ {X : Obj} → μ.η X ∘ F.₁ (η.η X) ≈ id + identityʳ : ∀ {X : Obj} → μ.η X ∘ η.η (F.₀ X) ≈ id + \end{minted} + \caption{Definition of Monad~\cite{agda-categories}} + \label{lst:monad} +\end{listing} -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 (in a pointful manner) written as \lstinline{f x >>= g} or using Haskell's do-notation: -\begin{lstlisting} +(Note: \mintinline{agda}|F.₀| is the functor action on objects, \mintinline{agda}|F.₁| is the functor action on morphisms and \mintinline{agda}|μ.η X| and \mintinline{agda}|η.η X| are the underlying morphisms of the respective natural transformation for \mintinline{agda}|X|) + +% For programmers a second equivalent definition is more useful: +For programmers the notion of Kleisli triple is more useful, a Kleisli triple consists of an action on \mintinline{agda}|F| on objects, a family of morphisms \mintinline{agda}|η| and a lifting operator on morphisms, the definition can be seen in listing~\ref{lst:kleisli}. + +\begin{listing}[H] + \begin{minted}{agda} +record KleisliTriple {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where + open Category C + field + F : Obj → Obj + η : ∀ (X : Obj) → X ⇒ F X + _* : ∀ {X Y} (f : X ⇒ F Y) → F X ⇒ F Y + + identityˡ : ∀ {X} → (η X)* ≈ id + identityʳ : ∀ {X Y} (f : X ⇒ F Y) → f * ∘ (η X) ≈ f + assoc : ∀ {X Y Z} (f : Y ⇒ F Z) (g : X ⇒ F Y) + → (f * ∘ g)* ≈ f * ∘ g * + sym-assoc : ∀ {X Y Z} (f : Y ⇒ F Z) (g : X ⇒ F Y) + → f * ∘ g * ≈ (f * ∘ g)* + *-resp-≈ : ∀ {X Y} {f g : X ⇒ F Y} → f ≈ g → f * ≈ g * + \end{minted} + \caption{Definition of Kleisli Triple~\cite{agda-categories}} + \label{lst:kleisli} +\end{listing} + +In functional programming languages like Haskell the Kleisli lifting (\mintinline{agda}|_*|) is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and \mintinline{agda}|η| 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 (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation: +\begin{minted}{haskell} do y <- f x g y -\end{lstlisting} +\end{minted} % todo change moggi citation to manes, once I got the original \begin{theorem}[\cite{moggi}] The notions of Kleisli triple and monad are equivalent. @@ -63,42 +117,39 @@ The crux of this proof is defining the triples, the proofs of the corresponding ''$\Rightarrow$'': -Given a Kleisli triple $(F, (\eta_X)_{X\in \vert C \vert}, \_^*)$, +Given a Kleisli triple $(F, \eta, \_^*)$, 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, +we get a Kleisli triple $(F, \eta, \_^*)$ 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. +% TODO agdaify this part + \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} + \begin{minted}{haskell} do x <- p y <- q return (x, y) - \end{lstlisting} + \end{minted} - \begin{lstlisting} + \begin{minted}{haskell} do y <- q x <- p return (x, y) - \end{lstlisting} + \end{minted} \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}$ @@ -117,4 +168,6 @@ Now we can express the above condition: \section{Stable Natural Numbers Object} -\section{Extensive and Distributive Categories} \ No newline at end of file +\section{Extensive and Distributive Categories} + +\section{Free objects} \ No newline at end of file