parametricity-meetup-talk.tex

%% LyX 2.3.3 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[english]{beamer}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
\usepackage{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{wasysym}
\usepackage[all]{xy}
\ifx\hypersetup\undefined
  \AtBeginDocument{%
    \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
  }
\else
  \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
\fi

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
% this default might be overridden by plain title style
\newcommand\makebeamertitle{\frame{\maketitle}}%
% (ERT) argument for the TOC
\AtBeginDocument{%
  \let\origtableofcontents=\tableofcontents
  \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
  \def\gobbletableofcontents#1{\origtableofcontents}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Parametricity properties]{Parametricity properties of purely functional code}
\subtitle{``Theorems for free'' demystified. A tutorial, with code examples in Scala}
\author{Sergei Winitzki}
\date{2020-03-24}
\institute[SFTTPL]{San Francisco Types, Theorems, and Programming Languages}
\setbeamertemplate{headline}{} % disable headline at top
\setbeamertemplate{navigation symbols}{} % disable navigation bar at bottom
\usepackage[all]{xy} % xypic
%\makeatletter
% Macros to assist LyX with XYpic when using scaling.
\newcommand{\xyScaleX}[1]{%
\makeatletter
\xydef@\xymatrixcolsep@{#1}
\makeatother
} % end of \xyScaleX
\makeatletter
\newcommand{\xyScaleY}[1]{%
\makeatletter
\xydef@\xymatrixrowsep@{#1}
\makeatother
} % end of \xyScaleY

% Double-stroked fonts to replace the non-working \mathbb{1}.
\usepackage{bbold}
\DeclareMathAlphabet{\bbnumcustom}{U}{BOONDOX-ds}{m}{n} % Use BOONDOX-ds or bbold.
\newcommand{\custombb}[1]{\bbnumcustom{#1}}
% The LyX document will define a macro \bbnum{#1} that calls \custombb{#1}.

\usepackage{relsize} % make math symbols larger or smaller
\usepackage{stmaryrd} % some extra symbols such as \fatsemi
% Note: using \forwardcompose inside a \text{} will cause a LaTeX error!
\newcommand{\forwardcompose}{\hspace{1.5pt}\ensuremath\mathsmaller{\fatsemi}\hspace{1.5pt}}


% Make underline green.
\definecolor{greenunder}{rgb}{0.1,0.6,0.2}
%\newcommand{\munderline}[1]{{\color{greenunder}\underline{{\color{black}#1}}\color{black}}}
\def\mathunderline#1#2{\color{#1}\underline{{\color{black}#2}}\color{black}}
% The LyX document will define a macro \gunderline{#1} that will use \mathunderline with the color `greenunder`.
%\def\gunderline#1{\mathunderline{greenunder}{#1}} % This is now defined by LyX itself with GUI support.

% Scala syntax highlighting. See https://tex.stackexchange.com/questions/202479/unable-to-define-scala-language-with-listings
%\usepackage[T1]{fontenc}
%\usepackage[utf8]{inputenc}
%\usepackage{beramono}
%\usepackage{listings}
% The listing settings are now supported by LyX in a separate section "Listings".
\usepackage{xcolor}

\definecolor{scalakeyword}{rgb}{0.16,0.07,0.5}
\definecolor{dkgreen}{rgb}{0,0.6,0}
\definecolor{gray}{rgb}{0.5,0.5,0.5}
\definecolor{mauve}{rgb}{0.58,0,0.82}
\definecolor{aqua}{rgb}{0.9,0.96,0.999}
\definecolor{scalatype}{rgb}{0.2,0.3,0.2}

\makeatother

\usepackage{listings}
\lstset{language=Scala,
morekeywords={{scala}},
otherkeywords={=,=>,<-,<\%,<:,>:,\#,@,:,[,],.,???},
keywordstyle={\color{scalakeyword}},
morekeywords={[2]{String,Short,Int,Long,Char,Boolean,Double,Float,BigDecimal,Seq,Map,Set,List,Option,Either,Future,Vector,Range,IndexedSeq,Try,true,false,None,Some,Left,Right,Nothing,Any,Array,Unit,Iterator,Stream}},
keywordstyle={[2]{\color{scalatype}}},
frame=tb,
aboveskip={1.5mm},
belowskip={0.5mm},
showstringspaces=false,
columns=fullflexible,
keepspaces=true,
basicstyle={\smaller\ttfamily},
extendedchars=true,
numbers=none,
numberstyle={\tiny\color{gray}},
commentstyle={\color{dkgreen}},
stringstyle={\color{mauve}},
frame=single,
framerule={0.0mm},
breaklines=true,
breakatwhitespace=true,
tabsize=3,
framexleftmargin={0.5mm},
framexrightmargin={0.5mm},
xleftmargin={1.5mm},
xrightmargin={1.5mm},
framextopmargin={0.5mm},
framexbottommargin={0.5mm},
fillcolor={\color{aqua}},
rulecolor={\color{aqua}},
rulesepcolor={\color{aqua}},
backgroundcolor={\color{aqua}},
mathescape=false,
extendedchars=true}
\renewcommand{\lstlistingname}{Listing}

\begin{document}
\global\long\def\gunderline#1{\mathunderline{greenunder}{#1}}%
\global\long\def\bef{\forwardcompose}%
\global\long\def\bbnum#1{\custombb{#1}}%
\frame{\titlepage}
\begin{frame}{Refactoring code by permuting the order of operations}
\begin{itemize}
\item \vspace{-0.15cm}Expected properties of refactored code: \\
~
\end{itemize}
First extract user information, then convert stream to list; or first
convert to list, then extract user information:

\texttt{\textcolor{blue}{\footnotesize{}db.getRows.toList.map(getUserInfo)}}
gives the same result as\\
\texttt{\textcolor{blue}{\footnotesize{}db.getRows.map(getUserInfo).toList}}~\\
\texttt{\textcolor{blue}{\footnotesize{}~}}{\footnotesize\par}

First extract user information, then exclude invalid rows; or first
exclude invalid rows, then extract user information:

\texttt{\textcolor{blue}{\footnotesize{}db.getRows.map(getUserInfo).filter(isValid)}}
gives the same result as \\
\texttt{\textcolor{blue}{\footnotesize{}db.getRows.filter(getUserInfo
andThen isValid).map(getUserInfo)}}~\\
\texttt{\textcolor{blue}{\footnotesize{}~}}{\footnotesize\par}
\begin{itemize}
\item These refactorings are guaranteed to be correct
\end{itemize}
\end{frame}

\begin{frame}{Summary of the type notation}

The short type notation helps in symbolic reasoning about types
\noindent \begin{center}
\begin{tabular}{|c|c|c|}
\hline 
\textbf{\small{}Description} & \textbf{\small{}Scala examples} & \textbf{\small{}Notation}\tabularnewline
\hline 
\hline 
{\footnotesize{}Typed value} & {\footnotesize{}}\lstinline!x: Int! & {\footnotesize{}$x^{:\text{Int}}$ or $x:\text{Int}$}\tabularnewline
\hline 
{\footnotesize{}Unit type} & {\footnotesize{}}\lstinline!Unit!{\footnotesize{}, }\lstinline!Nil!{\footnotesize{},
}\lstinline!None! & {\footnotesize{}$\bbnum 1$}\tabularnewline
\hline 
{\footnotesize{}Type parameter} & {\footnotesize{}}\lstinline!A! & {\footnotesize{}$A$}\tabularnewline
\hline 
{\footnotesize{}Product type} & {\footnotesize{}}\lstinline!(A, B)!{\footnotesize{} or }\lstinline!case class P(x: A, y: B)! & {\footnotesize{}$A\times B$}\tabularnewline
\hline 
{\footnotesize{}Co-product type} & {\footnotesize{}}\lstinline!Either[A, B]! & {\footnotesize{}$A+B$}\tabularnewline
\hline 
{\footnotesize{}Function type} & {\footnotesize{}}\lstinline!A => B! & {\footnotesize{}$A\rightarrow B$}\tabularnewline
\hline 
{\footnotesize{}Type constructor} & {\footnotesize{}}\lstinline!List[A]! & {\footnotesize{}$\text{List}^{A}$}\tabularnewline
\hline 
{\footnotesize{}Universal quantifier} & {\footnotesize{}}\lstinline!trait P \{ def f[A]: Q[A] \}! & {\footnotesize{}$P\triangleq\forall A.\,Q^{A}$}\tabularnewline
\hline 
{\footnotesize{}Existential quantifier} & {\footnotesize{}}%
\begin{minipage}[t]{0.43\paperwidth}%
{\footnotesize{}}\lstinline!sealed trait P[A]!{\footnotesize\par}

{\footnotesize{}}\lstinline!case class Q[A, B]() extends P[A]!{\footnotesize{}\vspace{0.2\baselineskip}
}{\footnotesize\par}%
\end{minipage} & {\footnotesize{}$P^{A}\triangleq\exists B.\,Q^{A,B}$}\tabularnewline
\hline 
\end{tabular}
\par\end{center}

Example: Scala code \lstinline!def flm(f: A => Option[B]): Option[A] => Option[B]!
is denoted by $\text{flm}:(A\rightarrow\bbnum 1+B)\rightarrow\bbnum 1+A\rightarrow\bbnum 1+B$
\end{frame}

\begin{frame}{Summary of the code notation}

The short code notation helps in symbolic reasoning about code
\noindent \begin{center}
\begin{tabular}{|c|c|}
\hline 
\textbf{\small{}Scala examples} & \textbf{\small{}Notation}\tabularnewline
\hline 
\hline 
{\small{}}\lstinline!()!{\small{} or }\lstinline!true!{\small{}
or }\lstinline!"abc"!{\small{} or }\lstinline!123! & {\small{}$1$, $\text{true}$, $\text{"abc"}$, $123$}\tabularnewline
\hline 
{\small{}}\lstinline!def f[A](x: A) = ...! & {\small{}$f^{A}(x^{:A})\triangleq...$}\tabularnewline
\hline 
{\small{}}\lstinline!\{ (x: A) => expr \}! & {\small{}$x^{:A}\rightarrow\text{expr}$}\tabularnewline
\hline 
{\small{}}\lstinline!f(x)!{\small{} or }\lstinline!x.pipe(f)!{\small{}
(Scala 2.13)} & {\small{}$f(x)$ or $x\triangleright f$}\tabularnewline
\hline 
{\small{}}\lstinline!val p: (A, B) = (a, b)! & {\small{}$p^{:A\times B}\triangleq a\times b$}\tabularnewline
\hline 
{\small{}}\lstinline!\{case (a, b) => expr\}!{\small{} or }\lstinline!p._1!{\small{}
or }\lstinline!p._2! & {\small{}$a\times b\rightarrow\text{expr}$ ~or~ $p\triangleright\pi_{1}$~or~
$p\triangleright\pi_{2}$}\tabularnewline
\hline 
{\small{}}\lstinline!Left[A, B](x)!{\small{} or }\lstinline!Right[A, B](y)! & {\small{}$x^{:A}+\bbnum 0^{:B}$ or $\bbnum 0^{:A}+y^{:B}$}\tabularnewline
\hline 
{\small{}\hspace*{-0.013\linewidth}}%
\begin{minipage}[c][1\totalheight][b]{0.5\columnwidth}%
{\small{}\vspace{0.14\baselineskip}
}{\footnotesize{}}\lstinline!val q: C = (p: Either[A, B]) match \{!{\footnotesize\par}

{\footnotesize{}~ ~}\lstinline!case Left(x)   => f(x)!{\footnotesize\par}

{\footnotesize{}~ ~}\lstinline!case Right(y)  => g(y)!{\footnotesize\par}

{\footnotesize{}}\lstinline!\}!{\small{}\vspace{0.2\baselineskip}
}{\small\par}%
\end{minipage}{\small{} \hspace*{-0.009\linewidth}} & {\small{}$q^{:C}\triangleq p^{:A+B}\triangleright\begin{array}{|c||c|}
 & C\\
\hline A & x^{:A}\rightarrow f(x)\\
B & y^{:B}\rightarrow g(y)
\end{array}$}\tabularnewline
\hline 
{\small{}}\lstinline!def f(x) = \{ ... f(y) ... \}! & {\small{}}%
\begin{minipage}[t]{0.3\columnwidth}%
\begin{center}
{\small{}\vspace{-0.64\baselineskip}
$f(x)\triangleq...~\overline{f}(y)~...$\vspace{0.15\baselineskip}
}
\par\end{center}%
\end{minipage}\tabularnewline
\hline 
{\small{}}\lstinline!f andThen g!{\small{} and }\lstinline!(f andThen g)(x)! & {\small{}$f\bef g$ and $x\triangleright f\bef g$~or~ $x\triangleright f\triangleright g$}\tabularnewline
\hline 
{\small{}}\lstinline!p.map(f).map(g)! & {\small{}$p\triangleright f^{\uparrow F}\triangleright g^{\uparrow F}$~or~
$p\triangleright f^{\uparrow F}\bef g^{\uparrow F}$}\tabularnewline
\hline 
\end{tabular}
\par\end{center}

\end{frame}

\begin{frame}{Refactored code: further examples}

Writing the previous examples as equations:

\vspace{0.3cm}\lstinline!def toList[A]: Stream[A] => List[A]! written
as {\small{}$\text{toList}^{A}:\text{Str}^{A}\rightarrow\text{List}^{A}$}{\small\par}

\vspace{-0.3cm}%
\begin{minipage}[c][1\totalheight][t]{0.26\columnwidth}%
\[
\xymatrix{\text{Str}^{A}\ar[r]\sp(0.55){\text{toList}^{A}}\ar[d]\sp(0.4){f^{\uparrow\text{Str}}} & \text{List}^{A}\ar[d]\sp(0.4){f^{\uparrow\text{List}}}\\
\xyScaleY{1.6pc}\xyScaleX{3.0pc}\text{Str}^{B}\ar[r]\sp(0.55){\text{toList}^{B}} & \text{List}^{B}
}
\]
%
\end{minipage}\hfill{}%
\begin{minipage}[c][1\totalheight][t]{0.68\columnwidth}%
\begin{center}
~\\
~\\
\lstinline!_.toList.map(f) == _.map(f).toList!{\small{}
\[
(f^{:A\rightarrow B})^{\uparrow\text{Str}}\bef\text{toList}^{B}=\text{toList}^{A}\bef f^{\uparrow\text{List}}
\]
}
\par\end{center}%
\end{minipage}

\vspace{0.3cm}\lstinline!def filt[A]: (A => Boolean) => Stream[A] => Stream[A]!

\vspace{-0.3cm}%
\begin{minipage}[c][1\totalheight][t]{0.26\columnwidth}%
\[
\xymatrix{\text{Str}^{A}\ar[r]\sp(0.55){\text{filt}^{A}(f\bef p)}\ar[d]\sp(0.4){f^{\uparrow\text{Str}}} & \text{Str}^{A}\ar[d]\sp(0.4){f^{\uparrow\text{Str}}}\\
\xyScaleY{1.6pc}\xyScaleX{3.0pc}\text{Str}^{B}\ar[r]\sp(0.55){\text{filt}^{B}(p)} & \text{Str}^{B}
}
\]
%
\end{minipage}\hfill{}%
\begin{minipage}[c][1\totalheight][t]{0.68\columnwidth}%
\begin{center}
{\small{}
\begin{align*}
 & \text{filt}^{A}:(A\rightarrow\bbnum 2)\rightarrow\text{Str}^{A}\rightarrow\text{Str}^{A}\\
 & (f^{:A\rightarrow B})^{\uparrow\text{Str}}\bef\text{filt}^{B}(p^{:B\rightarrow\bbnum 2})=\text{filt}^{A}(f\bef p)\bef f^{\uparrow\text{Str}}
\end{align*}
}
\par\end{center}%
\end{minipage}
\begin{itemize}
\item \vspace{0.3cm}A transformation before \lstinline!map! equals a transformation
after \lstinline!map!
\item This is called a \textbf{naturality law}
\item We expect it to hold if the code works the same way for all types
\end{itemize}
\end{frame}

\begin{frame}{Naturality laws: equations}

\vspace{-0.1cm}\textbf{Naturality law} for a function $t$ is an
equation involving an arbitrary function $f$ that permutes the order
of application of $t$ and of a lifted $f$

\vspace{-0.4cm}%
\begin{minipage}[c][1\totalheight][t]{0.26\columnwidth}%
\[
\xymatrix{\text{List}^{A}\ar[r]\sp(0.55){\text{headOpt}^{A}}\ar[d]\sp(0.4){f^{\uparrow\text{List}}} & \text{Opt}^{A}\ar[d]\sb(0.4){f^{\uparrow\text{Opt}}}\\
\xyScaleY{1.6pc}\xyScaleX{3.0pc}\text{List}^{B}\ar[r]\sp(0.55){\text{headOpt}^{B}} & \text{Opt}^{B}
}
\]
%
\end{minipage}\hfill{}%
\begin{minipage}[c][1\totalheight][b]{0.68\columnwidth}%
\begin{center}
\lstinline!list.map(f).headOption == list.headOption.map(f)!
\[
(f^{:A\rightarrow B})^{\uparrow\text{List}}\bef\text{headOpt}=\text{headOpt}\bef(f^{:A\rightarrow B})^{\uparrow\text{Opt}}
\]
\par\end{center}%
\end{minipage}
\begin{itemize}
\item Lifting $f$ before $t$ equals to lifting $f$ after $t$
\item Intuition: $t$ rearranges data in a collection, not looking at values
\end{itemize}
Further examples: 
\begin{itemize}
\item Reversing a list; $\text{reverse}^{A}:\text{List}^{A}\rightarrow\text{List}^{A}$
\end{itemize}
\begin{center}
\lstinline!list.map(f).reverse == list.reverse.map(f)!{\footnotesize{}
\[
(f^{:A\rightarrow B})^{\uparrow\text{List}}\bef\text{reverse}^{B}=\text{reverse}^{A}\bef(f^{:A\rightarrow B})^{\uparrow\text{List}}
\]
}{\footnotesize\par}
\par\end{center}
\begin{itemize}
\item The \lstinline!pure! method, \lstinline!pure[A]: A => L[A]!. Notation:
$\text{pu}_{L}:A\rightarrow L^{A}$
\end{itemize}
\begin{center}
\lstinline!pure(x).map(f) == pure(f(x))!{\footnotesize{}
\[
\text{pu}^{A}\bef(f^{:A\rightarrow B})^{\uparrow L}=f\bef\text{pu}^{B}
\]
}{\footnotesize\par}
\par\end{center}

\end{frame}

\begin{frame}{Reasoning with naturality: Simplifying the \lstinline!pure! method}

The naturality law of \lstinline!pure! for a functor $L$:

\vspace{-0.4cm}%
\begin{minipage}[c][1\totalheight][t]{0.26\columnwidth}%
\[
\xymatrix{A\ar[r]\sp(0.55){\text{pu}_{L}}\ar[d]\sp(0.4){f} & L^{A}\ar[d]\sp(0.4){f^{\uparrow L}}\\
\xyScaleY{1.6pc}\xyScaleX{3.0pc}B\ar[r]\sp(0.55){\text{pu}_{L}} & L^{B}
}
\]
%
\end{minipage}\hfill{}%
\begin{minipage}[c][1\totalheight][b]{0.68\columnwidth}%
\begin{center}
\lstinline!pure(a).map(f) == pure(f(a))!
\[
\text{pu}_{L}\bef f^{\uparrow L}=f\bef\text{pu}_{L}
\]
\par\end{center}%
\end{minipage}

\vspace{0.4cm}Fix a value $b^{:B}$ and set $A=\bbnum 1$ and $f\triangleq1\rightarrow b$
in the naturality law:

\vspace{-0.4cm}%
\begin{minipage}[c][1\totalheight][t]{0.26\columnwidth}%
\[
\xymatrix{\bbnum 1\ar[r]\sp(0.55){\text{pu}_{L}}\ar[d]\sp(0.4){1\rightarrow b} & L^{\bbnum 1}\ar[d]\sp(0.4){(1\rightarrow b)^{\uparrow L}}\\
\xyScaleY{1.6pc}\xyScaleX{3.0pc}B\ar[r]\sp(0.55){\text{pu}_{L}} & L^{B}
}
\]
%
\end{minipage}\hfill{}%
\begin{minipage}[c][1\totalheight][b]{0.68\columnwidth}%
\begin{center}
\lstinline!pure(()).map(_ => b) == pure(b)!
\[
\text{pu}_{L}\bef(1\rightarrow b)^{\uparrow L}=(1\rightarrow b)\bef\text{pu}_{L}
\]
\par\end{center}%
\end{minipage}

\vspace{0.4cm}We have expressed \lstinline!pure(b)! via a constant
value \lstinline!pure(())! of type \lstinline!L[Unit]!

The naturality law of \lstinline!pure! makes it equivalent to a ``wrapped
unit'' value

This simplifies the definition of a \lstinline!Pointed! typeclass:

\lstinline!abstract class Pointed[L[_]: Functor] \{ def wu: L[Unit] \}!

Examples: for \lstinline!Option!, \lstinline!wu = Some(())!. For
\lstinline!List!, \lstinline!wu = List(())!
\end{frame}

\begin{frame}{Naturality laws in typeclasses}

Another use of naturality laws is when implementing typeclasses
\begin{itemize}
\item Typeclasses require type constructors with methods \lstinline!map!,
\lstinline!filter!, \lstinline!fold!, \lstinline!flatMap!, \lstinline!pure!,
and others
\end{itemize}
To be useful for programming, the methods must satisfy certain laws
\begin{itemize}
\item \lstinline!map!: identity, composition
\item \lstinline!filter!: identity, composition, partial function, naturality
\item \lstinline!fold! (traverse): identity, composition, naturality
\item \lstinline!flatMap!: identity, associativity, naturality
\item \lstinline!pure!: naturality
\end{itemize}
We need to check the laws when implementing new typeclass instances

Usually, typeclass instances are written in fully parametric code
\end{frame}

\begin{frame}{Fully parametric code: example}

\textbf{Fully parametric} code: ``works in the same way for all types''
\begin{itemize}
\item Example of a fully parametric function:

\lstinline!def headOpt[A]: List[A] => Option[A] = \{!

~~\lstinline!case Nil => None!

~~\lstinline!case head :: tail => Some(head)!

\lstinline!\}!
\item The code does not use explicit types
\item The same code in the matrix notation:
\[
\text{headOpt}^{:\text{List}^{A}\rightarrow\bbnum 1+A}\triangleq\,\begin{array}{|c||cc|}
 & \bbnum 1 & A\\
\hline \bbnum 1 & \text{id} & \bbnum 0\\
A\times\text{List}^{A} & \bbnum 0 & h\times t\rightarrow h
\end{array}
\]
where $\text{List}^{A}\triangleq\bbnum 1+A\times\text{List}^{A}$
is a recursively defined type constructor: \lstinline!final case class List[A](x: Option[(A, List[A]])!
\end{itemize}
Naturality laws express the programmer's intuition about the properties
of fully parametric code
\end{frame}
~

Example of code that is \emph{not} fully parametric:
\begin{itemize}
\item An implementation of \lstinline!headOpt! that has special code for
\lstinline!Int! type
\end{itemize}
\begin{lstlisting}
def headOptBad[A]: List[A] => Option[A] = {
  case Nil                   => None
  case (head: Int) :: tail   => Some((head + 100).asInstanceOf[A])
  case head :: tail          => Some(head)
}
\end{lstlisting}
\vspace{-0\baselineskip}

\begin{itemize}
\item The code uses explicit run-time type detection
\end{itemize}
The function \lstinline!headOptBad! fails the naturality law:
\begin{lstlisting}
scala> headOptBad(List(1, 2, 3).map(x => s"value = $x"))
res0: Option[String] = Some(value = 1)

scala> headOptBad(List(1, 2, 3)).map(x => s"value = $x")
res1: Option[String] = Some(value = 101)
\end{lstlisting}
~

\begin{frame}{Full parametricity: The price we pay for ``free theorems''}

Free theorems only apply to \textbf{fully parametric} code:
\begin{itemize}
\item All argument types are combinations of type parameters
\item All type parameters are treated as unknown, arbitrary types
\item No hard-coded values of specific types (\lstinline!123: Int! or \lstinline!"abc": String!)
\item No side effects (printing, \lstinline!var x!, mutating values, writing
files, networking, starting or stopping new threads, GUI events, etc.)
\item No \lstinline!null!, no \lstinline!throw!ing of exceptions, no run-time
type comparison
\item No run-time code loading, no external libraries with unknown code
\end{itemize}
``Fully parametric'' is a stronger restriction than ``purely functional''
(referentially transparent)

Purely functional code is fully parametric if restricted to using
only \lstinline!Unit! type or type parameters
\begin{itemize}
\item No hard-coded values of specific types, and no run-time type detection
\end{itemize}
\end{frame}
\vspace{2\baselineskip}

Fully parametric programs are written using the 9 code constructions:
\begin{lstlisting}
def fmap[A, B](f: A => B): List[(A, A)] => List[(B, B)] = { // 3
   case Nil            => Nil
//   8   1                1,7 
   case head :: tail   => (f (head._1), f (head._2)) :: fmap(f)(tail)
//   8       6             2 4     6  5 2 4     6    7   9
}       // This code has used each of the nine allowed constructions.
\end{lstlisting}
\vspace{-0.2\baselineskip}

\begin{enumerate}
\item Use \lstinline!Unit! value (or a ``named \lstinline!Unit!''),
e.g.~\lstinline!()!, \lstinline!Nil!, or \lstinline!None!. Notation:
$1$
\item Use bound variable (a given argument of the function). Notation: $x$
\item Create function: \lstinline!{ x => expr(x) }!. Notation: $x\rightarrow\text{expr}\left(x\right)$
\item Use function: \lstinline!f(x)!. Notation: $f(x)$ or $x\triangleright f$
\item Create tuple: \lstinline!(a, b)!. Notation: $a\times b$
\item Use tuple: \lstinline!p._1!. Notation: $\nabla_{1}p$ or $p\triangleright\nabla_{1}$
\item Create disjunctive value: \lstinline!Left[A, B](x)!. Notation: $x^{:A}+\bbnum 0^{:B}$
\item Use disjunctive value: \lstinline!{ case ... }! (pattern-matching);
matrix code
\item Use recursive call: \lstinline!fmap(f)(tail)!. Notation: $\overline{\text{fmap}_{\text{List}}}(f)(t)$\vspace{0.2\baselineskip}
\end{enumerate}

\begin{frame}{Naturality laws and parametricity}

\begin{itemize}
\item The \textbf{parametricity theorem} guarantees that all naturality
laws hold as long as the method's code is fully parametric
\item This saves us time: \emph{no need} to check the naturality laws
\end{itemize}
Using the parametricity theorem is difficult
\begin{itemize}
\item The ``theorems for free'' (\href{https://people.mpi-sws.org/~dreyer/tor/papers/reynolds.pdf}{Reynolds};
\href{https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf}{Wadler})
approach needs to replace functions (one-to-one or many-to-one) by
``relations'' (many-to-many)
\begin{itemize}
\item Derive a law with relation variables, then replace them by functions
\end{itemize}
\item Alternative approach: analysis of dinatural transformations derives
the naturality laws directly (\href{https://www.sciencedirect.com/science/article/pii/0304397590901517}{Bainbridge et al.};
\href{https://www.researchgate.net/publication/262348393_On_a_Relation_on_Functions}{Backhouse};
\href{https://www.irif.fr/~delatail/dinat.pdf}{de Lataillade})
\begin{itemize}
\item See also a \href{https://arxiv.org/pdf/1908.07776}{2019 paper} by
Voigtländer
\end{itemize}
\item Plan:
\begin{itemize}
\item Start with natural transformations
\item Introduce profunctors and dinatural transformations
\item Commutativity laws for bifunctors and profunctors
\item Derive the naturality laws for dinatural transformations
\item Uniqueness of functor typeclass instances
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Natural transformations and their laws}

A \textbf{natural transformation} is a function $t$ with type signature
$F^{A}\rightarrow G^{A}$ that satisfies the naturality law $f^{\uparrow F}\bef t=t\bef f^{\uparrow G}$.
Notation $t:F\leadsto G$
\begin{itemize}
\item Many standard methods have the form of a natural transformation
\begin{itemize}
\item Examples: \lstinline!headOption!, \lstinline!lastOption!, \lstinline!reverse!,
\lstinline!swap!, \lstinline!map!, \lstinline!flatMap!, \lstinline!pure!
\end{itemize}
\item If there are several type parameters, use one at a time:
\begin{itemize}
\item For \lstinline!flatMap!, denote $\text{flm}:\left(A\rightarrow M^{B}\right)\rightarrow M^{A}\rightarrow M^{B}$,
fix $A$
\begin{itemize}
\item $\text{flm}:F^{B}\rightarrow G^{B}$ where $F^{B}\triangleq A\rightarrow M^{B}$
and $G^{B}\triangleq M^{A}\rightarrow M^{B}$
\end{itemize}
\item The naturality law $f^{\uparrow F}\bef\text{flm}=\text{flm}\bef f^{\uparrow G}$
then gives the equation
\[
\text{flm}\,(p^{:A\rightarrow M^{B}}\bef f^{\uparrow M})=\text{flm}\,(p^{:A\rightarrow M^{B}})\bef f^{\uparrow M}
\]
\end{itemize}
\end{itemize}
The naturality law for $t^{A}:F^{A}\rightarrow G^{A}$ when $F^{A}$,
$G^{A}$ are contrafunctors:

\vspace{-0.2\baselineskip}
\hfill{}%
\begin{minipage}[c][1\totalheight][t]{0.4\columnwidth}%
\[
\xymatrix{F^{A}\ar[r]\sp(0.55){t^{A}}\ar[d]\sp(0.4){(f^{:B\rightarrow A})^{\downarrow F}} & G^{A}\ar[d]\sp(0.4){f^{\downarrow G}}\\
\xyScaleY{1.7pc}\xyScaleX{3.5pc}F^{B}\ar[r]\sp(0.55){t^{B}} & G^{B}
}
\]
%
\end{minipage}\hfill{}%
\begin{minipage}[c][1\totalheight][b]{0.5\columnwidth}%
\[
f^{\downarrow F}\bef t=t\bef f^{\downarrow G}
\]
%
\end{minipage}

Mnemonic rule: if $t:F\leadsto G$ then the lifting to $F$ is on
the left, the lifting to $G$ is on the right
\end{frame}

\begin{frame}{Dinatural transformations and profunctors}

Some methods do \emph{not} have the type signature of the form $F^{A}\rightarrow G^{A}$
\begin{itemize}
\item \lstinline!find[A]: (A => Boolean) => List[A] => Option[A]!
\item \lstinline!fold[A, B]: List[A] => B => (A => B => B) => B! with respect
to \lstinline!B!
\begin{itemize}
\item The type parameter is in contravariant and covariant positions at
once
\item This gives us neither a functor nor a contrafunctor
\end{itemize}
\item Solution: use a profunctor $P^{X,Y}$ (contravariant in $X$, covariant
in $Y$) with equal type parameters: $P^{A,A}$
\end{itemize}
A \textbf{dinatural transformation} is a function $t$ with type signature
$P^{A,A}\rightarrow Q^{A,A}$ that satisfies the naturality law $f^{\downarrow P}\bef t\bef f^{\uparrow Q}=f^{\uparrow P}\bef t\bef f^{\downarrow Q}$
where $P^{X,Y}$ and $Q^{X,Y}$ are suitable profunctors
\begin{itemize}
\item \emph{All pure functions} have the type signature of a dinatural transformation
\item \emph{All }naturality laws (also for \lstinline!find!, \lstinline!fold!)
are derived in this way
\item The corresponding naturality law is guaranteed by parametricity
\item Proof of parametricity theorem is a direct proof that any pure function
$t$ satisfies its law, by induction on the code structure of $t$
\item The proof depends on the profunctor commutativity law and on the ``standard''
lifting codes for $f^{\uparrow P}$ and $f^{\downarrow P}$
\end{itemize}
\end{frame}

\begin{frame}{Type constructors with two type parameters}


\framesubtitle{In particular: bifunctors and profunctors}
\begin{itemize}
\item In Scala syntax: \lstinline!L[A, B]!. Example: \lstinline!type L[A, B] = Either[(A, B), B]!
\item In the type notation: $L^{A,B}$. Example: $L^{A,B}\triangleq A\times B+B$
\item If a type constructor is fully parametric, its type parameters will
be either in covariant or in contravariant positions
\item \textbf{Bifunctors}: both type parameters are always in covariant
positions
\begin{itemize}
\item Example: \lstinline!type L[A, B] = Either[(A, B), B]! is a bifunctor
\item Method \lstinline!bimap[A, B, C, D](f: A => C)(g: B => D): L[A, B] => L[C, D]!
\item Laws: identity and composition for \lstinline!bimap!
\end{itemize}
\item \textbf{Profunctors}: one type parameter contravariant, the other
covariant
\begin{itemize}
\item Example: \lstinline!type P[X, Y] = Option[X] => (Y, Y)! or {\footnotesize{}$P^{X,Y}\triangleq\bbnum 1+X\rightarrow Y\times Y$}{\footnotesize\par}
\item Method \lstinline!xmap[A, B, C, D](f: C => A)(g: B => D): P[A, B] => P[C, D]!
\item Laws: identity and composition for \lstinline!xmap!
\end{itemize}
\item If \lstinline!L[A, B]! is a functor separately in \lstinline!A!
and \lstinline!B!, is it a bifunctor?
\item If \lstinline!P[A, B]! is contravariant in \lstinline!A! and covariant
in \lstinline!B!, is it a profunctor?
\item They are --- as long as all liftings in \lstinline!A! commute with
liftings in \lstinline!B!
\begin{itemize}
\item These are the ``commutativity laws'' of bifunctors and profunctors
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Applying \lstinline!map! to bifunctors and profunctors}

\vspace{-0.1cm}The \lstinline!map! method can be applied with respect
to only one type parameter
\begin{itemize}
\item In a bifunctor \lstinline!L[A, B]!, fix \lstinline!B!. Denote the
resulting functor by $L^{\bullet,B}$
\begin{itemize}
\item In the Scala syntax with ``kind projector'': \lstinline!L[?, B]!
\item Lifting a function $f^{:U\rightarrow V}$ is denoted by $f^{\uparrow L^{\bullet,B}}:L^{U,B}\rightarrow L^{V,B}$
\item If fixing \lstinline!A! instead, a lifting is denoted by $f^{\uparrow L^{A,\bullet}}:L^{A,U}\rightarrow L^{A,V}$
\item \textbf{Commutativity law} for bifunctors: {\footnotesize{}$f^{\uparrow L^{\bullet,B}}\bef(g^{:B\rightarrow C})^{\uparrow L^{V,\bullet}}=g^{\uparrow L^{U,\bullet}}\bef f^{\uparrow L^{\bullet,C}}$} 
\end{itemize}
\item In a profunctor \lstinline!P[A, B]!, fix \lstinline!B!. The resulting
\emph{contrafunctor} is $P^{\bullet,B}$
\begin{itemize}
\item Lifting a function $f^{:U\rightarrow V}$ is denoted by $f^{\downarrow P^{\bullet,B}}:P^{V,B}\rightarrow P^{U,B}$
\item If fixing \lstinline!A! instead, a lifting is denoted by $f^{\uparrow P^{A,\bullet}}:P^{A,U}\rightarrow P^{A,V}$
\begin{itemize}
\item For brevity, we may denote these liftings by $f^{\downarrow P}$ and
$f^{\uparrow P}$ unambiguously
\end{itemize}
\item \textbf{Commutativity law} for profunctors: {\footnotesize{}$f^{\downarrow P}\bef g^{\uparrow P}=g^{\uparrow P}\bef f^{\downarrow P}$} 
\end{itemize}
\vspace{-0.0cm}
\[
\xymatrix{\xyScaleY{1.5pc}\xyScaleX{6.0pc}P^{A,B}\ar[r]\sb(0.55){(f^{:C\rightarrow A})^{\downarrow P}~~~}\ar[d]\sb(0.45){(g^{:B\rightarrow D})^{\uparrow P}} & P^{C,B}\ar[d]\sp(0.45){(g^{:B\rightarrow D})^{\uparrow P}}\\
P^{A,D}\ar[r]\sp(0.45){~~~~(f^{:C\rightarrow A})^{\downarrow P}} & P^{C,D}
}
\]

\item Commutativity laws hold for \emph{all} fully parametric type constructors 
\begin{itemize}
\item It is not necessary to verify the bifunctor and profunctor laws!
\end{itemize}
\item Proof is by induction on the type structure of $P^{X,Y}$
\end{itemize}
\end{frame}

\begin{frame}{Proof of the composition law of \lstinline!xmap!}

If $P^{A,B}$ is a functor in $a$ and a contrafunctor in $B$, define
\lstinline!xmap! by:

\vspace{-0.4cm}%
\begin{minipage}[c][1\totalheight][t]{0.33\columnwidth}%
\[
\xymatrix{\xyScaleY{2.0pc}\xyScaleX{8.0pc}P^{A,B}\ar[rd]\sb(0.55){\text{xmap}\left(f\right)\left(g\right)\,\triangleq~~~}\ar[r]\sp(0.55){(f^{:C\rightarrow A})^{\downarrow P}~~~} & P^{C,B}\ar[d]\sb(0.4){g^{\uparrow P}}\\
 & P^{C,D}
}
\]
%
\end{minipage}\hfill{}%
\begin{minipage}[c][1\totalheight][b]{0.6\columnwidth}%
\begin{center}
\[
\text{xmap}\,(f^{:C\rightarrow A})\,(g^{:B\rightarrow D})\triangleq f^{\downarrow P}\bef g^{\uparrow P}
\]
\par\end{center}%
\end{minipage}

The \lstinline!xmap! composition law: 
\[
\text{xmap}\left(f_{1}\right)\left(g_{1}\right)\bef\text{xmap}\left(f_{2}\right)\left(g_{2}\right)=\text{xmap}\left(f_{2}\bef f_{1}\right)\left(g_{1}\bef g_{2}\right)
\]
Proof uses the commutativity law, $f^{\downarrow P}\bef g^{\uparrow P}=g^{\uparrow P}\bef f^{\downarrow P}$,
for $f_{2}$ and $g_{1}$:
\begin{align*}
 & \text{xmap}\left(f_{1}\right)\left(g_{1}\right)\bef\text{xmap}\left(f_{2}\right)\left(g_{2}\right)=f_{1}^{\downarrow P}\bef\gunderline{g_{1}^{\uparrow P}\bef f_{2}^{\downarrow P}}\bef g_{2}^{\uparrow P}\\
 & =\gunderline{f_{1}^{\downarrow P}\bef f_{2}^{\downarrow P}}\bef\gunderline{g_{1}^{\uparrow P}\bef g_{2}^{\uparrow P}}=\left(f_{2}\bef f_{1}\right)^{\downarrow P}\bef\left(g_{1}\bef g_{2}\right)^{\uparrow P}\\
 & =\text{xmap}\left(f_{2}\bef f_{1}\right)\left(g_{1}\bef g_{2}\right)
\end{align*}

\end{frame}

\begin{frame}{The naturality law for dinatural transformations}

Given two profunctors $P^{X,Y}$ and $Q^{X,Y}$ and a function $t^{A}:P^{A,A}\rightarrow Q^{A,A}$ 

The naturality law is an equation for functions $P^{B,A}\rightarrow Q^{A,B}$:

\[
f^{\downarrow P^{\bullet,A}}\bef t^{A}\bef f^{\uparrow Q^{A,\bullet}}\overset{!}{=}f^{\uparrow P^{B,\bullet}}\bef t^{B}\bef f^{\downarrow Q^{\bullet,B}}
\]
Both sides must give the same result when applied to arbitrary $p:P^{B,A}$
\[
\xymatrix{\xyScaleY{1.8pc}\xyScaleX{2.5pc} & P^{A,A}\ar[r]\sp(0.5){t^{A}} & Q^{A,A}\ar[rd]\sb(0.4){f^{\uparrow Q^{A,\bullet}}\negthickspace\negthickspace}\\
P^{B,A}\ar[rd]\sp(0.55){~f^{\uparrow P^{B,\bullet}}}\ar[ru]\sb(0.65){\negthickspace\negthickspace\negthickspace f^{\downarrow P^{\bullet,A}}} &  &  & Q^{A,B}\\
 & P^{B,B}\ar[r]\sp(0.5){t^{B}} & Q^{B,B}\ar[ru]\sp(0.45){f^{\downarrow Q^{\bullet,B}}\negthickspace\negthickspace}
}
\]
This law reduces to natural transformation laws when $P$ and $Q$
are functors or contrafunctors
\end{frame}

\begin{frame}{Example: writing the naturality law for \lstinline!filter!}

\lstinline!def filter[A]: (A => Boolean) => F[A] => F[A]! for a filterable
functor $F$

Notation: $\text{filt}^{A}:\left(A\rightarrow\bbnum 2\right)\rightarrow F^{A}\rightarrow F^{A}$
(the type \lstinline!Boolean! is $\bbnum 2=\bbnum 1+\bbnum 1$)

Rewrite in the form of a dinatural transformation: 
\[
\text{filt}^{A}:P^{A,A}\rightarrow Q^{A,A}\quad,\quad P^{X,Y}\triangleq X\rightarrow\bbnum 2\quad,\quad Q^{X,Y}\triangleq F^{X}\rightarrow F^{Y}
\]
Write the code for the liftings using the specific types of $P$ and
$Q$:
\begin{align*}
(f^{:A\rightarrow B})^{\downarrow P^{\bullet,A}}=p^{:B\rightarrow\bbnum 2}\rightarrow f\bef p\quad, & \quad\quad f^{\uparrow P^{B,\bullet}}=\text{id}\quad,\\
(f^{:A\rightarrow B})^{\downarrow Q^{\bullet,B}}=q^{:F^{B}\rightarrow F^{B}}\rightarrow f^{\uparrow F}\bef q\quad, & \quad\quad f^{\uparrow Q^{A,\bullet}}=q^{:F^{A}\rightarrow F^{A}}\rightarrow q\bef f^{\uparrow F}\quad.
\end{align*}
Rewrite the naturality law $f^{\downarrow P^{\bullet,A}}\bef\text{filt}^{A}\bef f^{\uparrow Q^{A,\bullet}}\overset{!}{=}f^{\uparrow P^{B,\bullet}}\bef\text{filt}^{B}\bef f^{\downarrow Q^{\bullet,B}}$
as
\[
(p\rightarrow f\bef p)\bef\text{filt}\bef(q\rightarrow q\bef f^{\uparrow F})\overset{!}{=}\text{id}\bef\text{filt}\bef(q\rightarrow f^{\uparrow F}\bef q)\quad.
\]
To simplify this equation, apply both sides to an arbitrary value
$p^{:P^{B,A}}$

Evaluate the results and obtain the naturality law of \lstinline!filter!,
\[
\text{filt}\,(f\bef p)\bef f^{\uparrow F}\overset{!}{=}f^{\uparrow F}\bef\text{filt}\,(p)
\]

\end{frame}

\begin{frame}{Uniqueness of functor implementations}

Consequences of the parametricity theorem:

\textbf{Statement 1}: For any fully parametric type constructor $F^{A}$
covariant in $A$, there is a unique lawful and fully parametric implementation
of \lstinline!fmap! with type signature \lstinline!fmap[A, B]: (A => B) => F[A] => F[B]!

\textbf{Statement 2}: For any fully parametric type constructor $F^{A}$
contravariant in $A$, there is a unique lawful and fully parametric
implementation of \lstinline!cmap! with type signature \lstinline!cmap[A, B]: (B => A) => F[A] => F[B]!
\begin{itemize}
\item Note: many typeclasses may admit several lawful, fully parametric,
but non-equivalent implementations of a typeclass instance for the
same type constructor \lstinline!F[A]!. For example, \lstinline!Filterable!,
\lstinline!Monad!, \lstinline!Applicative! instances are not always
unique. But instances are unique for the functor and contrafunctor
type classes.
\end{itemize}
\end{frame}

\begin{frame}{Proof of Statement 1 (uniqueness of functor instances)}

For a given functor $F$, we can construct the ``standard'' $\text{fmap}$
(denoted by $...^{\uparrow F}$) that is involved in the naturality
laws

Suppose that there exists \emph{another} lawful and fully parametric
implementation $\text{fmap}^{\prime}(f)$:{\footnotesize{}
\[
\text{fmap}^{\prime}:\left(A\rightarrow B\right)\rightarrow F^{A}\rightarrow F^{B}\quad,\quad\quad\text{fmap}^{\prime}(f^{:A\rightarrow B})=\text{???}^{:F^{A}\rightarrow F^{B}}
\]
}We need to show that $\text{fmap}^{\prime}=\text{fmap}$

By parametricity, $\text{fmap}^{\prime}$ has a naturality law with
respect to $B$:{\footnotesize{}
\[
\text{fmap}^{\prime}(f^{:A\rightarrow B}\bef g^{:B\rightarrow C})\overset{!}{=}\text{fmap}^{\prime}(f)\bef g^{\uparrow F}=\text{fmap}^{\prime}(f)\bef\text{fmap}\left(g\right)
\]
} This suggests using the composition law for $\text{fmap}^{\prime}$:{\footnotesize{}
\[
\text{fmap}^{\prime}(f\bef g)=\text{fmap}^{\prime}(f)\bef\text{fmap}^{\prime}(g)\overset{!}{=}\text{fmap}^{\prime}(f)\bef\text{fmap}\left(g\right)
\]
}Since $f^{:A\rightarrow B}$ is arbitrary, we may choose $A=B$ and
$f=\text{id}^{:B\rightarrow B}$ to obtain{\footnotesize{}
\[
\gunderline{\text{fmap}^{\prime}(\text{id})}\bef\text{fmap}^{\prime}(g)=\text{fmap}^{\prime}(g)\overset{!}{=}\gunderline{\text{fmap}^{\prime}(\text{id})}\bef\text{fmap}\left(g\right)=\text{fmap}(g)
\]
}This must hold for arbitrary $g^{:B\rightarrow C}$, which proves
that $\text{fmap}_{F}^{\prime}=\text{fmap}_{F}$
\end{frame}

\begin{frame}{Plan for a proof of commutativity law for profunctors}

\begin{itemize}
\item Main idea: induction on the type expression of a profunctor $P^{X,Y}$
\item A fully parametric $P^{X,Y}$ must be a combination of \lstinline!Unit!
type ($\bbnum 1$), parameters $X$ and $Y$, products $A\times B$,
co-products $A+B$, exponentials $A\rightarrow B$, and type recursion
(use of $P$ in its definition)
\item For each of these cases, we need to show that the commutativity law
holds given that it holds for all sub-expressions
\begin{itemize}
\item Base case: show that the law holds for $P^{X,Y}\triangleq\bbnum 1$
and $P^{X,Y}\triangleq Y$
\item Induction steps: if the law holds for $P^{X,Y}$ and $Q^{X,Y}$, show
that it also holds for $P^{X,Y}+Q^{X,Y}$ and $P^{X,Y}\times Q^{X,Y}$
and $P^{Y,X}\rightarrow Q^{X,Y}$
\item Show that the law holds for a recursively defined $P^{X,Y}\triangleq S^{X,Y,P^{X,Y}}$
for a type constructor $S^{X,Y,R}$ contravariant in $X$, covariant
in $Y$ and $R$
\item We need to use the code of functor and contrafunctor instances for
products, co-products, function types, and recursive types
\end{itemize}
\item Example: For $R^{X,Y}\triangleq P^{X,Y}\times Q^{X,Y}$, the liftings
to $R$ are given by {\footnotesize{}$f^{\uparrow R}\triangleq p\times q\rightarrow f^{\uparrow P}(p)\times f^{\uparrow Q}(q)$}
and {\footnotesize{}$f^{\downarrow R}\triangleq p\times q\rightarrow f^{\downarrow P}(p)\times f^{\downarrow Q}(q)$}{\footnotesize\par}
\begin{itemize}
\item Write $f^{\downarrow R}\bef g^{\uparrow R}$ explicitly using $f^{\downarrow P}$,
$f^{\downarrow Q}$, $g^{\uparrow P}$, and $g^{\uparrow Q}$, and
show that $f^{\downarrow R}\bef g^{\uparrow R}=g^{\uparrow R}\bef f^{\downarrow R}$
by assuming that the same law already holds for $P$ and $Q$
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Plan for a proof of parametricity theorem}

\begin{itemize}
\item Need to prove the naturality law for $t^{A}:P^{A,A}\rightarrow Q^{A,A}$
written as
\[
(f^{:A\rightarrow B})^{\downarrow P^{\bullet,A}}\bef t^{A}\bef f^{\uparrow Q^{A,\bullet}}=f^{\uparrow P^{B,\bullet}}\bef t^{B}\bef f^{\downarrow Q^{\bullet,B}}
\]
\item The code of $t$ must be of the form $p\rightarrow\text{expr}$, where
``$\text{expr}$'' must be built up from some of the nine constructions
\item Main idea: induction on the code of ``$\text{expr}$'', assuming
that the naturality law holds for all sub-expressions
\item Example: induction step for code construction 3 (``create function'')
\begin{itemize}
\item The code of $t$ is $p\rightarrow z\rightarrow r$ and $Q^{X,Y}\triangleq Z^{Y,X}\rightarrow R^{X,Y}$ 
\item Inductive assumption is that any $x\rightarrow r$ satisfies the law;
let $x=p\times z$
\item Assume that the law holds for $u\triangleq p\times z\rightarrow r$,
$u:P^{A,A}\times Z^{A,A}\rightarrow R^{A,A}$
\item Derive the law for $t=p\rightarrow z\rightarrow u(p\times z)$ by
a direct calculation
\end{itemize}
\item There are some technical difficulties (dinatural transformations do
not generally compose) but these difficulties can be overcome with
tricks
\end{itemize}
\end{frame}

\begin{frame}{Summary}
\begin{itemize}
\item Fully parametric code enables powerful mathematical reasoning:
\begin{itemize}
\item Naturality laws can be used for guaranteed correct refactoring
\item Naturality laws allow us to reduce the number of type parameters
\item In typeclass instances, all naturality laws hold, no need to check
\item Functor, contrafunctor, and profunctor typeclass instances are unique
\item Bifunctors and profunctors obey the commutativity law
\end{itemize}
\item Full details and proofs are in the free upcoming book (Appendix D)
\begin{itemize}
\item Draft of the book: \texttt{\href{https://github.com/winitzki/sofp}{https://github.com/winitzki/sofp}}
\end{itemize}
\end{itemize}
\end{frame}

\end{document}