reasoning-natural-transformations.lyx

#LyX 2.3 created this file. For more info see http://www.lyx.org/
\lyxformat 544
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass beamer
\begin_preamble
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Natural transformations]{Properties of natural transformations}
\subtitle{With code examples in Scala}
\author{Sergei Winitzki}
\date{2020-05-30}
\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}
\end_preamble
\use_default_options true
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\use_microtype false
\use_dash_ligatures true
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing single
\use_hyperref true
\pdf_bookmarks true
\pdf_bookmarksnumbered false
\pdf_bookmarksopen false
\pdf_bookmarksopenlevel 1
\pdf_breaklinks false
\pdf_pdfborder false
\pdf_colorlinks true
\pdf_backref false
\pdf_pdfusetitle true
\papersize default
\use_geometry true
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification true
\use_refstyle 1
\use_minted 0
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style english
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\listings_params "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"
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\gunderline}[1]{\mathunderline{greenunder}{#1}}
{\underline{#1}}
\end_inset


\begin_inset FormulaMacro
\newcommand{\bef}{\forwardcompose}
{\fatsemi}
\end_inset


\begin_inset FormulaMacro
\newcommand{\bbnum}[1]{\custombb{#1}}
{\underline{#1}}
\end_inset


\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
frame{
\backslash
titlepage}
\end_layout

\end_inset


\begin_inset Note Note
status collapsed

\begin_layout Plain Layout
Beginning of slides.
\end_layout

\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Refactoring code by permuting the order of operations
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Note Note
status collapsed

\begin_layout Plain Layout
To introduce the topic, I begin with practical use examples.
 It is useful for a programmer to know that purely functional code can be
 refactored in ways that are guaranteed to be correct.
 To formulate this fact rigorously, one writes an equation called a "naturality
 law".
 Programmers need to know that these laws exist and can be used for rigorous
 reasoning about code.
 I will show some examples of such reasoning.
\end_layout

\begin_layout Plain Layout
An inquisitive programmer would now ask how to write the naturality law
 for any given function, and also how to prove that the law always holds
 for purely functional code.
 The main part of the talk will answer these questions.
\end_layout

\begin_layout Plain Layout
[Difficulty level 1]
\end_layout

\begin_layout Plain Layout
The name "naturality" comes from "natural transformations" of category theory.
 However, a software engineer needs only a simplified definition of natural
 transformations in the context of functional programming.
 We just need to learn to recognize a natural transformation by its type
 signature: a function between two functors sharing a type parameter.
 After that, the corresponding naturality law is straightforward to write.
\end_layout

\begin_layout Plain Layout
The type signature of a natural transformation is of this form:
\end_layout

\begin_layout Plain Layout
def nt[A]: F[A] => G[A] = ??? // Both F and G must be covariant in A, or
 both contravariant in A.
\end_layout

\begin_layout Plain Layout
Examples of natural transformations in Scala:
\end_layout

\begin_layout Plain Layout
def headOption[A]: List[A] => Option[A] = ...
 def reverse[A]: List[A] => List[A] = ...
 def zipWithIndex[A]: List[A] => List[(A, Int)] = ...
\end_layout

\begin_layout Plain Layout
However, not all widely used functions have the type signature of a natural
 transformation; for example, `find`, `filter`, or `foldLeft` do not.
 A more general approach is necessary.
\end_layout

\begin_layout Plain Layout
[Difficulty level 2]
\end_layout

\begin_layout Plain Layout
One completely general approach is based on the Reynolds-Wadler parametricity
 theorem (known from Wadler's "theorems for free" paper).
 The Reynolds-Wadler theorem is usually formulated using specially defined
 type and value "relations", which are hard to use and to understand for
 programmers who always work with functions and never with arbitrary relations.
\end_layout

\begin_layout Plain Layout
I will explain a different approach that derives parametricity properties
 directly, without using relations.
 In that approach, Wadler's "free theorems" are just naturality laws satisfied
 by any purely functional code with a given type signature.
 For this to work with arbitrary type signatures, we need to extend naturality
 laws from natural transformations to more general "dinatural" transformations
 (functions between two "profunctors" sharing a type parameter).
 I will introduce the notions of profunctors and dinatural transformations.
 I will then show a recipe for writing naturality laws for all type signatures,
 and give some examples.
\end_layout

\begin_layout Plain Layout
The recipe depends on being able to derive the code of `map` or `contramap`
 for any given covariant or contravariant type constructor.
 I will explain an algorithm for deriving that code mechanically.
\end_layout

\begin_layout Plain Layout
In most cases, it is enough for a programmer to know how to write the naturality
 law.
 Proofs are more complicated.
 Without going through the full details, I will outline the proofs of three
 parametricity properties that apply to purely functional code:
\end_layout

\begin_layout Plain Layout
[Difficulty level 3]
\end_layout

\begin_layout Plain Layout
(1) The `fmap` methods defined with respect to any two different type parameters
 will always commute.
\end_layout

\begin_layout Plain Layout
Example in Scala:
\end_layout

\begin_layout Plain Layout
type T[A, B, C] = ...
 // Define some type constructor, covariant with respect to 3 type parameters.
 // Now define `fmap` methods with respect to each type parameter: def fmap_A[A,
 B, C, Z](f: A => Z): T[A, B, C] => T[Z, B, C] = ??? def fmap_B[A, B, C,
 Z](f: B => Z): T[A, B, C] => T[A, Z, C] = ??? def fmap_C[A, B, C, Z](f:
 C => Z): T[A, B, C] => T[A, B, Z] = ??? Then fmap_A, fmap_B, and fmap_C
 pairwise commute, for example:
\end_layout

\begin_layout Plain Layout
fmap_A(f) andThen fmap_B(g) == fmap_B(g) andThen fmap_A(f)
\end_layout

\begin_layout Plain Layout
Proof is by induction on the type structure of T.
\end_layout

\begin_layout Plain Layout
(2) Any purely functional expression with type parameters will satisfy one
 naturality law per type parameter.
\end_layout

\begin_layout Plain Layout
This applies not only to functions, but generally to expressions of any
 type.
 The naturality law is written via the "recipe" derived earlier in the talk.
\end_layout

\begin_layout Plain Layout
Proof is by induction on the code structure of the given expression.
\end_layout

\begin_layout Plain Layout
[Difficulty level 2]
\end_layout

\begin_layout Plain Layout
(3) Any type constructor covariant with respect to a type parameter `A`
 has a unique purely functional `fmap` method with respect to `A` satisfying
 the functor laws.
\end_layout

\begin_layout Plain Layout
Proof is a short symbolic calculation that uses statement (2) and the functor
 laws.
\end_layout

\end_inset


\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.15cm}
\end_layout

\end_inset

Expected properties of refactored code: 
\begin_inset Newline newline
\end_inset


\begin_inset space ~
\end_inset


\end_layout

\begin_layout Standard
First extract user information, then convert stream to list; or first convert
 to list, then extract user information:
\end_layout

\begin_layout Standard

\family typewriter
\size footnotesize
\color blue
db.getRows.toList.map(getUserInfo)
\family default
\size default
\color inherit
 gives the same result as
\begin_inset Newline newline
\end_inset


\family typewriter
\size footnotesize
\color blue
db.getRows.map(getUserInfo).toList
\begin_inset Newline newline
\end_inset


\begin_inset space ~
\end_inset


\end_layout

\begin_layout Standard
First extract user information, then exclude invalid rows; or first exclude
 invalid rows, then extract user information:
\end_layout

\begin_layout Standard

\family typewriter
\size footnotesize
\color blue
db.getRows.map(getUserInfo).filter(isValid)
\family default
\size default
\color inherit
 gives the same result as 
\begin_inset Newline newline
\end_inset


\family typewriter
\size footnotesize
\color blue
db.getRows.filter(getUserInfo andThen isValid).map(getUserInfo)
\begin_inset Newline newline
\end_inset


\begin_inset space ~
\end_inset


\end_layout

\begin_layout Itemize
These refactorings are guaranteed to be correct...
\end_layout

\begin_deeper
\begin_layout Itemize
...
 because 
\family typewriter
\size footnotesize
\color blue
_.toList
\family default
\size default
\color inherit
 is a natural transformation 
\family typewriter
\size footnotesize
\color blue
Stream[A] => List[A]
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
and 
\family typewriter
\size footnotesize
\color blue
_.filter
\family default
\size default
\color inherit
 is also a natural transformation in disguise
\end_layout

\end_deeper
\begin_layout Itemize
Natural transformations satisfy the 
\begin_inset Quotes eld
\end_inset

naturality properties
\begin_inset Quotes erd
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Refactored code: equations
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Introduce short syntax to write those properties as equations:
\end_layout

\begin_layout Standard
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="6" columns="2">
<features tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size small
\color blue
def toList[A]: Stream[A] => List[A]
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $\text{toList}^{A}:\text{Str}^{A}\rightarrow\text{List}^{A}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size small
\color blue
val f: A => B
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $f^{:A\rightarrow B}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size small
\color blue
_.map(f)
\family default
\color inherit
 with type 
\family typewriter
\color blue
List[A] => List[B]
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $f^{\uparrow\text{List}}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size small
\color blue
_.toList.map(f)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $\text{toList}\bef f^{\uparrow\text{List}}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size small
\color blue
f andThen g
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $f\bef g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\family typewriter
\size small
\color blue
_.map(f).map(g) == _.map(f andThen g)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $f^{\uparrow\text{List}}\bef g^{\uparrow\text{List}}=(f\bef g)^{\uparrow\text{List}}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Standard
The 
\begin_inset Quotes eld
\end_inset

short syntax
\begin_inset Quotes erd
\end_inset

 is equivalent to Scala code
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Refactored code: equations
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.2cm}
\end_layout

\end_inset

Rewrite the previous examples as equations and type diagrams:
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.2cm}
\end_layout

\end_inset


\begin_inset listings
inline true
status open

\begin_layout Plain Layout

def toList[A]: Stream[A] => List[A]
\end_layout

\end_inset

 written as 
\size small

\begin_inset Formula $\text{toList}^{A}:\text{Str}^{A}\rightarrow\text{List}^{A}$
\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.3cm}
\end_layout

\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "26col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\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{4.0pc}\text{Str}^{B}\ar[r]\sp(0.55){\text{toList}^{B}} & \text{List}^{B}
}
\]

\end_inset


\end_layout

\end_inset


\begin_inset space \hfill{}
\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "68col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\align center
\begin_inset space ~
\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset space ~
\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset listings
inline true
status open

\begin_layout Plain Layout

_.toList.map(f) == _.map(f).toList
\end_layout

\end_inset


\size small

\begin_inset Formula 
\[
\text{toList}^{A}\bef f^{\uparrow\text{List}}=f^{\uparrow\text{Str}}\bef\text{toList}^{B}
\]

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.2cm}
\end_layout

\end_inset


\begin_inset listings
inline true
status open

\begin_layout Plain Layout

def filt[A]: (A => Boolean) => Stream[A] => Stream[A]
\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.3cm}
\end_layout

