parametricity-1-for-bifunctors.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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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{An extreme pragmatic un-academic approach}
\author{Sergei Winitzki}
\date{2020-02-01}
\institute[ABTB]{Academy by the Bay}
\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}{Parametricity properties and naturality laws}

\vspace{-0.3\baselineskip}
Four main results about \emph{purely functional} programs:
\begin{enumerate}
\item Parametricity theorem: programs automatically obey naturality laws
\begin{itemize}
\item Example: \lstinline!headOption: List[A] => Option[A]! satisfies \lstinline!list.map(f).headOption == list.headOption.map(f)!
\[
f^{\uparrow\text{List}}\bef\text{headOpt}=\text{headOpt}\bef f^{\uparrow\text{Opt}}
\]
\end{itemize}
\item Recipe for writing the naturality law, given a function's type signature
\begin{itemize}
\item Dinatural transformation \lstinline!t: P[A, A] => Q[A, A]! where
\lstinline!P[X, Y]! and \lstinline!Q[X, Y]! are profunctors (contravariant
in \lstinline!X! and covariant in \lstinline!Y!) has the naturality
law \lstinline!t(pba.xmap(f, identity)).xmap(identity, g) == t(pba.xmap(identity, g)).xmap(f, identity)!
\end{itemize}
\item Liftings with respect to different type parameters always commute
\begin{itemize}
\item Example: \lstinline!IO[E, A]! and \lstinline!io.map(f).mapError(g) == io.mapError(g).map(f)!
\end{itemize}
\item Functors and contrafunctors are uniquely derived from types
\begin{itemize}
\item Example: \lstinline!type F[A] = Either[(A, Int), String => A]! has
functor instance \lstinline[mathescape=false]!def fmap[A, B](f: A => B): Either[(A, Int), String => A] => Either[(B, Int), String => B] = \{ case Left(a, n) => Left(f(a), n); case Right(g) => Right(g andThen f) \}!
\end{itemize}
\end{enumerate}
\end{frame}
\vspace{2\baselineskip}

\textbf{Purely functional} 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
}
\end{lstlisting}
\vspace{-0.7\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) }!
\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). 
\item Use recursive call: \lstinline!fmap(f)(tail)!. Notation: $\overline{\text{fmap}_{\text{List}}}(f)(t)$
\end{enumerate}

\begin{frame}{Naturality laws: motivation}

A ``naturality law'' expresses the programmer's intuitions about
the properties of \textbf{fully parametric} code:
\begin{itemize}
\item Code is written once and works in the same way for all types

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

~~\lstinline!case Nil            => None!

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

\lstinline!\}!
\end{itemize}
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! assignment, writing
files, networking)
\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}
\end{frame}

\begin{frame}{Naturality laws: equations}

\vspace{-0.1cm}\textbf{Naturality law} for a transformation $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}%
\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}}
\]
%
\end{minipage}
\begin{itemize}
\item Lifting $f$ before transformation equals to lifting $f$ after transformation
\begin{itemize}
\item Intuition: $t$ rearranges data in a collection regardless of value
types
\end{itemize}
\end{itemize}
More 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}_{L}\bef(f^{:A\rightarrow B})^{\uparrow L}=f\bef\text{pu}_{L}
\]
}{\footnotesize\par}
\par\end{center}

\end{frame}

\begin{frame}{Why do we need to know about naturality laws}

Typeclasses: type constructors with methods \lstinline!map!, \lstinline!filter!,
\lstinline!fold!, \lstinline!flatMap!

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, composition, naturality
\end{itemize}
We need to check the laws when implementing a new typeclass instance
\begin{itemize}
\item The \textbf{parametricity theorem} guarantees that all naturality
laws hold as long as the method's code is purely functional
\item This saves us time: \emph{no need} to check the naturality laws
\end{itemize}
Proving 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})
\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 \textbf{purely functional}, 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!L[A, B]! defined above 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 but only if 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 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{2.0pc}\xyScaleX{6.0pc}P^{A,B}\ar[r]\sb(0.55){\text{xmap}_{P}(f^{:C\rightarrow A},\text{id})~~~}\ar[d]\sb(0.45){\text{xmap}_{P}(\text{id},g^{:B\rightarrow D})} & P^{C,B}\ar[d]\sp(0.45){\text{xmap}_{P}(\text{id},g^{:B\rightarrow D})}\\
P^{A,D}\ar[r]\sp(0.45){~~~~\text{xmap}_{P}(f,\text{id})} & P^{C,D}
}
\]

