algprog/tex/sections/01_introduction.tex

\chapter{Introduction}\label{chp: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.

\section{Functions}
A function $f : X \to 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') \to 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 \to A$, $id_A(x) = x$
    \item The constant function $b! : A \to B$ for $b \in B$ defined by $b!(x) = b$
    \item The inclusion function $i_A : A \to B$ for $A \subseteq B$ defined by $i_A(x) = x$
    \item Constants $b : 1 \to B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$.
    \item Composition of function $f : A \to B, g : B \to C$ called $g \circ f : A \to C$ defined by $(g \circ f)(x) = g(f(x))$.
    \item The empty function $¡ : \emptyset \to B$
    \item The singleton function $! : A \to 1$
  \end{enumerate}
\end{example}

\section{Data Types}\label{sec:datatypes}

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.

\subsection{Natural Numbers}
The type of natural numbers comes with a fold function $foldn : C \to (Nat \to C) \to Nat \to 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 \to Bool$ is defined by
          \[iszero = foldn\;true\;false!\]
    \item $plus : Nat \to Nat \to Nat$ is defined by
          \[plus = foldn\;id\;(succ \circ eval) \]
          where $eval : (A \to B) \to A \to B$ is defined by
          \[eval\;f\;a = f\;a\]

  \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
            \to C$ and $k : C \to 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 \to 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}
\subsection{Lists}\label{subsec:lists}
We will now look at the $List$ type and examine it for similar properties. Let us start with the fold function $foldr : C \to (A \to C \to C) \to List\;A \to C$, which is defined by
\begin{alignat*}{2}
   & foldr\;c\;h\;nil           &  & = c                       \\
   & foldr\;c\;h\;(cons\;x\;xs) &  & = h\;a\;(foldr\;c\;h\;xs)
\end{alignat*}

\begin{example}
  Again, let us define some functions using $foldr$.
  \begin{itemize}
    \item $length : List\;A \to Nat$ is defined by
          \[length = foldr\;zero\;(succ !)\]
    \item For $f : A \to B$ we can define $List$-mapping function $List\;f : List\;A \to List\;B$ by
          \[List\;f = foldr\;nil\;(cons \circ f)\]
  \end{itemize}
\end{example}

\begin{proposition}
  $foldr$ satisfies the following two rules
  \begin{enumerate}
    \item \customlabel{law:listident}{\textbf{Identity}}: $foldr\;nil\;cons = id_{List\;A}$
    \item \customlabel{law:listfusion}{\textbf{Fusion}}: for all $c : C$, $h, h' : Nat$
  \end{enumerate}
\end{proposition}

% TODO Use curried version of data types...