\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "26col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\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.5pc}\text{Str}^{B}\ar[r]\sp(0.55){\text{filt}^{B}(p)} & \text{Str}^{B}
}
\]

\end_inset


\end_layout

\end_inset


\begin_inset space \hfill{}
\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "72col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\align center

\size small
\begin_inset Formula 
\begin{align*}
 & \text{filt}^{A}:(A\rightarrow\bbnum 2)\rightarrow\text{Str}^{A}\rightarrow\text{Str}^{A}\\
 & f^{\uparrow\text{Str}}\bef\text{filt}^{B}(p)=\text{filt}^{A}(f\bef p)\bef f^{\uparrow\text{Str}}
\end{align*}

\end_inset


\size default

\begin_inset space ~
\end_inset

 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

_.map(f).filter(p) == _.filter(x => p(f(x))).map(f)
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.2cm}
\end_layout

\end_inset

A transformation before 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

map
\end_layout

\end_inset

 equals a transformation after 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

map
\end_layout

\end_inset


\end_layout

\begin_layout Itemize
This is called a 
\series bold
naturality law
\end_layout

\begin_layout Itemize
We expect it to hold if the code works the same way for all types
\end_layout

\begin_deeper
\begin_layout Itemize
The naturality law is a mathematical expression of the programmer's intuition
 about code 
