explaining-theorems-for-free.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{amstext}
\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[Theorems for free]{Explaining ``Theorems for Free'' and parametricity}
\subtitle{A tutorial, with code examples in Scala}
\author{Sergei Winitzki}
\date{2020-10-17}
\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: a theory about certain code refactorings}

\vspace{-0.1cm}Expected properties of code that manipulates collections:
\\
~
\begin{itemize}
\item \vspace{-0.2cm}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}
\item \vspace{-0.1cm}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}
\item These refactorings are guaranteed to be correct
\begin{itemize}
\item because \texttt{\textcolor{blue}{\footnotesize{}\_.toList}} is a \textbf{natural
transformation} \texttt{\textcolor{blue}{\footnotesize{}Stream{[}A{]}
=> List{[}A{]}}} 
\item ... and \texttt{\textcolor{blue}{\footnotesize{}\_.filter}} is also
a natural transformation in disguise\\
~
\end{itemize}
\item \vspace{-0.1cm}Natural transformations ``work the same way for all
types''
\begin{itemize}
\item ... and satisfy the ``naturality laws''
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Refactoring rules written as equations}

\begin{itemize}
\item \vspace{-0.1cm}The refactoring involving \lstinline!toList!:

\lstinline!def toList[A]: Stream[A] => List[A]!

For any function \lstinline!f: A => B!:

\lstinline!_.toList.map(f) == _.map(f).toList!
\item The refactoring involving \lstinline!filter!:

\lstinline!def filter[A]: Stream[A] => (A => Boolean) => Stream[A]!

For any function \lstinline!f: A => B! and predicate \lstinline!p: B => Boolean!:

\lstinline!_.filter(f andThen p).map(f) == _.map(f).filter(p)!
\item Generally: applying \lstinline!t[A]: F[A] => G[A]! \emph{before}
\lstinline!_.map(f)! equals applying \lstinline!t[B]: F[B] => G[B]!
\emph{after} \lstinline!_.map(f)!, for any function \lstinline!f: A => B!
\[
\xymatrix{\xyScaleY{2.8pc}\xyScaleX{5.5pc}\mathtt{F[A]}\ar[d]\sb(0.5){~\mathtt{\_.map(f)}\text{ for }\mathtt{F}}\ar[r]\sp(0.5){\mathtt{t[A]}} & \mathtt{G[A]}\ar[d]\sp(0.5){\mathtt{\_.map(f)}\text{ for }\mathtt{G}}\\
\mathtt{F[B]}\ar[r]\sp(0.5){\mathtt{t[B]}} & \mathtt{G[B]}
}
\]

\begin{itemize}
\item This is called a \textbf{naturality law}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Naturality laws: further examples}

\vspace{-0.1cm}\textbf{Naturality law} for a function \lstinline!t[A]: F[A] => G[A]!
is an equation that permutes the order of \lstinline!t! and of \lstinline!_.map(f)!,
for an arbitrary function \lstinline!f: A => B! 
\begin{itemize}
\item We expect it to hold if the code works the same way for all types
\item Intuition: \texttt{t} rearranges data in a collection, ``not looking''
at values
\end{itemize}
Further examples:
\begin{itemize}
\item The headOption method: \lstinline!headOption: List[A] => Option[A]!
\end{itemize}
\begin{center}
\lstinline!list.map(f).headOption == list.headOption.map(f)!
\par\end{center}
\begin{itemize}
\item Reverse a list: \lstinline!reverse[A]: List[A] => List[A]!
\end{itemize}
\begin{center}
\lstinline!list.map(f).reverse == list.reverse.map(f)!
\par\end{center}
\begin{itemize}
\item The \lstinline!pure! method: \lstinline!pure[A]: A => L[A]! or \lstinline!Id[A] => L[A]!
\end{itemize}
\begin{center}
\lstinline!pure(x).map(f) == pure(f(x))!
\par\end{center}
\begin{itemize}
\item Get length: \lstinline!length[A]: List[A] => Int! or \lstinline!List[A] => Const[Int, A]!
\end{itemize}
\begin{center}
\lstinline!length(list.map(f)) == length(list)!
\par\end{center}

\end{frame}

\begin{frame}{Naturality laws in typeclasses}

Another use of naturality laws is in 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

If naturality holds for \lstinline!flatMap!, \lstinline!filter!,
and \lstinline!pure!, then:
\begin{itemize}
\item The methods \lstinline!flatMap! and \lstinline!flatten: F[F[A]] => F[A]!
are equivalent 
\item The methods \lstinline!filter! and \lstinline!deflate: F[Option[A]] => F[A]!
are equivalent 
\item The methods \lstinline!pure: A => F[A]! and \lstinline!unit: F[Unit]!
are equivalent 
\begin{itemize}
\item Can simplify the definitions of some typeclasses 
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Naturality laws and ``theorems for free''}

