freie-monaden.tex

% Kompilieren mit: TEXINPUTS=minted/source: pdflatex -shell-escape %
\documentclass[12pt,compress,ngerman,utf8,t]{beamer}
\usepackage[ngerman]{babel}
\usepackage{ragged2e}
\usepackage{comment}
\usepackage{minted}
\usepackage{wasysym}
\usepackage{booktabs}
\usepackage{tikz}
\usetikzlibrary{calc}
\usepackage[all]{xy}
\usepackage[protrusion=true,expansion=false]{microtype}

\DeclareSymbolFont{extraup}{U}{zavm}{m}{n}
\DeclareMathSymbol{\varheart}{\mathalpha}{extraup}{86}
\DeclareMathSymbol{\vardiamond}{\mathalpha}{extraup}{87}

\DeclareUnicodeCharacter{2237}{$\dblcolon$}
\DeclareUnicodeCharacter{21D2}{$\Rightarrow$}
\DeclareUnicodeCharacter{2192}{$\rightarrow$}

\title[Freie Monaden]{\smiley{} Monaden als Monoidobjekte \smiley}
\author[Augsburger Curry Club]{
  \includegraphics[scale=0.1]{images/a-monad-is-just-1} \\\ \\
  Ingo Blechschmidt \\[0.1em] \scriptsize\texttt{<iblech@speicherleck.de>}}
\date[2017-03-17]{\vspace*{-1.5em}\scriptsize Hannover.FP \\ 17.
März 2017}

\useinnertheme[shadow=true]{rounded}
\useoutertheme{split}
\usecolortheme{orchid}
\usecolortheme{whale}
\setbeamerfont{block title}{size={}}

\useinnertheme{rectangles}

\usecolortheme{seahorse}
\definecolor{mypurple}{RGB}{150,0,255}
\setbeamercolor{structure}{fg=mypurple}
\definecolor{myred}{RGB}{150,0,0}
\setbeamercolor*{title}{bg=myred,fg=white}
\setbeamercolor*{titlelike}{bg=myred,fg=white}

\usefonttheme{serif}
\usepackage[T1]{fontenc}
\usepackage{libertine}