\begin_inset Quotes eld
\end_inset

working the same way for all types
\begin_inset Quotes erd
\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Naturality laws: equations
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.1cm}
\end_layout

\end_inset


\series bold
Naturality law
\series default
 for a function 
\begin_inset Formula $t$
\end_inset

 is an equation involving an arbitrary function 
\begin_inset Formula $f$
\end_inset

 that permutes the order of application of 
\begin_inset Formula $t$
\end_inset

 and of a lifted 
\begin_inset Formula $f$
\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.4cm}
\end_layout

\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "26col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\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{4.0pc}\text{List}^{B}\ar[r]\sp(0.55){\text{headOpt}^{B}} & \text{Opt}^{B}
}
\]

\end_inset


\end_layout

\end_inset


\begin_inset space \hfill{}
\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "b"
use_parbox 0
use_makebox 0
width "68col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\align center
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

_.map(f).headOption == _.headOption.map(f)
\end_layout

\end_inset


\begin_inset Formula 
\[
f^{\uparrow\text{List}}\bef\text{headOpt}=\text{headOpt}\bef f^{\uparrow\text{Opt}}
\]

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Itemize
Lifting 
\begin_inset Formula $f$
\end_inset

 before 
\begin_inset Formula $t$
\end_inset

 equals to lifting 
\begin_inset Formula $f$
\end_inset

 after 
\begin_inset Formula $t$
\end_inset


\end_layout

\begin_layout Itemize
Intuition: 
\begin_inset Formula $t$
\end_inset

 rearranges data in a collection, not looking at values
\end_layout

\begin_layout Standard
Further examples: 
\end_layout

\begin_layout Itemize
Reversing a list; 
\begin_inset Formula $\text{reverse}^{A}:\text{List}^{A}\rightarrow\text{List}^{A}$
\end_inset


\end_layout

\begin_layout Standard
\align center
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

_.map(f).reverse == _.reverse.map(f)
\end_layout

\end_inset


\size footnotesize

\begin_inset Formula 
\[
(f^{:A\rightarrow B})^{\uparrow\text{List}}\bef\text{reverse}^{B}=\text{reverse}^{A}\bef(f^{:A\rightarrow B})^{\uparrow\text{List}}
\]

\end_inset


\end_layout

\begin_layout Itemize
The 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure
\end_layout

\end_inset

 method, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure[A]: A => L[A]
\end_layout

\end_inset

.
 Notation: 
\begin_inset Formula $\text{pu}_{L}:A\rightarrow L^{A}$
\end_inset


\end_layout

\begin_layout Standard
\align center
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure(x).map(f) == pure(f(x))
\end_layout

\end_inset


\size footnotesize

\begin_inset Formula 
\[
\text{pu}^{A}\bef(f^{:A\rightarrow B})^{\uparrow L}=f^{:A\rightarrow B}\bef\text{pu}^{B}
\]

\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Natural transformations and their laws
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
A 
\series bold
natural transformation
\series default
 is a function 
\begin_inset Formula $t$
\end_inset

 with type signature 
\begin_inset Formula $F^{A}\rightarrow G^{A}$
\end_inset

 that satisfies the naturality law 
\begin_inset Formula $f^{\uparrow F}\bef t=t\bef f^{\uparrow G}$
\end_inset

.
 Notation 
\begin_inset Formula $t:F\leadsto G$
\end_inset


\end_layout

\begin_layout Standard
Mnemonic rule: if 
\begin_inset Formula $t:F\leadsto G$
\end_inset

 then the lifting to 
\begin_inset Formula $F$
\end_inset

 is on the left, the lifting to 
\begin_inset Formula $G$
\end_inset

 is on the right
\end_layout

\begin_layout Itemize
Many standard methods have the form of a natural transformation
\end_layout

\begin_deeper
\begin_layout Itemize
Examples: 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

headOption
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

lastOption
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

reverse
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

swap
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

map
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatMap
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure
\end_layout

\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
If there are several type parameters, use one at a time:
\end_layout

\begin_deeper
\begin_layout Itemize
For 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatMap
\end_layout

\end_inset