\begin{itemize}
\item The name ``theorems for free'' comes from a \href{https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf}{1989 paper}
by P.~Wadler
\begin{itemize}
\item \emph{From the type of a polymorphic function we can derive a theorem
it satisfies. Every function of the same type satisfies the same theorem.}
\end{itemize}
\item The ``theorems for free'' are laws that come in two flavors:
\begin{itemize}
\item Naturality laws (most often seen in practice)
\item Dinaturality laws (rarely seen) -- a generalized form of naturality
laws
\end{itemize}
\item The \textbf{parametricity theorem} says:
\begin{itemize}
\item Any \textbf{fully parametric} code \lstinline!t: P[A] => Q[A]! satisfies
a dinaturality law
\item There is a recipe for writing that law
\item One independent law is obtained per type parameter
\item In most cases, it is actually a naturality law
\end{itemize}
\item Usually, typeclass instances are written in fully parametric code
\begin{itemize}
\item Then it is not necessary to verify the naturality laws
\item Can simplify some typeclass definitions
\item Naturality laws save us time and simplify code
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{What did ``theorems for free'' ever do for us programmers?}

\begin{itemize}
\item ``Theorems for free'' guarantee naturality laws for fully parametric
code
\item To use ``theorems for free'' in practice, programmers need to:
\begin{itemize}
\item Recognize and write fully parametric code
\item Be able to write the refactoring that follows from naturality laws
\item Be able to implement \lstinline!_.map! for any covariant functor
(as well as \lstinline!_.contramap! for any contravariant functor)
\item Recognize that the refactoring is guaranteed by parametricity
\item Recognize simplifications in typeclasses
\end{itemize}
\end{itemize}
\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 type:

\lstinline!case class Data[A, B](x: Either[A, B] => B, y: (A, B) => A)!
\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 Naturality laws express the programmer's intuition about the properties
of fully parametric code
\end{itemize}
\end{frame}
~

Example of code that is \emph{not} fully parametric:
\begin{itemize}
\item A bad 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
\begin{itemize}
\item But the code is still purely functional and referentially transparent
\item ``Full parametricity'' is a stronger restriction on code
\end{itemize}
\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 of ``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 uses each of the nine allowed constructions.
\end{lstlisting}
\vspace{-0.2\baselineskip}

\begin{enumerate}
\item Use \lstinline!Unit! value (or equivalent type), e.g.~\lstinline!()!,
\lstinline!Nil!, \lstinline!None!
\item Use bound variable (a given argument of the function)
\item Create a function: \lstinline!{ x => expr(x) }!
\item Use a function: \lstinline!f(x)!
\item Create a tuple: \lstinline!(a, b)!
\item Use a tuple: \lstinline!p._1!
\item Create a disjunctive value: \lstinline!Left[A, B](x)!
\item Use a disjunctive value: \lstinline!{ case ... => ... }! (pattern-matching)
\item Use a recursive call: e.g., \lstinline!fmap(f)(tail)! within the
code of \lstinline!fmap!\medskip{}
\end{enumerate}

\begin{frame}{Approaches to using and proving the parametricity theorem}

Using the parametricity theorem à la Wadler 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
\item Need to learn how to work with relation values and relation types
\item Need to guess how to replace relations by functions in the end
\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
\item No need to use relations
\item For any type signature, can quickly write the naturality law
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Dinatural transformations and profunctors}

Some methods do \emph{not} have the type signature of the form \lstinline!F[A] => G[A]!
where both \lstinline!F! and \lstinline!G! are functors (or both
are contrafunctors)
\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
\begin{itemize}
\item But we can identify the variance for each occurrence of type parameter
\end{itemize}
\end{itemize}
\item Solution: use a \textbf{profunctor} \lstinline!P[X, Y]! (contravariant
in \lstinline!X!, covariant in \lstinline!Y!) but set equal type
parameters: \lstinline!P[A, A]!
\item Within any fully parametric type signature, each occurrence of a type
parameter is either covariant or contravariant
\end{itemize}
A \textbf{dinatural transformation} is a function \lstinline!t[A]: P[A, A] => Q[A, A]!
where \lstinline!P[X, Y]! and \lstinline!Q[X, Y]! are some profunctors
and \lstinline!t! satisfies the naturality law
\begin{itemize}
\item \emph{All pure functions} have the type signature of a dinatural transformation
\end{itemize}
\end{frame}

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

