styling

slides/code-examples/example.hs

@@ -4,3 +4,9 @@ hd (x : _) = x
 
 main :: IO ()
 main = print (hd []::[String])
+
+reverse :: [a] -> [a]
+reverse l = rev l []
+  where
+    rev []     a = a
+    rev (x:xs) a = rev xs (x:a)

slides/main.tex

@@ -140,6 +140,95 @@ Leon Vatthauer%\inst{1}
 \usepackage{MnSymbol} % for \squaredots
 \usepackage{listings}
 \lstset{mathescape}
+
+\usepackage{xcolor}
+
+\definecolor{codegray}{rgb}{0.5,0.5,0.5}
+\definecolor{string}{HTML}{79731B}
+\definecolor{keyword}{HTML}{447A59}
+\definecolor{background}{HTML}{E6E6E6}
+\definecolor{error}{HTML}{9B0511}
+\definecolor{agda-name}{HTML}{3b31f9}
+\definecolor{agda-keyword}{HTML}{fc970a}
+\definecolor{agda-constructor}{HTML}{08aa20}
+
+
+\lstdefinestyle{mystyle}{
+    backgroundcolor=\color{background},
+    % commentstyle=\color{codegreen},
+    % keywordstyle=\color{keyword},
+    numberstyle=\tiny\color{codegray},
+    stringstyle=\color{string},
+    basicstyle=\ttfamily\small,
+    breakatwhitespace=false,         
+    breaklines=true,                 
+    captionpos=b,                    
+    keepspaces=true,                 
+    numbers=left,                    
+    numbersep=5pt,                  
+    showspaces=false,                
+    showstringspaces=false,
+    showtabs=false,                  
+    tabsize=2
+}
+\lstdefinelanguage{myhaskell}{
+	keywords=[1]{
+		where
+	},
+	keywordstyle=[1]\color{agda-keyword},
+	keywords=[2]{
+		error
+	},
+	keywordstyle=[2]\color{error},
+	keywords=[3]{
+		head, reverse, rev
+	},
+	keywordstyle=[3]\color{agda-name},
+	morestring=[b]"
+}
+
+\lstdefinelanguage{myagda}{
+	keywords=[1]{
+		data, where
+	},
+	keywordstyle=[1]\color{agda-keyword},
+	keywords=[2]{
+		Delay, Set, foldl, Colist, reverse, reverseAcc, run_for_steps, run, for, steps, fin-colist, inf-colist, never, head, List, Maybe
+	},
+	keywordstyle=[2]\color{agda-name},
+	keywords=[3]{
+		now, later, zero, suc, just, nothing, nil, cons
+	},
+	keywordstyle=[3]\color{agda-constructor}
+}
+
+\lstset{style=mystyle}
+
+\usepackage{lmodern}
+
+\usepackage{tikz}
+\usetikzlibrary{shapes.callouts}
+
+\usepackage{xparse}
+
+\tikzset{
+    invisible/.style={opacity=0,text opacity=0},
+    visible on/.style={alt=#1{}{invisible}},
+    alt/.code args={<#1>#2#3}{%
+      \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path
+    },
+}
+
+\NewDocumentCommand{\mycallout}{r<> O{opacity=0.8,text opacity=1} m m}{%
+\tikz[remember picture, overlay]\node[align=left, fill=red!50, text width=15cm,
+#2,visible on=<#1>, rounded corners,
+draw,rectangle]
+at (#3) {#4};
+}
+
+\newcommand{\tikzmark}[1]{\tikz[overlay,remember picture,baseline=-0.5ex] \node (#1) {};}
+
+
 \begin{document}
 % Title page
 \begin{frame}[t,titleimage]{-}

slides/sections/00_intro.tex

@@ -1,72 +1,88 @@
 \begin{frame}[t, fragile]{Partiality in Haskell}{}
-Haskell allows users to define arbitrary partial functions, some can be spotted easily by their definition:
-\begin{lstlisting}[language=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}
-
-% TODO right of this add error bubble that shows what happens for `head []`
-
-others might be more subtle:
-
-\begin{lstlisting}[language=haskell]
+      \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{lstlisting}
+\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:
+  for head we can then do:
 
-\begin{lstlisting}
+  \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}
 
-But what about \lstinline|reverse|?
+  \item What about \lstinline|reverse|?
+\end{itemize}
 \end{frame}
 
 \begin{frame}[t, fragile]{Partiality in Agda}{Capretta's Delay Monad}
-Capretta's Delay Monad is a coinductive data type whose inhabitants can be viewed as suspended computations. 
-\begin{lstlisting}
+  \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}
-\lstinline|now| lifts a computation, while \lstinline|later| delays it by one time unit.
-
-The delay datatype contains a constant for non-termination:
-\begin{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):
 
-and we can define a function for \textit{running} a computation (for some amount of steps):
-
-\begin{lstlisting}
+    \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}[t, fragile]{Partiality in Agda}{Reversing (possibly infinite) lists}
-\begin{lstlisting}
+\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))
@@ -75,6 +91,6 @@ reverse : $\forall$ {A : Set} $\rightarrow$ Colist A $\rightarrow$ Delay (Colist
 reverse {A} = reverseAcc []
   where
     reverseAcc : Colist A $\rightarrow$ Colist A $\rightarrow$ Delay (Colist A)
-    reverseAcc = foldl ($\lambda$ xs x $\rightarrow$ x $\squaredots$ ($\sharp$ xs)) -- 'flip _$\squaredots$_' with extra steps
+    reverseAcc = foldl ($\lambda$ xs x $\rightarrow$ x $\squaredots$ ($\sharp$ xs))
 \end{lstlisting}
 \end{frame}