Work on introduction and the section on the formalization

thesis/.vscode/ltex.dictionary.en-US.txt

@@ -74,3 +74,6 @@ expressivity
 Friedrich-Alexander-Universität
 Erlangen-Nürnberg
 Goncharov
+denotational
+Plotkin
+monadic

thesis/bib.bib

@@ -348,3 +348,25 @@
   biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
   bibsource  = {dblp computer science bibliography, https://dblp.org}
 }
+
+@article{plotkin1975call,
+  title     = {Call-by-name, call-by-value and the $\lambda$-calculus},
+  author    = {Plotkin, Gordon D.},
+  journal   = {Theoretical computer science},
+  volume    = {1},
+  number    = {2},
+  pages     = {125--159},
+  year      = {1975},
+  publisher = {Elsevier}
+}
+
+@article{scott1993type,
+  title     = {A type-theoretical alternative to ISWIM, CUCH, OWHY},
+  author    = {Scott, Dana S},
+  journal   = {Theoretical Computer Science},
+  volume    = {121},
+  number    = {1-2},
+  pages     = {411--440},
+  year      = {1993},
+  publisher = {Elsevier}
+}

thesis/src/01_introduction.tex

@@ -1,16 +1,7 @@
 \chapter{Introduction}
 
-Haskell is considered a purely functional programming language, though the notion of purity used is an informal one, not to be confused with the standard notion of pure function, i.e.\ a function that does not have any side effects.
-For there are indeed Haskell functions that have side effects, consider the following function for retrieving the head of a list:
-
-\begin{minted}{haskell}
-head :: [a] -> a
-head (x:xs) = x 
-\end{minted}
-
-Indeed, this function is partial, since for empty lists it will cause an exception to be thrown by the Haskell compiler and thus Haskell does at least offer exceptions as a side effect.
-Furthermore, consider the following standard list reversal function
-
+Haskell is considered a purely functional programming language, though the notion of purity referenced is an informal one, not to be confused with the standard notion of pure function, which describes functions that do not have any side effects.
+Indeed, as a programming language that offers general recursion, Haskell does at least have to include partiality as a side effect. To illustrate this, consider the following standard list reversal function
 \begin{minted}{haskell}
 reverse :: [a] -> [a]
 reverse l = revAcc l []
@@ -18,21 +9,18 @@ reverse l = revAcc l []
     revAcc []     a = a
     revAcc (x:xs) a = revAcc xs (x:a)
 \end{minted}
-and regard the following infinite list
+and regard the following definition of an infinite list:
 \begin{minted}{haskell}
 ones :: [Int]
 ones = 1 : ones
 \end{minted}
+Of course the call \texttt{reverse ones} will never terminate, hence \texttt{reverse} is a partial function.
+Thus, in order to reason about Haskell programs, or generally programs of any programming language offering general recursion, one needs to be able to model partiality as a side effect.
 
-Now, notice that the call \texttt{reverse ones} will never terminate, thus Haskell does also offer non-termination as a side effect.
+Generally for modelling programming languages there are three prevailing methods. First is the operational approach introduced by Plotkin~\cite{plotkin1975call}, where partial functions are used that map programs to their resulting values, secondly there is the denotational approach by Scott~\cite{scott1993type}, where programming languages are interpreted mathematically, by functions capturing the ``meaning'' of programs.
+For this thesis we will consider the third, categorical approach that has been introduced by Moggi~\cite{moggi}.
+In the categorical approach programs are interpreted in categories, where objects represent types and monads are used to model side effects.
+The goal for this thesis is thus to study monads which are suitable for modeling partiality.
 
