% chktex-file 46 \section{Introduction} This is a summary of the course ``Algebra des Programmierens'' taught by Prof.\ Dr.\ Stefan Milius in the winter term 2023/2024 at the FAU~\footnote{Friedrich-Alexander-Universität Erlangen-Nürnberg}. The course is based on~\cite{poll1999algebra} with~\cite{adamek1990abstract} as a reference for category theory. Goal of the course is to develop a mathematical theory for semantics of data types and their accompanying proof principles. The chosen environment is the field of category theory. \subsection{Functions} A function $f : X \rightarrow Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$). More concretely $f$ is a relation $f \subseteq X \times Y$ which is \begin{itemize} \item \emph{left-total}, i.e.\ for all $x \in X$ exists some $y \in Y$ such that $(x,y) \in f$; \item \emph{right-unique}, i.e.\ any $(x,y),(x,y') \in f$ imply $y = y'$. \end{itemize} Often, one is also interested in the symmetrical properties, a function is called \begin{itemize} \item \emph{injective} or \emph{left-unique} if for every $x,x' \in X$ the implication $f(x) = f(x') \rightarrow x = x'$ holds; \item \emph{surjective} or \emph{right-total} if for every $y \in Y$ there exists an $x \in X$ such that $f(x) = y$; \item \emph{bijective} if it is injective and surjective. \end{itemize} \begin{example} \begin{enumerate} \item The identity function $id_A : A \rightarrow A$, $id_A(x) = x$ \item The constant function $b! : A \rightarrow B$ for $b \in B$ defined by $b!(x) = b$ \item The inclusion function $i_A : A \rightarrow B$ for $A \subseteq B$ defined by $i_A(x) = x$ \item Constants $b : 1 \rightarrow B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$. \item Composition of function $f : A \rightarrow B, g : B \rightarrow C$ called $g \circ f : A \rightarrow C$ defined by $(g \circ f)(x) = g(f(x))$. \item The empty function $¡ : \emptyset \rightarrow B$ \item The singleton function $! : A \rightarrow 1$ \end{enumerate} \end{example} \subsection{Data Types} Programs work with data that should ideally be organized in a useful manner. A useful representation for data in functional programming is by means of \emph{algebraic data types}. Some basic data types (written in Haskell notation) are \begin{minted}{haskell} data Bool = True | False data Nat = Zero | Succ Nat \end{minted} These data types are declared by means of constructors, yielding concrete descriptions how inhabitants of these types are created. \emph{Parametric data types} are additionally parametrized by another data type, e.g.\ \begin{minted}{haskell} data Maybe a = Nothing | Just a data Either a b = Left a | Right b data List a = Nil | Cons a (List a) \end{minted} Such data types (parametric or non-parametric) usually come with a principle for defining functions called recursion and in richer type systems (e.g.\ in a dependently typed setting) with a principle for proving facts about recursive functions called induction. Equivalently, every function defined by recursion can be defined via a \emph{fold}-function which satisfies an identity and fusion law, which replace the induction principle. Let us now consider two examples of data types and illustrate this. \subsubsection{Natural Numbers} The type of natural numbers comes with a fold function $foldn : C \rightarrow (Nat \rightarrow C) \rightarrow Nat \rightarrow C$ for every $C$, defined by \begin{alignat*}{2} & foldn\;c\;h\;zero & & = c \\ & foldn\;c\;h\;(suc\;n) & & = h\;(foldn\;c\;h\;n) \end{alignat*} \begin{example} Let us now consider some functions defined in terms of $foldn$. \begin{itemize} \item $iszero : Nat \rightarrow Bool$ is defined by \[iszero = foldn\;true\;false!\] \item $plus : Nat \rightarrow Nat \rightarrow Nat$ is defined by \[plus = foldn\;id (\lambda f\;n. succ (f\;n)) \] \end{itemize} \end{example} \begin{proposition} $foldn$ satisfies the following two rules \begin{enumerate} \item \customlabel{law:natident}{\textbf{Identity}}: $foldn\;zero\;succ = id_{Nat}$ \item \customlabel{law:natfusion}{\textbf{Fusion}}: for all $c : C$, $h, h' : Nat \rightarrow C$ and $k : C \rightarrow C'$ with $kc = c'$ and $kh = h'k$ follows $k \circ foldn\;c\;h = foldn\;c'\;h'$, or diagrammatically: % https://q.uiver.app/#q=WzAsNSxbMiwwLCJDIl0sWzQsMCwiQyJdLFsyLDIsIkMnIl0sWzQsMiwiQyciXSxbMCwwLCIxIl0sWzQsMCwiYyJdLFswLDIsImsiXSxbNCwyLCJjJyIsMl0sWzAsMSwiaCIsMl0sWzIsMywiaCciLDJdLFsxLDMsImsiLDFdXQ== \[ \begin{tikzcd}[ampersand replacement=\&] 1 \&\& C \&\& C \\ \\ \&\& {C'} \&\& {C'} \arrow["c", from=1-1, to=1-3] \arrow["k", from=1-3, to=3-3] \arrow["{c'}"', from=1-1, to=3-3] \arrow["h"', from=1-3, to=1-5] \arrow["{h'}"', from=3-3, to=3-5] \arrow["k"{description}, from=1-5, to=3-5] \end{tikzcd} \] implies % https://q.uiver.app/#q=WzAsMyxbMCwwLCJOYXQiXSxbMiwwLCJDIl0sWzIsMiwiQyciXSxbMSwyLCJrIl0sWzAsMSwiZm9sZG5cXDtjXFw7aCJdLFswLDIsImZvbGRuXFw7YydcXDtoJyIsMl1d \[ \begin{tikzcd}[ampersand replacement=\&] Nat \&\& C \\ \\ \&\& {C'} \arrow["k", from=1-3, to=3-3] \arrow["{foldn\;c\;h}", from=1-1, to=1-3] \arrow["{foldn\;c'\;h'}"', from=1-1, to=3-3] \end{tikzcd} \] \end{enumerate} \end{proposition} \begin{proof} Both follow by induction over an argument $n : Nat$: \begin{enumerate} \item~\ref{law:natident}: \begin{mycase} \case{} $n = zero$ \[foldn\;zero\;succ\;zero = zero = id\;zero\] \case{} $n = succ\;m$ \begin{alignat*}{1} foldn\;zero\;succ\;(succ\;m) & = succ (foldn\;zero\;succ\;m) \\&= succ\;m \tag{IH} \\&= id (succ\;m) \end{alignat*} \end{mycase} \item~\ref{law:natfusion}: \begin{mycase} \case{} $n = zero$ \[k(foldn\;c\;h\;zero) = k\;c = c' = foldn\;c'\;h'\;zero\] \case{} $n = succ\;m$ \begin{alignat*}{1} k(foldn\;c\;h\;(succ\;m)) & = k(h(foldn\;c\;h\;m)) \\&= h'(k(foldn\;c\;h\;m)) \\&= h'(foldn\;c'\;h'\;m) \tag{IH} \\&= foldn\;c'\;h'\;(succ\;m) \end{alignat*} \end{mycase} \end{enumerate} \end{proof} \begin{example} The identity and fusion laws can in turn be used to prove the following induction principle: For any predicate $p : Nat \rightarrow Bool$, \begin{enumerate} \item $p\;zero = true$ and \item $p \circ succ = p$ \end{enumerate} implies $p = true!$. This follows by % chktex 40 \begin{alignat*}{1} & p \\=\;&p \circ (foldn\;zero\;succ) \tag{\ref{law:natident}} \\=\;&foldn\;true\;id \tag{\ref{law:natfusion}} \\=\;&true! \circ (foldn\;zero\;succ) \tag{\ref{law:natfusion}} \\=\;&true!. \tag{\ref{law:natident}} \end{alignat*} Where the first application of~\ref{law:natfusion} is justified, since the diagram % https://q.uiver.app/#q=WzAsNSxbMiwwLCJOYXQiXSxbNCwwLCJOYXQiXSxbMiwyLCJCb29sIl0sWzQsMiwiQm9vbCJdLFswLDAsIjEiXSxbNCwwLCJ6ZXJvIl0sWzAsMSwic3VjYyJdLFsxLDMsInAiXSxbMCwyLCJwIl0sWzIsMywiaWQiLDFdLFs0LDIsInRydWUiLDJdXQ== \[\begin{tikzcd} 1 && Nat && Nat \\ \\ && Bool && Bool \arrow["zero", from=1-1, to=1-3] \arrow["succ", from=1-3, to=1-5] \arrow["p", from=1-5, to=3-5] \arrow["p", from=1-3, to=3-3] \arrow["id"{description}, from=3-3, to=3-5] \arrow["true"', from=1-1, to=3-3] \end{tikzcd}\] commutes by the requisite properties of $p$, and the second application of~\ref{law:natfusion} is justified, since the diagram % https://q.uiver.app/#q=WzAsNSxbMiwwLCJOYXQiXSxbNCwwLCJOYXQiXSxbMiwyLCJCb29sIl0sWzQsMiwiQm9vbCJdLFswLDAsIjEiXSxbNCwwLCJ6ZXJvIl0sWzAsMSwic3VjYyJdLFsxLDMsInRydWUhIl0sWzAsMiwidHJ1ZSEiXSxbMiwzLCJpZCIsMV0sWzQsMiwidHJ1ZSIsMl1d \[\begin{tikzcd} 1 && Nat && Nat \\ \\ && Bool && Bool \arrow["zero", from=1-1, to=1-3] \arrow["succ", from=1-3, to=1-5] \arrow["{true!}", from=1-5, to=3-5] \arrow["{true!}", from=1-3, to=3-3] \arrow["id"{description}, from=3-3, to=3-5] \arrow["true"', from=1-1, to=3-3] \end{tikzcd}\] trivially commutes. \end{example} \subsubsection{Lists}