algebra.tex

\begin{frame}[fragile]
\frametitle{Algebra}
\begin{block}{}
\begin{lstlisting}[style=java]
boolean boolean2boolean(boolean b) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{center}
How many possible programs can be written that satisfy the type?

We can calculate this \emph{algebraically}
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{Counting inhabitants}
\begin{block}{}
\begin{lstlisting}[style=java]
boolean boolean2boolean(boolean b) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{center}
The inhabitants of a function's type \ldots

is the return type raised to the power of its argument type
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{Counting inhabitants}
\begin{block}{}
\begin{lstlisting}[style=java]
boolean boolean2boolean(boolean b) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{block}{}
\lstinline{boolean} \textsuperscript{\lstinline{boolean}}

\lstinline{= 4}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Counting inhabitants}
\begin{block}{}
\begin{lstlisting}[style=java]
boolean boolean2boolean(boolean b) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{block}{Here are all the possible functions}
\begin{lstlisting}[style=java]
return true;  // 1
return false; // 2
return b;     // 3
return !b;    // 4
\end{lstlisting}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Counting inhabitants}
\begin{block}{What about this one?}
\begin{lstlisting}[style=java]
<A> A anything2anything(A a) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Counting inhabitants}
\begin{block}{What about this one?}
\begin{lstlisting}[style=java]
<A> A anything2anything(A a) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{center}
\begin{itemize}
\item<1-> Assume \lstinline{= 1}
\item<1-> Prove \lstinline{= 1} using \emph{the yoneda lemma}
\item<2-> \ldots using Java \ldots
\item<2-> you know, for giggles
\end{itemize}
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{Proof}
\begin{block}{Yoneda Lemma}
\begin{center}
\href{https://github.com/simple-machines/types-and-tests/blob/master/source/yoneda.java}{https://github.com/simple-machines/types-and-tests/blob/master/source/yoneda.java}
\end{center}
\end{block}
\end{frame}