\definecolor{darkred}{RGB}{220,0,0}
\newcommand{\hcancel}[5]{%
    \tikz[baseline=(tocancel.base)]{
        \node[inner sep=0pt,outer sep=0pt] (tocancel) {#1};
        \draw[darkred, line width=1mm] ($(tocancel.south west)+(#2,#3)$) -- ($(tocancel.north east)+(#4,#5)$);
    }%
}%

\renewcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\Id}{\mathrm{Id}}
\newcommand{\Hask}{\mathrm{Hask}}

\setbeamertemplate{navigation symbols}{}
%\setbeamertemplate{headline}{}

\setbeamertemplate{title page}[default][colsep=-1bp,rounded=false,shadow=false]
\setbeamertemplate{frametitle}[default][colsep=-2bp,rounded=false,shadow=false,center]

\newcommand*\oldmacro{}%
\let\oldmacro\insertshorttitle%
\renewcommand*\insertshorttitle{%
  \oldmacro\hfill\insertframenumber\,/\,\inserttotalframenumber\hfill}

\newcommand{\hil}[1]{{\usebeamercolor[fg]{item}{\textbf{#1}}}}
\setbeamertemplate{frametitle}{%
  \vskip0.5em%
  \leavevmode%
  \begin{beamercolorbox}[dp=1ex,center]{}%
      \usebeamercolor[fg]{item}{\textbf{\Large \insertframetitle}}
  \end{beamercolorbox}%
}

\setbeamertemplate{footline}{%
  \leavevmode%
  \hfill%
  \begin{beamercolorbox}[ht=2.25ex,dp=1ex,right]{}%
    \usebeamerfont{date in head/foot}
    \insertframenumber\,/\,\inserttotalframenumber\hspace*{1ex}
  \end{beamercolorbox}%
  \vskip0pt%
}

\newcommand{\backupstart}{
  \newcounter{framenumberpreappendix}
  \setcounter{framenumberpreappendix}{\value{framenumber}}
}
\newcommand{\backupend}{
  \addtocounter{framenumberpreappendix}{-\value{framenumber}}
  \addtocounter{framenumber}{\value{framenumberpreappendix}}
}

\setbeameroption{hide notes}
\setbeamertemplate{note page}[plain]

\begin{document}

\frame{\titlepage}

\frame{\tableofcontents}

\section{Monoide}

\subsection{Definition und Beispiele}

\begin{frame}[fragile]\frametitle{Monoide}
  Ein \hil{Monoid} besteht aus
  \begin{itemize}
    \item einer Menge~$M$,
    \item einer Abbildung~$({\circ}) : M \times M \to M$ und
    \item einem ausgezeichneten Element~$e \in M$,
  \end{itemize}
  sodass die \hil{Monoidaxiome} gelten: Für alle~$x,y,z \in M$
  \begin{itemize}
    \item $x \circ (y \circ z) = (x \circ y) \circ z$,
    \item $e \circ x = x$,
    \item $x \circ e = x$.
  \end{itemize}

  \visible<2>{\begin{center}
    \hil{Beispiele:} \\
    natürliche Zahlen, Listen, Endomorphismen,
    Matrizen, \ldots
    \\[1em]
    \hil{Nichtbeispiele:} \\
    natürliche Zahlen mit Subtraktion,
    nichtleere Listen, \ldots
  \end{center}}

  \vspace*{-22em}
  \begin{columns}
    \begin{column}{0.65\textwidth}
    \end{column}
    \begin{column}{0.4\textwidth}
      \scriptsize\begin{block}{}
      \begin{minted}{haskell}
class Monoid m where
    (<>) :: m -> m -> m
    unit :: m
      \end{minted}
      \end{block}
    \end{column}
  \end{columns}
\end{frame}

\note{
  \begin{itemize}
    \justifying
    \item Die natürlichen Zahlen bilden mit der Addition als Verknüpfung und der
    Null als ausgezeichnetes Element einen Monoid.
    \item Die natürlichen Zahlen bilden mit der Multiplikation als Verknüpfung
    und der Eins als ausgezeichnetes Element einen Monoid.
    \item Die Menge~$X^\star$ der endlichen Listen mit Einträgen aus einer
    Menge~$X$ (in Haskell also sowas wie~\texttt{[X]}, wobei da auch unendliche
    und partiell definierte Listen dabei sind) bildet mit der Konkatenation von
    Listen als Verknüpfung und der leeren Liste als ausgezeichnetes Element
    einen Monoid.
    \item Ist~$X$ irgendeine Menge, so bildet die Menge aller Abbildungen~$X
    \to X$ mit der Abbildungskomposition als Verknüpfung und der
    Identitätsabbildung als ausgezeichnetes Element einen Monoid.
    \item Die natürlichen Zahlen bilden mit der Subtraktionen keinen Monoid, da
    die Differenz zweier natürlicher Zahlen nicht immer wieder eine natürliche
    Zahl ist. Auch mit den ganzen Zahlen klappt es nicht, da die Subtraktion
    nicht assoziativ ist: $1 - (2 - 3) \neq (1 - 2) - 3$.
  \end{itemize}
}

\begin{frame}\frametitle{Axiome in Diagrammform}
  \[ \xymatrixcolsep{4pc}\xymatrixrowsep{4pc}\xymatrix{
    M \times M \times M \ar[r]^{\id \times ({\circ})} \ar[d]_{({\circ}) \times \id} & M \times M
    \ar[d]^{({\circ})} \\
    M \times M \ar[r]_{({\circ})} & M
  } \]
  \medskip
  \[ \xymatrixcolsep{4pc}\xymatrixrowsep{4pc}\xymatrix{
    & M \\
    M \ar[r]\ar[ru] & M \times M \ar[u] & \ar[l]\ar[lu] M
  } \]
\end{frame}

\note{\justifying
  Beide Diagramme sind Diagramme in der Kategorie der Mengen, d.\,h. die
  beteiligten Objekte~$M$, $M \times M$ und~$M \times M \times M$ sind Mengen
  und die vorkommenden Pfeile sind Abbildungen. Wer möchte, kann aber auch
  vorgeben, dass~$M$ ein Typ in Haskell ist (statt~$M \times M$ muss man
  dann~\texttt{(M,M)} denken) und dass die Pfeile Haskell-Funktionen sind.
  \medskip

  Das obere Diagramm ist wie folgt zu lesen.
  \medskip

  Ein beliebiges Element aus~$M \times M \times M$ hat die Form~$(x,y,z)$,
  wobei~$x$, $y$ und~$z$ irgendwelche Elemente aus~$M$ sind. Bilden wir ein
  solches Element nach rechts ab, so erhalten wir~$(x,y \circ z)$. Bilden wir
  dieses weiter nach unten ab, so erhalten wir~$x \circ (y \circ z)$.
  \medskip

  Wir können aber auch den anderen Weg gehen: Bilden wir~$(x,y,z)$ erst nach
  unten ab, so erhalten wir~$(x \circ y,z)$. Bilden wir dieses Element weiter
  nach rechts ab, so erhalten wir~$(x \circ y) \circ z$.
  \medskip

  Fazit: Genau dann \emph{kommutiert das Diagramm} -- das heißt beide Wege
  liefern gleiche Ergebnisse -- wenn die Rechenregel $x \circ (y \circ z) = (x
  \circ y) \circ z$ für alle Elemente~$x,y,z \in M$ erfüllt ist.
  \par
}

\note{\justifying
  Die Pfeile auf dem unteren Diagramm sind nicht beschriftet. Hier die
  Erklärung, was gemeint ist.
  \medskip

  Wir betrachten dazu ein beliebiges Element~$x \in M$ (untere linke Ecke im
  Diagramm). Nach rechts abgebildet erhalten wir~$(e,x)$. Dieses Element weiter
  nach oben abgebildet ergibt~$e \circ x$.
  \medskip

  Der direkte Weg mit dem Nordost verlaufenden Pfeil ergibt~$x$.
  \medskip

  Das linke Teildreieck kommutiert also genau dann, wenn die Rechenregel~$e
  \circ x = x$ für alle~$x \in M$ erfüllt ist. Analog kommutiert das rechte
  Teildreieck genau dann, wenn~$x \circ e = x$ für alle~$x \in M$.
  \par
}

\note{\justifying
  Wieso der Umstand mit der Diagrammform der Axiome? Das hat verschiedene
  schwache Gründe (es ist cool), aber auch einen starken inhaltlichen: Ein
  Diagramm dieser Art kann man nicht nur in der Kategorie interpretieren, in
  der es ursprünglich gedacht war (also der Kategorie der Mengen). Man kann es
  auch in anderen Kategorien interpretieren. Wählt man dazu speziell eine
  Kategorie von Endofunktoren, so erhält man die Definition einer Monade.
  \par
}

\begin{frame}[fragile]\frametitle{Monoidhomomorphismen}
  Eine Abbildung~$\varphi : M \to N$ zwischen Monoiden heißt genau dann
  \hil{Monoidhomomorphismus}, wenn
  \begin{itemize}
    \item $\varphi(e) = e$ und
    \item $\varphi(x \circ y) = \varphi(x) \circ \varphi(y)$ für alle~$x,y \in M$.
  \end{itemize}

  \begin{center}
    \hil{Beispiele:} \\
    \mintinline{haskell}{length :: [a] -> Int} \\
    \mintinline{haskell}{sum :: [Int] -> Int} \\[1em]
    \hil{Nichtbeispiele:} \\
    \mintinline{haskell}{reverse :: [a] -> [a]} \\
    \mintinline{haskell}{head :: [a] -> a} \\
  \end{center}
\end{frame}

\note{\scriptsize
  \begin{itemize}
    \justifying
    \item Es gelten die Rechenregeln
    \begin{align*}
      \texttt{length []} &= \texttt{0}, \\
      \texttt{length (xs ++ ys)} &= \texttt{length xs + length ys}
    \end{align*}
    für alle Listen~\texttt{xs} und~\texttt{ys}.
    Das ist der Grund, wieso die Längenfunktion ein Monoidhomomorphismus ist.

    Achtung: Bevor man eine solche Aussage trifft, muss man eigentlich genauer
    spezifizieren, welche Monoidstrukturen man in Quelle und Ziel meint. Auf
    dem Typ~\texttt{[a]} soll die Monoidverknüpfung durch Konkatenation gegeben
    sein, auf dem Typ~\texttt{Int} durch Addition.

    \item Es gilt die Rechenregel
    \begin{equation*}
      \texttt{sum (xs ++ ys) = sum xs + sum ys}
    \end{equation*}
    für alle Listen~\texttt{xs} und~\texttt{ys} von Ints.
    Das ist die halbe Miete zur Begründung, wieso~\texttt{sum} ein
    Monoidhomomorphismus ist.

    \item Die Rechenregel
    \begin{equation*}
      \texttt{reverse (xs ++ ys) = reverse xs ++ reverse ys}.
    \end{equation*}
    gilt \emph{nicht} für alle Listen~\texttt{xs} und~\texttt{ys}. Daher
    ist~\texttt{reverse} kein Monoidhomomorphismus.
  \end{itemize}
}

\subsection{Nutzen}

\begin{frame}\frametitle{Wozu?}
  \begin{itemize}
    \item Allgegenwärtigkeit
    \item Gemeinsamkeiten und Unterschiede
    \item Generische Beweise
    \item Generische Algorithmen
  \end{itemize}
\end{frame}

\note{
  \begin{itemize}
    \item Monoide gibt es überall.
    \item Das Monoidkonzept hilft, Gemeinsamkeiten und Unterschiede
    zu erkennen und wertschätzen zu können.
    \item Man kann generische Beweise für beliebige Monoide führen.
    \item Man kann generische Algorithmen mit beliebigen Monoiden basteln.
  \end{itemize}
}


\subsection{Freie Monoide}

\begin{frame}\frametitle{Freie Monoide}
  Gegeben eine Menge~$X$ ohne weitere Struktur.
  Wie können wir auf möglichst unspektakuläre Art und Weise daraus einen
  Monoid~$F(X)$ gewinnen?
  \medskip
  \pause

  Spoiler: Der gesuchte \hil{freie Monoid}~$F(X)$ auf~$X$ ist der Monoid der
  endlichen \hil{Listen} mit Elementen aus~$X$.
  \medskip
  \pause
  % auf der Konsole: Erzeuger passen und Relationen passen.

  Essenz der Freiheit: Jede beliebige Abbildung~$X \to M$ in einen Monoid~$M$
  stiftet genau einen Homomorphismus $F(X) \to M$.
  \[ \xymatrix{
    X \ar[rr]^{\texttt{phi}} \ar[rd]_{\texttt{inj}} && M \\
    & F(X) \ar@{-->}[ru]_{\texttt{cata phi}}
  } \]
\end{frame}

\note{\justifying
  In~$F(X)$ sollen neben den Elementen aus~$X$ gerade nur so viele
  weitere Elemente enthalten sein, sodass man eine Verknüpfung~$({\circ})$ und
  ein Einselement definieren kann.
  Es soll sich also jedes Element aus~$F(X)$ über die Monoidoperationen aus
  denen von~$X$ bilden lassen.
  \medskip

  In~$F(X)$ sollen nur die Rechenregeln gelten, die von den Monoidaxiomen
  gefordert werden.
  \medskip

  Die nach "`Essenz der Freiheit"' angegebene Forderung heißt auch
  \emph{universelle Eigenschaft}. Präzise formuliert lautet sie wie folgt:
  Ein Paar~$(F,\texttt{inj})$ bestehend aus einem Monoid~$F$ und einer
  Abbildung~$\texttt{inj} : X \to F$ heißt genau dann \emph{freier Monoid
  auf~$X$}, wenn für jedes Paar~$(M,\texttt{phi})$ bestehend aus einem
  Monoid~$M$ und einer Abbildung~$\texttt{phi} : X \to M$ genau ein
  Monoidhomomorphismus~$\texttt{cata phi} : F \to M$ existiert,
  sodass~$\texttt{phi} = \texttt{cata phi} \mathop{.} \texttt{inj}$.
  \medskip

  Man kann zeigen -- über ein kategorielles Standardargument -- dass je zwei
  Paare~$(F,\texttt{inj})$, welche diese universelle Eigenschaft erfüllen,
  vermöge eines eindeutigen Isomorphismus zueinander isomorph sind. Das
  rechtfertigt, von \emph{dem} freien Monoid über~$X$ zu sprechen.
  \par
}

\note{\justifying
  Man kann die universelle Eigenschaft schön in Haskell demonstrieren:
  \inputminted{haskell}{images/universal-property-free-monoid.hs}

  Ist~\texttt{phi} irgendeine Abbildung~\texttt{a -> m}, so ist~\texttt{cata
  phi} eine Abbildung~\texttt{[a] -> m}. Diese ist nicht nur irgendeine
  Abbildung, sondern wie gefordert ein Monoidhomomorphismus.
  \medskip

  Und mehr noch:
  Das Diagramm kommutiert tatsächlich, das heißt~\texttt{cata phi}
  und~\texttt{phi} haben in folgendem präzisen Sinn etwas miteinander zu
  tun: \texttt{cata phi . inj = phi}. Dabei ist~\texttt{inj :: a -> [a]} die
  Abbildung mit~\texttt{inj x = [x]}.
  \par
}

\note{\justifying
  Unsere Definition von "`unspektakulär"' soll sein: Alle Elemente in~$F(X)$
  setzen sich mit den Monoidoperationen aus denen aus~$X$ zusammen, und
  in~$F(X)$ gelten nur die Rechenregeln, die von den Monoidaxiomen erzwungen
  werden, aber keine weiteren.
  \medskip

  Das ist bei der Konstruktion von~$F(X)$ als Monoid der endlichen Listen
  über~$X$ auch in der Tat der Fall: Jede endliche Liste mit Einträgen aus~$X$
  ergibt sich als wiederholte Verknüpfung (Konkatenation) von Listen der
  Form~\texttt{inj x} mit~\texttt{x} aus~$X$. Und willkürliche Rechenregeln
  wie~\texttt{[a,b] ++ [b,a] == [c]} gelten, wie es auch sein soll,
  \emph{nicht}.
  \medskip

  Wieso fängt die universelle Eigenschaft genau diese Definition von
  Unspektakularität ein? Wenn man zu~$F(X)$ noch weitere Elemente hinzufügen
  würde (zum Beispiel unendliche Listen), so wird es mehrere oder keinen
  Kandidaten für~\texttt{cata phi} geben, aber nicht mehr nur einen. Genauso
  wenn man in~$F(X)$ durch Identifikation gewisser Elemente weitere
  Rechenregeln erzwingen würde.
  \par
}

\note{\justifying
  Wenn man tiefer in das Thema einsteigt, erkennt man, dass endliche Listen
  noch nicht der Weisheit letzter Schluss sind:
  \url{http://comonad.com/reader/2015/free-monoids-in-haskell/}
  \medskip

  Kurz zusammengefasst: Es stimmt schon, dass der Monoid der endlichen Listen
  über~$X$ der freie Monoid auf~$X$ ist, sofern man als Basiskategorie in der
  Kategorie der Mengen arbeitet. Wenn man dagegen in~$\Hask$ arbeitet, der
  Kategorie der Haskell-Typen und -Funktionen, so benötigt man eine leicht
  andere Konstruktion.
  \medskip

  Fun Fact: Die in dem Blog-Artikel angegebene Konstruktion ergibt sich
  \emph{unmittelbar} aus der universellen Eigenschaft. Es ist keine Überlegung
  und manuelle Suche nach einem geeigneten Kandidaten für~$F(X)$ nötig.
  (Bemerkung für Kategorientheorie-Fans: Das es so einfach geht, liegt an einer
  gewissen Vollständigkeitseigenschaft von~$\Hask$.)
  \par
}

\begin{frame}\frametitle{Freie Monoide}
  \begin{center}\Large
    Freie Monoide sind \ldots

    \only<1>{\ldots{} frei wie in Freibier?}%
    \only<2->{\hcancel{\ldots{} frei wie in Freibier?}{0pt}{3pt}{0pt}{-2pt}}

    \only<3>{\ldots{} frei wie in Redefreiheit?}%
    \only<4->{\hcancel{\ldots{} frei wie in Redefreiheit?}{0pt}{3pt}{0pt}{-2pt}}

    \only<5->{\ldots{} frei wie in \hil{linksadjungiert}! $\checkmark$}

  \end{center}

  \only<6>{Der Funktor~$F : \mathrm{Set} \to \mathrm{Mon}$ ist \hil{linksadjungiert}
  zum Vergissfunktor~$\mathrm{Mon} \to \mathrm{Set}$.}
\end{frame}

\note{\justifying
  Für jede algebraische Struktur \emph{Mumble} gibt es das Konzept des
  \emph{freien Mumbles über einer Menge}. Beispiele:
  \begin{itemize}\justifying
  \item Der freie Monoid über~$X$ ist der Monoid der endlichen Listen mit
  Einträgen aus~$X$.
  \item Der freie abelsche Monoid über~$X$ ist der abelsche Monoid der
  endlichen Multimengen von Elementen aus~$X$.
  \item Die freie Halbgruppe über~$X$ ist die Halbgruppe der nichtleeren Listen
  mit Einträgen aus~$X$.
  \item Das freie Magma über~$X$ ist das Magma der binären Bäume mit Elementen
  aus~$X$ an den Blättern.
  \item Der freie Ring über~$X$ ist der Ring der Polynome mit ganzzahligen
  Koeffizienten und den Elementen aus~$X$ als Polynomvariablen.
  \end{itemize}

  \scriptsize
  Zur Erinnerung: Eine Halbgruppe ist wie ein Monoid, nur, dass es nicht
  unbedingt ein neutrales Element geben muss. Ein Magna ist wie eine
  Halbgruppe, nur, dass die Verknüpfung nicht assoziativ sein muss. Ein Ring
  ist wie ein Körper, nur dass man keinerlei multiplikative Inverse fordert.
  \par
}

\section{Funktoren}

\subsection{Definition und Beispiele}

\begin{frame}[fragile]\frametitle{Funktoren}
  Ein \hil{Funktor}~$F : \C \to \D$ zwischen Kategorien~$\C$ und~$\D$ ordnet
  \begin{itemize}
    \item jedem Objekt~$X \in \C$ ein Objekt~$F(X) \in \D$ und
    \item jedem Morphismus~$f : X \to Y$ in~$\C$ ein Morphismus~$F(f) : F(X)
    \to F(Y)$ in~$\D$ zu,
  \end{itemize}
  sodass die \hil{Funktoraxiome} erfüllt sind:
  \begin{itemize}
    \item $F(\id_X) = \id_{F(X)}$,
    \item $F(g \circ f) = F(g) \circ F(f)$.
  \end{itemize}
  \vfill

  In Haskell kommen Funktoren~$\Hask \to \Hask$ vor:
  \begin{minted}{haskell}
class Functor f where
    fmap :: (a -> b) -> (f a -> f b)
-- fmap id      = id
-- fmap (g . f) = fmap g . fmap f
  \end{minted}
\end{frame}

\note{\justifying
  Fun Fact am Rande: Ein Theorem für lau garantiert, dass in Haskell das zweite
  Funktoraxiom aus dem ersten folgt.
  \par
}

\begin{frame}[fragile]\frametitle{Beispiele für Funktoren}
  \vspace*{-1em}
  \small
  \begin{minted}{haskell}
class Functor f where
    fmap :: (a -> b) -> (f a -> f b)

instance Functor [] where fmap f = map f

data Maybe a = Nothing | Just a
instance Functor Maybe where
    fmap f Nothing  = Nothing
    fmap f (Just x) = Just (f x)

data Id a = MkId a
instance Functor Id where
    fmap f (MkId x) = MkId (f x)

data Pair a = MkPair a a
instance Functor Pair where
    fmap f (MkPair x y) = MkPair (f x) (f y)
  \end{minted}
\end{frame}


\subsection{Funktoren als Container}

\begin{frame}[fragile]\frametitle{Funktoren als Container}
  Ist~\texttt{f} ein Funktor, so stellen wir uns den
  Typ~\texttt{f a} als einen Typ von Containern von Werten vom
  Typ~\texttt{a} vor.
  \medskip

  Je nach Funktor haben die Container eine andere Form.

  \vfill
  \begin{minted}{haskell}
class Functor f where
    fmap :: (a -> b) -> (f a -> f b)

data List  a = Nil     | Cons a [a]
data Maybe a = Nothing | Just a
data Id    a = MkId   a
data Pair  a = MkPair a a
data Unit  a = MkUnit
data Void  a
  \end{minted}
\end{frame}

\note{\justifying
  Die Vorstellung ist aus folgendem Grund plausibel: Aus einer
  Funktion~\texttt{a -> b} können wir mit \texttt{fmap} eine Funktion~\texttt{f
  a -> f b} machen. Also stecken wohl in einem Wert vom Typ~\texttt{f a}
  irgendwelche Werte vom Typ~\texttt{a}, die mit der gelifteten Funktion dann
  in Werte vom Typ~\texttt{b} umgewandelt werden.
  \par
}


\section{Monaden}

\subsection{Definition und Beispiele}

\note{\justifying
  Im Folgenden ist~$\Hask$ eine geeignete Kategorie von Haskell-Typen und
  -Funktionen. Die Objekte sollen also Haskell-Typen sein, und Morphismen
  zwischen je zwei Typen sollen durch Haskell-Funktionen des entsprechenden
  Typs gegeben sein.
  \medskip

  Die Kategorie~$\mathrm{End}(\Hask)$ ist die Kategorie der
  \emph{Endofunktoren} von~$\Hask$. Deren Objekte sind Funktoren~$\Hask \to
  \Hask$ (also das, was man in Haskell gewöhnlich als "`Funktor"' bezeichnet)
  und deren Morphismen sind natürliche Transformationen (siehe übernächste
  Folie).
  \par
}

\begin{frame}\frametitle{Monoidale Kategorien}
  \small
  \begin{tabular}{@{}ll@{}}
    \toprule
    $\mathrm{Set}$ & $\mathrm{End}(\Hask)$ \\\midrule
    Menge $M$ & Funktor $M$ \\
    Abbildung $M \to N$ & natürliche Transformation $\forall a. M a \to N a$ \\
    $M \times N$ & $M \circ N$ mit $(M \circ N) a = M (N a)$ \\
    nur linke Komponente ändern & nur äußere Schicht ändern \\
    nur rechte Komponente ändern & nur innere Schicht ändern \\
    \pause
    \hil{Monoid} & \hil{Monade} \\
    \bottomrule
  \end{tabular}

  \begin{center}
    \includegraphics[height=3.3cm]{images/a-monad-is-just-4}
    \qquad
    \includegraphics[height=3.3cm]{images/a-monad-is-just-5}
  \end{center}
\end{frame}

\note{\justifying
  In der Kategorientheorie ist eine natürliche Transformation~$\eta : F
  \Rightarrow G$ zwischen zwei Funktoren~$F, G : \C \to \D$ eine Familie von
  Morphismen~$\eta_X : F(X) \to G(X)$ (ein Morphismus für jedes Objekt~$X \in
  \C$), sodass für jeden Morphismus~$f : X \to Y$ in~$\C$ das Diagramm
  \[ \xymatrix{
    F(X) \ar[r]^{\eta_X} \ar[d]_{F(f)} & G(X) \ar[d]^{G(f)} \\
    F(Y) \ar[r]_{\eta_Y} & G(Y)
  } \]
  kommutiert.\par
}

\note{\justifying
  Spezialisiert auf den Spezialfall~$\C = \D = \Hask$ [und ein externes Hom in
  ein internes verwandelt, was auch immer das heißt] ist eine natürliche
  Transformation~$\texttt{eta} : F \Rightarrow G$ eine polymorphe
  Haskell-Funktion
  \begin{center}\inputminted{haskell}{images/natural-transformation.hs}\end{center}
  mit
  \begin{center}\inputminted{haskell}{images/natural-transformation-law.hs}\end{center}
  für alle Funktionen~\texttt{f :: a -> b}.
  \medskip

  Ein Theorem für lau garantiert aber, dass jede Funktion~\texttt{eta} des
  richtigen Typs automatisch diese Kompatibilitätsbedingung mit dem
  \texttt{fmap} von~\texttt{F} bzw. dem von~\texttt{G} erfüllt, weswegen man
  diese Bedingung nicht explizit fordern muss. (Vereinfacht gesprochen liegt
  der Grund dafür darin, dass eine Haskell-Funktion nicht in Abhängigkeit der
  konkreten Instanz der Typvariablen~\texttt{a} ihr Verhalten ändern kann.)
  \par
}

\note{\justifying
  Beispiele für natürliche Transformationen gibt es in Haskell viele:
  \begin{itemize}\justifying
  \item \texttt{maybeToList :: Maybe a -> [a]}

  \item \texttt{eitherToMaybe :: Either E a -> Maybe a}
  
  Dabei ist \texttt{E} ein bestimmter fester Typ.

  \item \texttt{listToMaybe :: [a] -> Maybe a}
  
  Dieses Beispiel zeigt, dass natürliche Transformationen durchaus
  Informationen vernichten dürfen.

  \item \texttt{sequence :: [M a] -> M [a]}
  
  Dabei ist \texttt{M} eine bestimmte feste Monade.

  \item \texttt{tail :: [a] -> [a]}

  \item \texttt{length :: [a] -> Int}
  
  Dabei steht auf der rechten Seite die Anwendung von \texttt{a} auf den
  \emph{konstanten Funktor bei \texttt{Int}}.
  \end{itemize}
}

\note{\justifying
  Die Kategorien~$\mathrm{Set}$ und~$\mathrm{End}(\Hask)$ können beide mit
  einer \emph{monoidalen Struktur} versehen werden. In der Kategorie der Mengen
  ist das die Operation~$(M,N) \mapsto M \times N$. In der Kategorie der
  Endofunktoren von~$\Hask$ ist es~$(M,N) \mapsto M \circ N$.
  \medskip

  In jeder monoidalen Kategorie (also einer Kategorie zusammen mit einer
  monoidalen Struktur) kann man von \emph{Monoid-Objekten} sprechen.
  Monoid-Objekte in~$\mathrm{Set}$ sind einfach ganz gewöhnliche Monoide.
  Monoid-Objekte in~$\mathrm{End}(\Hask)$ sind Monaden.
  \medskip

  Siehe auch: \\
  \url{http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html}.
  \par
}

\begin{frame}[fragile]\frametitle{Monaden}
  Eine \hil{Monade} besteht aus
  \begin{itemize}
    \item einem Funktor~$M$,
    \item einer natürlichen Transformation~$M \circ M \Rightarrow M$ und
    \item einer natürlichen Transformation~$\Id \Rightarrow M$,
  \end{itemize}
  sodass die \hil{Monadenaxiome} gelten.
  \pause

  \begin{minted}{haskell}
class (Functor m) => Monad m where
    join   :: m (m a) -> m a
    return :: a -> m a
  \end{minted}

  \begin{columns}
    \begin{column}{0.38\textwidth}
      \begin{block}{Listen}
        \scriptsize
        \begin{minted}{haskell}
concat    :: [[a]] -> [a]
singleton :: a     -> [a]
        \end{minted}
      \end{block}
    \end{column}
    \begin{column}{0.50\textwidth}
      \begin{block}{Maybe}
        \scriptsize
        \begin{minted}{haskell}
join :: Maybe (Maybe a) -> Maybe a
Just :: a -> Maybe a
        \end{minted}
      \end{block}
    \end{column}
  \end{columns}
\end{frame}

\note{\justifying
  Anschauliche Interpretation: Monaden sind spezielle Containertypen, die zwei
  Zusatzfähigkeiten haben: Ein Container von Containern von Werten soll man zu
  einem einfachen Container von Werten "`flatten"' können (\texttt{join}), und
  einen einzelnen Wert soll man in einen Container packen können
  (\texttt{return}).
  \par
}

\begin{frame}[fragile]\frametitle{Weitere Beispiele}
  \vspace*{-1em}
  \begin{minted}{haskell}
class (Functor m) => Monad m where
    join   :: m (m a) -> m a
    return :: a -> m a
  \end{minted}

  \begin{block}{Reader}
    \scriptsize
    \begin{minted}{haskell}
type Reader env a = env -> a

instance Functor (Reader env) where
    fmap f k = f . k

instance Monad (Reader env) where
    return x = \_   -> x
    join   k = \env -> k env env
    \end{minted}
  \end{block}

  \begin{block}{State}
    \scriptsize
    \begin{minted}{haskell}
type State s a = s -> (a,s)

instance Monad (State s) where
    return x = \s -> (x,s)
    join   k = \s -> let (k',s') = k s in k' s'
    \end{minted}
  \end{block}
\end{frame}

\note{\justifying
  Auch \texttt{State s} und \texttt{Reader env} passen in die "`Container mit
  Zusatzfähigkeit"'-Intuition, wenn man sich hinreichend verbiegt. Schaffst du
  das?
  \par
}


\subsection[Slogan]{"`Monoid in einer Kategorie von Endofunktoren"'}

\begin{frame}\frametitle{Die Monadenaxiome}
  {\scriptsize
  Sprechweise: Ein Wert vom Typ~\texttt{m (m (m a))} ist ein (äußerer) Container von
  (inneren) Containern von (ganz inneren) Containern von Werten vom
  Typ~\texttt{a}.\par}

  \[ \xymatrixcolsep{4pc}\xymatrixrowsep{4pc}\xymatrix{
    M \circ M \circ M \ar@{=>}[r]^{\text{innen join}} \ar@{=>}[d]_{\text{außen join}} & M \circ M
    \ar@{=>}[d]^{\text{join}} \\
    M \circ M \ar@{=>}[r]_{\text{join}} & M
  } \]
  \medskip
  \[ \xymatrixcolsep{4pc}\xymatrixrowsep{4pc}\xymatrix{
    & M \\
    M \ar@{=>}[r]_{\text{return}}\ar@{=>}[ru] & M \circ M \ar@{=>}[u]_{\text{join}} & \ar@{=>}[l]^{\text{innen
    return}}\ar@{=>}[lu] M
  } \]
\end{frame}

% Mündlich: Das Motto rezipieren.


\section{Freie Monaden}

\subsection{Definition}

\begin{frame}[fragile]\frametitle{Freie Monaden}
  Gegeben ein Funktor~\texttt{f} ohne weitere Struktur. Wie können wir auf
  möglichst ökonomische Art und Weise daraus eine
  Monade~\mintinline{haskell}{Free f} konstruieren?
  \[ \xymatrix{
    F \ar@{=>}[rr] \ar@{=>}[rd] && M \\
    & \operatorname{Free} F \ar@{==>}[ru]
  } \]
  \begin{minted}{haskell}
can :: (Functor f, Monad m)
    => (forall a. f a      -> m a)
    -> (forall a. Free f a -> m a)
  \end{minted}
\end{frame}


\subsection{Konstruktion}

\note{
  \scriptsize
  \inputminted{haskell}{images/definition-free-monad.hs}
}

\note{\justifying
  \texttt{Free f a} ist der Typ der "`\texttt{f}-förmigen"' Bäume mit Blättern
  vom Typ~\texttt{a}. Dabei flattened \texttt{join} einen~\texttt{f}-förmigen
  Baum von~\texttt{f}-förmigen Bäumen von irgendwelchen Werten zu einem
  einfachen~\texttt{f}-förmigen Baum dieser Werte.

  \begin{itemize}\justifying
    \item \texttt{Free Void} ist die \texttt{Id}-Monade.
    \item \texttt{Free Unit} ist die \texttt{Maybe}-Monade. Hier hat jeder
    Mutterknoten kein einziges Kind. Die Bezeichnung "`Mutterknoten"' ist also
    etwas euphemistisch.
    \item \texttt{Free Pair} ist die \texttt{Tree}-Monade. Hier hat jeder
    Mutterknoten genau zwei Kinder.
    \item \texttt{Free Id}   ist die \texttt{(Writer Nat)}-Monade. Hier hat
    jeder Mutterknoten genau ein Kind.
  \end{itemize}

  Die Listen-Monade ist übrigens nicht frei. Übungsaufgabe: Beweise das!
  \par
}


\subsection{Nutzen}

\begin{frame}\frametitle{Anwendungen freier Monaden}
  \begin{itemize}\justifying
    \item Viele wichtige Monaden sind frei.
    \item Freie Monaden kapseln das "`Interpreter-Muster"'.
    \item Freie Monaden können zur Konstruktion weiterer Monaden genutzt
    werden, etwa zum Koprodukt zweier Monaden, welches die Fähigkeiten zweier
    gegebener Monaden vereint.
  \end{itemize}
\end{frame}

\note{\justifying
  Die in diesen Folien gegebene Konstruktion der freien Monade hat ein
  Effizienzproblem -- genau wie bei der linksgeklammerten Verkettung von
  Listen. Mit der sog. Kodichtemonade, einer speziellen Links-Kan-Erweiterung,
  kann man das Problem lösen.
  \medskip

  Mehr zum Interpreter-Muster gibt es in einem Folgevortrag zu Effektsystemen.
  Kurz zusammengefasst: Wenn man maßgeschneidert eine Monade konstruieren
  möchte, welche genau einen gewissen Satz von Nebenwirkungen unterstützt, dann
  kann man das über freie Monaden. Und noch einfacher über "`freiere
  Monaden"' (da ist der Ausgangspunkt nur ein Typkonstruktor~\texttt{F}, der
  \emph{kein} Funktor sein muss).
  \medskip

  Ein Vorgeschmack in Form von Haskell-Code gibt es unter
  \url{https://github.com/iblech/vortrag-haskell/blob/master/freie-monaden.hs}.
  \par
}

\backupstart
\begin{frame}[plain]
  \begin{center}
  \includegraphics[scale=0.55]{images/a-monad-is-just-2}
  \end{center}

  \small\justifying
  Nach der Schule trifft Barbie Paul und Peter in der Bibliothek. "`Funktionale
  Programmierung ist fantastisch!"', freut sich Barbie. "`Ich weiß nicht", sagt
  Paul, "`was zum Teufel ist eine Monade noch mal?"'. "`Eine Monade ist einfach
  ein Monoid in einer Kategorie von Endofunktoren -- wo liegt das Problem?"',
  antwortet Barbie.
  \par
\end{frame}
\backupend

\end{document}

Monoide
* Definition und Beispiele
* Nutzen: Gemeinsamkeiten, generische Algorithmen, ...
* Freie Monoide: Ökonomieprinzip, universelle Eigenschaft

Funktoren als Container

Monaden
* Monaden als Container, die eine Art "join" unterstützen
* Monadenaxiome (mit Gegenüberstellung Set vs. End(Hask))

Freie Monaden
* Herleitung/Definition
* Universelle Eigenschaft
* Beispiel: Interpreter-Muster; State, Writer, Reader; State als Summe von Writer und Reader
* Ausblick: Performanceprobleme