\section{Partiality in Type Theory}

\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}
\begin{itemize}[<+->]
  \item In Agda every function has to be total and terminating, so how do we model partial functions?

  \item Simple errors can be modelled with the maybe monad
  \begin{multicols}{2}
    \begin{minted}{agda}
      data Maybe (A : Set) : Set where
        just    : A → Maybe A
        nothing : Maybe A
    \end{minted}
    \columnbreak
    \begin{minted}{agda}
      head : ∀ A → List A → Maybe A
      head nil         = nothing
      head (cons x xs) = just x
    \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}
  
\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. 
    \vskip 0.5cm
    \begin{minted}{agda}
      data Delay (A : Set) : Set where
        now : A → Delay A
        later : ∞ (Delay A) → Delay A
    \end{minted}
    \vskip 0.5cm
    \item The delay datatype contains a constant for non-termination:
    \vskip 0.5cm
    \begin{minted}{agda}
      never : Delay A
      never = later (♯ never)
    \end{minted}
    \vskip 0.5cm
    \item and we can define a function for \textit{running} a computation (for some amount of steps):
    \vskip 0.5cm
    \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}[t, fragile]{Partiality in Agda}{Capretta's Delay Monad}

\begin{itemize}
  \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 []
      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{itemize}
\end{frame}