mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
103 lines
No EOL
2.8 KiB
TeX
103 lines
No EOL
2.8 KiB
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} |