-Combining these observations we can draw the conclusion that in order to interpret the Haskell programming language, we will need a way to model general partiality as a side effect.
-Moggi has introduced a method for interpreting programming languages by means of category theory.
-Notably, one needs a monad that is suitable for modelling the desired effects.
-We will thus consider monads that are suitable for modelling partiality and the properties that they should have in \autoref{chp:partiality}.
-Capretta's delay monad is one such monad that is useful for modelling partiality in type theory.
-In a more general setting the delay monad however turns out to be not suitable, thus we will introduce a novel partiality monad that is defined using minimal assumptions in \autoref{chp:iteration}.
-Lastly, in \autoref{chp:setoids} we will give a concrete description of this very general monad in the category of setoids, where it instantiates to a specific quotient of the delay monad.
-
-\todo[inline]{Text needs a lot of work\ldots}
-\todo[inline]{Mention formalization and chapter.}
+We use the dependent programming language Agda~\cite{agda} as a safe and type-checked environment for reasoning in category theory, therefore in \autoref{chp:agda-cat} we start out by quickly introducing the Agda programming language as well as the category theory library that we will be working with. In \autoref{chp:partiality} we will then consider various properties that partiality monads should have and examine Capretta's delay monad~\cite{delay}, which has been introduced in type theory as a coinductive data type and then studied as a monad in the category of setoids. We will examine the delay monad in a general categorical setting, where however the delay monad will prove to be insufficient as a monad for modeling only partiality due to the too intensional notion of equality that this monad comes with. It is believed to be impossible to remedy this problem in a way that preserves the monadic structure without use of additional axioms, thus in \autoref{chp:iteration} we will draw on the inherent connection between iteration and recursion to define a suitable partiality monad in a general setting without extra axioms, by relating to previous research on iteration theories. This monad has first been introduced and studied in~\cite{uniformelgot} under weaker assumptions than we use, concretely by weakening the notion of Elgot algebra to the notion of uniform iteration algebra, which uses fewer axioms. During mechanization of the results concerning this monad it turned out that under the weaker assumptions, desirable properties like commutativity seem not to be provable, resulting in the adaptation of this monad.
+Lastly, in \autoref{chp:setoids} we will study this partiality monad in the category of setoids, where it will turn out to be equivalent to a certain quotient of the delay monad.

thesis/src/03_agda-categories.tex

@@ -68,7 +68,9 @@ or more succinctly using an anonymous \(\lambda\)-function
   repeat : {A : Set} (a : A) → coList A
   repeat a = a ∷ λ { .force → repeat a }
 \end{minted}
-In \autoref{chp:setoids} we will have to deal with such a coinductive type that is defined by constructors. To avoid the overhead of defining every data type twice and using mutual function definitions in the thesis, we will work in a type theory that does offer coinductive types with constructors and their respective corecursion and coinduction principles. However, in the formalization we stick to using coinductive records as to implement best practices. The translation between the two styles is straightforward, as illustrated by the previous example.
+In \autoref{chp:setoids} we will work with such a coinductive type that is defined by constructors, hence to avoid the overhead of defining every data type twice and using mutual function definitions in the thesis, we will work in a type theory that does offer coinductive types with constructors and their respective corecursion and coinduction principles.
+However, in the formalization we stick to using coinductive records as to implement best practices.
+The translation between the two styles is straightforward, as illustrated by the previous example.
 
 \section{Setoid Enriched Categories}
 Let us now consider how to implement category theory in Agda. The usual textbook definition of a category glosses over some design decisions that have to be made when implementing it in type theory. One would usually see something like this:
@@ -126,9 +128,10 @@ record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
 From this it should be clear how other basic notions like functors or natural transformations look in the library.
 
 \section{The formalization}
+Every result and used fact (except for \autoref{prop:liftingkleisli}) in this thesis has been proven either in our own formalization\footnote{\href{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}} or in the agda-categories library~\cite{agda-categories}.
+The formalization is meant to be used as a reference alongside this thesis, where concrete details of proofs can be looked up and verified.
+The preferred format for viewing the formalization is as automatically generated clickable HTML code\footnote{\href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}},
+where multiple annotations explaining the structure have been added in Markdown, however concrete explanations of the proofs and their main ideas are mostly just contained in this thesis.
 
-\improvement{Explain more}
-
-The Agda formalization of this thesis is structured similar to the agda-categories library, e.g.\ key concepts like monads and categories correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties, and possibly folders `Instances' for specific instances, and `Construction' for blueprints for constructing this concept (e.g.\ the Kleisli category of a monad would be in `Category.Construction.Kleisli').
-
-The source code of the formalization can be found \href{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}{here} (internal) or as clickable HTML \href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}{here} (public).
+In the future this formalization may be adapted into a separate library that uses the agda-categories library as a basis but is more focussed on the study of partiality monads and iteration theories.
+As such the formalization has been structured similar to the agda-categories library, where key concepts such as monads correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties.

thesis/src/04_partiality-monads.tex

@@ -81,9 +81,9 @@ To make the equational lifting property more comprehensible we can alternatively
 
 That is, if some computation \(p : TX\) terminates with the result \(x : X\), then \(p = return\;x\) must hold afterwards. This of course implies that running \(p\) multiple times yields the same result as running \(p\) once.
 
-\begin{theorem}[\cite{eqlm}]
+\begin{proposition}[\cite{eqlm}]\label{prop:liftingkleisli}
   If \(T\) is an equational lifting monad the Kleisli category \(\mathcal{C}^T\) is a restriction category.
-\end{theorem}
+\end{proposition}
 
 Definition~\ref{def:eqlm} combines all three properties stated at the beginning of the section, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads. For the rest of this chapter we will use these definitions to compare two monads that are commonly used to model partiality.