From 1a6f409cd1a6ddae6a670d40d867b6a9b22a16a3 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 14 Mar 2024 17:34:50 +0100 Subject: [PATCH] change file names to final chapter order, work on introduction. --- thesis/agda/Coind.agda | 4 ++ thesis/agda/Setoids.agda | 3 ++ thesis/main.tex | 22 ++++------- thesis/src/00_abstract.tex | 10 +++++ thesis/src/00_introduction.tex | 5 --- thesis/src/01_introduction.tex | 38 +++++++++++++++++++ ...preliminaries.tex => 02_preliminaries.tex} | 0 ...-categories.tex => 03_agda-categories.tex} | 0 ...ty-monads.tex => 04_partiality-monads.tex} | 0 .../{04_iteration.tex => 05_iteration.tex} | 2 +- thesis/src/{05_setoids.tex => 06_setoids.tex} | 0 .../{10_conclusion.tex => 07_conclusion.tex} | 0 12 files changed, 64 insertions(+), 20 deletions(-) create mode 100644 thesis/src/00_abstract.tex delete mode 100644 thesis/src/00_introduction.tex create mode 100644 thesis/src/01_introduction.tex rename thesis/src/{01_preliminaries.tex => 02_preliminaries.tex} (100%) rename thesis/src/{02_agda-categories.tex => 03_agda-categories.tex} (100%) rename thesis/src/{03_partiality-monads.tex => 04_partiality-monads.tex} (100%) rename thesis/src/{04_iteration.tex => 05_iteration.tex} (99%) rename thesis/src/{05_setoids.tex => 06_setoids.tex} (100%) rename thesis/src/{10_conclusion.tex => 07_conclusion.tex} (100%) diff --git a/thesis/agda/Coind.agda b/thesis/agda/Coind.agda index 7f20637..069d74f 100644 --- a/thesis/agda/Coind.agda +++ b/thesis/agda/Coind.agda @@ -1,4 +1,8 @@ {-# OPTIONS --guardedness #-} + +-- Agda code that is included in the thesis. +-- just for making sure that everything used in the thesis actually compiles ;) + open import Agda.Builtin.Equality module Coind where module Streams where diff --git a/thesis/agda/Setoids.agda b/thesis/agda/Setoids.agda index 01262b9..56250de 100644 --- a/thesis/agda/Setoids.agda +++ b/thesis/agda/Setoids.agda @@ -1,3 +1,6 @@ +-- Agda code that is included in the thesis. +-- just for making sure that everything used in the thesis actually compiles ;) + module Setoids where open import Level diff --git a/thesis/main.tex b/thesis/main.tex index 41dd334..87f31f3 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -205,13 +205,7 @@ % \chapter*{Licensing} % \doclicenseThis{} -\chapter*{Abstract} -Moggi famously showed how to use category theory (specifically monads) to model the semantics of effectful computations. -In this thesis we want to specifically examine how to model possibly non-terminating computations, which requires a monad supporting some form of partiality. -For that we will consider categorical properties that a monad that models partiality should satisfy and then compare concrete monads in view of these properties. -Capretta's delay monad is a typical example for a partiality monad, but it comes with a too intensional notion of built-in equality. -Since fixing this seems to be impossible without additional axioms, we will look at a novel approach to defining a partiality monad that works in a general setting by making use of previous research on iteration theories and drawing on the inherent connection between partiality and iteration. Lastly, we will see that in the category of setoids this partiality monad instantiates to a quotient of the delay monad. - +\include{src/00_abstract} \tableofcontents @@ -233,13 +227,13 @@ Since fixing this seems to be impossible without additional axioms, we will look \ifdraft{\linenumbers} -\include{src/00_introduction} -\include{src/01_preliminaries} -\include{src/02_agda-categories} -\include{src/03_partiality-monads} -\include{src/04_iteration} -\include{src/05_setoids} -\include{src/10_conclusion} +\include{src/01_introduction} +\include{src/02_preliminaries} +\include{src/03_agda-categories} +\include{src/04_partiality-monads} +\include{src/05_iteration} +\include{src/06_setoids} +\include{src/07_conclusion} \todo[inline]{Add fullstop behind every proof} diff --git a/thesis/src/00_abstract.tex b/thesis/src/00_abstract.tex new file mode 100644 index 0000000..27ff3d2 --- /dev/null +++ b/thesis/src/00_abstract.tex @@ -0,0 +1,10 @@ +\chapter*{Abstract} +Moggi famously showed how to use category theory (specifically monads) to model the semantics of effectful computations. + +In this thesis we will examine how to model possibly non-terminating computations, which requires a monad supporting some form of partiality. +For that we will consider categorical properties that a monad that models partiality should satisfy and then compare concrete monads in view of these properties. + +Capretta's delay monad is a typical example for a partiality monad, but it comes with a too intensional notion of built-in equality. +Since fixing this seems to be impossible without additional axioms, we will examine a novel approach of defining a partiality monad that works in a general setting by making use of previous research on iteration theories and drawing on the inherent connection between partiality and iteration. + +Finally, we will show that in the category of setoids this partiality monad instantiates to a quotient of the delay monad, yielding a concrete description of the partiality monad in this category. diff --git a/thesis/src/00_introduction.tex b/thesis/src/00_introduction.tex deleted file mode 100644 index ad8fadb..0000000 --- a/thesis/src/00_introduction.tex +++ /dev/null @@ -1,5 +0,0 @@ -\chapter{Introduction} - -\section{Motivation} -\info[inline]{Use introductory example from talk} -\todo[inline]{Give overview of thesis} \ No newline at end of file diff --git a/thesis/src/01_introduction.tex b/thesis/src/01_introduction.tex new file mode 100644 index 0000000..29fc1c9 --- /dev/null +++ b/thesis/src/01_introduction.tex @@ -0,0 +1,38 @@ +\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 + +\begin{minted}{haskell} +reverse :: [a] -> [a] +reverse l = revAcc l [] + where + revAcc [] a = a + revAcc (x:xs) a = revAcc xs (x:a) +\end{minted} +and regard the following infinite list +\begin{minted}{haskell} +ones :: [Int] +ones = 1 : ones +\end{minted} + +Now, notice that the call \texttt{reverse ones} will never terminate, thus Haskell does also offer non-termination as a side effect. + +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.} \ No newline at end of file diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/02_preliminaries.tex similarity index 100% rename from thesis/src/01_preliminaries.tex rename to thesis/src/02_preliminaries.tex diff --git a/thesis/src/02_agda-categories.tex b/thesis/src/03_agda-categories.tex similarity index 100% rename from thesis/src/02_agda-categories.tex rename to thesis/src/03_agda-categories.tex diff --git a/thesis/src/03_partiality-monads.tex b/thesis/src/04_partiality-monads.tex similarity index 100% rename from thesis/src/03_partiality-monads.tex rename to thesis/src/04_partiality-monads.tex diff --git a/thesis/src/04_iteration.tex b/thesis/src/05_iteration.tex similarity index 99% rename from thesis/src/04_iteration.tex rename to thesis/src/05_iteration.tex index f174350..2df5368 100644 --- a/thesis/src/04_iteration.tex +++ b/thesis/src/05_iteration.tex @@ -20,7 +20,7 @@ Recall the following notion from~\cite{elgotalgebras}, previously called \emph{c \end{itemize} \end{definition} -Consider an Elgot algebra over the identity functor \(Id : \C \rightarrow \C\) together with the trivial Id-algebra structure \(id : A \rightarrow A\). Morphisms of the form \(f : X \rightarrow A + X\) can then be viewed as modelling one iteration of a loop, where \(X \in \obj{\C}\) is the state space and \(A \in \obj{\C}\) the object of values. Intuitively, in such a setting the iteration operator \({(-)}^\sharp\) runs such a morphism in a loop until it terminates (or diverges), thus assigning it a solution. This is what the \ref{law:guardedfixpoint} axiom guarantees. On the other hand the \ref{law:uniformity} axiom states how to handle loop invariants and finally, the \ref{law:guardedcompositionality} axiom is the most sophisticated one, stating that compatible iterations can be combined into a single iteration with a merged state space. % chktex 2 +Consider an Elgot algebra over the identity functor \(Id : \C \rightarrow \C\) together with the trivial Id-algebra structure \(id : A \rightarrow A\). Morphisms of the form \(f : X \rightarrow A + X\) can then be viewed as modeling one iteration of a loop, where \(X \in \obj{\C}\) is the state space and \(A \in \obj{\C}\) the object of values. Intuitively, in such a setting the iteration operator \({(-)}^\sharp\) runs such a morphism in a loop until it terminates (or diverges), thus assigning it a solution. This is what the \ref{law:guardedfixpoint} axiom guarantees. On the other hand the \ref{law:uniformity} axiom states how to handle loop invariants and finally, the \ref{law:guardedcompositionality} axiom is the most sophisticated one, stating that compatible iterations can be combined into a single iteration with a merged state space. % chktex 2 The previous intuition gives rise to the following simpler definition that has been introduced in~\cite{uniformelgot}. diff --git a/thesis/src/05_setoids.tex b/thesis/src/06_setoids.tex similarity index 100% rename from thesis/src/05_setoids.tex rename to thesis/src/06_setoids.tex diff --git a/thesis/src/10_conclusion.tex b/thesis/src/07_conclusion.tex similarity index 100% rename from thesis/src/10_conclusion.tex rename to thesis/src/07_conclusion.tex