parametricity.tex

\begin{frame}[fragile]
\frametitle{Consider the following Java function \ldots}
\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?

i.e. from the type, how much knowledge have we gained?
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{What about this Java function \ldots}
\begin{block}{}
\begin{lstlisting}[style=java]
String string2string(String s) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{center}
from the type, how much knowledge have we gained?
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{OK now this Java function \ldots}
\begin{block}{}
\begin{lstlisting}[style=java]
<A> A any2any(A a) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{center}
How many possible programs can be written that satisfy the type?
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{Polymorphic values}
\begin{block}{By utilising \emph{polymorphic} values in a type \ldots}
\begin{center}
we have gained a \textbf{lot} of knowledge of our function's behaviour

In this case, we have obtained \emph{total} knowledge
\end{center}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Polymorphic values}
\begin{block}{Parametricity}
\begin{center}
This idea of using parametric polymorphism to determine a function's behaviour is called \emph{parametricity}
\end{center}
\end{block}
\end{frame}

\begin{frame}
\frametitle{What is Parametricity and Free Theorems}
\begin{block}{Philip Wadler \cite{wadler1989theorems} tells us:}
\begin{quotation}
Write down the definition of a polymorphic function on a piece of paper. Tell me its type, but be careful not to let me see the function's definition. I will tell you a theorem that the function satisfies.

The purpose of this paper is to explain the trick.
\end{quotation}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Try this Java function \ldots}
\begin{block}{}
\begin{lstlisting}[style=java]
List<String> strings2strings(List<String> s) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{center}
from the type, how much knowledge have we gained?
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{Polymorphic values}
\begin{block}{This type has no polymorphic values}
\begin{lstlisting}[style=java]
List<String> strings2strings(List<String> x) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Polymorphic values}
\begin{block}{Can we determine function behaviour?}
\begin{lstlisting}[style=java]
<T> List<T> anythings2anythings(List<T> x) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{block}{Theorem}
\textbf{every element in the resulting list, appears in the input list}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Polymorphic values}
\begin{block}{Some amount of function behaviour}
\begin{lstlisting}[style=java]
<T> List<T> anythings2anythings(List<T> x) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{block}{Theorem}
We have \textbf{some} amount of information, but not \textbf{total} information

Let's write an \emph{automated} test
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Polymorphic values and tests}
\begin{block}{Can we determine function behaviour?}
\begin{lstlisting}[style=java]
<T> List<T> anythings2anythings(List<T> x) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{block}{Tests}
\begin{lstlisting}[style=haskell]
prop_anythings2anythings1 :: Property
prop_anythings2anythings1 =
  property $ do
    x <- forAll alpha
    anythings2anythings [x] == [x]
\end{lstlisting}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Polymorphic values and tests}
\begin{block}{Can we determine function behaviour?}
\begin{lstlisting}[style=java]
<T> List<T> anythings2anythings(List<T> x) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{block}{Tests}
\begin{lstlisting}[style=haskell]
prop_anythings2anythings2 :: Property
prop_anythings2anythings2 =
  property $ do
    x <- forAll (list (linear 0 100) alpha)
    y <- forAll (list (linear 0 100) alpha)
    anythings2anythings (x ++ y) ==
      anythings2anythings y ++ anythings2anythings x
\end{lstlisting}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Types and tests}
\begin{block}{By this method, it becomes very explicit that \ldots}
\begin{itemize}
\item Types alone provide a \emph{proof} of a proposition
\item Polymorphic types provide \emph{additional theorems}
      
      i.e. free theorems
\item Tests provide a \emph{failed negative proof} of a proposition
\item This outcome is the \emph{only} difference between types and tests
\end{itemize}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Once-inhabitance}
\begin{block}{}
\begin{lstlisting}[style=haskell]
<T> T anything2anything(T x) {
  // hidden from view 
}
\end{lstlisting}
\end{block}
\begin{center}
This type is an example of \emph{once-inhabitance}

There is only one function with this type

\textbf{It is not possible to write tests for it \textemdash tests are redundant}
\end{center}
\end{frame}



\begin{frame}[fragile]
\frametitle{Types and tests}
\begin{block}{But these are trivial examples}
What about more realistic examples?
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Types and tests}
\begin{block}{}
\begin{lstlisting}[style=haskell]
-- the type implies this function does no I/O
validateWebForm ::
  f WebForm
  -> f (Either WebFormErrors ValidatedWebForm)

-- this function may do I/O
submitWebForm ::
  AppState
  -> WebForm
  -> IO (Response, AppState)
\end{lstlisting}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Types and tests}
\begin{block}{}
\begin{lstlisting}[style=haskell]
-- idempotence
prop_submitWebForm :: Property
prop_submitWebForm =
  property $ do
    w       <- forAll genWebForm
    s       <- forAll genAppState
    (_, s1) <- submitWebForm s (submitWebForm s w)
    (_, s2) <- submitWebForm s w
    s1 == s2
\end{lstlisting}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Types and tests}
\begin{block}{Types and tests \ldots}
\begin{itemize}
\item We use types \textbf{first}
\item Where types fall short, we use \textbf{automated tests}
\item Tests are written using the hedgehog\footnote{\tiny{hedgehog} \href{https://hackage.haskell.org/package/hedgehog}{\beamergotobutton{Link}}} library
\item Tests are deterministic

``works on my machine today''

$\rightarrow$

``works on all machines at all times''
\end{itemize}
\end{block}
\end{frame}