From 9fa6f8e0ed45f437ad2fac4a15337cd744b8b313 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 22 Jan 2024 17:57:12 +0100 Subject: [PATCH] small changes --- slides/bibliography.bib | 23 ++++++++------ slides/code-examples/example.hs | 1 - slides/code-examples/reverse.agda | 8 ++--- slides/main.tex | 6 ++-- slides/sections/00_intro.tex | 13 +++----- slides/sections/01_abstracting.tex | 50 +++++++++++++++--------------- slides/sections/02_goals.tex | 22 +------------ slides/sections/03_app.tex | 21 +++++++++++++ 8 files changed, 71 insertions(+), 73 deletions(-) create mode 100644 slides/sections/03_app.tex diff --git a/slides/bibliography.bib b/slides/bibliography.bib index e7a9291..b84b822 100644 --- a/slides/bibliography.bib +++ b/slides/bibliography.bib @@ -80,16 +80,19 @@ numpages = {38} } -@article{quotienting, - title = {Quotienting the delay monad by weak bisimilarity}, - volume = {29}, - doi = {10.1017/S0960129517000184}, - number = {1}, - journal = {Mathematical Structures in Computer Science}, - publisher = {Cambridge University Press}, - author = {CHAPMAN, JAMES and UUSTALU, TARMO and VELTRI, NICCOLÒ}, - year = {2019}, - pages = {67–92} +@inproceedings{quotienting, +author = {Chapman, James and Uustalu, Tarmo and Veltri, Niccol\`{o}}, +title = {Quotienting the Delay Monad by Weak Bisimilarity}, +year = {2015}, +isbn = {9783319251493}, +publisher = {Springer-Verlag}, +address = {Berlin, Heidelberg}, +url = {https://doi.org/10.1007/978-3-319-25150-9_8}, +doi = {10.1007/978-3-319-25150-9_8}, +abstract = {The delay datatype was introduced by Capretta [3] as a means to deal with partial functions as in computability theory in Martin-L\"{o}f type theory. It is a monad and it constitutes a constructive alternative to the maybe monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay monad quotiented by weak bisimilarity is still a monad. In this paper, we consider Hofmann's alternative approach [6] of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the semi-classical axiom of countable choice. We have fully formalized our results in the Agda dependently typed programming language.}, +booktitle = {Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 9399}, +pages = {110–125}, +numpages = {16} } @article{restriction, diff --git a/slides/code-examples/example.hs b/slides/code-examples/example.hs index b03e454..bccf63f 100644 --- a/slides/code-examples/example.hs +++ b/slides/code-examples/example.hs @@ -1,5 +1,4 @@ hd :: [a] -> a -hd [] = error "empty list" hd (x : _) = x main :: IO () diff --git a/slides/code-examples/reverse.agda b/slides/code-examples/reverse.agda index 5cda30f..ddc33c9 100644 --- a/slides/code-examples/reverse.agda +++ b/slides/code-examples/reverse.agda @@ -1,10 +1,6 @@ {-# OPTIONS --guardedness #-} open import Codata.Musical.Notation open import Data.Nat -open import Data.Nat.Show renaming (show to showℕ) -open import Function.Base -open import Relation.Binary.PropositionalEquality -open import Data.String using (String; _++_) module reverse where data Delay (A : Set) : Set where @@ -14,7 +10,7 @@ module reverse where run_for_steps : ∀ {A : Set} → 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 = later (♯ (run ♭ x for n steps)) + run later x for suc n steps = run ♭ x for n steps never : ∀ {A : Set} → Delay A never = later (♯ never) @@ -24,7 +20,7 @@ module reverse where _∷_ : A → ∞ (Colist A) → Colist A reverse : ∀ {A : Set} → Colist A → Delay (Colist A) - reverse {A} = reverseAcc [] + reverse {A} l = reverseAcc l [] where reverseAcc : Colist A → Colist A → Delay (Colist A) reverseAcc [] a = now a diff --git a/slides/main.tex b/slides/main.tex index 965005c..fab97c6 100644 --- a/slides/main.tex +++ b/slides/main.tex @@ -17,8 +17,8 @@ %ThirdLogo = template-art/FAUWortmarkeBlau.pdf, %WordMark=None, aspectratio=169, - fontsize=11, - fontbaselineskip=15, + fontsize=11.5, + fontbaselineskip=14, scale=1., InsertTotalFoot ]{styles/beamerthemefau} @@ -199,4 +199,6 @@ at (#3) {#4}; \printbibliography[heading=none] \end{frame} + \input{sections/03_app.tex} + \end{document} \ No newline at end of file diff --git a/slides/sections/00_intro.tex b/slides/sections/00_intro.tex index 61b6969..e6f57a7 100644 --- a/slides/sections/00_intro.tex +++ b/slides/sections/00_intro.tex @@ -1,20 +1,17 @@ \section{Partiality in Type Theory} \begin{frame}[t, fragile]{Partiality in Haskell}{} - Haskell allows users to define arbitrary partial functions + In Haskell we are able 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} - \mycallout<2->{22, 1.5}{ + \mycallout<2->{22.5, 1.5}{ ghci> head []\\ - *** Exception: empty list\\ - CallStack (from HasCallStack):\\ - error, called at example.hs:2:9 in main:Main + Exception: code-examples/example.hs:2:1-14: Non-exhaustive patterns in function head } \item<3-> others might be more subtle: @@ -27,7 +24,7 @@ revAcc (x:xs) a = revAcc xs (x:a) \end{minted} - \mycallout<4->{22, 2}{ + \mycallout<4->{22.5, 2}{ ghci> ones = 1 : ones\\ ghci> reverse ones\\ ... @@ -99,7 +96,7 @@ \item Now we can define a reverse function for possibly infinite lists: \begin{minted}{agda} reverse : ∀ {A : Set} → Colist A → Delay (Colist A) - reverse {A} = revAcc [] + reverse {A} l = revAcc l [] where revAcc : Colist A → Colist A → Delay (Colist A) revAcc [] a = now a diff --git a/slides/sections/01_abstracting.tex b/slides/sections/01_abstracting.tex index e4df5c6..6121617 100644 --- a/slides/sections/01_abstracting.tex +++ b/slides/sections/01_abstracting.tex @@ -1,25 +1,6 @@ \section{Categorical Notions of Partiality} -\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{itemize} - \item<2-> Take a Monad $T$ on $\mathcal{C}$, then values are denoted by objects $A$ and computations 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 monad $T$ for modelling partiality have? - -\begin{enumerate} - \item<5-> Commutativity (also entails strength) - \item<6-> Morphisms in $\mathcal{C}_T$ should be partial maps - \item<7-> There should be no other effect besides partiality -\end{enumerate} - -\end{frame} - -\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Preliminaries} +\begin{frame}[t, fragile]{Preliminaries} We work in category $\mathcal{C}$ that \begin{itemize}[<+->] \item has finite products @@ -40,9 +21,28 @@ What properties should a monad $T$ for modelling partiality have? \end{frame} +\begin{frame}[t, fragile]{Capturing Partiality}{Moggi's categorical semantics~\cite{moggi}} +Goal: interpret an effectul programming language in a category $\mathcal{C}$ + +\begin{itemize} + \item<2-> Take a Monad $T$ on $\mathcal{C}$, we view objects $A$ as types of values and objects $TA$ as types of computations. + \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 monad $T$ for modelling partiality have? + +\begin{enumerate} + \item<5-> Commutativity (also entails strength) + \item<6-> Morphisms in $\mathcal{C}_T$ should be partial maps + \item<7-> There should be no other effect besides partiality +\end{enumerate} + +\end{frame} + \newcommand{\tdom}{\text{dom}\;} -\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Restriction Categories~\cite{restriction}} +\begin{frame}[t, fragile]{Capturing Partiality}{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} @@ -62,7 +62,7 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. \end{block} \end{frame} -\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Equational Lifting Monads~\cite{eqlm}} +\begin{frame}[t, fragile]{Capturing Partiality}{Equational Lifting Monads~\cite{eqlm}} The following criterion guarantees that some form of partiality is the only possible side-effect: \pause \begin{definition} @@ -84,7 +84,7 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. \end{theorem} \end{frame} -\begin{frame}[t, fragile]{Capturing Partiality Categorically}{The Maybe Monad} +\begin{frame}[t, fragile]{Capturing Partiality}{The Maybe Monad} \begin{itemize}[<+->] \item $MX = X + 1$ \item The maybe monad is strong and commutative: @@ -106,7 +106,7 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. \end{itemize} \end{frame} -\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Capretta's Delay Monad~\cite{delay}} +\begin{frame}[t, fragile]{Capturing Partiality}{Capretta's Delay Monad~\cite{delay}} \begin{itemize}[<+->] \item Recall the delay codatatype: @@ -125,7 +125,7 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. \end{itemize} \end{frame} -\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Quotienting the Delay Monad~\cite{quotienting}} +\begin{frame}[t, fragile]{Capturing Partiality}{Quotienting the Delay Monad~\cite{quotienting}} Following the work by Chapman, Uustalu and Veltri we can quotient $D$ by the 'correct' kind of equality: \[\mprset{fraction={===}} \inferrule {p \downarrow c \\ q \downarrow c} {p \approx q}\hskip 2cm diff --git a/slides/sections/02_goals.tex b/slides/sections/02_goals.tex index 0c8e7c2..370e9d5 100644 --- a/slides/sections/02_goals.tex +++ b/slides/sections/02_goals.tex @@ -12,28 +12,8 @@ \item strong \item commutative \item an equational lifting monad + \item the initial pre-Elgot monad \end{itemize} \item Take the category of setoids and show that $K$ instantiates to $D_\approx$ \end{itemize} -\end{frame} - -\begin{frame}[t, fragile, blank]{Category Theory in Agda}{Setoid-enriched Categories} - \begin{minted}{agda} -record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where - field - Obj : Set o - _⇒_ : Obj → Obj → Set ℓ - _≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e - - id : ∀ {A} → (A ⇒ A) - _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C) - - field - assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} - → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) - identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f - identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f - equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B}) - ∘-resp-≈ : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i - \end{minted} \end{frame} \ No newline at end of file diff --git a/slides/sections/03_app.tex b/slides/sections/03_app.tex new file mode 100644 index 0000000..f9e6377 --- /dev/null +++ b/slides/sections/03_app.tex @@ -0,0 +1,21 @@ +\section*{Appendix} +\begin{frame}[t, fragile, blank]{App: Category Theory in Agda}{Setoid-enriched Categories} + \begin{minted}{agda} +record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where + field + Obj : Set o + _⇒_ : Obj → Obj → Set ℓ + _≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e + + id : ∀ {A} → (A ⇒ A) + _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C) + + field + assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} + → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) + identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f + identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f + equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B}) + ∘-resp-≈ : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i + \end{minted} +\end{frame} \ No newline at end of file