sofp.tex

%% LyX 2.3.7 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[10pt,russian,english,open=any,numbers=noenddot,index=totoc,bibliography=totoc,listof=totoc,fontsize=12pt]{scrbook}
\usepackage{amsmath}
\usepackage{mathpazo}
\usepackage{helvet}
\renewcommand{\ttdefault}{cmtt}
\usepackage{newtxmath}
\usepackage[T2A,T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[paperwidth=7.444in,paperheight=9.68in]{geometry}
\geometry{verbose,tmargin=1.3cm,bmargin=1.5cm,lmargin=2.4cm,rmargin=1.4cm,headsep=0.5cm,footskip=0.8cm}
\setcounter{secnumdepth}{3}
\usepackage{xcolor}
\usepackage{babel}
\usepackage{array}
\usepackage{verbatim}
\usepackage{refstyle}
\usepackage{wrapfig}
\usepackage{calc}
\usepackage{textcomp}
\usepackage{tipa}
\usepackage{tipx}
\usepackage{mathdots}
\usepackage{stmaryrd}
\usepackage{makeidx}
\makeindex
\usepackage{graphicx}
\usepackage{wasysym}
\usepackage[all]{xy}
\PassOptionsToPackage{normalem}{ulem}
\usepackage{ulem}
\usepackage[unicode=true,
 bookmarks=true,bookmarksnumbered=true,bookmarksopen=true,bookmarksopenlevel=2,
 breaklinks=true,pdfborder={0 0 0},pdfborderstyle={},backref=page,colorlinks=true]
 {hyperref}
\hypersetup{pdftitle={The Science of Functional Programming: A Tutorial, with Examples in Scala},
 pdfauthor={Sergei Winitzki},
 pdfsubject={Functional programming},
 pdfkeywords={Functional programming, Scala, Type theory, Category theory, Formal logic, Programming languages},
 linkcolor=hlink}

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.

\AtBeginDocument{\providecommand\subsecref[1]{\ref{subsec:#1}}}
\newcommand{\noun}[1]{\textsc{#1}}
\DeclareRobustCommand{\cyrtext}{%
  \fontencoding{T2A}\selectfont\def\encodingdefault{T2A}}
\DeclareRobustCommand{\textcyr}[1]{\leavevmode{\cyrtext #1}}

%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}
\RS@ifundefined{subsecref}
  {\newref{subsec}{name = \RSsectxt}}
  {}
\RS@ifundefined{thmref}
  {\def\RSthmtxt{theorem~}\newref{thm}{name = \RSthmtxt}}
  {}
\RS@ifundefined{lemref}
  {\def\RSlemtxt{lemma~}\newref{lem}{name = \RSlemtxt}}
  {}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
\newenvironment{lyxcode}
	{\par\begin{list}{}{
		\setlength{\rightmargin}{\leftmargin}
		\setlength{\listparindent}{0pt}% needed for AMS classes
		\raggedright
		\setlength{\itemsep}{0pt}
		\setlength{\parsep}{0pt}
		\normalfont\ttfamily}%
	 \item[]}
	{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usepackage[all]{xy} % xypic

% pstricks with support for pdflatex
%\usepackage{pdftricks}
%\begin{psinputs}
%   \usepackage{pstricks}
%   \usepackage{multido}
%\end{psinputs}
\usepackage{pstricks}

% Cover picture on first page.
\usepackage{wallpaper}
% Custom commands for cover page.
\usepackage[absolute,overlay]{textpos}

% No page numbers on "Part" pages.
\renewcommand*{\partpagestyle}{empty}

% Use a special "equal by definition" symbol.
\renewcommand*{\triangleq}{\overset{\lower1mm\hbox{\texttt{\tiny def}}} {=}}

% Running head: works, but results are not satisfactory.
%\usepackage{scrlayer-scrpage}
%\automark[subsection]{chapter}


% "Better text justification"? Actually, this causes a fatal error "auto expansion is only possible with scalable fonts".
%\usepackage{microtype}

% Fix the numbering of exercises: subsubsections appear as paragraphs but are numbered.
%\usepackage{titlesec} % Incompatible with komascript\textsf{'}s later versions.
% See https://tex.stackexchange.com/questions/7627/how-to-reference-paragraph
% See the `titlesec` package documentation at http://www.ctex.org/documents/packages/layout/titlesec.pdf
%\titleformat{\subsubsection}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
%\titlespacing{\subsubsection}{0pt}{5pt}{3\wordsep}
%\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
%\titlespacing{\subparagraph}{\parindent}{\parskip}{3\wordsep}
%\titlespacing{\paragraph}{0pt}{3pt}{2\wordsep}

\renewcommand*{\subsubsectionformat}{}
\RedeclareSectionCommand[ % Statement 1.2.3.4
  runin=true,
  afterskip=2ex,
  beforeskip=2.5pt plus 0.3pt minus 0.05pt,
  afterindent=false,
  font={\normalfont\normalsize\bfseries}
]{subsubsection}
\RedeclareSectionCommand[ % Proof
  runin=true,
  font={\normalfont\normalsize\bfseries},
  afterindent=false,
  afterskip=2ex,
  beforeskip=0pt
]{subparagraph}
\RedeclareSectionCommand[
  runin=true,
  font={\normalfont\normalsize\bfseries},
  afterskip=1.3ex,
  beforeskip=0pt
]{paragraph}

% Make page headers and page numbers smaller
\addtokomafont{pagehead}{\small}
\addtokomafont{pagenumber}{\small}

% 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}.

% 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}
\definecolor{teal}{rgb}{0,0.6,0}

% These settings are now in the Listings tab in LyX.
%\lstdefinestyle{myScalastyle}{
%  language=scala, % This should be defined first!!! Otherwise it overrides all customization via morekeywords / otherkeywords.
%  otherkeywords={{=,=>,<-,<\%,<:,>:,\#,@,*,+,-,/,::,:,[,]}},
%  frame=tb,
%  aboveskip=2mm,
%  belowskip=2mm,
%  showstringspaces=false,
%  columns=flexible,
%  basicstyle={\small\ttfamily},
%  extendedchars=true,
%  %numbers=none,
%  numberstyle=\tiny\color{gray},
%  keywordstyle=\color{blue},
%  commentstyle=\color{dkgreen},
%  stringstyle=\color{mauve},
%  frame=single,
%  framerule=0.01mm,
%  breaklines=true,
%  breakatwhitespace=true,
%  tabsize=3,
%  framexleftmargin=4mm, framexrightmargin=4mm,
%  xleftmargin=4mm, xrightmargin=4mm, % Making these margins the same has a good effect.
%  framextopmargin=0.5mm, framexbottommargin=.5mm,
%  fillcolor=\color{aqua},
%  rulecolor=\color{aqua},
%  rulesepcolor=\color{aqua},
%  backgroundcolor=\color{aqua},
%  mathescape=true,
%}

% Example usage: \begin{lstlisting}[style=myScalastyle]  object blah \end{lstlisting}
%\newenvironment{scala}{\begin{lstlisting}[style=myScalastyle]}{\end{lstlisting}}
%\lstnewenvironment{scala}{\lstset{style=myScalastyle}}{}

\usepackage[nocenter]{qtree} % simple tree drawing
\usepackage{relsize} % make math symbols larger or smaller; supports \smaller etc.
\usepackage{stmaryrd} % some extra symbols such as \fatsemi
% Note: using \forwardcompose inside a \text{} will cause a LaTeX error!
\newcommand{\forwardcompose}{\hspace{1.2pt}\ensuremath\mathsmaller{\fatsemi}\hspace{1.5pt}}
% this is ugly, I used this before I found \fatsemi:
%\newcommand{\bef}{\hspace{1.0pt}\ensuremath\raisebox{2pt}{$\mathsmaller{\mathsmaller{\circ}}$}\hspace{-2.9pt},}
%\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

% Increase the default vertical space inside table cells.
\renewcommand\arraystretch{1.4}

% Color for PDF hyperlinks.
\definecolor{hlink}{rgb}{0.06, 0.14, 0.48}

% 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.

\newcommand{\shui}{\begin{CJK}{UTF8}{gbsn}æ°´\end{CJK}}
\usepackage{CJKutf8} % For occasional Chinese characters. Also, add "russian" to documentclass.

% Prepare settings for imposing a color background for all displayed math. This will be done by a script later.
\usepackage{empheq} % Background on all displayed equations.
\definecolor{mathbg}{rgb}{1.0, .98, .87}
\newcommand*\mymathbgbox[1]{%
\setlength{\fboxsep}{0pt}%
\colorbox{mathbg}{\hspace{0.5mm}#1\hspace{0.5mm}}}
%\renewenvironment{align}{%
%\begin{empheq}[box=\mymathbgbox]{align}}{%
%\endalign\end{empheq}}
% Run a command such as LC_ALL=C sed -i bak -e \textsf{'}s|\\begin{align}|\\begin{empheq}[box=\\mymathbgbox]{align}|; s|\\end{align}|\\end{empheq}|' sofp-filterable.tex
% This is not used now because the results are not great.

% Better text quotes.
\renewcommand\textquotedblleft{\textsf{``}}
\renewcommand\textquotedblright{\textsf{''}}

% Better symbol for the pair mapper instead of \ogreaterthan and \varogreaterthan.
\newcommand{\boxrightarrow}{\mathbin{\ensuremath{%
\mathchoice%
  {\displaystyle{\boxminus}\kern-5.35pt\raisebox{0.75pt}{$\scriptstyle{\succ}$}}%
  {\boxminus\kern-5.35pt\raisebox{0.75pt}{$\scriptstyle{\succ}$}}%
  {\textstyle{\boxminus}\kern-5.35pt\raisebox{0.75pt}{$\scriptstyle{\succ}$}}%
  {\scriptstyle{\boxminus}\kern-3.7pt\raisebox{0.49pt}{$\scriptscriptstyle{\succ}$}}%
}% end of mathchoice with raisebox
\hspace{1.0pt}}}
\renewcommand{\ogreaterthan}{\boxrightarrow}
\renewcommand{\varogreaterthan}{\boxrightarrow}

\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,Option,Either,Future,Successful,LazyList,Vector,Range,IndexedSeq,true,false,None,List,Nil,Try,Success,Failure,Some,Left,Right,Nothing,Any,Array,Unit,Iterator,Stream,Throwable,Integer,Object}},
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}
\addto\captionsenglish{\renewcommand{\lstlistingname}{\inputencoding{latin9}Listing}}
\addto\captionsrussian{\renewcommand{\lstlistingname}{\inputencoding{koi8-r}ìÉÓÔÉÎÇ}}
\renewcommand{\lstlistingname}{\inputencoding{latin9}Listing}

\begin{document}
\extratitle{\input{sofp-cover-page}\hfill{}\thispagestyle{empty}The Science
of Functional Programming\hspace{1in}}
\title{The Science of Functional Programming}
\subtitle{A tutorial, with examples in Scala}
\author{by Sergei Winitzki, Ph.D.}
\date{Draft version of \today}
\publishers{Published by\textbf{ \href{http://lulu.com}{lulu.com}} in 2024}
\uppertitleback{{\footnotesize{}Copyright \copyright\  2018-2024 by Sergei Winitzki}\\
{\footnotesize{}~}\\
{\footnotesize{}\href{https://www.lulu.com/en/us/shop/sergei-winitzki/the-science-of-functional-programming-draft-version/paperback/product-1y5zzgje.html}{Print on-demand link at lulu.com}}\\
{\footnotesize{}~}\\
{\footnotesize{}ISBN (e-book): 978-0-359-76877-6}\\
{\footnotesize{}ISBN: 978-0-359-76877-6}\\
\\
{\scriptsize{}Source hash (sha256): 7f943ef5d41edc5f95b917eef1405a6a4e5a506f491d2200791e2bbbeeb0dbba}\\
{\scriptsize{}Git commit: f23c397141307f32ce60141128eb44473336f4d4}\\
{\scriptsize{}PDF file built by pdfTeX 3.141592653-2.6-1.40.25 (TeX Live 2023) on Fri, 26 Jan 2024 23:39:13 +0100 by Darwin 22.6.0}\\
~\\
{\scriptsize{}Permission is granted to copy, distribute and/or modify
this document under the terms of the GNU Free Documentation License,
Version 1.2 or any later version published by the Free Software Foundation;
with no Invariant Sections, no Front-Cover Texts, and no Back-Cover
Texts. A copy of the license is included in the appendix entitled
\textsf{``}GNU Free Documentation License\textsf{''} (Appendix~\ref{sec:GFDL}).}\\
{\scriptsize{}~}\\
{\scriptsize{}A }\emph{\scriptsize{}Transparent}{\scriptsize{} copy
of the source code for the book is available at }\texttt{\scriptsize{}\href{https://github.com/winitzki/sofp}{https://github.com/winitzki/sofp}}{\scriptsize{}
and includes LyX, LaTeX, graphics source files, and build scripts.
A full-color hyperlinked PDF file is available at }\texttt{\scriptsize{}\href{https://github.com/winitzki/sofp/releases}{https://github.com/winitzki/sofp/releases}}{\scriptsize{}
under \textsf{``}Assets\textsf{''}. The source code may be also included as a \textsf{``}file
attachment\textsf{''} named }\texttt{\scriptsize{}sofp-src.tar.bz2}{\scriptsize{}
within a PDF file. To extract, run }\texttt{\scriptsize{}`pdftk sofp.pdf
unpack\_files output .`}{\scriptsize{} and then }\texttt{\scriptsize{}`tar
jxvf sofp-src.tar.bz2`}{\scriptsize{}. See the file }\texttt{\scriptsize{}README.md}{\scriptsize{}
for build instructions.}}
\lowertitleback{{\scriptsize{}This book is a pedagogical in-depth tutorial and reference
on the theory of functional programming (FP) as practiced in the early
21$^{\text{st}}$ century. Starting from issues found in practical
coding, the book builds up the theoretical intuition, knowledge, and
techniques that programmers need for rigorous reasoning about types
and code. Examples are given in Scala, but most of the material applies
equally to other FP languages.}\\
{\scriptsize{}}\\
{\scriptsize{}The book\textsf{'}s topics include working with FP-style collections;
reasoning about recursive functions and types; the Curry-Howard correspondence;
laws, structural analysis, and code for functors, monads, and other
typeclasses based on exponential-polynomial data types; techniques
of symbolic derivation and proof; free typeclass constructions; and
parametricity theorems.}\\
{\scriptsize{}}\\
{\scriptsize{}Long and difficult, yet boring explanations are logically
developed in excruciating detail through 1871 Scala
code snippets, 189 statements with step-by-step derivations,
103 diagrams, 216 examples with tested Scala
code, and 295 exercises. Discussions build upon each
chapter\textsf{'}s material further.}\\
{\scriptsize{}}\\
{\scriptsize{}Beginners in FP will find tutorials about the map/reduce
programming style, type parameters, disjunctive types, and higher-order
functions. For more advanced readers, the book shows  the practical
uses of the Curry-Howard correspondence and the parametricity theorems
without unnecessary jargon; proves that all the standard monads (e.g.,
}\texttt{\scriptsize{}List}{\scriptsize{} or }\texttt{\scriptsize{}State}{\scriptsize{})
satisfy the monad laws; derives lawful instances of }\texttt{\scriptsize{}Functor}{\scriptsize{}
and other typeclasses from types; shows that monad transformers need
18 laws; and explains the use of parametricity for reasoning about
the Church encoding and the free typeclasses.}\\
{\scriptsize{}}\\
{\scriptsize{}Readers should have a working knowledge of programming;
e.g., be able to write code that prints the number of distinct words
in a sentence. The difficulty of this book\textsf{'}s mathematical derivations
is at the level of undergraduate multivariate calculus, similar to
that of multiplying matrices or simplifying the expressions:
\[
\frac{1}{x-2}-\frac{1}{x+2}\quad\text{ and }\quad\frac{d}{dx}\left((x+1)f(x)e^{-x}\right)\quad.
\]
}\\
{\scriptsize{}The author received a Ph.D.~in theoretical physics.
After a career in academic research, he works as a software engineer.}\\
}

\maketitle
\frontmatter\pagenumbering{roman}

\tableofcontents{}

\mainmatter\pagenumbering{arabic}
\global\long\def\gunderline#1{\mathunderline{greenunder}{#1}}%
\global\long\def\bef{\forwardcompose}%
\global\long\def\bbnum#1{\custombb{#1}}%
\global\long\def\pplus{{\displaystyle }{+\negmedspace+}}%

\begin{comment}
+ Each chapter is now a separate file. The LyX macro definitions should
be included at the top of each chapter file; then each chapter can
be previewed correctly by LyX, separately from other chapters, which
is faster. It is not necessary (but harmless) to copy the LaTeX preamble
from sofp.lyx to all chapter files.

+ No separate chapter for recursive types unless this is about \textsf{``}open\textsf{''}
co-products and \textsf{``}open\textsf{''} products. Recursive types are already covered
sufficiently. Perhaps this is too much and should be left for a future
edition.

- Write a summary of all results as a separate chapter with no proofs.

+ Cut the scope: no co-monads, no recursive open unions, no lenses
(?). Lenses can be added later. 

- Need to talk about monad recursion (? or cut the scope).

- Add code to the monad chapter 10 that shows defining a monad typeclass
instance for various constructions. I have this example code already,
but it was not included in the chapter. 
\end{comment}
\include{sofp-preface}

\part{Introductory level}

\include{sofp-nameless-functions}\include{sofp-induction}\include{sofp-disjunctions}\include{sofp-higher-order-functions}\include{sofp-curry-howard}\include{sofp-essay1}

\part{Intermediate level}

\include{sofp-functors}\include{sofp-reasoning}\include{sofp-typeclasses}\include{sofp-filterable}\include{sofp-monads}\include{sofp-applicative}\include{sofp-traversable}\include{sofp-essay2}

\part{Advanced level}

\include{sofp-free-type}\include{sofp-transformers}

\addpart{Discussions}

\include{sofp-summary}\include{sofp-essay3}

\addpart{Appendixes}


\appendix
\include{sofp-appendices}

\listoftables

\listoffigures

\printindex{}

\input{sofp-back-cover-page}
\end{document}