, denote 
\begin_inset Formula $\text{flm}:\left(A\rightarrow M^{B}\right)\rightarrow M^{A}\rightarrow M^{B}$
\end_inset

, fix 
\begin_inset Formula $A$
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Formula $\text{flm}:F^{B}\rightarrow G^{B}$
\end_inset

 where 
\begin_inset Formula $F^{B}\triangleq A\rightarrow M^{B}$
\end_inset

 and 
\begin_inset Formula $G^{B}\triangleq M^{A}\rightarrow M^{B}$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
The naturality law 
\begin_inset Formula $f^{\uparrow F}\bef\text{flm}=\text{flm}\bef f^{\uparrow G}$
\end_inset

 then gives the equation
\begin_inset Formula 
\[
\text{flm}\,(p^{:A\rightarrow M^{B}}\bef f^{\uparrow M})=\text{flm}\,(p^{:A\rightarrow M^{B}})\bef f^{\uparrow M}
\]

\end_inset

if we write out the code for 
\begin_inset Formula $f^{\uparrow F}$
\end_inset

 and 
\begin_inset Formula $f^{\uparrow G}$
\end_inset

:
\begin_inset Formula 
\[
f^{\uparrow F}=p^{:A\rightarrow M^{B}}\rightarrow p\bef f^{\uparrow M}\quad,\quad\quad f^{\uparrow G}=q^{:M^{A}\rightarrow M^{B}}\rightarrow q\bef f^{\uparrow M}
\]

\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
More practical uses of natural transformations I
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Recognize natural transformations in code and refactor
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.3cm}
\end_layout

\end_inset


\family typewriter
\size footnotesize
\color blue
def ensureName(name:
\begin_inset space ~
\end_inset

Option[String], id:
\begin_inset space ~
\end_inset

Long):
\begin_inset space ~
\end_inset

Option[(String, Long)] =
\end_layout

\begin_layout Standard

\family typewriter
\size footnotesize
\color blue
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset

 name.map((_, id))
\end_layout

\begin_layout Itemize
Recognize that the code works the same way for all types
\end_layout

\begin_layout Itemize
Introduce type parameters 
\family typewriter
\size footnotesize
\color blue
A
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
B
\family default
\size default
\color inherit
 instead of 
\family typewriter
\size footnotesize
\color blue
String
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
Long
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
The refactored code is a natural transformation:
\end_layout

\begin_layout Standard

\family typewriter
\size footnotesize
\color blue
def toOptionPair[A, B](x:
\begin_inset space ~
\end_inset

Option[A], b:
\begin_inset space ~
\end_inset

B):
\begin_inset space ~
\end_inset

Option[(A, B)] = 
\end_layout

\begin_layout Standard

\family typewriter
\size footnotesize
\color blue
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset

 x.map((_, b))
\end_layout

\begin_layout Standard
The type signature is of the form 
\family typewriter
\size footnotesize
\color blue
F[A] => G[A]
\family default
\size default
\color inherit
 if we define
\end_layout

\begin_layout Standard

\family typewriter
\size footnotesize
\color blue
type F[A] = (Option[A], B])
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
type G[A] = Option[(A, B)]
\end_layout

\begin_layout Standard
and consider 
\family typewriter
\size footnotesize
\color blue
B
\family default
\size default
\color inherit
 as a fixed type
\end_layout

\begin_layout Standard
Alternatively, consider 
\family typewriter
\size footnotesize
\color blue
A
\family default
\size default
\color inherit
 as a fixed type and obtain a natural transformation 
\family typewriter
\size footnotesize
\color blue
K[B] => L[B]
\family default
\size default
\color inherit
 with suitable definitions of 
\family typewriter
\size footnotesize
\color blue
K[B]
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
L[B]
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
The naturality law can be verified directly
\end_layout

\begin_deeper
\begin_layout Itemize
But it also follows from the product and co-product constructions for natural
 transformations (to be shown below)
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
More practical uses of natural transformations II
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Building up natural transformations from parts
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.3cm}
\end_layout

\end_inset


\family typewriter
\size footnotesize
\color blue
def toOptionList[A, B]:
\begin_inset space ~
\end_inset

List[(Option[A], B)] => List[Option[(A, B)]] =
\end_layout

\begin_layout Standard

\family typewriter
\size footnotesize
\color blue
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset

 _.map { case (x, b) => x.map((_, id)) }
\end_layout

\begin_layout Itemize
If we have a functor 
\begin_inset Formula $F$
\end_inset

 and a natural transformation 
\begin_inset Formula $G^{A}\rightarrow H^{A}$
\end_inset

, we can implement a natural transformation 
\begin_inset Formula $F^{G^{A}}\rightarrow F^{H^{A}}$
\end_inset


\end_layout

\begin_layout Itemize
In this example, the notation is 
\begin_inset Formula $F=\text{List}$
\end_inset

, 
\begin_inset Formula $G^{A}=(\bbnum 1+A)\times B$
\end_inset

, and 
\begin_inset Formula $H^{A}=\bbnum 1+A\times B$
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
The type notation such as 
\begin_inset Formula $(\bbnum 1+A)\times B$
\end_inset

 helps recognize type equivalences by using the rules of ordinary polynomial
 algebra:
\begin_inset Formula 
\[
(\bbnum 1+A)\times B\cong\bbnum 1\times B+A\times B\cong B+A\times B
\]

\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
Another example: 
\family typewriter
\size footnotesize
\color blue
List[(Try[A], B)] => List[Try[(A, B)]]
\family default
\size default
\color inherit
 with the same code as 