Given \lstinline!t[A]: P[A, A] => Q[A, A]! where \lstinline!P[X, Y]!
and \lstinline!Q[X, Y]! are profunctors

The naturality law requires that for any function \lstinline!f: A => B!,
\\
~

\vspace{-0.25cm}\lstinline!p.contramapPX(f).pipe(t).mapQY(f) == p.mapPY(f).pipe(t).contramapQX(f)!\\
~

\vspace{-0.25cm}Both sides must give the same result when applied
to arbitrary \lstinline!p: P[B, A]! 
\begin{itemize}
\item \emph{All }naturality laws (also for \lstinline!find!, \lstinline!fold!)
are derived in this way 
\item The code for \lstinline!map! and \lstinline!contramap! must be lawful
and fully parametric
\end{itemize}
\[
\xymatrix{\xyScaleY{1.8pc}\xyScaleX{5.5pc} & \mathtt{P[A,A]}\ar[r]\sp(0.5){\mathtt{t[A]}} & \mathtt{Q[A,A]}\ar[rd]\sb(0.45){\mathtt{\_.mapQY(f)}~~~}\\
\mathtt{P[B,A]}\ar[rd]\sp(0.55){~~~\mathtt{\_.mapPY(f)}}\ar[ru]\sb(0.55){~~~\mathtt{\_.contramapPX(f)}} &  &  & \mathtt{Q[A,B]}\\
 & \mathtt{P[B,B]}\ar[r]\sp(0.5){\mathtt{t[B]}} & \mathtt{Q[B,B]}\ar[ru]\sp(0.5){\mathtt{\_.contramapQX(f)}~~~~}
}
\]

\begin{itemize}
\item This law reduces to natural transformation laws when \lstinline!P!
and \lstinline!Q! are functors or contrafunctors
\end{itemize}
\end{frame}

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

\vspace{-0.15cm}Use a curried version of \lstinline!_.filter! for
convenience:

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

\vspace{-0.15cm}Rewrite as a dinatural transformation, \lstinline!filt[A]: P[A, A] => Q[A, A]!
with \lstinline!type P[X, Y] = X => Boolean! and \lstinline!type Q[X, Y] = F[X] => F[Y]!\\
~

\vspace{-0.15cm}Write the code for \lstinline!map! and \lstinline!contramap!
using the specific types of \lstinline!P! and \lstinline!Q!:
\begin{center}
\lstinline!p.contramapPX(f) == f andThen p! 
\par\end{center}

\begin{center}
\lstinline!p.mapPY(f) == p!
\par\end{center}

\begin{center}
\lstinline!q.contramapQX(f) == _.map(f) andThen q!
\par\end{center}

\begin{center}
\lstinline!q.mapQY(f) = q andThen _.map(f)!\\
~
\par\end{center}

\vspace{-0.15cm}Now write the dinaturality law and simplify: \lstinline!(f andThen p).pipe(filt) andThen _.map(f)) == _.map(f) andThen p.pipe(filt)!\\
~

\vspace{-0.15cm}Rewriting in terms of \lstinline!_.filter!, we obtain
the naturality law of \lstinline!filter!:

\lstinline!_.filter(f andThen p).map(f) = _.map(f).filter(p)!
\end{frame}

\begin{frame}{Other parametricity properties}

\begin{itemize}
\item Bifunctor \lstinline!map! calls commute if used with different type
parameters:

For any value \lstinline!b: B[X, Y]!, and any functions \lstinline!f: X => P!,
\lstinline!g: Y => Q!, 

the commutativity law holds: \lstinline!b.mapX(f).mapY(g) == b.mapY(g).mapX(f)!
\end{itemize}
\[
\xymatrix{\xyScaleY{2.8pc}\xyScaleX{5.5pc}\mathtt{B[X,Y]}\ar[d]\sb(0.5){~\mathtt{\_.mapY(g)}}\ar[r]\sp(0.5){\mathtt{\_.mapX(f)}} & \mathtt{B[P,Y]}\ar[d]\sp(0.5){\mathtt{\_.mapY(g)}}\\
\mathtt{B[X,Q]}\ar[r]\sp(0.5){\mathtt{\_.mapX(f)}} & \mathtt{B[P,Q]}
}
\]

\begin{itemize}
\item Example: \lstinline!zio.IO[E, A]! has \lstinline!_.mapError! and
\lstinline!_.map!
\item A given functor's lawful and fully parametric method \lstinline!map!
is unique 
\begin{itemize}
\item Note: many typeclasses may admit several lawful, fully parametric,
but inequivalent 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}
\item Analogous results for \lstinline!contramap!, contrafunctors, and
profunctors
\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 Appendix D of the upcoming book
\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}