\item Commutativity laws hold for \emph{all} purely functional type constructors
\begin{itemize}
\item It is not necessary to verify the bifunctor and profunctor laws!
\end{itemize}
\end{itemize}
\end{frame}

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

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}$
\begin{itemize}
\item Many standard methods have the form of a natural transformation
\item \lstinline!pure!, \lstinline!headOption!, \lstinline!lastOption!,
\lstinline!reverse!, \lstinline!swap!, \lstinline!map!, \lstinline!flatMap!
\item If there are several type parameters, use one at a time:
\begin{itemize}
\item For \lstinline!flatMap!, denote by $\text{flm}_{M}:\left(A\rightarrow M^{B}\right)\rightarrow M^{A}\rightarrow M^{B}$,
fix $A$
\item  $\text{flm}_{M}:F^{B}\rightarrow G^{B}$ where $F^{B}\triangleq A\rightarrow M^{B}$
and $G^{B}\triangleq M^{A}\rightarrow M^{B}$
\item The naturality law is then written as the equation
\[
\text{flm}_{M}(p^{:A\rightarrow M^{B}}\bef f^{\uparrow M})=\text{flm}_{M}(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.8\baselineskip}
\begin{minipage}[c][1\totalheight][t]{0.26\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]\sb(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.68\columnwidth}%
\[
(f^{:B\rightarrow A})^{\downarrow F}\bef t^{B}=t^{A}\bef(f^{:B\rightarrow A})^{\downarrow G}
\]
then $t$ is a natural transformation $F\leadsto G$%
\end{minipage}
\end{frame}

\begin{frame}{Dinatural transformations and profunctors}

Some methods do 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}
\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 The corresponding naturality law is guaranteed by parametricity
\item \emph{All }naturality laws (also for \lstinline!find!, \lstinline!fold!)
are derived in this way
\end{itemize}
\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.45){f^{\uparrow Q^{A,\bullet}}}\\
P^{B,A}\ar[rd]\sp(0.55){f^{\uparrow P^{B,\bullet}}}\ar[ru]\sb(0.55){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}}}
}
\]

\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}$

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}_{F}\bef(q\rightarrow q\bef f^{\uparrow F})\overset{!}{=}\text{id}\bef\text{filt}_{F}\bef(q\rightarrow f^{\uparrow F}\bef q)\quad.
\]
To simplify the form of the naturality law, apply both sides to an
arbitrary value $p^{:P^{B,A}}=p^{:B\rightarrow\bbnum 2}$

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

\end{frame}

\begin{frame}{Uniqueness of functor implementations}

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

\textbf{Statement 2}: For any purely functional type constructor $F^{A}$
contravariant in $A$, there is a unique lawful and purely functional
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, purely functional,
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.
\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}_{F}$
that is involved in the naturality laws. Suppose that there exists
\emph{another} lawful and purely functional implementation $\text{fmap}_{F}^{\prime}(f)$.
We need to show that $\text{fmap}_{F}^{\prime}=\text{fmap}_{F}$.{\footnotesize{}
\[
\text{fmap}_{F}^{\prime}:\left(A\rightarrow B\right)\rightarrow F^{A}\rightarrow F^{B}\quad,\quad\quad\text{fmap}_{F}^{\prime}(f^{:A\rightarrow B})=\text{???}^{:F^{A}\rightarrow F^{B}}\quad.
\]
} Now, $\text{fmap}_{F}^{\prime}$ has a naturality law with respect
to $B$:{\footnotesize{}
\[
\text{fmap}_{F}^{\prime}(f^{:A\rightarrow B}\bef g^{:B\rightarrow C})\overset{!}{=}\text{fmap}_{F}^{\prime}(f)\bef g^{\uparrow F}\quad.
\]
} Use the composition law for $\text{fmap}_{F}^{\prime}$:{\footnotesize{}
\[
\text{fmap}_{F}^{\prime}(f\bef g)=\text{fmap}_{F}^{\prime}(f)\bef\text{fmap}_{F}^{\prime}(g)\overset{!}{=}\text{fmap}_{F}^{\prime}(f)\bef g^{\uparrow F}\quad.
\]
}Since $f^{:A\rightarrow B}$ is arbitrary, we can choose $A=B$ and
$f=\text{id}^{:B\rightarrow B}$ to obtain{\footnotesize{}
\[
\gunderline{\text{fmap}_{F}^{\prime}(\text{id})}\bef\text{fmap}_{F}^{\prime}(g)=\text{fmap}_{F}^{\prime}(g)\overset{!}{=}\gunderline{\text{fmap}_{F}^{\prime}(\text{id})}\bef g^{\uparrow F}=g^{\uparrow F}=\text{fmap}_{F}(g)\quad.
\]
}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 purely functional $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}$; also 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$.
\begin{itemize}
\item We need to use the code of functor and contrafunctor instances for
products, co-products, exponentials, and recursive types.
\item Example: Define $R^{X,Y}\triangleq P^{X,Y}\times Q^{X,Y}$, then the
lifting to $R$ is given by $f^{\uparrow R}\triangleq p\times q\rightarrow f^{\uparrow P}(p)\times f^{\uparrow Q}(q)$
\end{itemize}
\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 the 9 purely functional
code 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 Purely functional code enables powerful mathematical reasoning:
\begin{itemize}
\item Any type constructor \lstinline!F[A]! has the form of a diagonal
profunctor \lstinline!P[A, A]!
\item Functor, contrafunctor, and profunctor instances are unique
\item Any purely functional code obeys a naturality law
\item Bifunctors and profunctors obey a commutativity law
\end{itemize}
\item Full details and proofs are in the upcoming book (Appendix D)
\begin{itemize}
\item Source (\LaTeX) for the book: \texttt{\href{https://github.com/winitzki/sofp}{https://github.com/winitzki/sofp}}
\end{itemize}
\end{itemize}
\end{frame}

\end{document}