bsc-leon-vatthauer/slides/sections/00_intro.tex

\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}
      \mycallout<2->{22, 1.5}{
        ghci> head []\\
        *** Exception: empty list\\
        CallStack (from HasCallStack):\\
        error, called at example.hs:2:9 in main:Main
      }
    \item<3->
    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}
    
    \mycallout<4->{22, 2}{
    ghci> ones = 1 : ones\\
    ghci> reverse ones\\
    ...
    }
  \end{itemize}

\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{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}

  \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{minted}{agda}
data Delay (A : Set) : Set where
  now : A → Delay A
  later : ∞ (Delay A) → Delay A
\end{minted}
    \item The delay datatype contains a constant for non-termination:
    \begin{minted}{agda}
never : Delay A
never = later (♯ never)
\end{minted}
    \item and we can define a function for \textit{running} a computation (for some amount of steps):

    \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}
  \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}
\end{frame}