slides/code-examples/reverse.agda

@@ -1,4 +1,5 @@
 {-# OPTIONS --guardedness #-}
+-- open import Codata.Musical.Colist hiding (_++_)
 open import Codata.Musical.Notation
 open import Data.Nat
 open import Data.Nat.Show renaming (show to showℕ)

slides/sections/00_intro.tex

@@ -55,18 +55,13 @@
     \end{minted}
   \end{multicols}
 
-  \item What about \mintinline{agda}|reverse| for (possibly) infinite lists:
-  \begin{minted}{agda}
-    data Colist (A : Set) : Set where
-      [] : Colist A
-      _∷_ : A → ∞ (Colist A) → Colist A
-  \end{minted}
+  \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}
@@ -97,6 +92,13 @@
 
 \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 []

slides/sections/01_abstracting.tex

@@ -13,6 +13,21 @@ What properties should a monad $T$ for modelling partiality 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
   \item<7-> There should be no other effect besides partiality
 \end{enumerate}
@@ -84,6 +99,9 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
   \end{theorem}
 \end{frame}
 
+% write on board:
+% equational lifting: do x <- p; return (return x, x) = do x <- p; return (p, x)
+
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{The Maybe Monad}
 \begin{itemize}[<+->]
   \item $MX = X + 1$
@@ -125,6 +143,10 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
 \end{itemize}
 \end{frame}
 
+% write on board:
+% \eta = now
+% given f : X \rightarrow TY, f* is defined by corecursion.
+
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{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={===}}
@@ -149,6 +171,7 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
 \end{frame}
 
 \begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras}
+\pause
 The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}~\cite{elgotalgebras}:
 \begin{definition}
   A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
@@ -177,7 +200,7 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet
     \item \textbf{Fixpoint}: $f^\dagger = [ \eta , f^\dagger ]^* \circ f$
     \\for $f : X \rightarrow T(Y + X)$
     \item \textbf{Uniformity}: $f \circ h = T(id + h) \circ g \Rightarrow f^\dagger \circ h = g^\dagger$
-    \\for $f : X \rightarrow T(Y + X) , g : Z \rightarrow T(Y + Z), h : Z \rightarrow X$
+    \\for $f : X \rightarrow T(Y + X) , g : Z \rightarrow T(Y + Z)$
     \item \textbf{Naturality}: $g^* \circ f^\dagger = ([ (T inl) \circ g , \eta \circ inr ]^* \circ f )^\dagger$
     \\for $f : X \rightarrow T(Y + X), g : Y \rightarrow TZ$
     \item \textbf{Codiagonal}: $f^{\dagger\dagger} = (T[id , inr ] \circ f)^\dagger$
@@ -191,6 +214,9 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
 
 \end{frame}
 
+
+% TODO 
+% maybe dont talk about elgot monads at all, give intuition for the initial pre Elgot monad.
 \begin{frame}[t, fragile]{Partiality from Iteration}{pre-Elgot Monads~\cite{uniformelgot}}
   Relaxing the requirements for Elgot monads we get the following weaker concept:
   \begin{definition}
@@ -224,6 +250,7 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
       \item $X + 1$ is the initial (pre-)Elgot monad ($\Rightarrow K \cong (-)+1 \cong D_\approx$)
     \end{itemize}
     
+    % \\$\Rightarrow$ $X+1$ is the initial pre-Elgot Monad and also the initial Elgot Monad.
     \item \textbf{Assuming countable choice:}
     \begin{itemize}[<+->]
       \item The initial pre-Elgot monad and the initial Elgot monad coincide
@@ -231,4 +258,9 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
     \end{itemize}
     
   \end{itemize}
-\end{frame}
+\end{frame}
+
+
+%% TODOs:
+% cite stefan
+% cite sergey