\family typewriter
\size footnotesize
\color blue
toOptionList[A, B]
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
Denote 
\family typewriter
\size footnotesize
\color blue
Try[A]
\family default
\size default
\color inherit
 by 
\begin_inset Formula $E+A$
\end_inset

 where 
\begin_inset Formula $E$
\end_inset

 denotes the type of the exception
\begin_inset Formula 
\[
\text{List}^{\left(E+A\right)\times B}\rightarrow\text{List}^{E+A\times B}
\]

\end_inset


\end_layout

\begin_layout Itemize
To prove the general property, write out the naturality law
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
More practical uses of natural transformations III
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Using a constant functor (
\begin_inset Quotes eld
\end_inset

phantom type parameter
\begin_inset Quotes erd
\end_inset

)
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.3cm}
\end_layout

\end_inset


\family typewriter
\size footnotesize
\color blue
def length[A]:
\begin_inset space ~
\end_inset

List[A] => Int = { _.length }
\end_layout

\begin_layout Itemize
The type signature is of the form 
\family typewriter
\size footnotesize
\color blue
F[A] => G[A]
\family default
\size default
\color inherit
 or 
\begin_inset Formula $F^{A}\rightarrow G^{A}$
\end_inset

 if we define 
\begin_inset Formula $F=\text{List}$
\end_inset

 and 
\begin_inset Formula $G^{A}=\text{Int}$
\end_inset

, so that 
\begin_inset Formula $G^{A}$
\end_inset

 is a constant functor
\end_layout

\begin_layout Itemize
The naturality law gives 
\begin_inset Formula $f^{\uparrow F}\bef\text{length}=\text{length}\bef f^{\uparrow G}$
\end_inset

, but 
\begin_inset Formula $F^{\uparrow G}=\text{id}$
\end_inset

, so 
\begin_inset Formula $f^{\uparrow F}\bef\text{length}=\text{length}$
\end_inset

 for any 
\begin_inset Formula $f^{:A\rightarrow B}$
\end_inset


\end_layout

\begin_layout Itemize
We can choose 
\begin_inset Formula $f(x)=c$
\end_inset

 with any constant 
\begin_inset Formula $c$
\end_inset

 
\end_layout

\begin_deeper
\begin_layout Itemize
The length of a list does not depend on the values stored in the list
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Reasoning with naturality I: Simplifying the 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure
\end_layout

\end_inset

 method
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.2cm}
\end_layout

\end_inset

The naturality law of 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure
\end_layout

\end_inset

 for a functor 
\begin_inset Formula $L$
\end_inset

:
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.4cm}
\end_layout

\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "26col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\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_inset


\end_layout

\end_inset


\begin_inset space \hfill{}
\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "b"
use_parbox 0
use_makebox 0
width "68col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\align center
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure(a).map(f) == pure(f(a))
\end_layout

\end_inset


\begin_inset Formula 
\[
\text{pu}_{L}\bef f^{\uparrow L}=f\bef\text{pu}_{L}
\]

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.2cm}
\end_layout

\end_inset

Fix a value 
\begin_inset Formula $b^{:B}$
\end_inset

 and set 
\begin_inset Formula $A=\bbnum 1$
\end_inset

 and 
\begin_inset Formula $f\triangleq1\rightarrow b$
\end_inset

 in the naturality law:
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.4cm}
\end_layout

\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "26col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\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_inset


\end_layout

\end_inset


\begin_inset space \hfill{}
\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "b"
use_parbox 0
use_makebox 0
width "68col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\align center
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure(()).map(_ => b) == pure(b)
\end_layout

\end_inset


\begin_inset Formula 
\[
\text{pu}_{L}\bef(1\rightarrow b)^{\uparrow L}=(1\rightarrow b)\bef\text{pu}_{L}
\]

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.2cm}
\end_layout

\end_inset

We have expressed 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure(b)
\end_layout

\end_inset

 via a constant value 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure(())
\end_layout

\end_inset

 of type 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

L[Unit]
\end_layout

\end_inset


\end_layout

\begin_layout Standard
The resulting function 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure
\end_layout

\end_inset

 will automatically satisfy the naturality law!
\end_layout

\begin_layout Standard
The naturality law of 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

pure
\end_layout

\end_inset

 makes it 
\emph on
equivalent
\emph default
 to a 
\begin_inset Quotes eld
\end_inset

wrapped unit
\begin_inset Quotes erd
\end_inset

 value
\end_layout

\begin_layout Standard
This simplifies the definition of a 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

Pointed
\end_layout

\end_inset

 typeclass:
\end_layout

\begin_layout Standard
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

abstract class Pointed[L[_]: Functor] 
\backslash
{ def wu: L[Unit] 
\backslash
}
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Examples: for 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

Option
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

wu = Some(())
\end_layout

\end_inset

.
 For 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

List
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

wu = List(())
\end_layout

\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Reasoning with naturality II: 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatMap
\end_layout

\end_inset

 and 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatten
\end_layout

\end_inset


\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.2cm}
\end_layout

\end_inset

Use the curried type signature for 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatMap
\end_layout

\end_inset

 for a monad 
\begin_inset Formula $M$
\end_inset

:
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.3cm}
\end_layout

\end_inset


\family typewriter
\size footnotesize
\color blue
def flatMap[A, B]:
\begin_inset space ~
\end_inset

(A => M[B])=> M[A] => M[B]
\family default
\size default
\color inherit
 
\begin_inset Formula 
\[
\text{flm}^{A,B}:(A\rightarrow M^{B})\rightarrow M^{A}\rightarrow M^{B}
\]

