From 7f3330f45ce47c115bcd84219c6a395028bd39e2 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 11 Jan 2024 13:38:32 +0100 Subject: [PATCH] Work on slides --- .gitignore | 1 + slides/.vscode/settings.json | 2 + slides/code-examples/example.hs | 9 ++-- slides/main.tex | 82 ++++++------------------------ slides/sections/00_intro.tex | 82 +++++++++++++++--------------- slides/sections/01_abstracting.tex | 56 ++++++++++++++++++++ slides/sections/02_goals.tex | 24 +++++++++ 7 files changed, 145 insertions(+), 111 deletions(-) create mode 100644 slides/sections/01_abstracting.tex create mode 100644 slides/sections/02_goals.tex diff --git a/.gitignore b/.gitignore index 564842d..6492c42 100644 --- a/.gitignore +++ b/.gitignore @@ -51,3 +51,4 @@ slides/*.pdf _region_.tex *.xdv thesis/_minted-main/ +slides/_minted-main/ diff --git a/slides/.vscode/settings.json b/slides/.vscode/settings.json index 68ca5e0..659398f 100644 --- a/slides/.vscode/settings.json +++ b/slides/.vscode/settings.json @@ -7,7 +7,9 @@ "-synctex=1", "-interaction=nonstopmode", "-file-line-error", + "-shell-escape", "-pdf", + "-xelatex", "-outdir=%OUTDIR%", "main.tex" ], diff --git a/slides/code-examples/example.hs b/slides/code-examples/example.hs index 32c0418..0ca1ee8 100644 --- a/slides/code-examples/example.hs +++ b/slides/code-examples/example.hs @@ -3,10 +3,11 @@ hd [] = error "empty list" hd (x : _) = x main :: IO () -main = print (hd []::[String]) +main = do + print (Main.reverse ([1,2,3]::[Int])) + print (hd []::[String]) reverse :: [a] -> [a] -reverse l = rev l [] +reverse = reverseAcc [] where - rev [] a = a - rev (x:xs) a = rev xs (x:a) + reverseAcc = foldl (flip (:)) diff --git a/slides/main.tex b/slides/main.tex index 82cd63e..5b1ac36 100644 --- a/slides/main.tex +++ b/slides/main.tex @@ -24,8 +24,8 @@ ]{styles/beamerthemefau} % ---------------------------------------------------------------------------------------- % Input and output encoding -\usepackage[T1]{fontenc} -\usepackage[utf8]{inputenc} +% \usepackage[T1]{fontenc} +% \usepackage[utf8]{inputenc} % ---------------------------------------------------------------------------------------- % Language settings \usepackage[english]{babel} @@ -36,6 +36,7 @@ % - We use serif for math environements % - isomath is used for upGreek letters % ---------------------------------------------------------------------------------------- +\usepackage{fvextra} \usepackage{isomath} \usefonttheme[onlymath]{serif} \usepackage{exscale} @@ -49,7 +50,7 @@ % ======================================================================================== % Setup for Titlepage % ---------------------------------------------------------------------------------------- -\title{Implementing Notions of Partiality and Delay\\ in Agda} +\title{Implementing Categorical Notions of Partiality and Delay in Agda} \subtitle{Subtitle} \author[L. Vatthauer]{ Leon Vatthauer%\inst{1} @@ -138,71 +139,18 @@ Leon Vatthauer%\inst{1} % The main document % ------------------------------------------------ \usepackage{MnSymbol} % for \squaredots -\usepackage{listings} -\lstset{mathescape} - -\usepackage{xcolor} - -\definecolor{codegray}{rgb}{0.5,0.5,0.5} -\definecolor{string}{HTML}{79731B} -\definecolor{keyword}{HTML}{447A59} -\definecolor{background}{HTML}{E6E6E6} -\definecolor{error}{HTML}{9B0511} -\definecolor{agda-name}{HTML}{3b31f9} -\definecolor{agda-keyword}{HTML}{fc970a} -\definecolor{agda-constructor}{HTML}{08aa20} - - -\lstdefinestyle{mystyle}{ - backgroundcolor=\color{background}, - % commentstyle=\color{codegreen}, - % keywordstyle=\color{keyword}, - numberstyle=\tiny\color{codegray}, - stringstyle=\color{string}, - basicstyle=\ttfamily\small, - breakatwhitespace=false, - breaklines=true, - captionpos=b, - keepspaces=true, - numbers=left, - numbersep=5pt, - showspaces=false, - showstringspaces=false, - showtabs=false, - tabsize=2 -} -\lstdefinelanguage{myhaskell}{ - keywords=[1]{ - where - }, - keywordstyle=[1]\color{agda-keyword}, - keywords=[2]{ - error - }, - keywordstyle=[2]\color{error}, - keywords=[3]{ - head, reverse, rev - }, - keywordstyle=[3]\color{agda-name}, - morestring=[b]" +\usepackage{minted} +\setminted[agda]{ + linenos=true, + breaklines=true, + encoding=utf8, + fontsize=\small, + % frame=lines } +\usepackage{multicol} -\lstdefinelanguage{myagda}{ - keywords=[1]{ - data, where - }, - keywordstyle=[1]\color{agda-keyword}, - keywords=[2]{ - Delay, Set, foldl, Colist, reverse, reverseAcc, run_for_steps, run, for, steps, fin-colist, inf-colist, never, head, List, Maybe - }, - keywordstyle=[2]\color{agda-name}, - keywords=[3]{ - now, later, zero, suc, just, nothing, nil, cons - }, - keywordstyle=[3]\color{agda-constructor} -} - -\lstset{style=mystyle} +\usepackage{fontspec} +\setmonofont{Noto Sans Mono} \usepackage{lmodern} @@ -236,6 +184,8 @@ at (#3) {#4}; \end{frame} \input{sections/00_intro.tex} +\input{sections/01_abstracting.tex} +\input{sections/02_goals.tex} % Stylized outline %\begin{frame}[title]{-} diff --git a/slides/sections/00_intro.tex b/slides/sections/00_intro.tex index 736910f..97bda1f 100644 --- a/slides/sections/00_intro.tex +++ b/slides/sections/00_intro.tex @@ -1,27 +1,28 @@ +\section{Partiality in Type Theory} \begin{frame}[t, fragile]{Partiality in Haskell}{} - \begin{itemize}[<+->] - \item Haskell allows users to define arbitrary partial functions, some can be spotted easily by their definition: + \begin{itemize} + \item<1-> Haskell allows users to define arbitrary partial functions, some can be spotted easily by their definition: \vskip 1cm - \begin{lstlisting}[language=myhaskell, linewidth=12cm] + \begin{minted}{agda} head :: [a] -> a -head [] = error "empty list" +head [] = error "empty list" head (x:xs) = x -\end{lstlisting} - \mycallout<3->{21, 1.5}{ +\end{minted} + \mycallout<2->{21, 1.5}{ ghci> head []\\ *** Exception: empty list\\ CallStack (from HasCallStack):\\ error, called at example.hs:2:9 in main:Main } - \item + \item<3-> others might be more subtle: \vskip 1cm - \begin{lstlisting}[language=myhaskell, linewidth=12cm] -reverse l = rev l [] -where - rev [] a = a - rev (x:xs) a = rev xs (x:a) -\end{lstlisting} + \begin{minted}{agda} +reverse :: [a] -> [a] +reverse = reverseAcc [] + where + reverseAcc = foldl (flip (:)) +\end{minted} \mycallout<4->{21, 2}{ ghci> ones = 1 : ones\\ @@ -30,7 +31,6 @@ where } \end{itemize} -% TODO right of this add error bubble that shows `reverse ones` \end{frame} \begin{frame}[t, fragile]{Partiality in Agda}{The Maybe Monad} @@ -38,59 +38,59 @@ In Agda every function has to be total and terminating, so how do we model parti \begin{itemize}[<+->] \item Simple errors can be modelled with the maybe monad - \begin{lstlisting}[linewidth=14cm, language=myagda] + \begin{minted}{agda} data Maybe (A : Set) : Set where - just : A $\rightarrow$ Maybe A + just : A → Maybe A nothing : Maybe A -\end{lstlisting} +\end{minted} for head we can then do: - \begin{lstlisting}[linewidth=14cm, language=myagda] -head : $\forall$ A $\rightarrow$ List A $\rightarrow$ Maybe A -head nil = nothing + \begin{minted}{agda} +head : ∀ A → List A → Maybe A +head nil = nothing head (cons x xs) = just x -\end{lstlisting} +\end{minted} - \item What about \lstinline|reverse|? + \item What about \mintinline{agda}|reverse|? \end{itemize} \end{frame} \begin{frame}[t, fragile]{Partiality in Agda}{Capretta's Delay Monad} \begin{itemize}[<+->] \item Capretta's Delay Monad is a \textbf{coinductive} data type whose inhabitants can be viewed as suspended computations. - \begin{lstlisting}[linewidth=20cm, language=myagda] + \begin{minted}{agda} data Delay (A : Set) : Set where - now : A $\rightarrow$ Delay A - later : $\infty$ (Delay A) $\rightarrow$ Delay A -\end{lstlisting} + now : A → Delay A + later : ∞ (Delay A) → Delay A +\end{minted} \item The delay datatype contains a constant for non-termination: - \begin{lstlisting}[linewidth=20cm, language=myagda] + \begin{minted}{agda} never : Delay A -never = later ($\sharp$ never) -\end{lstlisting} +never = later (♯ never) +\end{minted} \item and we can define a function for \textit{running} a computation (for some amount of steps): - \begin{lstlisting}[linewidth=20cm, language=myagda] -run_for_steps : Delay A $\rightarrow$ $\mathbb{N}$ $\rightarrow$ Delay A + \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 $\flat$ x for n steps -\end{lstlisting} +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{lstlisting}[language=myagda] -foldl : $\forall$ {A B : Set} $\rightarrow$ (A $\rightarrow$ B $\rightarrow$ A) $\rightarrow$ A $\rightarrow$ Colist B $\rightarrow$ Delay A -foldl c n [] = now n -foldl c n (x $\squaredots$ xs) = later ($\sharp$ foldl c (c n x) ($\flat$ xs)) +\begin{minted}{agda} +foldl : ∀ {A B : Set} → (A → B → A) → A → Colist B → Delay A +foldl c n [] = now n +foldl c n (x ∷ xs) = later (♯ foldl c (c n x) (♭ xs)) -reverse : $\forall$ {A : Set} $\rightarrow$ Colist A $\rightarrow$ Delay (Colist A) +reverse : ∀ {A : Set} → Colist A → Delay (Colist A) reverse {A} = reverseAcc [] where - reverseAcc : Colist A $\rightarrow$ Colist A $\rightarrow$ Delay (Colist A) - reverseAcc = foldl ($\lambda$ xs x $\rightarrow$ x $\squaredots$ ($\sharp$ xs)) -\end{lstlisting} + reverseAcc : Colist A → Colist A → Delay (Colist A) + reverseAcc = foldl (λ xs x → x ∷ (♯ xs)) +\end{minted} \end{frame} \ No newline at end of file diff --git a/slides/sections/01_abstracting.tex b/slides/sections/01_abstracting.tex new file mode 100644 index 0000000..b9f874e --- /dev/null +++ b/slides/sections/01_abstracting.tex @@ -0,0 +1,56 @@ +\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{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 +\end{itemize} +\end{frame} + +\begin{frame}[t, fragile]{The Maybe Monad} +\begin{itemize} + \item Short definition + \item is equational lifting monad +\end{itemize} +\end{frame} + +\begin{frame}[t, fragile]{The Delay Monad} +\begin{itemize} + \item Definition + \item Strong-Bisimilarity + \item Weak-Bisimilarity (Monad?) +\end{itemize} +\end{frame} + +\begin{frame}[t, fragile]{Iteration} +\begin{itemize} + \item Elgot-Algebras + \item Free Elgot-Algebras yield monad K + \item K is equational lifting + \item K instantiates to maybe and delay +\end{itemize} +\end{frame} \ No newline at end of file diff --git a/slides/sections/02_goals.tex b/slides/sections/02_goals.tex new file mode 100644 index 0000000..4783537 --- /dev/null +++ b/slides/sections/02_goals.tex @@ -0,0 +1,24 @@ +\section{Implementation in Agda} + +\begin{frame}[t, fragile]{Goals} + \begin{itemize} + \item Formalize delay monad (categorically as terminal coalgebra) + properties + \item Formalize K + properties + \item Case study on Setoids + \end{itemize} +\end{frame} + +\begin{frame}[t, fragile]{Category theory in Agda} + agda-categories +\end{frame} + +\begin{frame}[t, fragile]{What I managed to show} + TODO +\end{frame} + +\begin{frame}[t, fragile]{Further work} +\begin{itemize} + \item Show that $\tilde{D}$ is monad (under conditions) + \item Show that $K \cong \tilde{D}$ (under conditions) +\end{itemize} +\end{frame} \ No newline at end of file