leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

work on slides

Browse source
This commit is contained in:
Leon Vatthauer 2024-01-14 18:12:29 +01:00
parent 5557dd1d6a
commit 985cbefd63
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
4 changed files with 204 additions and 97 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
slides/bibliography.bib
View file

@ -1 +1,50 @@
@article{moggi,
author = {Moggi, Eugenio},
title = {Notions of Computation and Monads},
year = {1991},
issue_date = {July 1991},
publisher = {Academic Press, Inc.},
address = {USA},
volume = {93},
number = {1},
issn = {0890-5401},
url = {https://doi.org/10.1016/0890-5401(91)90052-4},
doi = {10.1016/0890-5401(91)90052-4},
journal = {Inf. Comput.},
month = {jul},
pages = {55–92},
numpages = {38}
}
@article{restriction,
author = {Cockett, J. R. B. and Lack, Stephen},
title = {Restriction Categories I: Categories of Partial Maps},
year = {2002},
issue_date = {January},
publisher = {Elsevier Science Publishers Ltd.},
address = {GBR},
volume = {270},
number = {1–2},
issn = {0304-3975},
url = {https://doi.org/10.1016/S0304-3975(00)00382-0},
doi = {10.1016/S0304-3975(00)00382-0},
abstract = {Given a category with a stable system of monics, one can form the corresponding category of partial maps. To each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. This structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. Categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call MCat. The construction of categories of partial maps provides a 2-functor Par:Mcat→Cat. We show that Par can be made into an equivalence of 2-categories between MCat and a 2-category of restriction categories. The underlying ordinary functor Par&r0:Mcat&0 → Ca t0 of the above 2-functor Par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of M-categories and of restriction categories. We also consider the problem of how to turn a formal system of subobjects into an actual system of subobjects. A formal system of subobjects is given by a functor into the category sLat of semilattices. This structure gives rise to a restriction category which, via the above equivalence of 2-categories, gives an M-category. This M-category contains the universal realization of the given formal subobjects as actual subobjects.},
journal = {Theor. Comput. Sci.},
month = {1},
pages = {223–259},
numpages = {37}
}
@article{eqlm,
title = {Equational Lifting Monads},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {29},
pages = {22},
year = {1999},
note = {CTCS '99, Conference on Category Theory and Computer Science},
issn = {1571-0661},
doi = {https://doi.org/10.1016/S1571-0661(05)80303-2},
url = {https://www.sciencedirect.com/science/article/pii/S1571066105803032},
author = {Anna Bucalo and Carsten Führmann and Alex Simpson},
abstract = {We introduce the notion of an “equational lifting monad” : a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus equational lifting monads precisely capture the (partial) equational properties of partial map classifiers. The representation theorem also provides a tool for transferring non-equational properties of partial map classifiers to equational lifting monads.}
}

33
slides/main.tex
View file

@ -18,7 +18,7 @@
%WordMark=None,
aspectratio=169,
fontsize=11,
fontbaselineskip=13,
fontbaselineskip=15,
scale=1.,
InsertTotalFoot
]{styles/beamerthemefau}
@ -140,13 +140,14 @@ Leon Vatthauer%\inst{1}
% ------------------------------------------------
\usepackage{MnSymbol} % for \squaredots
\usepackage{minted}
\setminted[agda]{
\setminted{
autogobble=true,
linenos=true,
breaklines=true,
encoding=utf8,
fontsize=\small,
% frame=lines
fontsize=\small
}
\usepackage{multicol}
@ -157,6 +158,7 @@ Leon Vatthauer%\inst{1}
\usepackage{lmodern}
\usepackage{tikz}
\usepackage{tikz-cd}
\usetikzlibrary{shapes.callouts}
\usepackage{xparse}
@ -180,18 +182,19 @@ at (#3) {#4};
\begin{document}
% Title page
\begin{frame}[t,titleimage]{-}
\titlepage%
\end{frame}
% Title page
\begin{frame}[t,titleimage]{-}
\titlepage%
\end{frame}
\input{sections/00_intro.tex}
\input{sections/01_abstracting.tex}
\input{sections/02_goals.tex}
% sections
\input{sections/00_intro.tex}
\input{sections/01_abstracting.tex}
\input{sections/02_goals.tex}
% Stylized outline
%\begin{frame}[title]{-}
%\tableofcontents
%\end{frame}
% bibliography
\begin{frame}[t]{Bibliography}
\printbibliography[heading=none]
\end{frame}
\end{document}

120
slides/sections/00_intro.tex
View file

@ -1,19 +1,15 @@
\section{Partiality in Type Theory}
% TODO
% - remove vskips and use begin{listing}
% - add colist definition
\begin{frame}[t, fragile]{Partiality in Haskell}{}
Haskell allows users to define arbitrary partial functions
\begin{itemize}
\item<1-> Some can be spotted easily by their definition:
\vskip 0.5cm
\begin{minted}{haskell}
head :: [a] -> a
head [] = error "empty list"
head (x:xs) = x
\end{minted}
head :: [a] -> a
head [] = error "empty list"
head (x:xs) = x
\end{minted}
\mycallout<2->{22, 1.5}{
ghci> head []\\
*** Exception: empty list\\
@ -24,12 +20,12 @@ head (x:xs) = x
others might be more subtle:
\vskip 0.5cm
\begin{minted}{haskell}
reverse :: [a] -> [a]
reverse l = revAcc l []
where
revAcc [] a = a
revAcc (x:xs) a = revAcc xs (x:a)
\end{minted}
reverse :: [a] -> [a]
reverse l = revAcc l []
where
revAcc [] a = a
revAcc (x:xs) a = revAcc xs (x:a)
\end{minted}
\mycallout<4->{22, 2}{
ghci> ones = 1 : ones\\
@ -41,63 +37,75 @@ reverse l = revAcc l []
\end{frame}
\begin{frame}[t, fragile]{Partiality in Agda}{The Maybe Monad}
In Agda every function has to be total and terminating, so how do we model partial functions?
\begin{itemize}[<+->]
\item In Agda every function has to be total and terminating, so how do we model partial functions?
\item Simple errors can be modelled with the maybe monad
\begin{listing}[H]
\begin{minted}{agda}
data Maybe (A : Set) : Set where
just : A → Maybe A
nothing : Maybe A
\end{minted}
\end{listing}
for head we can then do:
\vskip 0.5cm
\begin{minted}{agda}
head : ∀ A → List A → Maybe A
head nil = nothing
head (cons x xs) = just x
\end{minted}
\begin{multicols}{2}
\begin{minted}{agda}
data Maybe (A : Set) : Set where
just : A → Maybe A
nothing : Maybe A
\end{minted}
\columnbreak
\begin{minted}{agda}
head : ∀ A → List A → Maybe A
head nil = nothing
head (cons x xs) = just x
\end{minted}
\end{multicols}
\item What about \mintinline{agda}|reverse|?
\end{itemize}
\end{frame}
\begin{frame}[t, fragile]{Partiality in Agda}{Capretta's Delay Monad}
\begin{itemize}[<+->]
\begin{itemize}
\item Capretta's Delay Monad is a \textbf{coinductive} data type whose inhabitants can be viewed as suspended computations.
\vskip 0.5cm
\begin{minted}{agda}
data Delay (A : Set) : Set where
now : A → Delay A
later : ∞ (Delay A) → Delay A
\end{minted}
data Delay (A : Set) : Set where
now : A → Delay A
later : ∞ (Delay A) → Delay A
\end{minted}
\vskip 0.5cm
\item The delay datatype contains a constant for non-termination:
\vskip 0.5cm
\begin{minted}{agda}
never : Delay A
never = later (♯ never)
\end{minted}
never : Delay A
never = later (♯ never)
\end{minted}
\vskip 0.5cm
\item and we can define a function for \textit{running} a computation (for some amount of steps):
\vskip 0.5cm
\begin{minted}{agda}
run_for_steps : Delay A → ℕ → Delay A
run now x for n steps = now x
run later x for zero steps = later x
run later x for suc n steps = run ♭ x for n steps
\end{minted}
run_for_steps : Delay A → ℕ → Delay A
run now x for n steps = now x
run later x for zero steps = later x
run later x for suc n steps = run ♭ x for n steps
\end{minted}
\end{itemize}
\end{frame}
\begin{frame}[c, fragile]{Partiality in Agda}{Reversing (possibly infinite) lists}
\centering
\begin{minted}{agda}
reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
reverse {A} = revAcc []
where
revAcc : Colist A → Colist A → Delay (Colist A)
revAcc [] a = now a
revAcc (x ∷ xs) a = later (♯ revAcc (♭ xs) (x ∷ (♯ a)))
\end{minted}
\begin{frame}[t, fragile]{Partiality in Agda}{Capretta's Delay Monad}
\begin{itemize}
\item Now we can define a reverse function for possibly infinite lists:
\vskip 0.5cm
\begin{minted}{agda}
data Colist (A : Set) : Set where
[] : Colist A
_∷_ : A → ∞ (Colist A) → Colist A
\end{minted}
\vskip 0.5cm
\begin{minted}{agda}
reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
reverse {A} = revAcc []
where
revAcc : Colist A → Colist A → Delay (Colist A)
revAcc [] a = now a
revAcc (x ∷ xs) a = later (♯ revAcc (♭ xs) (x ∷ (♯ a)))
\end{minted}
\end{itemize}
\end{frame}

99
slides/sections/01_abstracting.tex
View file

@ -1,36 +1,81 @@
\section{Categorical Notions of Partiality}
% \begin{frame}[t, fragile]{Classifying Partiality Monads}
% A partiality monad should have the following properties:
% \begin{itemize}
% \item The following two programs should yield equal results:
% \begin{multicols}{2}
% \begin{minted}{haskell}
% do x <- p
% y <- q
% return (x, y)
% \end{minted}
\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Moggi's categorical semantics~\cite{moggi}}
Goal: interpret an effectul programming language in a category $\mathcal{C}$
% \begin{minted}{haskell}
% do y <- q
% x <- p
% return (x, y)
% \end{minted}
% \end{multicols}
% where p and q are (partial) computations.
% \end{itemize}
% \end{frame}
\begin{frame}[t, fragile]{Capturing Partiality Categorically}
\begin{itemize}
\item moggi denotational semantics (values A, computations TA)
\item restriction categories
\item equational lifting monads
\item<2-> Take a Monad $T$ on $\mathcal{C}$, then values are denoted by objects $A$ and programs by $TA$
\item<3-> Programs form a category $\mathcal{C}_T$ with $\mathcal{C}_T(X,Y) := \mathcal{C}(X, TY)$
\end{itemize}
\onslide<4->
What properties should a partiality monad $T$ have?
\begin{enumerate}
\item<5-> Commutativity (also entails strength), i.e. the following programs should yield equal results:
\begin{multicols}{2}
\begin{minted}{haskell}
do x <- p
y <- q
return (x, y)
\end{minted}
\begin{minted}{haskell}
do y <- q
x <- p
return (x, y)
\end{minted}
\end{multicols}
where p and q are programs.
\item<6-> Morphisms in $\mathcal{C}_T$ should be partial maps (How?)
\end{enumerate}
\end{frame}
\newcommand{\tdom}{\text{dom}}
\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Restriction Categories~\cite{restriction}}
\begin{definition}<1->
A restriction structure on $\mathcal{C}$ is a mapping $\tdom : \mathcal{C}(X,Y) \rightarrow \mathcal{C}(X,X)$ with the following properties:
\begin{alignat}{1}
f \circ (\tdom f) &= f\\
(\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\\
\tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\\
(\tdom h) \circ f &= f \circ \tdom (h \circ f)
\end{alignat}
for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow KY, g : X \rightarrow KZ, h: Y \rightarrow KZ$.
\end{definition}
Intuitively $\tdom f$ captures the domain of definiteness of $f$.
\begin{block}{Remark}<2->
Every category has a trivial restriction structure $\tdom f = id$, we call categories with a non-trivial restriction structure \textit{restriction categories}.
\end{block}
\end{frame}
\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Equational Lifting Monads~\cite{eqlm}}
The following criterion is sufficient for guaranteeing that the kleisli category is a restriction category:
\begin{definition}
A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ==
\[\begin{tikzcd}
TX && {TX \times TX} \\
\\
&& {T(TX \times X)}
\arrow["\Delta", from=1-1, to=1-3]
\arrow["\tau", from=1-3, to=3-3]
\arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
\end{tikzcd}\]
\end{definition}
\pause
\begin{theorem}
The Kleisli category of an equational lifting monad is a restriction category.
\end{theorem}
\end{frame}
% TODO is the maybe monad an equational lifting monad? Ask sergey
\begin{frame}[t, fragile]{The Maybe Monad}
\begin{itemize}
\item Short definition
@ -38,6 +83,8 @@
\end{itemize}
\end{frame}
% TODO is delay equational lifting?? maybe rethink the story here...
\begin{frame}[t, fragile]{The Delay Monad}
\begin{itemize}
\item Definition