\end_inset


\end_layout

\begin_layout Standard
The naturality law with respect to the type parameter 
\family typewriter
\size footnotesize
\color blue
A
\family default
\size default
\color inherit
:
\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{-0.4cm}
\end_layout

\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "26col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\begin_inset Formula 
\[
\xymatrix{M^{A}\ar[rd]\sp(0.55){\text{flm}\,(f\bef g)}\ar[d]\sb(0.4){f^{\uparrow M}}\\
\xyScaleY{1.6pc}\xyScaleX{4.0pc}M^{B}\ar[r]\sp(0.45){\text{flm}\,(g)} & M^{C}
}
\]

\end_inset


\end_layout

\end_inset


\begin_inset space \hfill{}
\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "b"
use_parbox 0
use_makebox 0
width "68col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\align center
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

_.flatMap(f andThen g) == _.map(f).flatMap(g)
\end_layout

\end_inset


\begin_inset Formula 
\[
\text{flm}\,(f^{:A\rightarrow B}\bef g^{:B\rightarrow M^{C}})=f^{\uparrow M}\bef\text{flm}\,(g)\quad.
\]

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
vspace{0.2cm}
\end_layout

\end_inset

Express 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatMap
\end_layout

\end_inset

 through 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatten
\end_layout

\end_inset

:
\end_layout

\begin_layout Standard
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

_.flatMap(f) == _.map(f).flatten
\end_layout

\end_inset


\begin_inset Formula 
\[
\text{flm}\,(g)=g^{\uparrow M}\bef\text{ftn}
\]

\end_inset

Express 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatten
\end_layout

\end_inset

 through 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatMap
\end_layout

\end_inset

:
\begin_inset Formula 
\[
\text{ftn}=\text{flm}\,(\text{id}^{:M^{A}\rightarrow M^{A}})
\]

\end_inset

The function 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatten
\end_layout

\end_inset

 is equivalent to 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

flatMap
\end_layout

\end_inset

 with naturality law
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Reasoning with naturality III: The covariant Yoneda identity
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
We have shown that the set of all natural transformations 
\begin_inset Formula $A\rightarrow L^{A}$
\end_inset

 is equivalent to the set of all values 
\begin_inset Formula $L^{\bbnum 1}$
\end_inset


\end_layout

\begin_layout Standard
This property can be generalized to any type 
\begin_inset Formula $Z$
\end_inset

 instead of the unit type (
\begin_inset Formula $\bbnum 1$
\end_inset

):
\end_layout

\begin_layout Standard
The set of all natural transformations 
\begin_inset Formula $\left(Z\rightarrow A\right)\rightarrow L^{A}$
\end_inset

 is equivalent to the set of all values 
\begin_inset Formula $L^{Z}$
\end_inset

, where 
\begin_inset Formula $Z$
\end_inset

 is a fixed type
\end_layout

\begin_layout Standard
To indicate that 
\begin_inset Formula $Z$
\end_inset

 is fixed by 
\begin_inset Formula $A$
\end_inset

 is varying within the natural transformation, use a type signature with
 the universal quantifier:
\begin_inset Formula 
\begin{align*}
\big(\forall A.\,A & \rightarrow L^{A}\big)\cong L^{\bbnum 1}\\
\big(\forall A.\,\left(Z\rightarrow A\right) & \rightarrow L^{A}\big)\cong L^{Z}\quad\quad\text{-- the covariant Yoneda identity}
\end{align*}

\end_inset


\end_layout

\begin_layout Standard
To prove:
\end_layout

\begin_layout Enumerate
Implement the isomorphism, 
\begin_inset Formula $p:\big(\forall A.\,\left(Z\rightarrow A\right)\rightarrow L^{A}\big)\rightarrow L^{Z}$
\end_inset

 and 
\begin_inset Formula $q:L^{Z}\rightarrow\forall A.\,\left(Z\rightarrow A\right)\rightarrow L^{A}$
\end_inset


\end_layout

\begin_layout Enumerate
Show that 
\begin_inset Formula $p\bef q=\text{id}$
\end_inset

 and 
\begin_inset Formula $q\bef p=\text{id}$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Reasoning with naturality IV: other derivations
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Naturality laws are often used in derivations of various typeclass laws
\end_layout

\begin_layout Standard
Within the 11 existing chapters of my upcoming free book, 
\begin_inset Quotes eld
\end_inset


\emph on
The Science of Functional Programming
\emph default

\begin_inset Quotes erd
\end_inset

 (
\family typewriter
\size small

\begin_inset CommandInset href
LatexCommand href
target "https://github.com/winitzki/sofp"

\end_inset


\family default
\size default
), naturality laws are used at least 31 times in about 100 derivations
\end_layout

\begin_layout Itemize
Examples of such derivations:
\end_layout

\begin_deeper
\begin_layout Itemize
Composition of two co-pointed functors is again co-pointed
\end_layout

\begin_deeper
\begin_layout Itemize
A functor 
\begin_inset Formula $F$
\end_inset

 is co-pointed if there exists a natural transformation 
\begin_inset Formula $\text{ex}:\forall A.\,F^{A}\rightarrow A$
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
The product of two monads is again a monad
\end_layout

\begin_layout Itemize
The product of two monad transformers is again a monad transformer
\end_layout

\end_deeper
\begin_layout Standard
The most useful derivation technique is rewriting equations
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Example: properties of horizontal and vertical composition
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Bartosz Milewski's book 
\begin_inset Quotes eld
\end_inset

Category theory for programmers
\begin_inset Quotes erd
\end_inset

