\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:
    \vskip 1cm
    \begin{lstlisting}[language=myhaskell, linewidth=12cm]
head :: [a] -> a
head [] = error "empty list"
head (x:xs) = x
\end{lstlisting}
      \mycallout<3->{21, 1.5}{
        ghci> head []\\
        *** Exception: empty list\\
        CallStack (from HasCallStack):\\
        error, called at example.hs:2:9 in main:Main
      }
    \item
    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}
    
    \mycallout<4->{21, 2}{
    ghci> ones = 1 : ones\\
    ghci> reverse ones\\
    ...
    }
  \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}
In Agda every function has to be total and terminating, so how do we model partial functions?

\begin{itemize}[<+->]
  \item Simple errors can be modelled with the maybe monad
  \begin{lstlisting}[linewidth=14cm, language=myagda]
data Maybe (A : Set) : Set where
  just : A $\rightarrow$ Maybe A
  nothing : Maybe A
\end{lstlisting}

  for head we can then do:

  \begin{lstlisting}[linewidth=14cm, language=myagda]
head : $\forall$ A $\rightarrow$ List A $\rightarrow$ Maybe A
head nil = nothing
head (cons x xs) = just x
\end{lstlisting}

  \item What about \lstinline|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]
data Delay (A : Set) : Set where
  now : A $\rightarrow$ Delay A
  later : $\infty$ (Delay A) $\rightarrow$ Delay A
\end{lstlisting}
    \item The delay datatype contains a constant for non-termination:
    \begin{lstlisting}[linewidth=20cm, language=myagda]
never : Delay A
never = later ($\sharp$ never)
\end{lstlisting}
    \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
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}
  \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))

reverse : $\forall$ {A : Set} $\rightarrow$ Colist A $\rightarrow$ 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}
\end{frame}