slides.tex

\documentclass[serif,mathserif,professionalfont,10pt]{beamer}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{etex}
\usepackage{graphicx}
\usepackage{textgreek}

\usepackage{amssymb}

\usepackage{color}
\definecolor{grey}{gray}{0.6}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegreen}{rgb}{0,1,0}
\definecolor{slideblue}{rgb}{0,0,1}
\definecolor{slidepurple}{rgb}{0,1,1}
\definecolor{slidegray}{rgb}{0.5,0.5,0.5}
\definecolor{slideivory}{rgb}{1,1,0.9}
\definecolor{slideblueb}{rgb}{0,0.5,0.8}
\newcommand{\highlight}[1]{\textcolor{slidered}{#1}}
\newcommand{\sred}[1]{\textcolor{slidered}{#1}}
\newcommand{\sblue}[1]{\textcolor{slideblue}{#1}}
\newcommand{\sblueb}[1]{\textcolor{slideblueb}{#1}}
\newcommand{\sgreen}[1]{\textcolor{slidegreen}{#1}}
\newcommand{\sgray}[1]{\textcolor{slidegray}{#1}}
\newcommand{\spurple}[1]{\textcolor{purple}{#1}}

\beamertemplatenavigationsymbolsempty
\usetheme{Boadilla}
\usecolortheme{beaver}

\makeatletter
\def\mkcommand#1{\expandafter\gdef\csname #1\endcsname}
\makeatother

\def\module#1{\message{#1}\section{#1}\sectlabel{#1}}

\newenvironment{ModuleHead}{\par\begingroup\tiny}{\endgroup\par\medskip}

% \DeclareUnicodeCharacter{7472}{\ensuremath{^\mathsf{D}}} % MODIFIER LETTER CAPITAL D
% \DeclareUnicodeCharacter{9723}{\ensuremath{\square}} % WHITE MEDIUM SQUARE
% \DeclareUnicodeCharacter{119920}{\ensuremath{\mathbf{I}}} % MATHEMATICAL BOLD ITALIC CAPITAL I
% \DeclareUnicodeCharacter{119991}{\ensuremath{_\mathsf{B}}} % MATHEMATICAL SCRIPT SMALL B
% \DeclareUnicodeCharacter{120008}{\ensuremath{_\mathsf{S}}} % MATHEMATICAL SCRIPT SMALL S
% \DeclareUnicodeCharacter{120001}{\ensuremath{_\mathsf{L}}} % MATHEMATICAL SCRIPT SMALL L
% \DeclareUnicodeCharacter{119997}{\ensuremath{_\mathsf{H}}} % MATHEMATICAL SCRIPT SMALL H
% \DeclareUnicodeCharacter{8348}{\ensuremath{_\mathsf{t}}} % MATHEMATICAL SCRIPT SMALL T
% \DeclareUnicodeCharacter{8339}{\ensuremath{_\mathsf{x}}} % MATHEMATICAL SCRIPT SMALL X
% \DeclareUnicodeCharacter{119925}{\ensuremath{\mathcal{N}}} % MATHEMATICAL BOLD ITALIC CAPITAL N
% \DeclareUnicodeCharacter{119924}{\ensuremath{\mathcal{M}}} % MATHEMATICAL BOLD ITALIC CAPITAL M
% \DeclareUnicodeCharacter{7484}{\ensuremath{\mathsf{O}}} % MODIFIER LETTER CAPITAL O
% \DeclareUnicodeCharacter{9678}{\ensuremath{\mathsf{BULLSEYE}}} % BULLSEYE
% \DeclareUnicodeCharacter{8667}{\ensuremath{\Rrightarrow}} % rightwards triple arrow
% \DeclareUnicodeCharacter{8255}{\ensuremath{\smile}} % undertie, subscript-converse
% \DeclareUnicodeCharacter{8265}{\ensuremath{! \! ? }} % exclamation question mark
% \DeclareUnicodeCharacter{9632}{\ensuremath{ \square }} % black square
% \DeclareUnicodeCharacter{9679}{\ensuremath{ \boldsymbol{\cdot} }} % black circle
% \DeclareUnicodeCharacter{9675}{\ensuremath{ \boldsymbol{\circ} }} % white circle

\title{A tale of theories and data-structures}
\author[Carette, Al-hassy, Kahl]{Jacques Carette, Musa Al-hassy, Wolfram Kahl}
\institute[McMaster]{McMaster University, Hamilton}

\newtheorem{claim}{Claim}

\begin{document}

\frame{\titlepage}

\begin{frame}
\frametitle{Lists and Monoids}
\begin{claim}
A \sred{List} is a \sred{Free Monoid}
\end{claim}
What does that really mean? \\

\pause
\vspace*{4mm}
\sred{Fancy explanation}: The functor from the category \textsf{Types} of \sgreen{types and function}, with
\texttt{List} as its object mapping and \texttt{map} for homomorphism,
to the category \textsf{Monoid} of \sgreen{monoids and monoid homomorphisms}, is \sblue{left
adjoint} to the forgetful functor (from \textsf{Monoid} to \textsf{Types}).
%
% What is the difference between ``the category (types, functions)'' and ``Set''?
%

\pause
\vspace*{4mm}
\texttt{List} (equipped with constructors \texttt{[]}, \texttt{::} and
functions \texttt{map}, \texttt{++},
\texttt{singleton}, and \texttt{foldr}) is the
\sblue{language of monoids}. In other words, \texttt{List} 
is the canonical term syntax for 
\sblue{computing with monoids}.

\pause
\vspace*{4mm}
Why on earth would we care about that? Let's see!

% Go to Agda code.  Show definitions of
% Monoid. Monoid Homomorphism. Forgetful functor.
% Then definition of Free and the Adjunction.
\vfill
\end{frame}

\begin{frame}
\frametitle{Non-categorical version}
The requirements roughly translate to\\
Monoid:
\begin{itemize}
\item Need a \emph{container} $C$ of $\alpha$
\item with a distinguished container $ε$ devoid of $\alpha$'s
\item a binary operation $*$ that puts two containers together
\item such that $ε$ is a left/right unit for $*$.
\end{itemize}
Functor:
\begin{itemize}
\item A way to apply a $(\alpha → \beta)$ function to a $C\, \alpha$ to get a $C \, \beta$
\item which ``plays well'' with $\mathsf{id}, ∘, ≡$ and $*$.
\end{itemize}
Adjunction:
\begin{itemize}
\item An operation \texttt{singleton} embedding an $\alpha$ as a container $C \, \alpha$
\item an operation \texttt{foldr} (over arbitrary Monoid)
\item such that both operations ``play well'' with each other.
\end{itemize}
Extremely handy:
\begin{itemize}
\item Induction principle
\end{itemize}
\end{frame}
% Notice how I never said ``Monad'' ?
%
% Monads ≅ closure operators
%

\begin{frame}
\frametitle{The plot thickens}
Given an arbitrary type $A$ : \\ \vspace*{4mm}
\begin{tabular}{lll}
\textbf{Theory} & \textbf{Free Structure} & CoFree \\ \hline
Carrier & Identity $A$ & Identity $A$ \\
Pointed & Maybe $A$ & --\\ \hline
Unary & Eventually $A$, $ℕ × A$ &  ? \\
Involutive & $A ⊎ A$ & A × A \\ \hline
Magma & Tree $A$ &  ? \\
Semigroup & NEList $A$ & ? \\ \hline
Monoid & List\, $A$ & ? \\
Left Unital Semigroup & List $A × ℕ$ & ? \\
Right Unital Semigroup & $ℕ ×$ List $A$ & ? \\ \hline
\end{tabular}\\ \vspace*{4mm}
\pause
What is the \sblue{Free Structure}? It is ``the''
\sred{\textbf{term language in normal form}} associated to the theory.\\
\end{frame}

\begin{frame}
\frametitle{Benefits}
Benefits of the formal approach:
\begin{itemize}
\item Obvious: Dispell silly conjectures/errors
\item Discover some neat relationships between algebraic theories and data-structures
\item \texttt{fold} (aka the counit)
\item Induction
\end{itemize} \vspace*{4mm}
\pause
Examples: counit for Unary, Involutive
\vfill
\end{frame}

\begin{frame}
\frametitle{Extending the tale}
Given an arbitrary type A : \\ \vspace*{4mm}
\begin{tabular}{ll}
\textbf{Theory} & \textbf{Free Structure} \\ \hline
Carrier & Identity $A$ \\
Pointed & Maybe $A$ \\ \hline
Unary & $ℕ × A$  \\
Involutive & $A ⊎ A$ \\ \hline
Magma & Tree $A$  \\
Semigroup & NEList $A$  \\ \hline
Monoid & List $A$ \\
Left Unital Semigroup & List $A × ℕ$ \\
Right Unital Semigroup & $ℕ ×$ List $A$ \\ \hline
\sred{Commutative Monoid} & \sred{?} \\
\sred{Group} & \sred{?} \\
\sred{Abelian Group} & \sred{?} \\
\sred{Idempotent Comm. Monoid} & \sred{?} \\
\end{tabular}
\end{frame}

\begin{frame}
\frametitle{Commutative Monoid and Bag}
\begin{definition}
A \emph{Bag} (over a type A) is an unordered finite collection
of $x$ where $x\,:\,A$.
\end{definition}
\pause
Implementation?
\begin{itemize}
\item<2-> Inductive type
\begin{itemize}
\item<3-> Ordered!
\end{itemize}
\item<4-> $A \rightarrow \mathbb{N}$
\begin{itemize}
\item<5-> No finite support!
\end{itemize}
\item<6-> $A \rightarrow \mathbb{N}$ plus finite support
\begin{itemize}
\item<7-> ``Finite support'' is hard to say constructively $\ldots$
\item<8-> Summing over all elements of $A$ is even harder $\ldots$
\item<9-> Can build a decidable equiv. relation on $A$ from $A \rightarrow \mathbb{N}$!
\end{itemize}
\item<10-> $\texttt{List}\ A$ up to bag-equality (aka permutations)
\begin{itemize}
\item<11-> almost works!
\item<12-> Commutative Monoid uses $\equiv$
\end{itemize}
\end{itemize}
\begin{theorem}[Within Martin-Löf Type Theory]<13->
  There's no \emph{free} functor from Types to Commutative Monoids using $\equiv$.
  % $\neg\exists$ \emph{left adjoint} to Commutative
  % Monoids over an arbitrary type (in MLTT).
\end{theorem}
\end{frame}

\begin{frame}
\frametitle{Change the question!}
\begin{definition}
A \emph{DBag} over a type $A$ with dec. $=$ is an unordered
collection of $x$ where $x~:~A$.
\end{definition}
\pause
\begin{definition}
A \emph{Bag} over a setoid $A$ is an unordered
collection of $x$ where $x : \texttt{Carrier}\, A$.
\end{definition}
\pause
Implementation attempts:
\begin{itemize}
\item<4->Nils Anders Danielsson's
\textit{Bag Equivalence via a Proof-Relevant Membership Relation}
\begin{itemize}
\item<5->Too many parts over $\equiv$
\end{itemize}
\item<6->Erik Palmgren's \textit{Setoid Families}
\begin{itemize}
\item<7->Extremely complex, forget the actual dead end.
\end{itemize}
\item<8->Mimick above with our own Proof-Relevant $\in$ over
  Setoid
\begin{itemize}
\item<9->Proof that \texttt{fold} well-behaved very hard.
\end{itemize}
\item<10->Bag-equality in new version of Agda!
\begin{itemize}
\item<11->Still assumes $\equiv$.
\end{itemize}
\item<12->Experimental library with permutations over tables
$\newline\Rightarrow$ proof that \texttt{fold} is well-behaved
\hfill \pause\alert{Success!}
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Key ingredients of Bag}
Distilling the insights from $\sim \! 1000$ lines of Agda \pause
\begin{itemize}
\item<1-> Internalize length of ``list'' into a record \texttt{Seq} ---\texttt{subst} is evil!
\item<2-> Table of A is $\texttt{Fin}\, \mathbb{N} \rightarrow A$ (finite
  support)
\item<3-> Equivalence of sequences $S$ and $T$ is
\begin{itemize}
\item<4-> A permutation between $|S|$ and $|T|$, i.e.
\item<5-> An equivalence between $\texttt{Fin}~ |S|$ and $\texttt{Fin}~ |T|$
\item<6-> A proof that permuting the elements of $T$ gives a
pointwise Setoid-equivalence to those of $S$.
\end{itemize}
\item<7-> Use previous infrastructure built to move between proofs
on permutations and proofs on types (work on $\Pi$ languages
w/ Amr Sabry)
\item<8-> Create an abstract interface for Multiset, MultisetHom and 
``functorial'' MultisetHom
\item<9-> Satisfies interface $\Rightarrow$\ left
adjoint to Commutative Monoid
\item<10-> Bag satisfies the interface
\item<11-> Use \texttt{abstract} in key places to prevent normalization
in proof goals
\item<12-> Never use \texttt{subst} ---even when building the identity permutation
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Extending the tale, take 2}
Given an arbitrary type A : \\ \vspace*{4mm}
\begin{tabular}{llll}
\textbf{Theory} & \textbf{Structure} & Over & Equality \\ \hline
Carrier & Identity A & Type  & $\equiv$ \\
Pointed & Maybe A & Type & $\equiv$\\ \hline
Unary & ℕ × A &  Type & $\equiv$\\
Involutive & A ⊎ A & Type & $\equiv$ \\ \hline
Magma & Tree A &  Type & $\equiv$\\
Semigroup & NEList A & Type & $\equiv$\\ \hline
Monoid & List A & Type & $\equiv$\\
Left Unital Semigroup & List A × ℕ & Type & $\equiv$\\
Right Unital Semigroup & ℕ × List A & Type & $\equiv$\\ \hline
Commutative Monoid & Bag & Setoid &  proof-relevant permutations \\
Group & ? & ? & ? \\
Abelian Group & Hybrid Sets & Setoid &  proof-relevant permutations\\
Idemp. Comm. Monoid & Set & Setoid &  logical equivalence \\
\end{tabular}
\end{frame}

\begin{frame}
\frametitle{What's the deal with those axioms?}
\begin{itemize}
\item Works easily:
\begin{itemize}
\item Associativity: $\forall x, y, z.\ x * (y * z) \equiv (x * y) *z$;
\item Left-unit: $\forall x.\ e * x \equiv x$;
\item Right-unit: $\forall x.\ x * e \equiv x$
\item Involutive: $\forall x.\ inv (inv x) \equiv x$
\end{itemize}
\item Hard:
\begin{itemize}
\item Commutativity: $\forall x, y.\ x * y \equiv y * x$
\end{itemize}
\item Very Hard:
\begin{itemize}
\item Idempotence: $\forall x.\ x * x \equiv x$
\end{itemize}
\end{itemize}
\pause
Found the secret ingredient in \textit{Algebraic Theories in Monoidal
  Categories} by L. Mauri: structural context rules (weakening,
exchange, contraction).
\end{frame}

\begin{frame}
\frametitle{More tale to tell}
\begin{itemize}
\item $\bot$, $\top$, $\mathbb{B}$, $\mathbb{N}$, $\mathbb{Z}$ show up
as \sred{initial objects}.
\item Bivariate (but $\times$ and $\uplus$ are adjoint to diagonal,
  not forgetful functor)
\item Indexed sets of operations
\end{itemize}
\end{frame}

% Where do these (math theories) show up?
\begin{frame}
\frametitle{Potential data-structures}
\sred{left-zero monoid}, pointed unary, idempotent unary, commutative
magma, pointed magma, quasigroup, loop, semilattice, medial magma,
left semimedial magma, left distributive magma, idempotent magma,
zeropotent magma, left unary magma, Steiner magma, null semigroup, BCI algebra, BCK
algebra, squag, sloop, Moufang quasigroup, loop, left shelf, shelf,
rack, spindle, quandle, Kei, involutive semigroup, band, rectangular
band, hemigroup, pseudo inverse algebra, ringoid, left near semiring,
near semiring, semifield, semiring, semirng, pre-dioid, dioid, star semiring,
idempotent dioid, ring, commutative ring, idempotent semiring, Stone algebra,
Kleene lattice, Kleene algebra, Heyting algebra, Goedel algebra, ortho
lattice, directoid, semiheap, idempotent semiheap, heap, meadow, wheel.
\end{frame}

% Where do these (data structures) show up?
\begin{frame}
\frametitle{Structures looking for a home}
Difference list, stack, queue, finite map, rose tree, digraph,
multigraph, partitions, oriented cycles, colorings, tri-colorings,
hedges, derangements, ballots, commutative parenthesizations, linear
order, permutations, even permutations, chains, oriented sets, even
sets, octopus, vertebrae.
\end{frame}

\begin{frame}
\frametitle{Math and CS}
Given an arbitrary type A : \\ \vspace*{4mm}
\begin{tabular}{llll}
\textbf{Theory} & \textbf{Structure} & Over & Equality \\ \hline
Carrier & Identity A & Type  & $\equiv$ \\
Pointed & Maybe A & Type & $\equiv$\\ \hline
Unary & ℕ × A &  Type & $\equiv$\\
Involutive & A ⊎ A & Type & $\equiv$ \\ \hline
Magma & Tree A &  Type & $\equiv$\\
Semigroup & NEList A & Type & $\equiv$\\ \hline
Monoid & List A & Type & $\equiv$\\
Left Unital Semigroup & List A × ℕ & Type & $\equiv$\\
Right Unital Semigroup & ℕ × List A & Type & $\equiv$\\ \hline
Commutative Monoid & Bag & Setoid &  proof-relevant permutations \\
Group & ? & ? & ? \\
Abelian Group & Hybrid Sets & Setoid &  proof-relevant permutations\\
Idemp. Comm. Monoid & Set & Setoid &  logical equivalence \\
\end{tabular}

\vspace*{3mm}
\url{https://github.com/JacquesCarette/TheoriesAndDataStructures}
\end{frame}


\end{document}