, Chapter 10, defines the horizontal and the vertical composition of natural
 transformations
\end_layout

\begin_layout Standard
The vertical composition of 
\begin_inset Formula $\alpha:F^{A}\rightarrow G^{A}$
\end_inset

 and 
\begin_inset Formula $\beta:G^{A}\rightarrow H^{A}$
\end_inset

 is the ordinary function composition 
\begin_inset Formula $\left(\alpha\bef\beta\right):F^{A}\rightarrow H^{A}$
\end_inset


\end_layout

\begin_layout Standard
The horizontal composition of 
\begin_inset Formula $\alpha:F^{A}\rightarrow G^{A}$
\end_inset

 and 
\begin_inset Formula $\alpha^{\prime}:F^{\prime A}\rightarrow G^{\prime A}$
\end_inset

 is 
\begin_inset Formula $\left(\alpha\star\alpha^{\prime}\right):F^{F^{\prime A}}\rightarrow G^{G^{\prime A}}$
\end_inset


\end_layout

\begin_layout Itemize
Both compositions again give natural transformations
\end_layout

\begin_layout Standard
If we have four natural transformations 
\begin_inset Formula $\alpha$
\end_inset

, 
\begin_inset Formula $\beta$
\end_inset

, 
\begin_inset Formula $\alpha^{\prime}$
\end_inset

, 
\begin_inset Formula $\beta^{\prime}$
\end_inset

 with type signatures
\begin_inset Formula 
\begin{align*}
\alpha & :F^{A}\rightarrow G^{A}\quad,\quad\beta:G^{A}\rightarrow H^{A}\quad,\\
\alpha^{\prime} & :F^{\prime A}\rightarrow G^{\prime A}\quad,\quad\beta^{\prime}:G^{\prime A}\rightarrow H^{\prime A}\quad,
\end{align*}

\end_inset

we can write the distributive law,
\begin_inset Formula 
\[
\left(\alpha\bef\beta\right)\star(\alpha^{\prime}\bef\beta^{\prime})=(\alpha\star\alpha^{\prime})\bef(\beta\star\beta^{\prime})
\]

\end_inset

To prove that these properties hold, write out the naturality laws
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Other constructions of natural transformations
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Natural transformations can be combined in several other ways
\end_layout

\begin_layout Standard
Given natural transformations 
\family typewriter
\size footnotesize
\color blue
a[A]: F[A] => G[A]
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
b[A]: K[A] => L[A]
\family default
\size default
\color inherit
:
\end_layout

\begin_layout Itemize
pair product, 
\family typewriter
\size footnotesize
\color blue
((F[A], K[A])) => (G[A], L[A])
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
pair co-product, 
\family typewriter
\size footnotesize
\color blue
Either[F[A], K[A]] => Either[G[A], L[A]]
\family default
\size default
\color inherit
 
\end_layout

\begin_layout Itemize
pair exponential, 
\family typewriter
\size footnotesize
\color blue
(F[A] => K[A]) => (G[A] => L[A])
\family default
\size default
\color inherit
 where 
\family typewriter
\size footnotesize
\color blue
F[A]
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
G[A]
\family default
\size default
\color inherit
 must be contrafunctors
\end_layout

\begin_deeper
\begin_layout Itemize
are natural transformations implemented by combining 
\family typewriter
\size footnotesize
\color blue
a[A]
\family default
\size default
\color inherit
 and 
\family typewriter
\size footnotesize
\color blue
b[A]
\family default
\size default
\color inherit
 
\end_layout

\end_deeper
\begin_layout Standard
Also, the identity function 
\family typewriter
\size footnotesize
\color blue
identity[A]: A => A
\family default
\size default
\color inherit
 and the constant unit function of type 
\family typewriter
\size footnotesize
\color blue
A => Unit
\family default
\size default
\color inherit
 are natural transformations
\end_layout

\begin_layout Standard
It follows that any purely functional combination of natural transformations
 is again a natural transformation
\end_layout

\begin_layout Standard
No need to verify the naturality law in each case
\end_layout

\begin_layout Standard
Example: 
\family typewriter
\size footnotesize
\color blue
(Option[A], B) => Option[(A, B)]
\family default
\size default
\color inherit
 
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Summary of the type notation
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
The short type notation helps in symbolic reasoning about types
\end_layout

\begin_layout Standard
\noindent
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="10" columns="3">
<features tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
\size small
Description
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
\size small
Scala examples
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
\size small
Notation
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Typed value
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

x: Int
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $x^{:\text{Int}}$
\end_inset

 or 
\begin_inset Formula $x:\text{Int}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Unit type
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

Unit
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

Nil
\end_layout

\end_inset

, 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

None
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $\bbnum 1$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Type parameter
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

A
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $A$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Product type
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

(A, B)
\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

case class P(x: A, y: B)
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $A\times B$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Co-product type
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

Either[A, B]
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $A+B$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Function type
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

A => B
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $A\rightarrow B$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Type constructor
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

List[A]
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $\text{List}^{A}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Universal quantifier
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

trait P 
\backslash
{ def f[A]: Q[A] 
\backslash
}
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $P\triangleq\forall A.\,Q^{A}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
Existential quantifier
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "43page%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

sealed trait P[A]
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

case class Q[A, B]() extends P[A]
\end_layout

\end_inset


\begin_inset VSpace 20baselineskip%
\end_inset


\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size footnotesize
\begin_inset Formula $P^{A}\triangleq\exists B.\,Q^{A,B}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Standard
Example: Scala code 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

def flm(f: A => Option[B]): Option[A] => Option[B]
\end_layout

\end_inset

 is denoted by 
\begin_inset Formula $\text{flm}:(A\rightarrow\bbnum 1+B)\rightarrow\bbnum 1+A\rightarrow\bbnum 1+B$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Summary of the code notation
\end_layout

\end_inset


\begin_inset Separator latexpar
\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
The short code notation helps in symbolic reasoning about code
\end_layout

\begin_layout Standard
\noindent
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="12" columns="2">
<features tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
\size small
Scala examples
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\series bold
\size small
Notation
\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

()
\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

true
\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

\begin_inset Quotes eld
\end_inset

abc
\begin_inset Quotes erd
\end_inset


\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

123
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $1$
\end_inset

, 
\begin_inset Formula $\text{true}$
\end_inset

, 
\begin_inset Formula $\text{"abc"}$
\end_inset

, 
\begin_inset Formula $123$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

def f[A](x: A) = ...
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $f^{A}(x^{:A})\triangleq...$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout


\backslash
{ (x: A) => expr 
\backslash
}
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $x^{:A}\rightarrow\text{expr}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

f(x)
\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

x.pipe(f)
\end_layout

\end_inset

 (Scala 2.13)
\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $f(x)$
\end_inset

 or 
\begin_inset Formula $x\triangleright f$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

val p: (A, B) = (a, b)
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $p^{:A\times B}\triangleq a\times b$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout


\backslash
{case (a, b) => expr
\backslash
}
\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

p._1
\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

p._2
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $a\times b\rightarrow\text{expr}$
\end_inset

 
\begin_inset space ~
\end_inset

or
\begin_inset space ~
\end_inset

 
\begin_inset Formula $p\triangleright\pi_{1}$
\end_inset


\begin_inset space ~
\end_inset

or
\begin_inset space ~
\end_inset

 
\begin_inset Formula $p\triangleright\pi_{2}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

Left[A, B](x)
\end_layout

\end_inset

 or 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

Right[A, B](y)
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $x^{:A}+\bbnum 0^{:B}$
\end_inset

 or 
\begin_inset Formula $\bbnum 0^{:A}+y^{:B}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset space \hspace*{}
\length -1.3line%
\end_inset


\begin_inset Box Frameless
position "c"
hor_pos "c"
has_inner_box 1
inner_pos "b"
use_parbox 0
use_makebox 0
width "50col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout

\size small
\begin_inset VSpace 14baselineskip%
\end_inset


\size footnotesize

\begin_inset listings
inline true
status open

\begin_layout Plain Layout

val q: C = (p: Either[A, B]) match 
\backslash
{
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

\size footnotesize
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset


\begin_inset listings
inline true
status open

\begin_layout Plain Layout

case Left(x)   => f(x)
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

\size footnotesize
\begin_inset space ~
\end_inset

 
\begin_inset space ~
\end_inset


\begin_inset listings
inline true
status open

\begin_layout Plain Layout

case Right(y)  => g(y)
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

\size footnotesize
\begin_inset listings
inline true
status open

\begin_layout Plain Layout


\backslash
}
\end_layout

\end_inset


\size small

\begin_inset VSpace 20baselineskip%
\end_inset


\end_layout

\end_inset

 
\begin_inset space \hspace*{}
\length -0.9line%
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $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}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

def f(x) = 
\backslash
{ ...
 f(y) ...
 
\backslash
}
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "30col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open

\begin_layout Plain Layout
\align center

\size small
\begin_inset VSpace -64baselineskip%
\end_inset


\begin_inset Formula $f(x)\triangleq...~\overline{f}(y)~...$
\end_inset


\begin_inset VSpace 15baselineskip%
\end_inset


\end_layout

\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

f andThen g
\end_layout

\end_inset

 and 
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

(f andThen g)(x)
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $f\bef g$
\end_inset

 and 
\begin_inset Formula $x\triangleright f\bef g$
\end_inset


\begin_inset space ~
\end_inset

or
\begin_inset space ~
\end_inset

 
\begin_inset Formula $x\triangleright f\triangleright g$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset listings
inline true
status open

\begin_layout Plain Layout

p.map(f).map(g)
\end_layout

\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout

\size small
\begin_inset Formula $p\triangleright f^{\uparrow F}\triangleright g^{\uparrow F}$
\end_inset


\begin_inset space ~
\end_inset

or
\begin_inset space ~
\end_inset

 
\begin_inset Formula $p\triangleright f^{\uparrow F}\bef g^{\uparrow F}$
\end_inset


\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator parbreak
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Summary
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Use naturality laws to obtain refactoring guaranteed to be correct
\end_layout

\begin_layout Itemize
Recognize and refactor code to use natural transformations
\end_layout

\begin_layout Itemize
Naturality laws allow us to reduce the number of type parameters in certain
 functions
\end_layout

\begin_layout Itemize
Short notation for code helps derive properties via symbolic calculations
\end_layout

\begin_deeper
\begin_layout Itemize
which is more efficient than 
\begin_inset Quotes eld
\end_inset

staring at diagrams
\begin_inset Quotes erd
\end_inset


\end_layout

\end_deeper
\begin_layout Itemize
Full details and proofs are in the free upcoming book
\end_layout

\begin_deeper
\begin_layout Itemize
Draft of the book: 
\family typewriter

\begin_inset CommandInset href
LatexCommand href
target "https://github.com/winitzki/sofp"

\end_inset


\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Note Note
status open

\begin_layout Plain Layout
End of slides.
\end_layout

\end_inset


\end_layout

\end_body
\end_document